card_le — Mathlib

English

Dually, if every pair of lines intersects in a unique point, then |L| ≤ |P|.

Русский

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

LaTeX

$$$\\langle \\text{HasPoints}\\ P\\ L \\rangle\\Rightarrow |L| \\le |P|$$$

Lean4

/-- If a nondegenerate configuration has a unique point on any two lines, then `|L| ≤ |P|`. -/
theorem card_le [HasPoints P L] [Fintype P] [Fintype L] : Fintype.card L ≤ Fintype.card P :=
  @HasLines.card_le (Dual L) (Dual P) _ _ _ _

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