two_lt_pointCount

Mathlib.Combinatorics.Configuration

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

← MathLib Explorer

English

For any line l in a finite projective plane, pointCount P l > 2.

Русский

Для любой прямой l в конечной проективной плоскости pointCount P l превышает 2.

LaTeX

$$$ 2 < \operatorname{pointCount} P l $$$

Lean4

theorem two_lt_pointCount [Finite P] [Finite L] (l : L) : 2 < pointCount P l := by
  simpa only [pointCount_eq P l, Nat.succ_lt_succ_iff] using one_lt_order P L

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

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

Разделы

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

Аффилиация

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