English
An induction principle for closure membership for predicates with two arguments: if a predicate holds for generators in s and is preserved by the product, then it holds for all products of elements from closure s.
Русский
Принцип индукции по замыканию для предикатов с двумя аргументами: если свойство верно для элементов из s и сохраняется под произведением, то оно верно и для любых произведений элементов closure s.
LaTeX
$$closure_induction₂ {motive} (mem) (one_left) (one_right) (mul_left) (mul_right) {x} {y} (hx) (hy) : motive x y hx hy$$
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₂ {motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop}
(mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), motive x y (subset_closure hx) (subset_closure hy))
(one_left : ∀ x hx, motive 1 x (one_mem _) hx) (one_right : ∀ x hx, motive x 1 hx (one_mem _))
(mul_left : ∀ x y z hx hy hz, motive x z hx hz → motive y z hy hz → motive (x * y) z (mul_mem hx hy) hz)
(mul_right : ∀ x y z hx hy hz, motive z x hz hx → motive z y hz hy → motive z (x * y) hz (mul_mem hx hy)) {x y : M}
(hx : x ∈ closure s) (hy : y ∈ closure s) : motive 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₂
| one => exact one_right x hx
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
