affineIndependent_of_ne — Mathlib

English

Two distinct points are affinely independent.

Русский

Две различных точки являются аффинно независимыми.

LaTeX

$$$\\operatorname{affineIndependent}_k \\big( ![p_1,p_2] \\big)$ при $p_1\\neq p_2$$$

Lean4

/-- Two different points are affinely independent. -/
theorem affineIndependent_of_ne {p₁ p₂ : P} (h : p₁ ≠ p₂) : AffineIndependent k ![p₁, p₂] :=
  by
  rw [affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0]
  let i₁ : { x // x ≠ (0 : Fin 2) } := ⟨1, by simp⟩
  have he' : ∀ i, i = i₁ := by
    rintro ⟨i, hi⟩
    ext
    fin_cases i
    · simp at hi
    · simp [i₁]
  haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
  apply linearIndependent_unique
  rw [he' default]
  simpa using h.symm

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