English
Let p be a property of elements x ∈ span R s depending on the membership hx ∈ span R s. If p holds for every x ∈ s (with hx = subset_span h), and p holds for 0, and p is preserved under addition and scalar multiplication (i.e., if p x hx and p y hy then p (x + y) (add_mem ...), and if p x hx then p (a • x) (smul_mem ...)), then p holds for all x ∈ span R s.
Русский
Пусть p — свойство элемента x ∈ span R s, зависящее от принадлежности hx ∈ span R s. Если p выполняется для каждого x ∈ s (соответствующе hx = subset_span h), и p выполняется для 0, и p сохраняется при сложении и умножении на скаляры (т. е. если p x hx и p y hy то выполняется p (x + y) и т. д., и если p x hx тогда p (a • x)), то p выполняется для всех x ∈ span R s.
LaTeX
$$$\\forall p:\\; (M \\to \\text{Prop})\\;\\Big(\\, \\text{mem} \\_p : \\forall x\\in s, p(x, (subset\_span\\ h_x)) \\Big)\n\\;\\land\\; \\Big( p(0, (Submodule.zero\_mem _)) \\Big)\n\\;\\land\\; \\Big( \\forall x,y,hx,hy,\\; p(x,hx) \\to p(y,hy) \\to p(x+y, (Submodule.add\_mem _ hx hy)) \\Big)\n\\;\\land\\; \\Big( \\forall a,x,hx,\\; p(x,hx) \\to p(a\\cdot x, (Submodule.smul\_mem _ _ hx)) \\Big) \n\\;\\Rightarrow\\; \\forall {x} (hx : x ∈ span R s),\\; p(x, hx) $$$
Lean4
/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition and scalar multiplication, then `p` holds for all elements of the span of
`s`. -/
@[elab_as_elim]
theorem span_induction {p : (x : M) → x ∈ span R s → Prop} (mem : ∀ (x) (h : x ∈ s), p x (subset_span h))
(zero : p 0 (Submodule.zero_mem _)) (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›))
(smul : ∀ (a : R) (x hx), p x hx → p (a • x) (Submodule.smul_mem _ _ ‹_›)) {x} (hx : x ∈ span R s) : p x hx :=
by
let p : Submodule R M :=
{ carrier := {x | ∃ hx, p x hx}
add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
zero_mem' := ⟨_, zero⟩
smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩ }
exact span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id
