coplanar_of_fact_finrank_eq_two

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#coplanar_of_fact_finrank_eq_two

← MathLib Explorer

English

If there is a fact that finrank k V equals 2, then Coplanar k s holds.

Русский

Если существует факт, что \operatorname{finrank}_k V = 2, то Coplanar(k,s) верно.

LaTeX

$$Fact(finrank_k V = 2) → Coplanar(k,s)$$

Lean4

/-- A set of points in a two-dimensional space is coplanar. -/
theorem coplanar_of_fact_finrank_eq_two (s : Set P) [h : Fact (finrank k V = 2)] : Coplanar k s :=
  coplanar_of_finrank_eq_two s h.out

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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