Theorems · Theorem · logic and foundations
Cardinal.lift_le
∀ {a b : Cardinal.{v}}, Cardinal.lift.{u, v} a ≤ Cardinal.lift.{u, v} b ↔ a ≤ b- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 78 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement and proof · cited by 2,598
- Cardinal.liftstatement · cited by 583
- Cardinal.liftInitialSegproof · cited by 8
- InitialSeg.le_iff_leproof · cited by 4
Cited by78
Results whose statement or proof uses this declaration.
- LinearIndependent.cardinal_lift_le_rankproof · cited by 16
- Cardinal.aleph0_le_liftproof · cited by 10
- Cardinal.lift_mk_le_lift_mk_of_injectiveproof · cited by 10
- LinearMap.rank_le_of_injectiveproof · cited by 9
- lift_rank_range_leproof · cited by 7
- Cardinal.lift_le_aleph0proof · cited by 5
- Cardinal.lift_succproof · cited by 4
- Ordinal.nfpFamily_lt_ord_liftproof · cited by 4
- AlgebraicIndependent.lift_cardinalMk_le_trdegproof · cited by 4
- Ordinal.card_iSup_le_liftproof · cited by 3
- Algebraic.cardinalMk_lift_le_maxproof · cited by 3