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