range_eq_top_of_surjective — Mathlib

English

If f is surjective, then the construction rangeRestrict yields a surjective map and its range is the top subgroup.

Русский

Если f сюръективен, то rangeRestrict образует сюръективное отображение и его образ равен верхней подгруппе.

LaTeX

$$rangeRestrict_surjective(f) ∧ range_eq_top_of_surjective(f)$$

Lean4

/-- The range of a surjective monoid homomorphism is the whole of the codomain. -/
@[to_additive (attr := simp) /-- The range of a surjective `AddMonoid` homomorphism is the whole of the codomain. -/
    ]
theorem range_eq_top_of_surjective {N} [Group N] (f : G →* N) (hf : Function.Surjective f) :
    f.range = (⊤ : Subgroup N) :=
  range_eq_top.2 hf

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