Theorems · Theorem · logic and foundations
Cardinal.lift_id
∀ (a : Cardinal.{u}), Cardinal.lift.{u, u} a = aA cardinal lifted to the same universe equals itself.
- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 163 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 83 definitions · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.lift_id'proof · cited by 43
Cited by163
Results whose statement or proof uses this declaration.
- LinearIndependent.cardinal_le_rankproof · cited by 14
- rank_mul_rankproof · cited by 8
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- Cardinal.sum_le_lift_mk_mul_iSupproof · cited by 5
- Cardinal.mk_ordinalproof · cited by 4
- hasCardinalLT_iff_cardinal_mk_ltproof · cited by 4
- lift_rank_mul_lift_rankproof · cited by 4
- Cardinal.sum_le_lift_mk_mul_iSup_liftproof · cited by 4
- Cardinal.mk_natproof · cited by 3
- Cardinal.mk_preimage_of_injectiveproof · cited by 3
- Cardinal.mk_quaternionAlgebraproof · cited by 3
- OrderIso.cof_congrproof · cited by 3