English
Let s be an affine subspace of P. If p1 and p2 lie in s, p3 does not, and p1 ≠ p2, then p1, p2, p3 are affinely independent.
Русский
Пусть s — аффинное подпространство P. Если точки p1, p2 принадлежат s, p3 не принадлежит s, и p1 ≠ p2, то p1, p2, p3 аффинно независимы.
LaTeX
$$$ p_1 \\neq p_2 \\land p_1 \\in s \\land p_2 \\in s \\land p_3 \\notin s \\implies \\operatorname{AffineIndependent}_k(p_1,p_2,p_3). $$$
Lean4
/-- If distinct points `p₁` and `p₂` lie in `s` but `p₃` does not, the three points are affinely
independent. -/
theorem affineIndependent_of_ne_of_mem_of_mem_of_notMem {s : AffineSubspace k P} {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂)
(hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∉ s) : AffineIndependent k ![p₁, p₂, p₃] :=
by
have ha : AffineIndependent k fun x : { x : Fin 3 // x ≠ 2 } => ![p₁, p₂, p₃] x :=
by
rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]
convert affineIndependent_of_ne k hp₁p₂
ext x
fin_cases x <;> rfl
refine ha.affineIndependent_of_notMem_span ?_
intro h
refine hp₃ ((AffineSubspace.le_def' _ s).1 ?_ p₃ h)
simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage]
intro x
fin_cases x <;> simp +decide [hp₁, hp₂]
