book集

!txt ── book1/1a-1 ──
!txt 第一冊専用: 文、集合変数、等号。
section a
word ⊤ ⊥
word ¬
word and or ⇒ ⇔
raw 
word ⟹ ⟺
word ∀ ∃
word ∈ ⊂ =
raw 
abbr ∀+
abbr ∃+
abbr chain
!prop ⇔3 from ⇔\n at=3
!thm O
 ⇔3* := `( [ chain |P1^ ⇔ |P2^ ⇔ |P3^ ] ) ⟺ ( [ chain |P1^ ⇒ |P2^ ⇒ |P3^ ⇒ |P1^ ] )`
 ⇔3* p-| O
 ⇔3 h-| O
raw 
word {/}
lower {/}

!txt ── book1/1a-2 ──
!txt 第一冊専用: 集合変数の量化と有界量化。
word \cls
abbr cls
abbr cls+
txt 以下の左辺では `$_X` が表記上無視されます。
abbr Cls
raw 「(クラスの)元である」という関係が重要です。Mathelでは「p-Formへの代入」も記述できます。 
word ∈_
txt cvt …`$X ∈_ \{ cls $x | $P \}`≃ `$P` の `$x` に `$X` を代入したもの
txt- 例　`Y ∈_ \{ cls X | x ∈ X \}`≃`x ∈ Y`

!txt ── book1/1a-3 ──
!txt book1/1a-3.php migration fixture
word ⊂_ =_
prop ⊂_.
prop =_.
txt- 集合は自然にクラスと見なされます。 Form内でc-Formがあるべき所にあるs-Form ${\tt X}$ は $\{x \mid x \in {\tt X}\}$ に置き換えられます。 例　`x ∈_ X`≃`x ∈_ \{ cls x | x ∈ X \}`
br
br
txt 通常の教科書と逆で、この教科書では`⊂`の定義が`⊂_`の定義から誘導されます。
prop ⊂. := `X ⊂ Y ⟺ X ⊂_ Y`
raw 次の$\Longleftarrow$は外延性公理と呼ばれます。 
prop =. := `X = Y ⟺ X =_ Y`
prop- =..
thm W.
 =.. / W. p-| O
 =.. h-| W.

!txt ── book1/1a-4 ──
!txt 第一冊専用: 写像。
word ！ ∃！
prop ！.
prop ∃！.
raw 
abbr ！
abbr ∃！

!txt ── book1/1b-1 ──
!txt 第一冊専用: 空集合、一点集合、対。
section b
word \V
prop \V.
form `x ∈_ \V`
thm O
 `x ∈_ \V` p-| O
form `X ⊂_ \V`
thm O
 `X ⊂_ \V` p-| O
raw 
word ∅
prop ∅.
thm W.
 goal := `x {/}∈ ∅`
 goal / W. p-| O
 goal h-| W.
thm W.
 goal := `∅ ⊂ X`
 goal // W. p-| O
 goal h-| W.
prop- ∅..
thm W.
 ∅.. // W. p-| O
 ∅.. h-| W.

!txt ── book1/1b-2 ──
!txt 第一冊専用: 集合の内部を条件で切り出す限定分離。
raw クラスが集合となるか、が議論されます。 
word Exi
prop Exi.
raw 集合の部分クラスは集合である、ことが要請されます。これが公理 ax_s0 です。 
prop ax_s0
raw 
raw (大きすぎて)集合になれないクラスは固有クラスと呼ばれます。最初の例はRusselクラスです。 
word \V0
prop \V0.
thm O
 goal := `¬ Exi \V0`
 goal p-| O
 goal h-| O
thm ax_s0
 goal := `¬ Exi \V`
 goal p-| `∃ X \, \V0 ⊂_ X ⟹ Exi \V0`
 goal =| ax_s0

!txt ── book1/1b-3 ──
raw 指定した元だけを持つ集合を作ります。1以上の自然数 ${\tt n}$ に対して 
word set\n
abbr set
prop set\n.

!txt ── book1/1c-1 ──
!txt 第一冊専用: 二つの集合の和・共通部分・差。
section c
word ∪ ∩ ∖
prop ∪. := `X ∪ Y =_ \{ cls x | x ∈ X or x ∈ Y \}`
prop ∩. := `X ∩ Y =_ \{ cls x | x ∈ X and x ∈ Y \}`
prop ∖. := `X ∖ Y =_ \{ cls x | x ∈ X and x {/}∈ Y \}`
raw 
thm W.
 goal := `[ chain X ⊂ Y ⟺ X ∪ Y = Y ⟺ X ∩ Y = X ]`
 goal / ⇔3 //// W. p-| O
 goal h-| W.

!txt ── book1/1c-2 ──
word ⋃ ⋂
word ⋂_
prop ⋃. := `⋃ calX =_ \{ cls x | [ ∃ X ∈_ calX . x ∈ X ] \}`
prop ⋂. := `calX {/}= ∅ ⟹ ⋂ calX =_ \{ cls x | [ ∀ X ∈_ calX . x ∈ X ] \}`
!prop ⋂.'
!thm W.
 ⋂.' / ⋂. / ∅.. p-| O
 ⋂.' h-| W.
raw 
thm W.
 goal := `X = ⋃ \{ set X \}`
 goal /// W. p-| O
 goal h-| W.
thm W.
 goal := `X = ⋂ \{ set X \}`
 goal /// W.' p-| O
 goal h-| W.
thm W.
 goal := `X ∪ Y = ⋃ \{ set X ; Y \}`
 goal //// W. p-| O
 goal h-| W.
thm W.
 goal := `X ∩ Y = ⋂ \{ set X ; Y \}`
 goal /// W.' p-| O
 goal h-| W.

!txt ── book1/1c-3 ──
!txt 第一冊専用: 冪集合。
word ℘
prop ℘.
raw 
prop- wp0
thm W.
 wp0 //// W. p-| O
 wp0 h-| W.
prop- wp1
thm W.
 wp1 //// W. p-| O
 wp1 h-| W.
review-link book1-1

book1/book1-1.book

`book1/book1-1.book`