English
Let s be a subset of a ring R and p(x) a predicate on x ∈ closure(s). If p holds for every element of s and is preserved under addition, negation, and multiplication, and holds for 0 and 1, then p holds for all x ∈ closure(s).
Русский
Пусть s — подмножество кольца R и p(x) — предикат над элементами x, принадлежащими closure(s). Если выполняется, что p верно для каждого элемента из s и сохраняется при сложении, отризании и умножении, а также для 0 и 1, то p верно для всех x ∈ closure(s).
LaTeX
$$$\\forall x\\subseteq R,\\; [P(x,\\, hx)] \\Rightarrow ...$$
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 _)) (one : p 1 (one_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 : Subring 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⟩
one_mem' := ⟨_, one⟩ }
closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
