Theorems · Theorem · logic and foundations

Cardinal.mk_embedding_eq_arrow_of_lift_le

∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α) →
    Cardinal.mk (β' ↪ α) = Cardinal.mk (β' → α)

Defined in: Mathlib.SetTheory.Cardinal.Arithmetic
Cited by: 1 results in Mathlib
Foundations: Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Infinite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Cardinalstatement and proof · 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
LE.le.antisymmproof · cited by 507
Infinitestatement and proof · cited by 352
Nonempty.someproof · cited by 340
Equiv.reflproof · cited by 274
Function.Embedding.injectiveproof · cited by 111
Equiv.cardinal_eqproof · cited by 35
Cardinal.aleph0_le_mkproof · cited by 32

Cited by1

Results whose statement or proof uses this declaration.

Cardinal.mk_embedding_eq_arrow_of_leproof · cited by 0