coplanar

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#Collinear.coplanar

English

Collinear implies Coplanar.

Русский

Коллинеарность влечет Koplanarность.

LaTeX

$$Collinear(k,s) → Coplanar(k,s)$$

Lean4

/-- Collinear points are coplanar. -/
theorem coplanar {s : Set P} (h : Collinear k s) : Coplanar k s :=
  le_trans h one_le_two

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru