map_surjective — Mathlib

English

Surjectivity of PLift.map f is equivalent to surjectivity of f.

Русский

Сюръективность отображения PLift.map f эквивалентна сюръективности f.

LaTeX

$$$\\forall {\\alpha \\beta} {f : \\alpha \\rightarrow \\beta}, \\operatorname{Surjective}(\\mathrm{PLift.map} f) \\Leftrightarrow \\operatorname{Surjective}(f)$$$

Lean4

@[simp]
theorem map_surjective : Surjective (PLift.map f) ↔ Surjective f :=
  (down_surjective.of_comp_iff _).trans <| Surjective.of_comp_iff' up_bijective _

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