map_top_of_surjective — Mathlib

English

Let f: G →* N be surjective. Then the image of the top subgroup of G under f is the top subgroup of N.

Русский

Пусть f: G →* N сюръективно. Тогда образ верхней подгруппы G под действием f равен верхней подгруппе N.

LaTeX

$$$ (\\top_G).map f = \\top_N $$$

Lean4

@[to_additive]
theorem map_top_of_surjective (f : G →* N) (h : Function.Surjective f) : Subgroup.map f ⊤ = ⊤ :=
  by
  rw [eq_top_iff]
  intro x _
  obtain ⟨y, hy⟩ := h x
  exact ⟨y, trivial, hy⟩

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