pointCount_eq_pointCount — Mathlib

English

In a finite projective plane, all lines contain the same number of points; equivalently, pointCount is constant across L.

Русский

Во всех прямых в конечной проективной плоскости содержится одинаковое число точек.

LaTeX

$$$\\forall l,m\\in L, \\text{pointCount}(P,l) = \\text{pointCount}(P,m)$$$

Lean4

theorem pointCount_eq_pointCount [Finite P] [Finite L] (l m : L) : pointCount P l = pointCount P m := by
  apply lineCount_eq_lineCount (Dual P)

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