▽くるるの数学ﾉｰﾄ
●05/21 20:15
2025-05-21構造の定義Mathlib.ModelTheory構造定義ここまでの定義はだいたい残っている状態からｽﾀｰﾄするとする｡構造のﾕﾆﾊﾞｰｽになる型が必要で､とかでもいいんだけど､区別をつけたいので新しい型Vを定義｡ただ自然数でｲﾝﾃﾞｯｸｽしているだけ｡inductive V : Type| obj (n : Nat) : Vderiving Repr, DecidableEqderiving Reprをつけているので#evalして表示することができる｡DecidableEqは型の要素が等しいかどうかが決定できるかどうかってやつ｡構造はMathlib.ModelTheory.BasicでFirstOrder.Language.Structureとして下記のように定義されている｡/-- A first-order structure on a type

▽5号館のつぶやき
●05/03 21:57
2025年 05月 03日今朝は珍しく風が収まらずに雨になったらしい今朝は雨でした｡朝はまだ降っていましたが､ほとんど上がってきていたようです｡昨日は風が強くて､風が収まってから雨になると思っていたのですが､今回は珍しく風が収まらずに雨になってようです｡こちらが風のｸﾞﾗﾌ｡今朝になって､雨が収まってきた頃に､風も収まってきたようです｡西の方から､晴れてきていました｡雨と風が収まったら､気温も上がってきて､昨日を越えてきました｡夜の間は気温が下がらなかったようで､今朝も暖かいままでした｡日中は意外と日差しもあり､予想よりは暖かくなったようです｡結局､最高気温は18℃を越えて､屋内は暑いくらいになりました｡夕方はｵﾚﾝｼﾞ色の夕焼けがだんだんと染まってきました｡染まり始めです｡いい感じに染まってきました｡黄色いはずのﾚﾝｷﾞｮｳの花がｵﾚﾝｼﾞ色に変わっています｡今朝の雲

▽/dev/wd0a
●04/18 11:10
2025-04-17■帰ってきました｡研究雑記などを書くためにresearchmapの研究ﾌﾞﾛｸﾞを使っていたのですが､最近､researchmapがﾌﾞﾛｸﾞ機能を見捨てつつあるように感じているので､移転先を探しています｡とりあえず､ここも復活させます｡どう使うかは未定です｡wd0 2025-04-17 18:21 読者になる広告を非表示にするもっと読むｺﾒﾝﾄを書く帰ってきました｡ 研究雑記などを書くため…▼ ▶20252025 / 4

▽hiroki_fの日記
●03/25 16:28
hiroki_f’s diary読者になる

▽難関大学への数学
●05/12 04:59
力