card_points_eq_card_lines

Mathlib.Combinatorics.Configuration

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

← MathLib Explorer

English

For a finite projective plane, the number of points equals the number of lines: |P| = |L|.

Русский

Для конечной проективной плоскости число точек равно числу прямых: |P| = |L|.

LaTeX

$$$|P| = |L|$$$

Lean4

theorem card_points_eq_card_lines [Fintype P] [Fintype L] : Fintype.card P = Fintype.card L :=
  le_antisymm (HasLines.card_le P L) (HasPoints.card_le P L)

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

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

Разделы

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

Аффилиация

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