← ファイル一覧
（保存にはログインが要ります）
book1/book1-2.book
ヘッダ
行番号
title 第一冊 第二部 import book1-1
!txt ── book1/2a-1 ── !txt 第一冊専用: 順序対と成分。 section a word \pr abbr pr raw <br> word ◁ ▷ prop ◁. prop ▷. prop- pr:0 thm W. pr:0 p-| ◁. ,, ▷. pr:0 =| W. !txt ── book1/2a-2 ── !txt 第一冊専用: 直積と関係。 word ^^pr prop ^^pr. := `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}` raw <br>一般の集合に対して定義域・値域を作ります。<br> word ^◁ ^▷ prop ^◁. := `^◁ (R) =_ \{ cls x | ∃ y \, \< pr x ; y \> ∈ R \}` prop ^▷. := `^▷ (R) =_ \{ cls y | ∃ x \, \< pr x ; y \> ∈ R \}` word* *^ap prop *^ap. := `R *^ap (A) =_ \{ cls y | ∃ x (x ∈ A and \< pr x ; y \> ∈ R) \}` !txt ── book1/2a-3 ── !txt 第一冊専用: 定義域、値域、像。 word Rel prop Rel. := `Rel =_ \{ cls R | [ ∀ p ∈ R . [ ∃ x ; y p = \< pr x ; y \> ] ] \}` prop- Rel.' thm W. Rel.' / ⊂. / ^^pr. / ^◁. / ^▷. p-| O Rel.' =| W. ∖ =. prop- Rel.. thm W. Rel.. p-| ◁. ,, ▷. Rel.. =| W. !txt ── book1/2a-4 ── !txt 第一冊専用: 逆関係と合成。 word ^sw prop ^sw. := `R ^sw =_ \{ \< pr y ; x \> Cls x ; y | \< pr x ; y \> ∈ R \}` prop- ^sw:0 thm W. ^sw:0 / ⊂. / ^^pr. / ^sw. / ^^pr. p-| pr:0 ^sw:0 =| W. ∖ =. prop- ^sw:I thm W. ^sw:I /2 =. / ^sw. / ^sw. p-| pr:0 ,, Rel.. ^sw:I =| W. raw <br> word ∘ prop ∘. prop- comp:0 thm W. comp:0 / ⊂. / ^^pr. / ∘. / ^^pr. p-| pr:0 comp:0 =| W. ∖ =. prop- comp:A thm W. comp:A /2 =. / ∘. / ∘. / ∘. / ∘. p-| ◁. ,, ▷. ,, Rel.. comp:A =| W. prop- comp:X thm W. comp:X /2 =. / ^sw. / ∘. / ^sw. p-| pr:0 comp:X =| W. !txt ── book1/2b-1 ── !txt 第一冊専用: 写像。 section b word → prop →. := `X → Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . ∃！ y \, (\< pr x ; y \> ∈ f) ] \}` !txt ── book1/2b-3 ── !txt 第一冊専用: 単射・全射・全単射。 word ->I ->S 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 ] \}` word ∩_ word ->IS prop ->IS. := `X ->IS Y =_ (X ->I Y) ∩_ (X ->S Y)` !txt ── book1/2c-1 ── !txt 第一冊専用: 写像による集合の大きさの比較。 section c word =# le# <# prop =#. prop le#. prop <#. !txt ── book1/2c-2 ── !txt 第一冊専用: ベルンシュタインの構成。 raw カントール＝ベルンシュタインの定理<br> form `X le# Y and Y le# X ⟹ X =# Y` thm W. ,, ax_s0 goal* := `[ chain X le# Y le# X ] ⟹ X =# Y` Lfixed := `f ∈ X ->I Y and g ∈ Y ->I X ⟹ [ ∃ A (A ⊂ X and A = (X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A)))) ]` C_ := `\{ cls B ∈ ℘ |X | (|X ∖ ^▷ (|g)) ⊂ B and (|g *^ap (|f *^ap (B))) ⊂ B \}` LeCbd := `C_ ⊂_ ℘ |X` LeCbd /// W. p-| pr:0 `Exi C_` p-| LeCbd LeFamily := `[ ∀ B (B ∈ |C ⇔ (B ⊂ |X and (|X ∖ ^▷ (|g)) ⊂ B and (|g *^ap (|f *^ap (B))) ⊂ B)) ]` LeFamily / `|C =_ C_` // W. p-| pr:0 LeX := `|X ∈ |C` LeX / LeFamily ///// W. p-| `|f ∈ |X ->I |Y` //// W. ,, `|g ∈ |Y ->I |X` //// W. ,, pr:0 LeNon := `|C {/}= ∅` LeNon / ∅.. p-| LeX Lmono := `A ⊂ B and B ⊂ |X and |f ∈ |X → |Y and |g ∈ |Y → |X ⟹ (|g *^ap (|f *^ap (A))) ⊂ (|g *^ap (|f *^ap (B)))` Lmono ///// W. p-| pr:0 LeCap := `⋂ |C =_ ⋂_ |C` LeCap p-| LeNon ,, ⋂.' ,, ∅.. LeSub := `⋂ |C ⊂ |X` LeSub // W. p-| LeNon ,, LeX LeKsub := `B ∈ |C ⟹ ⋂ |C ⊂ B` LeKsub p-| LeCap ,, ⊂. LeDsubB := `B ∈ |C ⟹ (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C))) ⊂ B` LeDsubB p-| LeFamily ,, Lmono ,, LeKsub ,, LeSub ,, ⊂. ,, ∪. ,, `|f ∈ |X ->I |Y` / ->I. ,, `|g ∈ |Y ->I |X` / ->I. LeD1 := `(|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C))) ⊂ ⋂ |C` LeD1 p-| LeCap ,, LeDsubB ,, ⊂. LeGval := `\< pr y ; x \> ∈ |g ⟹ x ∈ |X` LeGval p-| `|g ∈ |Y ->I |X` / ->I. / →. / ⊂. / ^^pr. ,, pr:0 LeDX := `(|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C))) ⊂ |X` LeDX p-| ⊂. ,, ∪. ,, ∖. ,, *^ap. ,, LeGval LeDclosed := `(|g *^ap (|f *^ap ((|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C)))))) ⊂ ((|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C))))` LeDclosed p-| Lmono ,, LeD1 ,, LeSub ,, ⊂. ,, ∪. ,, `|f ∈ |X ->I |Y` / ->I. ,, `|g ∈ |Y ->I |X` / ->I. LeDin := `(|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C))) ∈ |C` LeDin p-| LeFamily ,, LeDX ,, LeDclosed ,, ⊂. ,, ∪. LeD2 := `⋂ |C ⊂ (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C)))` LeD2 p-| LeCap ,, LeDin ,, ⊂. Lfix := `⋂ |C = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (⋂ |C)))` Lfix / =.. p-| LeD1 ,, LeD2 Lfixed_c := `[ ∃ A (A ⊂ |X and A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (A)))) ]` Lfixed_c p-| LeSub ,, Lfix Lfixed_c =| W. ,, `|C =_ C_` ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` Lfixed_c e-| W. ,, `Exi C_` ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` Lfixed_c =| W. ,, ax_s0 ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` Lfixed d-| W. ,, ax_s0 Lpiece := `f ∈ X ->I Y and g ∈ Y ->I X and A ⊂ X and A = (X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A))) ⟹ [ ∃ h \, h ∈ X ->IS Y ]` H_ := `\{ \< pr x ; y \> Cls x ; y | x ∈ |X and y ∈ |Y and ((x ∈ |A and \< pr x ; y \> ∈ |f) or (x ∈ |X ∖ |A and \< pr y ; x \> ∈ |g)) \}` LeHbd := `H_ ⊂_ |X ^^pr |Y` LeHbd /// W. p-| pr:0 `Exi H_` p-| LeHbd LeHmem := `[ ∀ u ; v (\< pr u ; v \> ∈ |H ⇔ (u ∈ |X and v ∈ |Y and ((u ∈ |A and \< pr u ; v \> ∈ |f) or (u ∈ |X ∖ |A and \< pr v ; u \> ∈ |g)))) ]` LeHmem / `|H =_ H_` p-| pr:0 Lclosed := `(|g *^ap (|f *^ap (|A))) ⊂ |A` Lclosed / W. p-| `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` ,, ∪. LeCupIn := `B = K ∪ T and z ∈ T ⟹ z ∈ B` LeCupIn / W. p-| ∪. LclosedPt := `[ ∀ z (z ∈ |g *^ap (|f *^ap (|A)) ⟹ z ∈ |A) ]` LclosedPt p-| `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` ,, LeCupIn LnotK := `[ ∀ x ∈ |X ∖ |A . x {/}∈ |X ∖ ^▷ (|g) ]` LnotK / W. p-| `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` ,, ∪. ,, ∖. Lrange := `K = U ∖ R and x ∈ U and x {/}∈ K ⟹ x ∈ R` Lrange / W. p-| ∖. Lpair := `[ ∀ x ∈ ^▷ (|g) . [ ∃ y ∈ |Y . \< pr y ; x \> ∈ |g ] ]` Lpair /// W. p-| `|g ∈ |Y ->I |X` //// W. ,, ^▷. ,, pr:0 Loutside := `[ ∀ x ∈ |X ∖ |A . [ ∃ y ∈ |Y . \< pr y ; x \> ∈ |g ] ]` Loutside // W. p-| LnotK ,, Lrange ,, Lpair LeImage := `u ∈ R *^ap (B) and \< pr u ; v \> ∈ S ⟹ v ∈ S *^ap (R *^ap (B))` LeImage / W. p-| *^ap. LeDif := `u ∈ U ∖ B ⟹ u {/}∈ B` LeDif / W. 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)` LsepBase p-| LeImage ,, LeDif LinvBranch := `[ ∀ x ; y (x ∈ |X ∖ |A and \< pr x ; y \> ∈ |H ⟹ y ∈ |Y and \< pr y ; x \> ∈ |g) ]` LinvBranch ///// W. p-| ∖. ,, pr:0 ,, LeHmem Lsep := `[ ∀ x ; y (x ∈ |X ∖ |A and \< pr x ; y \> ∈ |H ⟹ y {/}∈ |f *^ap (|A)) ]` Lsep p-| `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` ,, LclosedPt ,, LinvBranch ,, LsepBase LmapBd := `|H ⊂ |X ^^pr |Y` LmapBd p-| LeHbd ,, `|H =_ H_` ,, ⊂. ,, ^^pr. Lftot := `[ ∀ x ∈ |X . [ ∃ y \, \< pr x ; y \> ∈ |f ] ]` Lftot p-| `|f ∈ |X ->I |Y` / ->I. / →. Lfval := `\< pr x ; y \> ∈ |f ⟹ y ∈ |Y` Lfval p-| `|f ∈ |X ->I |Y` / ->I. / →. / ⊂. / ^^pr. ,, pr:0 LmapTot := `[ ∀ x ∈ |X . [ ∃ y \, \< pr x ; y \> ∈ |H ] ]` LmapTot p-| Lftot ,, Lfval ,, Loutside ,, LeHmem ,, ∖. ,, pr:0 Lfuniq := `x ∈ |X and \< pr x ; y0 \> ∈ |f and \< pr x ; y1 \> ∈ |f ⟹ y0 = y1` Lfuniq p-| `|f ∈ |X ->I |Y` / ->I. / →. Lginj := `\< pr y0 ; x \> ∈ |g and \< pr y1 ; x \> ∈ |g ⟹ y0 = y1` Lginj p-| `|g ∈ |Y ->I |X` / W. LmapUniq := `[ ∀ x ; y0 ; y1 (\< pr x ; y0 \> ∈ |H and \< pr x ; y1 \> ∈ |H ⟹ y0 = y1) ]` LmapUniq p-| LeHmem ,, Lfuniq ,, Lginj ,, ∖. ,, pr:0 Lmap := `|H ∈ |X → |Y` Lmap / W. p-| LmapBd ,, LmapTot ,, LmapUniq Lfinj := `\< pr x0 ; y \> ∈ |f and \< pr x1 ; y \> ∈ |f ⟹ x0 = x1` Lfinj p-| `|f ∈ |X ->I |Y` / W. Lgfun := `y ∈ |Y and \< pr y ; x0 \> ∈ |g and \< pr y ; x1 \> ∈ |g ⟹ x0 = x1` Lgfun p-| `|g ∈ |Y ->I |X` / ->I. / →. LinjPt := `[ ∀ x0 ; x1 ; y (\< pr x0 ; y \> ∈ |H and \< pr x1 ; y \> ∈ |H ⟹ x0 = x1) ]` LinjPt p-| LeHmem ,, Lfinj ,, Lgfun ,, Lsep ,, ∖. ,, *^ap. ,, pr:0 Linj := `|H ∈ |X ->I |Y` Linj / W. p-| Lmap ,, LinjPt Lback := `[ ∀ y ∈ |Y ∖ (|f *^ap (|A)) . [ ∃ x ∈ |X ∖ |A . \< pr y ; x \> ∈ |g ] ]` Lgtot := `[ ∀ y ∈ |Y . [ ∃ x \, \< pr y ; x \> ∈ |g ] ]` Lgtot p-| `|g ∈ |Y ->I |X` / ->I. / →. Lgval := `\< pr y ; x \> ∈ |g ⟹ x ∈ |X` Lgval p-| `|g ∈ |Y ->I |X` / ->I. / →. / ⊂. / ^^pr. ,, pr:0 Lback p-| Lgtot ,, Lgval ,, Lginj ,, `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` ,, ∖. ,, ^▷. ,, *^ap. ,, ∪. ,, pr:0 LsurjPt := `[ ∀ y ∈ |Y . [ ∃ x \, \< pr x ; y \> ∈ |H ] ]` LsurjPt p-| LeHmem ,, Lback ,, `|A ⊂ |X` ,, ∖. ,, *^ap. ,, ⊂. ,, pr:0 Lsurj := `|H ∈ |X ->S |Y` Lsurj / W. p-| Lmap ,, LsurjPt Lbij := `|H ∈ |X ->IS |Y` Lbij / W. p-| Linj ,, Lsurj Lpiece_c := `[ ∃ h \, h ∈ |X ->IS |Y ]` Lpiece_c p-| Lbij Lpiece_c =| W. ,, `|H =_ H_` ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` ,, `|A ⊂ |X` ,, `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` Lpiece_c e-| W. ,, `Exi H_` ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` ,, `|A ⊂ |X` ,, `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` Lpiece_c =| W. ,, ax_s0 ,, `|f ∈ |X ->I |Y` ,, `|g ∈ |Y ->I |X` ,, `|A ⊂ |X` ,, `|A = (|X ∖ ^▷ (|g)) ∪ (|g *^ap (|f *^ap (|A)))` Lpiece d-| W. ,, ax_s0 Lbuild := `[ ∀ f ; g (f ∈ X ->I Y and g ∈ Y ->I X ⟹ [ ∃ h \, h ∈ X ->IS Y ]) ]` Lbuild p-| Lfixed ,, Lpiece goal* / le#. / =#. p-| Lbuild goal* =| W. ,, ax_s0 !txt ── book1/2c-3 ── !txt 第一冊専用: カントールの定理。 raw <b>カントールの定理</b><br> form `X <# ℘ X` raw <br> thm W. ,, ax_s0 goal* := `X <# ℘ X` Lle_c := `|X le# ℘ |X` Lef := `f_ ⊂_ |X ^^pr ℘ |X` `Exi f_` p-| Lef f_ := `\{ \< pr x ; \{ set x \} \> Cls x | x ∈ |X \}` Lef /// W. p-| set1. LeI := `|f ∈ |X ->I ℘ |X` LeI / ->I. / →. / ⊂. / `|f =_ f_` / ^^pr. / ℘. / ⊂. / set1. p-| pr:0 ,, set1. Lle_c / W. p-| LeI Lle_c =| W. ,, `|f =_ f_` Lle_c e-| W. ,, `Exi f_` Lle_c =| W. ,, ax_s0 Lle := `X le# ℘ X` Lle a-| W. ,, ax_s0 LnoSPt := `f {/}∈ X ->S ℘ X` A_ := `\{ cls x ∈ |X | {/}∃ y \, (\< pr x ; y \> ∈ |f and x ∈ y) \}` LeA := `A_ ⊂_ |X` LeA // W. p-| O `Exi A_` p-| LeA Le0 := `|A ∈ ℘ |X` Le0 // W. / `|A =_ A_` p-| O Luniq := `g ∈ U → V and x ∈ U and \< pr x ; y0 \> ∈ g and \< pr x ; y1 \> ∈ g ⟹ y0 = y1` Luniq / W. ///// W. p-| pr:0 Ldiag := `|f ∈ |X → ℘ |X and x ∈ |X and \< pr x ; |A \> ∈ |f ⟹ ⊥` Ldiag ///// W. p-| Luniq ,, pr:0 ,, `|A =_ A_` Lmem := `|f ∈ |X → ℘ |X and \< pr x ; y \> ∈ |f ⟹ x ∈ |X` Lmem / →. / ⊂. / ^^pr. p-| pr:0 `|f {/}∈ |X ->S ℘ |X` / W. p-| Le0 ,, Ldiag ,, Lmem `|f {/}∈ |X ->S ℘ |X` =| W. ,, `|A =_ A_` `|f {/}∈ |X ->S ℘ |X` e-| W. ,, `Exi A_` `Exi A_` p-| O `|f {/}∈ |X ->S ℘ |X` =| W. ,, ax_s0 LnoSPt a-| W. ,, ax_s0 LbiS := `h ∈ X ->IS Y ⟹ h ∈ X ->S Y` LbiS / ->IS. p-| O Lneq := `X {/}=# ℘ X` Lneq / W. p-| LnoSPt ,, LbiS goal* / W. p-| Lle ,, Lneq goal* =| W. ,, ax_s0 review-link book1-2
保存にはログイン（ページ編集の権限）が要ります。