現代数学概説Ⅰ
1章 $1 例題9 M⊆M', N⊆N⇒MxN⊆M'xN'であって、
(MxN).c(Ωmn) = (M.c(Ωm)xN') ∪ (M'xN.(Ω=N')).
注) AxBはA,Bの直積を表す。A.c(Ωxx)はAの補集合で(Ω)内は母集合を表す。
Ωmn=M'xN', Ωm=M', Ωn=N'.
----------------------------------------
a) 補集合の定義より、
(MxN).c = (M'xN')-MxN.
b1) (M.c(Ωm)xN') =(M'-M)xN' = M'xN'-MxN'
b2) (M'xN.c(Ωn)) =M'x(N'-N) = M'xN'-M'xN
c) b1,2より
(M.c(Ωm)xN') ∪ (M'xN.(Ω=N')) = (M'xN'-MxN') ∪ (M'xN'-M'xN)
= (M'xN')-MxN.
よって、a,c)より
(MxN).c(Ωmn) = (M.c(Ωm)xN') ∪ (M'xN.(Ω=N')).
---------------------------------------
Coq証明も付けたい所だけど、直積の形式化が良く分からない。
俺のCoq技はこの程度です。また、現代数学概説Ⅰの例題をこなす目的は、SOFTWARE FOUNDATIONSの中に出てくる非形式的証明の練習である。
現代数学概説Ⅰ最後のページは602。。
この調子では何年かかるか。。汗）
Coq解説のSOFTWARE FOUNDATIONSを手掛けて、初めてわかりました。
数学勉強はロールプレイイングゲーム？？
とにかく進みながら経験値を高めて本丸を攻略する。
行きずまったら、リセットボタン。。汗）
SOFTWARE FOUNDATIONSは
～Logic.vまでを３回目攻略中でもうすぐ終わりそうです。
本丸は「ホーア論理」先は長い。。
