包含関係
word(cc,p) … \(\subset\) \(\subsetneq\)def …【\({\sf X} \subset {\sf Y}\)】≃【\(\forall {\sf x} \in {\sf X} . {\sf x} \in {\sf Y}\)】
def …【\({\sf X} \subsetneq {\sf Y}\)】≃【\({\sf X} \subset {\sf Y} , {\sf X} \neq {\sf Y}\)】
word(ss,p) … \(\subset\) \(\subsetneq\)
\({\subset.}\)【\(X \subset Y \Longleftrightarrow X \subset Y\)】
\({\subsetneq}.\)【\(X \subsetneq Y \Longleftrightarrow X \subsetneq Y\)】
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
2項述語に対する1項述語
abbr …【\(\mathop{{\sf p}} \cdots \text{自}\)】≈【\(\forall {\sf x} \, ( {\sf x} \mathop{{\sf p}} {\sf x} )\)】abbr …【\(\mathop{{\sf p}} \cdots \text{推}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} \, ( {\sf x} \mathop{{\sf p}} {\sf y} \mathop{{\sf p}} {\sf z} \Longrightarrow {\sf x} \mathop{{\sf p}} {\sf z} )\)】
次のようなabbrは自動で準備されます。
abbr …【\(\mathop{{\sf p}} \cdots \text{自推}\)】≈【\(\mathop{{\sf p}} \cdots \text{自} , \mathop{{\sf p}} \cdots \text{推}\)】
\({=}自推\)【\(= \cdots \text{自推}\)】\(\,{\blacktriangleleft}\,\text{O}\)
\({\subset}自推\)【\(\subset \cdots \text{自推}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\subsetneq}推\)【\(( X \subsetneq Y \subset Z ) \mathbin{\rm o\!r} ( X \subset Y \subsetneq Z ) \Longrightarrow X \subsetneq Z\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
集合の全体、空集合
word(,c) … \(\text{Set}\)def …【\(\text{Set}\)】≃【\(\{ x \mid \top \} \)】
\(\text{Set0}\)【\(x \in \text{Set}\)】\(\,{\blacktriangleleft}\,\text{O}\)
\(\text{Set1}\)【\(X \subset \text{Set}\)】\(\,{\blacktriangleleft}\,\text{O}\)
word(,s) … \(\emptyset\)
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \} \)】
\(\emptyset0\)【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\emptyset1\)【\(\emptyset \subset X\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
有限集合の生成(外延記法)
word(s\(^{\tt n}\),s)! …【\(\{ {\sf X}_{1} , \cdots , {\sf X}_{\tt n} \}\)】\(\text{set}_{\tt n}.\)【\(\{ X_{1} , \cdots , X_{\tt n} \} = \{ x \mid x = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} x = X_{\tt n} \} \)】
例えば【\(\{ x , \{ x , y \} \}\)】はSetで、現れる2つのsetはword(ss,s)です。
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\) \(\mathop\setminus\)def …【\({\sf X} \cup {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \mathbin{\rm o\!r} {\sf x} \in {\sf Y} \} \)】
def …【\({\sf X} \cap {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} , {\sf x} \in {\sf Y} \} \)】
def …【\({\sf X} \mathop\setminus {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} , {\sf x} \notin {\sf Y} \} \)】
word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
\(\cup.\)【\(X \cup Y = X \cup Y\)】
\(\cap.\)【\(X \cap Y = X \cap Y\)】
\(\setminus.\)【\(X \mathop\setminus Y = X \mathop\setminus Y\)】
\({\subset}\text{u}\)【\(X \subset Y \Longleftrightarrow X \cup Y = Y\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\subset}\text{a}\)【\(X \subset Y \Longleftrightarrow X \cap Y = X\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
2項関数に対する1項述語
abbr …【\(\mathop{{\sf f}} \cdots \text{換}\)】≈【\(\forall {\sf x} , {\sf y} \, ( {\sf x} \mathop{{\sf f}} {\sf y} = {\sf y} \mathop{{\sf f}} {\sf x} )\)】abbr …【\(\mathop{{\sf f}} \cdots \text{結}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} \, ( {\sf x} \mathop{{\sf f}} ( {\sf y} \mathop{{\sf f}} {\sf z} ) = ( {\sf x} \mathop{{\sf f}} {\sf y} ) \mathop{{\sf f}} {\sf z} )\)】
abbr …【\(\mathop{{\sf f}} \cdots \text{巾}\)】≈【\(\forall {\sf x} \, ( {\sf x} \mathop{{\sf f}} {\sf x} = {\sf x} )\)】
\({\cup}換結巾\)【\(\cup \cdots \text{換結巾}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
\({\cap}換結巾\)【\(\cap \cdots \text{換結巾}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
abbr …【\(\mathop{{\sf f}} , {\sf E} \cdots \text{単}\)】≈【\(\forall {\sf x} ( {\sf x} \mathop{{\sf f}} {\sf E} = {\sf x} = {\sf E} \mathop{{\sf f}} {\sf x} )\)】
\({\cup}単\)【\(\cup , \emptyset \cdots \text{単}\)】\(\,{\blacktriangleleft}\,\mathbb{D}.\)
abbr …【\(\mathop{{\sf f}} \cdots \text{換} \, {\sf A}\)】≈【\(\forall {\sf x} , {\sf y} {\sf A} . ( {\sf x} \mathop{{\sf f}} {\sf y} = {\sf y} \mathop{{\sf f}} {\sf x} )\)】
abbr …【\(\mathop{{\sf f}} \cdots \text{結} \, {\sf A}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} {\sf A} . ( {\sf x} \mathop{{\sf f}} ( {\sf y} \mathop{{\sf f}} {\sf z} ) = ( {\sf x} \mathop{{\sf f}} {\sf y} ) \mathop{{\sf f}} {\sf z} )\)】
次のようなabbrも自動で準備されます。
abbr …【\(\mathop{{\sf f}} \cdots \text{換結} \, {\sf A}\)】≈【\(\mathop{{\sf f}} \cdots \text{換} \, {\sf A} , \mathop{{\sf f}} \cdots \text{結} \, {\sf A}\)】