Theorems · Theorem · logic and foundations
Cardinal.lift_lift
∀ (a : Cardinal.{u_1}), Cardinal.lift.{w, max v u_1} (Cardinal.lift.{v, u_1} a) = Cardinal.lift.{max v w, u_1} a- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 53 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.symmproof · cited by 3,681
- Cardinalstatement and proof · cited by 2,598
- Cardinal.liftstatement · cited by 583
- Equiv.transproof · cited by 337
- Equiv.uliftproof · cited by 115
- Equiv.cardinal_eqproof · cited by 35
- Cardinal.inductionOnproof · cited by 19
Cited by53
Results whose statement or proof uses this declaration.
- Cardinal.lift_aleph0proof · cited by 41
- HasCardinalLT.of_injectiveproof · cited by 9
- rank_span_leproof · cited by 9
- HasCardinalLT.of_surjectiveproof · cited by 7
- Ordinal.lift_iSup_add_one_lt_of_lt_cofproof · cited by 6
- Cardinal.lift_lt_univ'proof · cited by 6
- Cardinal.lift_sumproof · cited by 5
- Cardinal.lift_univproof · cited by 5
- lift_rank_mul_lift_rankproof · cited by 4
- Ordinal.lift_cof_iSup_add_oneproof · cited by 4
- rank_matrix_moduleproof · cited by 3
- IsBaseChange.lift_rank_eqproof · cited by 3