book集

section 準備

subsection 空集合、2項関数
word ∅
prop ∅.
prop/thm ∅.' ◀ W.
prf ∅.' // W. -| O p; ∅.' -| W. h;
br
word ∪ ∩ ∖
prop ∪. <- `X ∪ Y =_ \{ cls x | x ∈ X or x ∈ Y \}`
prop ∩. <- `X ∩ Y =_ \{ cls x ∈ X | x ∈ Y \}`
prop ∖. <- `X ∖ Y =_ \{ cls x ∈ X | x {/}∈ Y \}`

subsection 順序対、直積
word \pr
abbr pr
word ◁ ▷
prop ◁.
prop ▷.
prop/thm pr:0 ◀ W.
prf pr:0 -| ◁. , ▷. p; pr:0 -| W. h;
br
word ^^pr
prop ^^pr. <- `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}`
word* *^ap
prop *^ap.
txt \(R(A)\) は \(A\) の \(R\) による像。主定理の説明では \(R[A]\) と書く。

subsection 写像、集合の大きさ比較
txt \(X \to Y\) は \(X\) から \(Y\) への写像全体の集合（写像は順序対の集合）。矢印の上の I・S・IS は単射・全射・全単射を表す。
word → →I →S →IS
prop →. <- `X → Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] \}`
!prop/thm →.' ◀ W.
prf →.' /// W.!=. -| O p; →.' -| W. h;
prop →I. <- `X →I Y =_ \{ cls f ∈ X → Y | ∀ y \, [ ！ x \, \< pr x ; y \> ∈ f ] \}`
prop →S. <- `X →S Y =_ \{ cls f ∈ X → Y | [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ f ] ] \}`
prop →IS.
!prop/thm →IS.' <- `X →IS Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] and [ ∀ y ∈ Y . [ ∃！ x \, \< pr x ; y \> ∈ f ] ] \}` ◀ W.
prf →IS.' ///// W.!=. -| pr:0 p; →IS.' -| W. h;
br
word =# ≤#
prop =#.
prop ≤#.
!prop/thm =#.' ◀ W.
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
!prop/thm ≤#.' ◀ W.
prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h;
br
word \fn
abbr fn

