of_surjective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_surjective (f : X → Y) (hf : Function.Surjective 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_surjective
        (Function.Surjective.comp ULift.up_surjective (Function.Surjective.comp hf ULift.down_surjective)))
      h

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