Theorems · Theorem · logic and foundations
Cardinal.lift_umax
Cardinal.lift.{max u v, u} = Cardinal.lift.{v, u}lift.{max u v, u} equals lift.{v, u}.
Unfortunately, the simp lemma doesn't work.
- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 56 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 by56
Results whose statement or proof uses this declaration.
- Ordinal.lift_cofproof · cited by 8
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- Ordinal.nfpFamily_lt_ord_liftproof · cited by 4
- lift_rank_mul_lift_rankproof · cited by 4
- Cardinal.sum_le_lift_mk_mul_iSup_liftproof · cited by 4
- Ordinal.lift_cof_iSup_add_oneproof · cited by 4
- IsBaseChange.lift_rank_eq_of_le_nonZeroDivisorsproof · cited by 3
- MvPolynomial.rank_eq_liftproof · cited by 3
- Cardinal.univ_umaxproof · cited by 3
- rank_fun_infiniteproof · cited by 2
- IsAlgClosed.cardinal_le_max_transcendence_basisproof · cited by 2
- Cardinal.prod_eq_of_fintypeproof · cited by 2