of_injective — Mathlib

English

If h has HasCardinalLT X κ and f: Y → X is injective, then HasCardinalLT Y κ.

Русский

Если у X есть HasCardinalLT κ и есть инъекция f: Y → X, то HasCardinalLT Y κ.

LaTeX

$$HasCardinalLT X κ → (f : Y → X) → Function.Injective f → HasCardinalLT Y κ$$

Lean4

theorem of_injective (f : Y → X) (hf : Function.Injective f) : HasCardinalLT Y κ :=
  by
  dsimp [HasCardinalLT] at h ⊢
  rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]
  rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h
  exact
    lt_of_le_of_lt
      (Cardinal.mk_le_of_injective
        (Function.Injective.comp ULift.up_injective (Function.Injective.comp hf ULift.down_injective)))
      h

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