English
If R and S are finite sets and R is a right transversal of H in G with 1 ∈ R, and if closure of S equals the whole group, then the closure of the image set inside H generated by R and S equals the top of H.
Русский
Если R и S — конечные множества, R является правой трансперверсалью H в G с 1 ∈ R, и замыкание S дает всю группу, то замыкание изображения внутри H дает верхушку множества H.
LaTeX
$$$\\operatorname{closure}\\big((R*S).image(g \\mapsto ⟨g \\cdot (h_R(g))^{-1}, \\; \\text{mem}⟩) : \\text{Set}~H\\big) = \\top$$$
Lean4
/-- **Schreier's Lemma**: If `R : Finset G` is a `rightTransversal` of `H : Subgroup G`
with `1 ∈ R`, and if `G` is generated by `S : Finset G`, then `H` is generated by the `Finset`
`(R * S).image (fun g ↦ g * (hR.toRightFun g)⁻¹)`. -/
theorem closure_mul_image_eq_top' [DecidableEq G] {R S : Finset G} (hR : IsComplement (H : Set G) R) (hR1 : (1 : G) ∈ R)
(hS : closure (S : Set G) = ⊤) :
closure (((R * S).image fun g => ⟨_, hR.mul_inv_toRightFun_mem g⟩ : Finset H) : Set H) = ⊤ :=
by
rw [Finset.coe_image, Finset.coe_mul]
exact closure_mul_image_eq_top hR hR1 hS
