Symbol Reference: ⪯ — Cardinality Injection Order Predicate (⪯, AST Constructor: TpLessEq)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

⪯ \(\preceq\) — Cardinality Injection Order Predicate (⪯, AST Constructor: TpLessEq)

Binary cardinality preorder A ⪯ B asserting existence of an injective class-function from A into B (Entry DefPiPredicateModel (3.39)).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
⪯
\(\preceq\)
Category Predicate Symbol (Binary Class Relation)
SML AST Constructor HP (TpLessEq of ('Class_EXP * 'Class_EXP)) [in datatype Truth_p, typetheory.ML:681]
Constructor Arguments 1. Domain class A : Class; 2. Codomain class B : Class
Metatype / Signature Class × Class → Bool
Binder Status No — Binary Predicate Symbol (Cardinality Injection Preorder)
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \preceq
How to Understand It

SML AST Constructor: HP (TpLessEq of ('Class_EXP * 'Class_EXP)) in Truth_p (typetheory.ML:681). Takes two class arguments (A : Class, B : Class).
Canonical Law / Usage (A ⪯ B) ⟷ ∃(f:Class)((f is injective) ∧ (A⊆Dom(f)) ∧ (f[A]⊆B))
Related Symbols & Kernel Entries