section 主定理
txt 単射 \(f : X \to Y\)、\(g : Y \to X\) に対して \(\Phi(B) = (X \setminus g[Y]) \cup g[f[B]]\) とする。
txt \(\Phi(B) \subset B\) を満たす集合 \(B\) すべてに属する \(X\) の元を集めて \(A\) とする（\(B = X\) が候補の1つ）。
txt \(\Phi\) は包含を保つ。各候補 \(B\) で \(A \subset B\)，\(\Phi(A) \subset \Phi(B) \subset B\) より \(\Phi(A) \subset A\)。
txt もう一度包含を保つことから \(\Phi(A)\) も候補になり \(A \subset \Phi(A)\)。
txt よって \(\Phi(A) = A\) で、\(g\) の単射性から \(g(y) \in A \iff y \in f[A]\)。
txt \(A\) の上では \(f\)、\(X \setminus A\) の上では \(g\) の逆を使って \(f' : X \to Y\) を作る。
txt \(f'\) は \(A\) を \(f[A]\) へ、\(X \setminus A\) を \(Y \setminus f[A]\) へ全単射に移す。
thm `[ chain X ≤# Y ≤# X ] ⟹ X =# Y` ◀ W. , ax_s
prf hyF <- `|f ∈ |X →I |Y` ;
    hyG <- `|g ∈ |Y →I |X` ;
    hyF0 <- `\< pr x ; y \> ∈ |f ⟹ x ∈ |X and y ∈ |Y` -| hyF // W.' , pr:0 p;
    hyG0 <- `\< pr y ; x \> ∈ |g ⟹ y ∈ |Y and x ∈ |X` -| hyG // W.' , pr:0 p;
    Φ := `｢ fn B ↦ (|X ∖ |g *^ap (|Y)) ∪ |g *^ap (|f *^ap (B)) ｣` ;
    |A_ := `\{ cls x ∈ |X | [ ∀ B \, (Φ ( B ) ⊂ B ⟹ x ∈ B) ] \}` ;
    hyA <- `|A =_ |A_` ;
    LAs <- `|A_ ⊂_ |X` -| O p;
    Φmono <- `B ⊂ C ⟹ Φ ( B ) ⊂ Φ ( C )` //// W. -| O p;
    Φsub <- `Φ ( |A ) ⊂ |A` / ⊂. / hyA [&l // W. -| hyG0 || &r -| hyA , Φmono , ⊂.] p;
    Φfix <- `|A = Φ ( |A )` / =. -| Φsub , Φmono , hyA , ⊂. p;
    |f'_ := `\{ \< pr x ; y \> Cls x ; y | (x ∈ |A and \< pr x ; y \> ∈ |f) or (x {/}∈ |A and \< pr y ; x \> ∈ |g) \}` ;
    hyf' <- `|f' =_ |f'_` ;
    LsubC <- `|f'_ ⊂_ |X ^^pr |Y` / W.!=. -| hyF0 , hyG0 p;
    LHfn <- `[ ∀ x ∈ |X . [ ∃！ y \, \< pr x ; y \> ∈ |f' ] ]` -| hyF // W. , hyG / W. , Φsub //// W. , hyf' , pr:0 p;
    LHbij <- `[ ∀ y ∈ |Y . [ ∃！ x \, \< pr x ; y \> ∈ |f' ] ]` -| hyF / W. , hyG // W.!=. , Φfix //// W. , hyf' , pr:0 p;
    `|X =# |Y` /// W.' -| hyf' , LsubC , LHfn , LHbij v;
    Lall2 <- `f ∈ X →I Y and g ∈ Y →I X ⟹ X =# Y` -| W. , ax_s h[fix];
    goal / ≤#.' -| Lall2 p;
    goal -| W. , ax_s h;
!txt ∃除去に置き換えた（10-06）：Lall・Lsub2・Lall1 と多ソートの段・h[lift] をやめ、hyA・hyf' を Lall2 の h[fix] で消す（根拠 LAs・LsubC・主張の sos の ax_s）。持ち上げ（multisort→tfl）に頼らなくなった。prf 1623→1182字・証明器 約0.34→0.20秒。下のメモの段名（Lall・Lsub2・Lall1）と秒は当時のもの。
!txt B,Cがs-Form(集合)のとき `B ⊂_ C` を使うのかシステムとしては問題ないが、外道な感じがしてきた。`B ⊂_ C`と書けば勝手に展開してくれるけど、それは便利でもあり怖いものでもある。
!txt 集合どうしの ⊂_・=_ を ⊂・= に戻した（10-05）：開いた定義が prf に出る（/ ⊂.・/ =.・sos の ⊂.）。Φmono・LHfn・LHbij は //// W. に（cvt が黙って開いていた1段ぶん）。速さは同じ（主定理 約0.76秒・依頼20本）、prf +19字。
!txt 速さ（10-04）：1回しか使わない仮定の段（hyF1・hyF2・hyG1・hyG2）を使う段へ直接書いたら、証明器への依頼が 26→20本・約2割速くなった（Codex の案）。残りは Prover9 の小さな段（各 0.007〜0.02秒＝ほぼ起動の時間）と Vampire 3段。slash・sos・投げ先を変えるだけでは縮まない＝縮めるなら組み立てを変える。
!txt LsubC・Lsub2 を消せるか（10-04）：f'_ を有界（Cls ∈ X ^^pr Y）にすれば Lsub2 は不要・LsubC は -| O の1段か消せる（LHfn・LHbij に hyf' / W.!=. と hyF0／hyG0 が要る）＝1522〜1569字。ただし証明器 約0.49→0.8秒（有界にしたこと自体で Lall1 の Vampire と LHfn・LHbij が重くなる）。有界にしないまま Lsub2 だけ消すのは無理（Lall1 が f'_ ⊂ X × Y を得る道が無い）＝速さを取って今の形。

articles1/25.book

`articles1/25.book`