independent_pair_iff_ne — Mathlib

English

Let u, v be points in the projective space P_K(V). Then the two-point set {u, v} is independent if and only if u ≠ v.

Русский

Пусть u, v — точки в проективном пространстве ℙ_K(V). Тогда пара точек {u, v} линейно независима тогда и только если u ≠ v.

LaTeX

$$$\forall u,v \in \mathbb{P}_K V,\; \operatorname{Independent}([u,v]) \iff u \neq v$$$

Lean4

/-- Two points in a projective space are independent if and only if the points are not equal. -/
@[simp]
theorem independent_pair_iff_ne (u v : ℙ K V) : Independent ![u, v] ↔ u ≠ v := by
  rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]

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