未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
freek100/25.book
ヘッダ
行番号
title Cantor-Schröder-Bernsteinの定理 formel /common/default thmel /common/default option review quick:true;
section 論理と集合・クラス subsection 論理記号 word ⊥ word ¬ word and or ⇒ ⇔ word ⟹ ⟺ lower ⟹ lower ⟺ word ∀ ∃ subsection 省略記法 abbr chain abbr ∀ abbr ∃ abbr ∀+ abbr ∃+ word {/} lower {/} subsection 2項述語 word ∈_ word ⊂_ =_ prop ⊂_. prop =_. word ∈ ⊂ = subsection 内包記法 word \cls abbr cls abbr cls+ abbr Cls abbr ！ abbr ∃！ subsection 集合をクラスと見なすこと prop ⊂. <- `X ⊂ Y ⟺ X ⊂_ Y` prop =. <- `X = Y ⟺ X =_ Y` word Exi prop Exi. prop ax_s newpage section 基本的な集合関数 subsection 空集合、有限集合 word ∅ prop ∅. prop/thm ∅.' ◀ W. prf ∅.' // W. -| O p; ∅.' -| W. h; subsection 合併、共通部分、差 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; subsection 直積、像 word ^^pr prop ^^pr. <- `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}` word* *^ap prop *^ap. newpage section 集合の大きさ比較 subsection 写像 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 | [ ∀ x ; z ; y \, ( \< pr x ; y \> ∈ f and \< pr z ; y \> ∈ f ⟹ x = z ) ] \}` prop →S. <- `X →S Y =_ \{ cls f ∈ X → Y | [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ f ] ] \}` !prop/thm →I.' ◀ W. prf →I.' ///// W.!=. -| pr:0 p; →I.' -| W. h; !prop/thm →S.' ◀ W. prf Le <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ y ∈ Y` / W.' -| pr:0 p; →S.' /// W.!→. -| Le p; →S.' -| W. h; prop →IS. subsection 濃度の比較 word =# ≤# prop =#. prop ≤#. !prop/thm =#.' ◀ W. prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h; !prop/thm ≤#.' ◀ W. prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h; txt Cantor-Schröder-Bernsteinの定理 !let/thm CSBpiece <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = (X ∖ (g *^ap (Y))) ∪ (g *^ap (f *^ap (A))) ⟹ X =# Y` ◀ W. ,, ax_s prf K_ := `\{ cls p ∈ (X ∖ A) ^^pr Y | [ ∃ x ; y \, ( p = \< pr x ; y \> and \< pr y ; x \> ∈ g ) ] \}` ; K^ := `[ ∀ p (p ∈ K ⇔ (p ∈ (X ∖ A) ^^pr Y and [ ∃ x ; y \, ( p = \< pr x ; y \> and \< pr y ; x \> ∈ g ) ])) ]` ; L1^ := `K ⊂ X ^^pr Y` ; L2^ := `[ ∀ u ; v (\< pr u ; v \> ∈ K ⟹ (u ∈ X ∖ A and v ∈ Y and \< pr v ; u \> ∈ g)) ]` ; L3^ := `[ ∀ u ; v (u ∈ X ∖ A and v ∈ Y and \< pr v ; u \> ∈ g ⟹ \< pr u ; v \> ∈ K) ]` ; H_ := `((f ∩ (A ^^pr Y)) ∪ K)` ; Φ_ := `(X ∖ (g *^ap (Y))) ∪ (g *^ap (f *^ap (A)))` ; LeGval <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ x ∈ X` / W.' -| pr:0 p; LeUnL <- `P ⊂ P ∪ Q` -| ∪. ,, ⊂. p; LeUnR <- `Q ⊂ P ∪ Q` -| ∪. ,, ⊂. p; LeDif <- `u ∈ U ∖ B ⟹ u {/}∈ B` -| ∖. p; LeSubE <- `A ⊂ X and x ∈ A ⟹ x ∈ X` -| ⊂. p; LeGdom <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ y ∈ Y` / W.' -| pr:0 p; LeKmem <- `K^ ⟹ L1^ and L2^ and L3^` / ⊂. -| pr:0 ,, ∖. ,, ^^pr. p; LeTsub <- `L1^ and A ⊂ X ⟹ H_ ⊂ X ^^pr Y` / ⊂. / ∪. / ∩. / ^^pr. -| O p; LeHcase <- `L2^ and A ⊂ X and \< pr x ; y \> ∈ H_ ⟹ ((x ∈ A and \< pr x ; y \> ∈ f) or (x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g))` / ∪. / ∩. / ^^pr. / ∖. -| pr:0 p; LeHinA <- `A ⊂ X and x ∈ X and y ∈ Y and x ∈ A and \< pr x ; y \> ∈ f ⟹ \< pr x ; y \> ∈ H_` / ∪. / ∩. / ^^pr. / ∖. -| pr:0 p; LeHinB <- `L3^ and A ⊂ X and x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g ⟹ \< pr x ; y \> ∈ H_` / ∪. / ∩. / ^^pr. / ∖. -| pr:0 p; Lclosed <- `A = Φ_ ⟹ (g *^ap (f *^ap (A))) ⊂ A` -| LeUnR p; Loutside <- `g ∈ Y → X and A = Φ_ ⟹ [ ∀ x ∈ X ∖ A . [ ∃ y ∈ Y . \< pr y ; x \> ∈ g ] ]` -| LeUnL ,, ⊂. ,, ∖. ,, *^ap. ,, LeGdom p; LsepBase <- `F ∈ U →I V and G ∈ V →I U and [ ∀ z (z ∈ G *^ap (F *^ap (B)) ⟹ z ∈ B) ] and x ∈ U ∖ B and y ∈ V and \< pr y ; x \> ∈ G ⟹ y {/}∈ F *^ap (B)` -| *^ap. ,, LeDif p; Lsep <- `f ∈ X →I Y and g ∈ Y →I X and A = Φ_ and x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g ⟹ y {/}∈ f *^ap (A)` -| Lclosed ,, ⊂. ,, LsepBase p; LmapTot <- `L3^ and f ∈ X → Y and g ∈ Y → X and A ⊂ X and A = Φ_ ⟹ [ ∀ x ∈ X . [ ∃ y \, \< pr x ; y \> ∈ H_ ] ]` -| →. ,, LeGval ,, LeHinA ,, LeSubE ,, Loutside ,, LeHinB ,, ∖. v; Lfuniq <- `f ∈ X → Y and x ∈ X and \< pr x ; y0 \> ∈ f and \< pr x ; y1 \> ∈ f ⟹ y0 = y1` / →. -| O p; LmapUniq <- `L2^ and f ∈ X → Y and g ∈ Y →I X and A ⊂ X ⟹ [ ∀ x ; y0 ; y1 (\< pr x ; y0 \> ∈ H_ and \< pr x ; y1 \> ∈ H_ ⟹ y0 = y1) ]` -| LeHcase ,, Lfuniq ,, →I.' ,, LeDif ,, LeSubE p; LinjAB <- `f ∈ X →I Y and g ∈ Y →I X and A = Φ_ and x0 ∈ A and \< pr x0 ; y \> ∈ f and x1 ∈ X ∖ A and y ∈ Y and \< pr y ; x1 \> ∈ g ⟹ ⊥` -| Lsep ,, *^ap. p; LinjPt <- `L2^ and f ∈ X →I Y and g ∈ Y →I X and g ∈ Y → X and A ⊂ X and A = Φ_ ⟹ [ ∀ x0 ; x1 ; y (\< pr x0 ; y \> ∈ H_ and \< pr x1 ; y \> ∈ H_ ⟹ x0 = x1) ]` -| LeHcase ,, →I.' ,, LinjAB ,, Lfuniq v; LinA <- `A = Φ_ and x ∈ A and x ∈ g *^ap (Y) ⟹ x ∈ (g *^ap (f *^ap (A)))` -| ∪. ,, ∖. p; Lback <- `g ∈ Y → X and g ∈ Y →I X and A = Φ_ ⟹ [ ∀ y ∈ Y ∖ (f *^ap (A)) . [ ∃ x ∈ X ∖ A . \< pr y ; x \> ∈ g ] ]` / ∖. -| →. ,, LeGval ,, →I.' ,, LinA ,, *^ap. p; Lsurj0 <- `g ∈ Y → X and g ∈ Y →I X and A ⊂ X and A = Φ_ ⟹ [ ∀ y ∈ Y . ([ ∃ x \, (x ∈ X and x ∈ A and \< pr x ; y \> ∈ f) ] or [ ∃ x \, (x ∈ X ∖ A and \< pr y ; x \> ∈ g) ]) ]` -| Lback ,, *^ap. ,, ∖. ,, LeSubE p; LsurjPt <- `L3^ and g ∈ Y → X and g ∈ Y →I X and A ⊂ X and A = Φ_ ⟹ [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ H_ ] ]` -| Lsurj0 ,, LeHinA ,, LeHinB p; Lmap <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = Φ_ and L1^ and L2^ and L3^ ⟹ H_ ∈ X → Y` / →. -| LmapTot ,, LmapUniq ,, LeTsub ,, →I.' p; Lpiece_c <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = Φ_ and L1^ and L2^ and L3^ ⟹ H_ ∈ X →IS Y` / →IS. / ∩. -| Lmap ,, LinjPt ,, LsurjPt ,, →I.' ,, →S.' p; LeEK <- `Exi K_` --| ax_s v; LeKE <- `[ ∃ K \, K^ ]` -| LeEK p; Lpiece_K <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = Φ_ and K^ ⟹ H_ ∈ X →IS Y` -| Lpiece_c ,, LeKmem v; CSBpiece / =#.' -| Lpiece_K ,, LeKE v; CSBpiece -| W. ,, ax_s h; thm `[ chain X ≤# Y ≤# X ] ⟹ X =# Y` ◀ W. ,, ax_s prf A_ := `\{ cls x ∈ X | [ ∀ B ((B ⊂ X and (X ∖ (g *^ap (Y))) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B) ⟹ x ∈ B) ] \}` ; Φ_ := `(X ∖ (g *^ap (Y))) ∪ (g *^ap (f *^ap (A)))` ; M^ := `[ ∀ x (x ∈ A ⇔ (x ∈ X and [ ∀ B ((B ⊂ X and (X ∖ (g *^ap (Y))) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B) ⟹ x ∈ B) ])) ]` ; LeEA <- `Exi A_` --| ax_s v; LeGval <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ x ∈ X` / W.' -| pr:0 p; LeImX <- `g ∈ Y → X ⟹ g *^ap (Z) ⊂ X` -| *^ap. ,, ⊂. ,, LeGval p; Lmono <- `[ chain A ⊂ B ⊂ X ] and f ∈ X → Y and g ∈ Y → X ⟹ (g *^ap (f *^ap (A))) ⊂ (g *^ap (f *^ap (B)))` /// W.' -| pr:0 p; LeSub <- `M^ ⟹ A ⊂ X` / ⊂. -| O p; LeLow <- `M^ and B ⊂ X and (X ∖ (g *^ap (Y))) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B ⟹ A ⊂ B` / ⊂. -| O p; LeTrans <- `[ chain P ⊂ Q ⊂ R ] ⟹ P ⊂ R` -| ⊂. p; LeUnSub <- `P ⊂ B and Q ⊂ B ⟹ P ∪ Q ⊂ B` -| ∪. ,, ⊂. p; LeUnL <- `P ⊂ P ∪ Q` -| ∪. ,, ⊂. p; LeUnR <- `Q ⊂ P ∪ Q` -| ∪. ,, ⊂. p; LeDsubB <- `f ∈ X → Y and g ∈ Y → X and M^ and B ⊂ X and (X ∖ (g *^ap (Y))) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B ⟹ Φ_ ⊂ B` -| Lmono ,, LeLow ,, LeTrans ,, LeUnSub v; LeDX <- `g ∈ Y → X ⟹ Φ_ ⊂ X` -| LeImX ,, ⊂. ,, ∪. ,, ∖. p; LeD1 <- `f ∈ X → Y and g ∈ Y → X and M^ ⟹ Φ_ ⊂ A` -| LeDsubB ,, LeDX ,, ⊂. v; LeDc1 <- `f ∈ X → Y and g ∈ Y → X and M^ ⟹ (g *^ap (f *^ap (Φ_))) ⊂ (g *^ap (f *^ap (A)))` -| Lmono ,, LeD1 ,, LeSub v; LeDclosed <- `f ∈ X → Y and g ∈ Y → X and M^ ⟹ (g *^ap (f *^ap (Φ_))) ⊂ (Φ_)` -| LeDc1 ,, LeTrans ,, LeUnR v; LeD2 <- `f ∈ X → Y and g ∈ Y → X and M^ ⟹ A ⊂ Φ_` -| LeLow ,, LeDX ,, LeUnL ,, LeDclosed v; LeAnti <- `[ chain X ⊂ Y ⊂ X ] ⟹ X = Y` / =. -| ⊂. p; Lfixed_c <- `f ∈ X → Y and g ∈ Y → X and M^ ⟹ A ⊂ X and A = Φ_` -| LeSub ,, LeD1 ,, LeD2 ,, LeAnti v; LeAE <- `[ ∃ A \, M^ ]` -| LeEA p; Lfixed <- `f ∈ X →I Y and g ∈ Y →I X ⟹ [ ∃ A (A ⊂ X and A = Φ_) ]` / →I.' -| Lfixed_c ,, LeAE v; goal / ≤#.' -| Lfixed ,, CSBpiece p; goal -| W. ,, ax_s h;
表示（保存しません）
保存にはMatheliaへのログインが要ります。