English
Let S_i be a family of subgroups of G, and C a predicate on x with hx: x ∈ ⨆ i, S_i. If for all i and x ∈ S_i, C x hx, and C 1 (one_mem _), and C respects multiplication, then C holds for all x ∈ ⨆ i, S_i.
Русский
Пусть {S_i} — семейство подпгрупп, а C — предикат на элементы с принадлежностью к ⨆ i, S_i. Если для каждого i и x ∈ S_i выполняется C x (mem_iSup_of_mem i hx), C 1 и C(mx), и C сохраняется под умножением, то C верно для всех x ∈ ⨆ i, S_i.
LaTeX
$$$\\text{Let } S:\\iota\\to\\mathrm{Subgroup}(G),\\ C:\\forall x, (x\\in\\langle S_i\\rangle)\\to\\mathrm{Prop}. \\\\ hp(i,x,hx): x\\in S_i \\Rightarrow C(x, mem\\_iSup\_of\_mem i hx). \\\\ h1: C(1,one\\_mem _). \\\\ hmul: \\forall x y, C x hx \\to C y hy \\to C(xy, mul\\_mem hx hy). \\\\ \\forall {x} (hx): C x hx.$$
Lean4
@[to_additive]
theorem closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
| 1, _ => by simp
| n + 2, _ =>
calc
closure (s ^ (n + 2))
_ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
_ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
_ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
_ = closure s := sup_idem _
