English
An induction principle: if a property holds on a generating set and is preserved under affine combinations, it holds on the whole affine span.
Русский
Принцип индукции по аффинной оболочке: свойство выполняется на порождающем множестве и сохраняется при аффинных комбинациях, значит, выполняется на всей оболочке.
LaTeX
$$$\text{If } x \in \operatorname{affineSpan}(k,s)\text{ and } p\text{ holds on } s\text{ and is closed under } c(u-v)+w,\ \text{then } p(x).$$$
Lean4
/-- An induction principle for span membership. If `p` holds for all elements of `s` and is
preserved under certain affine combinations, then `p` holds for all elements of the span of `s`. -/
@[elab_as_elim]
theorem affineSpan_induction {x : P} {s : Set P} {p : P → Prop} (h : x ∈ affineSpan k s) (mem : ∀ x : P, x ∈ s → p x)
(smul_vsub_vadd : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)) : p x :=
(affineSpan_le (Q := ⟨p, smul_vsub_vadd⟩)).mpr mem h
