English
If a set of vectors s spans V, then the affine hull of p together with those vectors translated to p spans the entire space P.
Русский
Если множество векторов s линe заставляет покрывать V, то афинная оболочка точки p вместе с векторами, перенесёнными к p, покрывает всё пространство P.
LaTeX
$$$\\operatorname{affineSpan}_k\\big\\({p}\\ \\cup\\ (\\{v + p : v \\in s\\})\\big) = \\top\\quad\\text{whenever } \\operatorname{span}_k(\\operatorname{range}(s)) = \\top$$$
Lean4
/-- Suppose a set of vectors spans `V`. Then a point `p`, together with those vectors added to `p`,
spans `P`. -/
theorem affineSpan_singleton_union_vadd_eq_top_of_span_eq_top {s : Set V} (p : P)
(h : Submodule.span k (Set.range ((↑) : s → V)) = ⊤) : affineSpan k ({ p } ∪ (fun v => v +ᵥ p) '' s) = ⊤ :=
by
convert ext_of_direction_eq _ ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩
rw [direction_affineSpan, direction_top,
vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _), eq_top_iff, ← h]
apply Submodule.span_mono
rintro v ⟨v', rfl⟩
use (v' : V) +ᵥ p
simp
