English
If the vector span of a set is finite-dimensional, then inserting a point preserves a finite-dimensional vector span.
Русский
Если векторное разложение множества конечномера, то добавление точки сохраняет конечномерность.
LaTeX
$$$\operatorname{FiniteDimensional}_k\bigl(\operatorname{vectorSpan}_k(\operatorname{insert} p (s))\bigr).$$$
Lean4
/-- A set of points is collinear if and only if they can all be
expressed as multiples of the same vector, added to the same base
point. -/
theorem collinear_iff_exists_forall_eq_smul_vadd (s : Set P) :
Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ r : k, p = r • v +ᵥ p₀ :=
by
rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)
· simp [collinear_empty]
· rw [collinear_iff_of_mem hp₁]
constructor
· exact fun h => ⟨p₁, h⟩
· rintro ⟨p, v, hv⟩
use v
intro p₂ hp₂
rcases hv p₂ hp₂ with ⟨r, rfl⟩
rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
use r - r₁
simp [vadd_vadd, ← add_smul]
