English
Let p be a predicate with p(x) defined on M. If p holds for all x ∈ s and is preserved under multiplication, then p holds for all x ∈ closure(s).
Русский
Пусть p — булева предикаты на M. Если p выполняется для всех x ∈ s и сохраняется под умножением, то p выполняется для всех x ∈ closure(s).
LaTeX
$$$\\text{If } p:\\, M \\to \\mathrm{Prop},\\; (\\forall x\\in s,\\; p(x)) \\land (\\forall x,y,\\; p(x) \\to p(y) \\to p(xy)) \\Rightarrow (\\forall x \\in \\mathrm{closure}(s),\\; p(x))$$$
Lean4
/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under multiplication, then `p` holds for all elements of the closure of `s`. -/
@[to_additive (attr := elab_as_elim) /-- An induction principle for additive closure membership. If
`p` holds for all elements of `s`, and is preserved under addition, then `p` holds for all
elements of the additive closure of `s`. -/
]
theorem closure_induction {p : (x : M) → x ∈ closure s → Prop} (mem : ∀ (x) (h : x ∈ s), p x (subset_closure h))
(mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) : p x hx :=
let S : Subsemigroup M :=
{ carrier := {x | ∃ hx, p x hx}
mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩ }
closure_le (S := S) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
