book集

section 基本的な集合関数

subsection 空集合、有限集合
word ∅
prop ∅.
prop/thm ∅.' ◀ W.
prf ∅.' // W. -| O p;
    ∅.' -| W. h;
word set\n
abbr set
prop set\n.

subsection 合併、共通部分、差
word ∩
prop ∩. <- `X ∩ Y =_ \{ cls x ∈ X | x ∈ Y \}`

subsection べき集合
word ℘
prop ℘.
!prop/thm ℘.' ◀ W.
prf ℘.' -| W. p;

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 \}`

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 →IS.

subsection 濃度の比較
word =# ≤# <#
prop =#.
prop ≤#.
prop <#.
!prop/thm =#.' ◀ W.
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
!prop/thm ≤#.' ◀ W.
prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h;
txt Cantorの定理
thm `X <# ℘ X` ◀ W. ,, ax_s
prf α_ := `\{ \< pr x ; \{ set x \} \> Cls x | x ∈ X \}` ;
    Leα <- `α_ ⊂_ X ^^pr ℘ X` // W.'!=. -| set1. p;
    LeI <- `α =_ α_ ⟹ α ∈ X →I ℘ X` /// W.'!=. -| pr:0 ,, set1. p;
    goal_l <- `X ≤# ℘ X` --| ≤#.' ,, ax_s ,, Leα ,, LeI v;
    A_ := `\{ cls x ∈ X | {/}∃ y \, (\< pr x ; y \> ∈ f and x ∈ y) \}` ;
    LeA <- `A =_ A_ and f ∈ X → ℘ X ⟹ A ∈ ℘ X and {/}∃ x \, \< pr x ; A \> ∈ f` / W.' -| pr:0 p;
    goal_r <- `f {/}∈ X →S ℘ X` --| LeA ,, ax_s ,, →S. v;
    goal / W.' [&l -| goal_l || &r // W.' -| goal_r] p;
    goal -| W. ,, ax_s h;

freek100/63.book

`freek100/63.book`