逆像のf-1 を f^* と書く。 // SerND 共通部分の逆像 target f^*(C)∩f^*(D) = f^*(C∩D) proof target f^*(C)∩f^*(D) ⊆ f^*(C∩D) proof assume x∈(f^*(C)∩f^*(D)) ---(ass) expand by (集合の共通部分) x∈f^*(C) ∧ x∈f^*(D) expand $.1, $.2 by (写像の逆像) …

// SerND 集合のド・モルガンの法則target X＼(A∩B) = (X＼A)∪(X＼B) proof target X＼(A∩B) ⊆ (X＼A)∪(X＼B) proof assume x∈X＼(A∩B) ---(ass) expand by (集合の差) x∈X ∧ ¬(x∈A∩B) expand $.2.1 by (集合の共通部分) x∈X ∧ ¬(x∈A ∧ x∈B) rewrite $.2 by …

名前の管理が甘い、名前空間が粗末 ユニコードを考慮してない。アスキー偏重。 Mizar以外は、スクリプト言語またはそのシンタックスシュガー。 ブロック構造を意識してないか曖昧。 文書構造を意識してないか粗末 型クラスがあと付けで歪んでいたり問題を抱…

キーワード 意味 備考 target 目標は…である。 proof end （これから）証明しよう。 set …と置く。 by the way ところで リーフの開始 remark …であることを注意しておく。 concat …との連言を作る。 ∧導入 select …を抜き出すと、 ∧除去 add …との選言を作…

Mizar Isar let fix assume assume set let set def consider ... such that obtain ... where take (no equivalent) per cases ... proof ... qed suppose next assume (no keyword) have thus show hence then show thesis (?thesis) proof ... end proof …