srange_eq_top_of_surjective — Mathlib

English

If f is surjective, then f.srange = ⊤; the range is the entire codomain.

Русский

Если f сюръективен, то образ f равен всему кодовому множеству.

LaTeX

$$$f.srange = (\top : Subsemigroup N)\;\text{ при суръективности } f$$$

Lean4

/-- The range of a surjective semigroup hom is the whole of the codomain. -/
@[to_additive (attr := simp) /-- The range of a surjective `AddSemigroup` hom is the whole of the codomain. -/
    ]
theorem srange_eq_top_of_surjective {N} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :
    f.srange = (⊤ : Subsemigroup N) :=
  srange_eq_top_iff_surjective.2 hf

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