order — Mathlib

English

Under HasLines, for any p ∈ P and l ∈ L with p not lying on l, lineCount L p equals pointCount P l.

Русский

При наличии HasLines и при условии, что p не принадлежит l, число прямых через p равно числу точек на l.

LaTeX

$$$\\text{lineCount}(L,p) = \\text{pointCount}(P,l)$ when $p\\notin l$$$

Lean4

theorem order [Finite P] [Finite L] : order (Dual L) (Dual P) = order P L :=
  congr_arg (fun n => n - 1) (lineCount_eq_pointCount _ _)

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