lineCount_eq_pointCount — Mathlib

English

For any p ∈ P and l ∈ L, the number of lines through p equals the number of points on l.

Русский

Для любой точки p и прямой l число прямых через p равно числу точек на l.

LaTeX

$$$\\text{lineCount}(L,p) = \\text{pointCount}(P,l)$ for appropriate p,l$$

Lean4

theorem lineCount_eq_pointCount [Finite P] [Finite L] (p : P) (l : L) : lineCount L p = pointCount P l :=
  Exists.elim (exists_point l) fun q hq =>
    (lineCount_eq_lineCount L p q).trans <| by
      cases nonempty_fintype P
      cases nonempty_fintype L
      exact HasLines.lineCount_eq_pointCount (card_points_eq_card_lines P L) hq

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