range_eq_top — Mathlib

English

The image of the identity map on G, i.e. range of the constant map 1: G →* N, is the trivial subgroup: {e}.

Русский

Образ единичного гомоморфизма 1: G →* N есть тривиальная подгруппа: {e}.

LaTeX

$$ (1 : G →* N).range = ⊥ $$

Lean4

@[to_additive]
theorem range_eq_top {N} [Group N] {f : G →* N} : f.range = (⊤ : Subgroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_range, coe_top]) Set.range_eq_univ

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