closure_range_of — Mathlib

English

The generators of FreeGroup generate the whole FreeGroup; the closure of their set is top.

Русский

Генераторы FreeGroup порождают всю FreeGroup; свёртка их множества даёт верхнюю границу.

LaTeX

$$$\\operatorname{closure}(\\{\\text{of}(a) : a \\in \\alpha\\}) = \\top$$$

Lean4

/-- The generators of `FreeGroup α` generate `FreeGroup α`. That is, the subgroup closure of the
set of generators equals `⊤`. -/
@[to_additive (attr := simp)]
theorem closure_range_of (α) : Subgroup.closure (Set.range (FreeGroup.of : α → FreeGroup α)) = ⊤ :=
  by
  rw [← range_lift_eq_closure, lift_of_eq_id]
  exact MonoidHom.range_eq_top.2 Function.surjective_id

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