affineIndependent_of_ne_of_notMem_of_mem_of_mem

English

Let s be an affine subspace. If p2 ≠ p3, p1 ∉ s, p2 ∈ s, p3 ∈ s, then p1, p2, p3 are affinely independent.

Русский

Пусть s — аффинное подпространство. Если p2 ≠ p3, p1 ∉ s, p2 ∈ s, p3 ∈ s, тогда p1, p2, p3 аффинно независимы.

LaTeX

$$$ p_2 \\neq p_3 \\land p_1 \\notin s \\land p_2 \\in s \\land p_3 \\in 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_notMem_of_mem_of_mem {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
  rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]
  convert affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₂p₃.symm hp₃ hp₂ hp₁ using 1
  ext x
  fin_cases x <;> rfl

Похожие утверждения