English
Let G be a group and k ⊆ G. If P is a predicate on G such that P holds for 1 and all elements of k, and P is preserved under multiplication and taking inverses, then P holds for every element of the closure of k.
Русский
Пусть G — группа и k ⊆ G. Пусть P — свойство на G, такое что P выполняется для 1 и для каждого элемента из k, и сохраняется при умножении и взятии обратного. Тогда P выполняется для каждого элемента замыкания k.
LaTeX
$$$ \\forall P:\\, G \\to \\mathrm{Prop},\\;\\Big( (\\forall x \\in k,\; P(x)) \\land P(1) \\land (\\forall x,y:\\, P(x) \\land P(y) \\Rightarrow P(xy)) \\land (\\forall x:\\, P(x) \\Rightarrow P(x^{-1})) \\Big) \\Rightarrow \\forall g:\\, g \\in \\mathrm{closure}(k) \\Rightarrow P(g) $$$
Lean4
/-- An induction principle for closure membership. If `p` holds for `1` and all elements of `k`, and
is preserved under multiplication and inverse, then `p` holds for all elements of the closure
of `k`.
See also `Subgroup.closure_induction_left` and `Subgroup.closure_induction_right` for versions that
only require showing `p` is preserved by multiplication by elements in `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 is preserved under addition and inverses, then `p`
holds for all elements of the additive closure of `k`.
See also `AddSubgroup.closure_induction_left` and `AddSubgroup.closure_induction_left` for
versions that only require showing `p` is preserved by addition by elements in `k`. -/
]
theorem closure_induction {p : (g : G) → g ∈ closure k → Prop} (mem : ∀ x (hx : x ∈ k), p x (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))
(inv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx)) {x} (hx : x ∈ closure k) : p x hx :=
let K : Subgroup G :=
{ carrier := {x | ∃ hx, p x hx}
mul_mem' := fun ⟨_, ha⟩ ⟨_, hb⟩ ↦ ⟨_, mul _ _ _ _ ha hb⟩
one_mem' := ⟨_, one⟩
inv_mem' := fun ⟨_, hb⟩ ↦ ⟨_, inv _ _ hb⟩ }
closure_le (K := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
