English
Let p be a predicate on pairs (x,y) with x,y ∈ closure(s) that is preserved under left and right multiplication by elements in closure(s) and holds for all pairs from s. Then p holds for all pairs in closure(s) × closure(s).
Русский
Пусть p — предикат на паре (x,y) с x,y ∈ closure(s), сохраняющийся при левой и правой умножении парами из closure(s) и выполняется для всех пар из s. Тогда p выполняется для всех пар в closure(s) × closure(s).
LaTeX
$$$\\forall p:\\, (M \\times M)\\to \\mathrm{Prop},\\; (\\forall x,y\\in s,\\; p(x,y)) \\land (\\forall x,y,z,\\; p(x,z)\\to p(y,z)\\to p(xy,z)) \\land (\\forall x,y,z,\\; p(z,x)\\to p(z,y)\\to p(zxy)) \\Rightarrow \\forall x,y\\in \\mathrm{closure}(s),\\; p(x,y)$$$
Lean4
/-- An induction principle for closure membership for predicates with two arguments. -/
@[to_additive (attr := elab_as_elim) /-- An induction principle for additive closure membership for
predicates with two arguments. -/
]
theorem closure_induction₂ {p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
(mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
(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 z x hz hx → p z y hz hy → p z (x * y) hz (mul_mem hx hy)) {x y : M}
(hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy := by
induction hx using closure_induction with
| mem z hz =>
induction hy using closure_induction with
| mem _ h => exact mem _ _ hz h
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ hy h₁ h₂
