English
Let G be a group. For a predicate P on pairs (x,y) with x,y ∈ closure(k), if P holds for all (x,y) with x,y ∈ k in the first argument and the second argument, and P is closed under the group operations on both sides, then P holds for all pairs (x,y) with x,y ∈ closure(k).
Русский
Пусть G — группа. Для предиката P на пары (x,y) с x,y ∈ closure(k) если P выполняется для всех пар с x,y из k на соответствующих местах, и P сохраняется при операциях группы с обеих сторон, тогда P выполняется для всех пар (x,y) с x,y ∈ closure(k).
LaTeX
$$$ \forall P:\, (G \times G) \to \mathrm{Prop},\;\Big( \forall x,y:\; x \in k \land y \in k \Rightarrow P(x,y,(\subseteq \mathrm{closure}(k))(x),(\subseteq \mathrm{closure}(k))(y)) \Big) \Rightarrow \forall x,y:\; x,y \in \mathrm{closure}(k) \Rightarrow P(x,y,\cdot,\cdot) $$$
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 : G) → x ∈ closure k → y ∈ closure k → Prop}
(mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy))
(one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
(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 : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
(inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy)
(inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy)) {x y : G} (hx : x ∈ closure k)
(hy : y ∈ closure k) : 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 _ _ h hz
| one => exact one_left _ (subset_closure hz)
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| inv _ _ h => exact inv_left _ _ _ _ h
| one => exact one_right x hx
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
| inv _ _ h => exact inv_right _ _ _ _ h
