lift_mk_le_lift_mk_of_injective — Mathlib

English

If f is injective, lift(|α|) ≤ lift(|β|).

Русский

Если f: α → β инъективна, то lift(|α|) ≤ lift(|β|).

LaTeX

$$$\\mathrm{lift}\\,|\\alpha| \\le \\mathrm{lift}\\,|\\beta|$$$

Lean4

theorem lift_mk_le_lift_mk_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Injective f) :
    Cardinal.lift.{v} (#α) ≤ Cardinal.lift.{u} (#β) :=
  by
  rw [← Cardinal.mk_range_eq_of_injective hf]
  exact Cardinal.lift_le.2 (Cardinal.mk_set_le _)

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