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}.\)