coplanar_iff_finrank_le_two — Mathlib

English

A subset of a Coplanar set is Coplanar.

Русский

Подмножество копланарного множества копланарно.

LaTeX

$$hs ⊆ s2 ∧ Coplanar(k, s2) → Coplanar(k, s1)$$

Lean4

/-- A set of points, whose `vectorSpan` is finite-dimensional, is coplanar if and only if their
`vectorSpan` has dimension at most `2`. -/
theorem coplanar_iff_finrank_le_two {s : Set P} [FiniteDimensional k (vectorSpan k s)] :
    Coplanar k s ↔ finrank k (vectorSpan k s) ≤ 2 :=
  by
  have h : Coplanar k s ↔ Module.rank k (vectorSpan k s) ≤ 2 := Iff.rfl
  rw [← finrank_eq_rank] at h
  exact mod_cast h

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