English
There exists a finite subset T of H such that its size is bounded by index(H) times the size of S, and T generates H (closure of T equals top).
Русский
Существует конечное подмножество T ⊆ H такого размера, что |T| ≤ [H:G] · |S| и T порождает H (closure(T) = верх).
LaTeX
$$$\\exists T : Finset(H), \\#T \\le H.index \\cdot \\#S \\land closure(T : Set(H)) = \\top$$$
Lean4
theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure (S : Set G) = ⊤) :
∃ T : Finset H, #T ≤ H.index * #S ∧ closure (T : Set H) = ⊤ :=
by
letI := H.fintypeQuotientOfFiniteIndex
haveI : DecidableEq G := Classical.decEq G
obtain ⟨R₀, hR, hR1⟩ := H.exists_isComplement_right 1
haveI : Fintype R₀ := Fintype.ofEquiv _ hR.rightQuotientEquiv
let R : Finset G := Set.toFinset R₀
replace hR : IsComplement (H : Set G) R := by rwa [Set.coe_toFinset]
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]
refine ⟨_, ?_, closure_mul_image_eq_top' hR hR1 hS⟩
calc
_ ≤ #(R * S) := Finset.card_image_le
_ ≤ #R * #S := Finset.card_mul_le
_ = H.index * S.card := congr_arg (· * S.card) ?_
calc
#R = Fintype.card R := (Fintype.card_coe R).symm
_ = _ := (Fintype.card_congr hR.rightQuotientEquiv).symm
_ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H)
_ = H.index := by rw [index_eq_card, Nat.card_eq_fintype_card]
