English
Let G be a group and s a subset of G. Let closure(s) denote the subgroup generated by s. If a predicate p on G, extended to elements of closure(s), satisfies: (i) p(a) holds for every a ∈ s, when viewed as p(a) at the corresponding element of closure(s); (ii) p(a) holds for a⁻¹ whenever p(a) holds for a ∈ s; (iii) p is closed under multiplication: if p(x) and p(y) hold for x,y in closure(s) then p(xy) holds; and p(1) holds. Then p holds for all elements of closure(s).
Русский
Пусть G — группа, S — подмножество G, closure(S) — порожденная им подгруппа. Пусть p — предикат на G, который для элементов closure(S) трактуется естественным образом. Если p выполняется для единицы, а также для любых x ∈ S и их обратных x⁻¹, и сохранен под произведение (если p(x) и p(y), то p(xy)), и сохранено p(1), то p верно для всех элементов closure(S).
LaTeX
$$$\\text{Let } p:G\\to(\\mathrm{closure}(S)\\to\\mathrm{Prop}) \\, \\text{be a predicate. If}\\;\\\\\n\\quad (\\forall x\\in S)\, p(x,(\\mathrm{subset\_closure}(x) )) ,\\quad (\\forall x\\in S)\\, p(x^{-1},(\\mathrm{inv\_mem}(\\mathrm{subset\_closure}(x)))) ,\\\\\n\\quad p(1,(\\mathrm{one\_mem} _)),\\quad (\\forall x,y\\, hx,hy),\\ p(x,hx)\\to p(y,hy)\\to p(xy,(\\mathrm{mul\_mem} hx hy))) \\, \\\\to\\\\\n\\quad \\forall {x}, x\\in\\mathrm{closure}(S)\\;:\\; p(x,h) \\text{ holds, where } h:x\\in\\mathrm{closure}(S).$$$
Lean4
/-- An induction principle for closure membership. If `p` holds for `1` and all elements of
`k` and their inverse, and is preserved under multiplication, then `p` holds for all elements of
the closure of `k`. -/
@[to_additive (attr := elab_as_elim) /--
An induction principle for additive closure membership. If `p` holds for `0` and all
elements of `k` and their negation, and is preserved under addition, then `p` holds for all
elements of the additive closure of `k`. -/
]
theorem closure_induction'' {p : (g : G) → g ∈ closure s → Prop} (mem : ∀ x (hx : x ∈ s), p x (subset_closure hx))
(inv_mem : ∀ x (hx : x ∈ s), p x⁻¹ (inv_mem (subset_closure hx))) (one : p 1 (one_mem _))
(mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (h : x ∈ closure s) : p x h :=
closure_induction_left one (fun x hx y _ hy => mul x y _ _ (mem x hx) hy)
(fun x hx y _ => mul x⁻¹ y _ _ <| inv_mem x hx) h
