English
A mirrored version of the lineMap span invariance under unit weights holds for all nontrivial k, showing resilience of the affine span under line-mapped deformations.
Русский
Повторение инвариантности афинного пространства под линейными отображениями с единичными весами для всех ненулевых k.
LaTeX
$$$\affineSpan_k(\Set.range( \lambda q: AffineMap.lineMap p q)) = \affineSpan_k(\Set.range s)$$$
Lean4
/-- A weighted sum, as an affine map on the points involved. -/
def weightedVSubOfPoint (w : ι → k) : (ι → P) × P →ᵃ[k] V
where
toFun p := s.weightedVSubOfPoint p.fst p.snd w
linear := ∑ i ∈ s, w i • ((LinearMap.proj i).comp (LinearMap.fst _ _ _) - LinearMap.snd _ _ _)
map_vadd' := by
rintro ⟨p, b⟩ ⟨v, b'⟩
simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, ← sub_add_eq_add_sub,
smul_add, Finset.sum_add_distrib]
