| 3.76 |
| Title |
Ordered pair(Dunaev's tagged class pair) #DefDunaevOrderedPair #label-ordered-pair-dunaev-s-tagged-class-pair |
| Classification |
Definition |
| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{B} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/exists-binder.html}{\exists} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/exists-binder.html}{\exists} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
CpOPair |
| Scheme of Types |
0(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression],[B@Class.Expression])=(({{∅,{∅}}}∪{[x@Class.Expression]|∃([a@Variable]:[Class@Type])(([a@Class.Expression]∈[A@Class.Expression])∧([x@Class.Expression]={{{{[a@Class.Expression]}}},{∅}}))})∪({{∅,{∅,{∅}}}}∪{[x@Class.Expression]|∃([a@Variable]:[Class@Type])(([a@Class.Expression]∈[B@Class.Expression])∧([x@Class.Expression]={{{{[a@Class.Expression]}}},{∅,{∅}}}))})))) |
| Kernel Note |
Dunaev tagged class ordered pair (A,B) = mark(A,1) ∪ mark(B,2), sound for arbitrary proper classes. |
| Verification |
Definitional (Kernel AST) · Standalone Entry (DefDunaevOrderedPair) → · (3.76) · #DefDunaevOrderedPair |
|