Theorems · Theorem · logic and foundations
Cardinal.lift_mk_le
∀ {α : Type v} {β : Type w},
Cardinal.lift.{max u w, v} (Cardinal.mk α) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk β) ↔ Nonempty (α ↪ β)- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, 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 · cited by 2,598
- Function.Embeddingstatement and proof · cited by 988
- Cardinal.mkstatement and proof · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- Equiv.uliftproof · cited by 115
- Function.Embedding.congrproof · cited by 5
Cited by10
Results whose statement or proof uses this declaration.
- Cardinal.natCast_lt_aleph0proof · cited by 47
- Cardinal.lift_mk_le'proof · cited by 20
- Cardinal.mk_range_le_liftproof · cited by 15
- Cardinal.mk_image_le_liftproof · cited by 6
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_ltproof · cited by 2
- Cardinal.mk_preimage_of_injective_liftproof · cited by 2
- Equiv.Perm.not_isSolvableproof · cited by 1
- FirstOrder.Language.card_functions_sum_skolem₁proof · cited by 1
- FirstOrder.Language.Sentence.realize_cardGeproof · cited by 0