sss \(\mathrm{sss}\) — Semi-Singleton Subclass Relation (sss, Entry DefSemiSingletonSubclass (3.36))
Binary relation s sss t used to uniformly encode both set-valued and proper-class-valued fibers in lambda families (Entries RulClassComprehension (3.01)).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
sss
\(\mathrm{sss}\)
|
| Category | Predicate Symbol (Binary Class Relation) |
| SML AST Constructor | Sss_def_entry [Defined Binary Predicate, entries.ML:DefSemiSingletonSubclass (3.36)] |
| Constructor Arguments | 1. Subclass s : Class; 2. Target class t : Class |
| Metatype / Signature | Class × Class → Bool |
| Binder Status | No — Binary Predicate Symbol |
| Defining Kernel Entries (ML Labels) | See Related Symbols & Kernel Entries below. |
| LaTeX Form | \mathrm{sss} |
| How to Understand It | SML AST Constructor: Defined binary class predicate in Entry DefSemiSingletonSubclass (3.36) ( |
| Canonical Law / Usage | (s sss t) ⟷ (((t set) ∧ (s={t})) ∨ ((t proper) ∧ (s⊆t) ∧ (s is a semi-singleton))) |
| Related Symbols & Kernel Entries |