Theorems · Theorem · logic and foundations
Ordinal.lsub_typein
Deprecated since 2026-03-27Mathlib marks this declaration as deprecated.
∀ (o : Ordinal.{u}), Ordinal.lsub ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o- Defined in
- Mathlib.SetTheory.Ordinal.Family
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Ordinalstatement and proof · cited by 1,688
- LE.le.antisymmproof · cited by 507
- RelEmbeddingstatement · cited by 281
- Ordinal.typeproof · cited by 207
- Ordinal.ToTypestatement and proof · cited by 143
- PrincipalSeg.toRelEmbeddingstatement and proof · cited by 129
- LT.lt.trans_eqproof · cited by 65
- Ordinal.typeinstatement and proof · cited by 60
- Ordinal.lsubstatement and proof · cited by 43
- Ordinal.enumproof · cited by 39
- Ordinal.type_toTypeproof · cited by 28
Cited by2
Results whose statement or proof uses this declaration.
- Ordinal.cof_lsub_def_nonemptyproof · cited by 3
- Ordinal.blsub_idproof · cited by 1