English
Let s be a Collinear set, with p1, p2 ∈ s and p1 ≠ p2. Then the affine span of s equals the line through p1 and p2: line(k, p1, p2) = affineSpan(k, s).
Русский
Пусть s — коллинеарный набор, p1, p2 ∈ s и p1 ≠ p2. Тогда аффинальная оболочка s равна прямой через p1 и p2: line(k, p1, p2) = affineSpan(k, s).
LaTeX
$$Collinear_k(s) → p1 ∈ s → p2 ∈ s → p1 ≠ p2 → line_k(p1,p2) = affineSpan_k(s)$$
Lean4
/-- The affine span of any two distinct points of a collinear set of points equals the affine
span of the whole set. -/
theorem affineSpan_eq_of_ne {s : Set P} (h : Collinear k s) {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
(hp₁p₂ : p₁ ≠ p₂) : line[k, p₁, p₂] = affineSpan k s :=
le_antisymm (affineSpan_mono _ (Set.insert_subset_iff.2 ⟨hp₁, Set.singleton_subset_iff.2 hp₂⟩))
(affineSpan_le.2 fun _ hp => h.mem_affineSpan_of_mem_of_ne hp₁ hp₂ hp hp₁p₂)
