English
Characterize membership in the affine span of an inserted point: p ∈ affineSpan_k(insert p2 s) iff there exists r and p0 ∈ s with p = r(p2 - p1) + p0 where p1 ∈ s.
Русский
Характеризуем принадлежность p афинной оболочке вставленной точки: p ∈ affineSpan_k(insert p2 s) тогда и только тогда, когда существуют r и p0 ∈ s такие, что p = r(p2 - p1) + p0,, где p1 ∈ s.
LaTeX
$$$p \\in \\operatorname{affineSpan}_k(\\operatorname{insert} p_2 s) \\iff \\exists r \\in k,\\exists p_0 \\in s,\\ p = r \\cdot (p_2 - p_1) + p_0$$$
Lean4
/-- Given a point `p₁` in an affine subspace `s`, and a point `p₂`, a point `p` is in the span of
`s` with `p₂` added if and only if it is a multiple of `p₂ -ᵥ p₁` added to a point in `s`. -/
theorem mem_affineSpan_insert_iff {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) :
p ∈ affineSpan k (insert p₂ (s : Set P)) ↔ ∃ r : k, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁ : V) +ᵥ p0 :=
by
rw [← mem_coe] at hp₁
rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),
direction_affineSpan_insert hp₁, Submodule.mem_sup]
constructor
· rintro ⟨v₁, hv₁, v₂, hv₂, hp⟩
rw [Submodule.mem_span_singleton] at hv₁
rcases hv₁ with ⟨r, rfl⟩
use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁
symm at hp
rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp
rw [hp, vadd_vadd]
· rintro ⟨r, p₃, hp₃, rfl⟩
use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁, vsub_mem_direction hp₃ hp₁
rw [vadd_vsub_assoc]
