Theorems · Definition · logic and foundations
Cardinal.liftInitialSeg
Cardinal.{u} ≤i Cardinal.{max u v}Cardinal.lift as an InitialSeg.
- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement · cited by 2,598
- Cardinal.liftproof · cited by 583
- InitialSegstatement · cited by 70
- OrderEmbedding.ltEmbeddingproof · cited by 9
- OrderEmbedding.ofMapLEIffproof · cited by 6
Cited by8
Results whose statement or proof uses this declaration.
- Cardinal.lift_leproof · cited by 78
- Cardinal.lift_ltproof · cited by 39
- Cardinal.lift_injectiveproof · cited by 12
- Cardinal.lt_lift_iffproof · cited by 4
- Cardinal.lift_preAlephproof · cited by 2
- Cardinal.mem_range_lift_of_leproof · cited by 1
- Cardinal.le_lift_iffproof · cited by 0
- Cardinal.liftInitialSeg_toFunstatement and proof · cited by 0