English
The direction of the affine span after inserting a point into a nonempty affine subspace is the sum of the span of the difference with a fixed point and the original direction.
Русский
Направление афинной оболочки после вставки точки в непустое афинное подпространство равно сумме порождаемого подпространства разности и исходного направления.
LaTeX
$$$\\mathrm{direction}(\\operatorname{affineSpan}_k(\\operatorname{insert} p_2 (s))) = \\operatorname{span}_k\\{ p_2 - p_1 \\} \\sqcup s.\\mathrm{direction}$$$
Lean4
/-- The direction of the span of the result of adding a point to a nonempty affine subspace is the
sup of the direction of that subspace and of any one difference between that point and a point in
the subspace. -/
theorem direction_affineSpan_insert {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) :
(affineSpan k (insert p₂ (s : Set P))).direction = Submodule.span k {p₂ -ᵥ p₁} ⊔ s.direction :=
by
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]
change (s ⊔ affineSpan k { p₂ }).direction = _
rw [direction_sup hp₁ (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]
simp
