English
For subgroups H and K, the join equals the closure of the product of their underlying sets: H ⊔ K = closure((H:Set G)*(K:Set G)).
Русский
Для подпгрупп H и K объединение равно замыканию произведения множителей: H ⊔ K = closure((H:Set G)*(K:Set G)).
LaTeX
$$$H \\lor K = \\mathrm{closure}\\big((H : \\mathrm{Set} G)\\cdot (K : \\mathrm{Set} G)\\big)$$$
Lean4
@[to_additive]
theorem smul_mem_of_mem_closure_of_mem {X : Type*} [MulAction G X] {s : Set G} {t : Set X} (hs : ∀ g ∈ s, g⁻¹ ∈ s)
(hst : ∀ᵉ (g ∈ s) (x ∈ t), g • x ∈ t) {g : G} (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t := by
induction hg using Subgroup.closure_induction'' generalizing x with
| one => simpa
| mem g' hg' => exact hst g' hg' x hx
| inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
| mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)
