← ファイル一覧
（保存にはログインが要ります）
1_basis/sample3.book
ヘッダ
行番号
title Russellのパラドクス import 2_sc1 mathel default thmel default
br txt 以上のような基礎の準備は、通常は、他のbookに書いておいてそれをincludeすることで実行されます。 txt このbookでは \(\cup\) の冪等性 を目標とします。 word ∪ prop ∪. := `X ∪ Y =_ \{ cls x | x ∈ X or x ∈ Y \}` raw \(\cup\) の冪等性<br> !let goal := `X ∪ X = X` thm goal -| W. prf goal // W. p-| O; goal h-| W. ;
表示（保存しません）
保存にはMatheliaへのログインが要ります。