book集

section 主定理
!txt \chi_A =_ { <x, n> in X times 2 | x in A <=> n = 0 \} のように作ると良くない？ ∪ ∖ はいらなくなる？
!txt 2026-10-14：articles2new/52a-x で試した。\(\chi_A\) を内包 \(\{ (x, v) \in X \times \{a, b\} \mid x \in A \iff v = a \}\) で作ると ∪ も ∖ も要らない（40行・この本は48行）。ただし逆向きの対応に逆像 \(f^{-1}[\{a\}]\) を使う。
txt \(a \neq b\) とする。\(A \subset X\) に、\(A\) の上で \(a\)、\(X \setminus A\) の上で \(b\) をとる写像 \(\chi_A = (A \times \{a\}) \cup ((X \setminus A) \times \{b\})\) を対応させると、\(\wp X\) から \(X \to \{a, b\}\) への全単射になる。
txt 逆に、写像 \(f : X \to \{a, b\}\) には \(\{ x \in X \mid f(x) = a \}\) を対応させる（分出公理で集合になる）。
thm `a {/}= b ⟹ ℘ X =# X → \{ set a ; b \}` ◀ W. , ax_s
prf hyab <- `|a {/}= |b` ;
    Lχm <- `\< pr x ; y \> ∈ A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} ⟺ (x ∈ A and y = |a) or (x ∈ |X and x {/}∈ A and y = |b)` /// W.!=. -| pr:0 p;
    Lχ <- `A ⊂ |X ⟹ A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} ∈ |X → \{ set |a ; |b \}` / →.' [&l //// W.'!=. -| O || &r -| Lχm , hyab] p;
    Lχi <- `A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} = C ^^pr \{ set |a \} ∪ (|X ∖ C) ^^pr \{ set |b \} ⟹ A = C` / =. -| Lχm , hyab p;
    hyg <- `|g ∈ |X → \{ set |a ; |b \}` ;
    P_ := `\{ cls x ∈ |X | \< pr x ; |a \> ∈ |g \}` ;
    hyP <- `|P =_ P_` ;
    `P_ ⊂_ |X` /// W.!=. -| O p;
    LPm <- `x ∈ |P ⟺ x ∈ |X and \< pr x ; |a \> ∈ |g` -| hyP p;
    LPx <- `|P ⊂ |X` / ⊂. -| LPm p;
    Ls1 <- `z ∈ |g ⟹ z ∈ |P ^^pr \{ set |a \} ∪ (|X ∖ |P) ^^pr \{ set |b \}` -| LPm , Lχm , set2.' , hyg / →.' / ^^pr. v;
    Ls2p <- `\< pr x ; y \> ∈ |P ^^pr \{ set |a \} ∪ (|X ∖ |P) ^^pr \{ set |b \} ⟹ \< pr x ; y \> ∈ |g` -| LPm , Lχm , set2.' , hyg / →.' v;
    Lzp <- `z ∈ |P ^^pr \{ set |a \} ∪ (|X ∖ |P) ^^pr \{ set |b \} ⟹ [ ∃ x ; y \, z = \< pr x ; y \> ]` / ∪. / ^^pr. -| O p;
    `[ ∃ A \, A ⊂ |X and |g = A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} ]` / =. -| LPx , Ls1 , Lzp , Ls2p p;
    Lex <- `g ∈ X → \{ set a ; b \} ⟹ [ ∃ A \, A ⊂ X and g = A ^^pr \{ set a \} ∪ (X ∖ A) ^^pr \{ set b \} ]` -| W. , ax_s h[fix];
    |F_ := `\{ \< pr A ; A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} \> Cls A | A ∈ ℘ |X \}` ;
    hyF <- `|F =_ |F_` ;
    LFm <- `\< pr A ; g \> ∈ |F ⟺ A ⊂ |X and g = A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \}` -| hyF / ℘. , pr:0 p;
    LFz <- `z ∈ |F ⟹ [ ∃ A \, A ⊂ |X and z = \< pr A ; A ^^pr \{ set |a \} ∪ (|X ∖ A) ^^pr \{ set |b \} \> ]` -| hyF / ℘. p;
    `|F_ ⊂_ ℘ |X ^^pr (|X → \{ set |a ; |b \})` / ^^pr. / ℘. -| Lχ p;
    LF0 <- `|F ⊂ ℘ |X ^^pr (|X → \{ set |a ; |b \})` / ⊂. / ^^pr. / ℘. -| LFz , Lχ p;
    LF1 <- `[ ∀ A ∈ ℘ |X . [ ∃！ g \, \< pr A ; g \> ∈ |F ] ]` / ℘. -| LFm p;
    LF2 <- `[ ∀ g ∈ (|X → \{ set |a ; |b \}) . [ ∃！ A \, \< pr A ; g \> ∈ |F ] ]` -| LFm , Lχi , Lex p;
    LFi <- `|F ∈ ℘ |X →IS (|X → \{ set |a ; |b \})` / →IS.' -| LF0 , LF1 , LF2 p;
    `℘ |X =# |X → \{ set |a ; |b \}` / =#.' -| LFi p;
    goal -| W. , ax_s h[fix];
!txt 外せなかったもの（10-16）：Ls1・Ls2p の sos の set2.'（Lχm の中の \{ set |a ; |b \} は閉じたまま使う＝hyg / set2.'・goal にも付けると Vampire が時間切れ）。LF0 の / ⊂. / ^^pr. / ℘. は W.（// W.・W.!=.・W.!→.）にすると Lχ と噛み合わない。

articles2/52a.book

`articles2/52a.book`