English
An induction principle for closure membership: if a predicate holds for elements of s and is preserved under the monoid operation, then it holds for all elements of closure s.
Русский
Принцип математической индукции по замыканию: если свойство выполняется для элементов s и сохраняется под умножением, то оно выполняется и для всех элементов closure s.
LaTeX
$$closure_induction {s} {motive} (mem) (one) (mul) {x} (hx) : motive x hx$$
Lean4
/-- An induction principle for closure membership. If `p` holds for `1` and 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 `0` and all
elements of `s`, and is preserved under addition, then `p` holds for all elements of the
additive closure of `s`. -/
]
theorem closure_induction {s : Set M} {motive : (x : M) → x ∈ closure s → Prop}
(mem : ∀ (x) (h : x ∈ s), motive x (subset_closure h)) (one : motive 1 (one_mem _))
(mul : ∀ x y hx hy, motive x hx → motive y hy → motive (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) :
motive x hx :=
let S : Submonoid M :=
{ carrier := {x | ∃ hx, motive x hx}
one_mem' := ⟨_, one⟩
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
