surjective_of_target_eq_univ — Mathlib

English

If a partial equivalence e has its target equal to the whole codomain, then e is surjective.

Русский

Если у частичного эквивалента e цель равна всему кодомоторному множеству, то e сюръективен.

LaTeX

$$$\\text{If } e:\\PartialEquiv\\alpha\\beta \\text{ and } e.\\text{target}=\\mathrm{univ}, \\text{ then } \\text{Surjective}(e\\toFun).$$$

Lean4

theorem surjective_of_target_eq_univ (h : e.target = univ) : Surjective e :=
  surjective_iff_surjOn_univ.mpr <| e.surjOn.mono (by simp) (by simp [h])

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