srange_eq_top_iff_surjective — Mathlib

English

For a semigroup hom f: M → N, f.srange equals ⊤ if and only if f is surjective.

Русский

Для полугомомера f: M → N образ f равен ⊤ тогда и только тогда, когда f сюръективен.

LaTeX

$$$f.srange = (\top : Subsemigroup N) \iff \mathrm{Function.Surjective}\, f$$$

Lean4

@[to_additive]
theorem srange_eq_top_iff_surjective {N} [Mul N] {f : M →ₙ* N} :
    f.srange = (⊤ : Subsemigroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ

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