affineIndependent_of_ne_of_mem_of_notMem_of_mem

English

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

Русский

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

LaTeX

$$$ p_1 \\neq p_3 \\land p_1 \\in s \\land p_2 \\notin 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_mem_of_notMem_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 (1 : Fin 3) 2)]
  convert affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₁p₃ hp₁ hp₃ hp₂ using 1
  ext x
  fin_cases x <;> rfl

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