English
For a nontrivial base ring k, transporting all other points along a line through p over a unit weight preserves the affine span of a set s.
Русский
При ненулевом кольце k перенос остальных точек вдоль линии через базовую точку p по единичному весу сохраняет афинное пространство множества s.
LaTeX
$$$\text{affineSpan}_k(\operatorname{Set.range}(\lambda q. \text{AffineMap.lineMap } p q)) = \text{affineSpan}_k(s)$$$
Lean4
/-- Given a set of points, together with a chosen base point in this set, if we affinely transport
all other members of the set along the line joining them to this base point, the affine span is
unchanged. -/
theorem affineSpan_eq_affineSpan_lineMap_units [Nontrivial k] {s : Set P} {p : P} (hp : p ∈ s) (w : s → Units k) :
affineSpan k (Set.range fun q : s => AffineMap.lineMap p ↑q (w q : k)) = affineSpan k s :=
by
have : s = Set.range ((↑) : s → P) := by simp
conv_rhs => rw [this]
apply le_antisymm <;> intro q hq <;>
erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢ <;>
obtain ⟨t, μ, rfl⟩ := hq <;>
use t <;>
[use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹] <;>
simp [smul_smul]
