English
Let N be an additive monoid with R-module structure, and s ⊆ M, t ⊆ N. Let P be a predicate on pairs (x,y) with hx ∈ span R s and hy ∈ span R t. If P holds for all pairs (x,y) with x ∈ s and y ∈ t, and P holds when either coordinate is 0 (with the other fixed in its span), and P is preserved under addition in either coordinate and under scalar multiplication in either coordinate, then P(a,b) holds for all a ∈ span R s and b ∈ span R t.
Русский
Пусть N (, M) — пары модулей с заданной структурой. Пусть P — предикат на пары (x,y) с hx ∈ span R s и hy ∈ span R t. Если P выполняется для всех пар x ∈ s и y ∈ t, и P выполняется при 0 в любой из координат, и P сохраняется при сложении и умножении на скаляры в обеих координатах, то P(a,b) выполняется для всех a ∈ span R s и b ∈ span R t.
LaTeX
$$$$\\forall {N} (\\text{AddCommMonoid } N) [\\text{Module } R N] \\{t : \\text{Set } N\\}, \\{p :(x:M) \\to (y:N) \\to x\\in span R s \\to y\\in span R t \\to Prop\\},$$\n$$ (\\forall x \\in s, \\forall y \\in t, p(x,y,hx,hy)) \\,\\land\\, (\\forall y, hy, p(0,y,zero\_mem,hy)) \\,\\land\\, (\\forall x, hx, y, hy, hz, p(x,z,hx,hz) \\to p(y,z,hy,hz) ) \\,\\land\\, (\\forall x, hx, y, hy, hz, p(x,y,hx,hy) \\to p(x,z,hx,hz)) \\Rightarrow \\forall a,b, ha,hb, p(a,b,ha,hb) $$$$
Lean4
/-- An induction principle for span membership. This is a version of `Submodule.span_induction`
for binary predicates. -/
theorem span_induction₂ {N : Type*} [AddCommMonoid N] [Module R N] {t : Set N}
{p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop}
(mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ t), p x y (subset_span hx) (subset_span hy))
(zero_left : ∀ y hy, p 0 y (zero_mem _) hy) (zero_right : ∀ x hx, p x 0 hx (zero_mem _))
(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))
(smul_left : ∀ (r : R) x y hx hy, p x y hx hy → p (r • x) y (smul_mem _ r hx) hy)
(smul_right : ∀ (r : R) x y hx hy, p x y hx hy → p x (r • y) hx (smul_mem _ r hy)) {a : M} {b : N}
(ha : a ∈ Submodule.span R s) (hb : b ∈ Submodule.span R t) : p a b ha hb := by
induction hb using span_induction with
| mem z hz =>
induction ha using span_induction with
| mem _ h => exact mem_mem _ _ h hz
| zero => exact zero_left _ _
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| smul _ _ _ h => exact smul_left _ _ _ _ _ h
| zero => exact zero_right a ha
| add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
| smul _ _ _ h => exact smul_right _ _ _ _ _ h
