English
An induction principle for closure membership: if p holds for all elements of s, for 0, and is preserved under addition, negation, and multiplication, then p holds for all elements of closure(s).
Русский
Принцип индукции по замыкании: если свойство p выполняется на s, на 0 и сохраняется при сложении, взятии противоположного и умножении, то оно выполняется для всех элементов closure(s).
LaTeX
$$$\\text{If } p\\text{ holds for } s, for }0,\\text{ and is closed under }+,-,\\cdot,\\text{ then } p\\text{ holds for all }\\mathrm{closure}(s).$$$
Lean4
/-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
elements of the closure of `s`. -/
@[elab_as_elim]
theorem closure_induction {s : Set R} {p : (x : R) → x ∈ closure s → Prop}
(mem : ∀ (x) (hx : x ∈ s), p x (subset_closure hx)) (zero : p 0 (zero_mem _))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (neg : ∀ x hx, p x hx → p (-x) (neg_mem hx))
(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 K : NonUnitalSubring R :=
{ carrier := {x | ∃ hx, p x hx}
mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
neg_mem' := fun ⟨_, hpx⟩ ↦ ⟨_, neg _ _ hpx⟩
zero_mem' := ⟨_, zero⟩ }
closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
