English
In the setting of Schreier's Lemma, under the same hypotheses, the generated subgroup inside H equals the top element in the lattice of subgroups of H, i.e. the subgroup generated by the given set is all of H.
Русский
В условиях Леммы Шрейера подгруппа, порожденная указанным множеством внутри H, совпадает с верхней точкой в решетке подгрупп H, то есть равна H.
LaTeX
$$$\\operatorname{closure}\\big((R*S).image(g \\mapsto ⟨g \\cdot (h_R(g))^{-1}, \\; \\text{mem}\\rangle)\\big) = \\top$$$
Lean4
/-- **Schreier's Lemma**: If `R : Set G` is a `rightTransversal` of `H : Subgroup G`
with `1 ∈ R`, and if `G` is generated by `S : Set G`, then `H` is generated by the `Set`
`(R * S).image (fun g ↦ g * (hR.toRightFun g)⁻¹)`. -/
theorem closure_mul_image_eq_top (hR : IsComplement H R) (hR1 : (1 : G) ∈ R) (hS : closure S = ⊤) :
closure ((R * S).image fun g => ⟨g * (hR.toRightFun g : G)⁻¹, hR.mul_inv_toRightFun_mem g⟩ : Set H) = ⊤ :=
by
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]
exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))
