⊆ \(\subseteq\) — Subclass Inclusion Predicate (⊆, AST Constructor: TpSub)
Binary subclass inclusion predicate X ⊆ Y defined by ∀(z:Class)((z∈X) → (z∈Y)) (Entry DefSubclass (3.06)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
⊆
\(\subseteq\)
|
| Category | Predicate Symbol (Binary Class Relation) |
| SML AST Constructor | HP (TpSub of ('Class_EXP * 'Class_EXP)) [in datatype Truth_p, typetheory.ML:679] |
| Constructor Arguments | 1. Subclass X : Class; 2. Superclass Y : Class |
| Metatype / Signature | Class × Class → Bool |
| Binder Status | No — Defined Binary Predicate Symbol (Subclass Inclusion) |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \subseteq |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | ∀(X:Class)∀(Y:Class)((X ⊆ Y) ⟷ (∀(z:Class)((z ∈ X) → (z ∈ Y)))) |
| Related Symbols & Kernel Entries |