two_lt_lineCount

Mathlib.Combinatorics.Configuration

URI: https://scilib.ai/kg/mathlib#Configuration.ProjectivePlane.two_lt_lineCount

← MathLib Explorer

English

For any point p in a finite projective plane, lineCount L p > 2.

Русский

Для любой точки p в конечной проективной плоскости lineCount L p превышает 2.

LaTeX

$$$ 2 < \operatorname{lineCount}(L,p) $$$

Lean4

theorem two_lt_lineCount [Finite P] [Finite L] (p : P) : 2 < lineCount L p := by
  simpa only [lineCount_eq L p, Nat.succ_lt_succ_iff] using one_lt_order P L

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

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

Разделы

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

Аффилиация

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