pointCount_eq — Mathlib

English

In a finite projective plane, for every line l the number of points on l equals the order of the plane plus one.

Русский

В конечной проективной плоскости для любой прямой l число точек на l равно порядку плоскости плюс один.

LaTeX

$$$ \operatorname{pointCount}(P,l) = \operatorname{order}(P,L) + 1$$$

Lean4

theorem pointCount_eq [Finite P] [Finite L] (l : L) : pointCount P l = order P L + 1 :=
  (lineCount_eq (Dual P) _).trans (congr_arg (fun n => n + 1) (Dual.order P L))

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