English
Let s be a subset of R and P(x,y) a predicate on pairs with x,y ∈ closure(s). If P holds when x,y ∈ s and is preserved under coordinatewise addition, negation, and multiplication, then P holds for all x,y ∈ closure(s).
Русский
Пусть s — подмножество кольца R, а P(x,y) — предикат на пары с x,y ∈ closure(s). Если P верно для всех пар из s и сохраняется по координатной операции сложения, отрицания и умножения, тогда P верно для всех x,y ∈ closure(s).
LaTeX
$$$\\forall s\\subseteq R,\\; \\forall P:(x,y)\\mapsto x \\in \\mathrm{closure}(s) \\to y \\in \\mathrm{closure}(s) \\to \\mathrm{Prop},\\text{(conditions ...)} \\Rightarrow \\forall x,y: R,\\; x\\in \\mathrm{closure}(s) \\to y\\in \\mathrm{closure}(s) \\to P(x,y)$$$
Lean4
/-- An induction principle for closure membership, for predicates with two arguments. -/
@[elab_as_elim]
theorem closure_induction₂ {s : Set R} {p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop}
(mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
(zero_left : ∀ x hx, p 0 x (zero_mem _) hx) (zero_right : ∀ x hx, p x 0 hx (zero_mem _))
(one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
(neg_left : ∀ x y hx hy, p x y hx hy → p (-x) y (neg_mem hx) hy)
(neg_right : ∀ x y hx hy, p x y hx hy → p x (-y) hx (neg_mem hy))
(add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
(add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
(mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
(mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz)) {x y : R}
(hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy := by
induction hy using closure_induction with
| mem z hz =>
induction hx using closure_induction with
| mem _ h => exact mem_mem _ _ h hz
| zero => exact zero_left _ _
| one => exact one_left _ _
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| neg _ _ h => exact neg_left _ _ _ _ h
| zero => exact zero_right x hx
| one => exact one_right x hx
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
| neg _ _ h => exact neg_right _ _ _ _ h
