dependent_pair_iff_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Two points in a projective space are dependent if and only if they are equal. -/
@[simp]
theorem dependent_pair_iff_eq (u v : ℙ K V) : Dependent ![u, v] ↔ u = v :=
  by
  rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2]
  dsimp only [Function.comp_def, Matrix.cons_val]
  simp only [not_and, not_forall, not_not, ← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep,
    Classical.imp_iff_right_iff]
  exact Or.inl (rep_nonzero v)

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