Collinear — Mathlib

English

A set is collinear if and only if the rank of its vector span is at most 1.

Русский

Множество точек коллинеарно тогда и только тогда, когда ранг векторного разложения не более единицы.

LaTeX

$$$\operatorname{Collinear}_k(s) \iff \operatorname{rank}_k\bigl(\operatorname{vectorSpan}_k(s)\bigr) \le 1$$$

Lean4

/-- A set of points is collinear if their `vectorSpan` has dimension
at most `1`. -/
def Collinear (s : Set P) : Prop :=
  Module.rank k (vectorSpan k s) ≤ 1

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