2 初等的な集合関数

2.1 外延記法

Formel ではword familyも使用できます。指定した元だけを持つ集合を作ります。1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
Formel は \(\cdots\) や \({\tt n}\) をしかるべく処理します。例　 \(\{ x , \{ x , y \} \}\) ≈ \(\mathsf{set}_{2} ( x , \mathsf{set}_{2} ( x , y ) )\)

定義familyも使用できます。Bookで次のset\({\tt n}\).が紹介されると \(\mathbb{W}.\) は無限列になります。
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)
ソース98行目にもhidden propがあり \({\tt n}\) が入っています。at \n=1..4 は「\({\tt n}\)=1,2,3,4 のそれぞれについて示す」という意味です。prfの /1 =. は「1番目の要素だけを =. で展開する」です。
対集合公理
ax_set2 … \(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.

2.2 べき集合

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)
べき集合公理
ax_℘ … \(\dot\exists \{ A \mid A \subset X \}\) \(\blacktriangleleft\) ℘.

ソース118行目に次の初等的定理のprfがあります。
\({\tt P}\) / W. は「\({\tt P}\) を 〇. で展開したもの」でしたが \({\tt P}\) / W.' は「〇.' があれば 〇.' で、無ければ 〇. で展開したもの」です。
/ W.'!=. は / W.' を行うが =. だけは使わない（=まで展開してしまうのは展開しすぎで証明が通らない）。
// W.'!=. は / W.'!=. / W.'!=. です。
\(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.3 和・積

word(c,c) … \(\bigcup\)  \(\bigcap\)
⋃_. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
⋂_. … \(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
\(\bigcap \emptyset = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

クラスの和・積は綺麗に定義でき、集合の和・積の定義はそこから誘導されます。
word(s,s)R … \(\bigcup\)  \(\bigcap\)
⋃. … \(\bigcup \mathcal{X} = \bigcup \mathcal{X}\)
⋂. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
和集合公理
ax_⋃ … \(\dot\exists \{ x \mid \exists X \in \mathcal{X} . x \in X \}\) \(\blacktriangleleft\) ⋃.

⋂.|cvt … \(\mathcal{X} \neq \emptyset \Longrightarrow \forall x ( x \in \bigcap \mathcal{X} \Longleftrightarrow \forall X \in \mathcal{X} . x \in X )\) 　です。
⋂. のように \(P \Longrightarrow ( Q \Longleftrightarrow R )\) の形の定義では、/ はこれを同値な \(Q \Longleftrightarrow ( P \Longrightarrow R ) , ( \neg P \Longrightarrow Q )\) に変形してから計算されます。
/ ⋂. では \(x \in \bigcap \mathcal{X} \Longleftrightarrow ( \mathcal{X} \neq \emptyset \Longrightarrow \forall X \in \mathcal{X} . x \in X ) , ( \mathcal{X} = \emptyset \Longrightarrow x \in \bigcap \mathcal{X} )\) です。
正確には、再展開を防ぐため、最後の \(\bigcap\) は一旦 \(\bigcap\) にされ、最終結果で \(\bigcap\) に戻されます。

2集合の合併・共通部分が良く使用されます。
word(ss,s) … \(\cup\)  \(\cap\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \mid x \in X , x \in Y \}\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2.4 内包記法の拡張

次のものは左辺のソース $_X がtex表記されない特殊な例です（しかも通常の数学で普通に用いられている）。
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)