map_srange — Mathlib

English

If f is surjective, then its srange is the top subsemigroup of the codomain; i.e., f.srange = ⊤.

Русский

Если f сюръективен, то образ f на подполугруппу равен всей кодовой области: f.srange = ⊤.

LaTeX

$$$f.srange = (\top : Subsemigroup N)$$$

Lean4

@[to_additive]
theorem map_srange (g : N →ₙ* P) (f : M →ₙ* N) : f.srange.map g = (g.comp f).srange := by
  simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f

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