theorem ext {a b : Set α} (h : ∀ (x : α), x ∈ a ↔ x ∈ b) : a = b := funext (fun x ↦ propext (h x))事実 半形式的：$`\text{Fact ext}\\ \text{For } a, b : \mathrm{Set}\: \alpha \\ \text{When } \forall (x : α),\, x \in a \iff x \in b \\ \text{…

https://m-hiyama.hatenablog.com/entry/20161210/1481350849 の昔のコード、以前は問題なかった。 <img width="600" src="http://www.chimaira.org/img3/Mizar.jpg" >((画像は https://it.wikipedia.org/wiki/Mizar より)) 今は、行内のHTMLコメントで…

対応表： 定理記述 関数定義 定理のステートメント 関数{定義}?のヘッド 証明項 計算項 定理記述する 関数定義する から導出された定理 から定義された定理 構文と意味は混同される。 関数そのもの（型の圏の射）と関数定義という構文対象 定理そのもの（命…