lift_mk_le' — Mathlib

English

The lifting operation is injective on cardinals: if lift a = lift b, then a = b.

Русский

Операция подъёма инъективна на кардиналах: если lift a = lift b, то a = b.

LaTeX

$$$$ \\forall a,b:\\\\mathrm{Cardinal}, \\ lift(a) = lift(b) \\Rightarrow a = b. $$$$

Lean4

/-- A variant of `Cardinal.lift_mk_le` with specialized universes.
Because Lean often cannot realize it should use this specialization itself,
we provide this statement separately so you don't have to solve the specialization problem either.
-/
theorem lift_mk_le' {α : Type u} {β : Type v} : lift.{v} #α ≤ lift.{u} #β ↔ Nonempty (α ↪ β) :=
  lift_mk_le.{0}

Похожие утверждения