lineCount_eq — Mathlib

English

In a finite projective plane, for every point p the number of lines through p equals the order of the plane plus one.

Русский

В конечной проективной плоскости для любой точки p число лучей, проходящих через p, равно порядку плоскости плюс один.

LaTeX

$$$ \operatorname{lineCount}(L,p) = \operatorname{order}(P,L) + 1$$$

Lean4

theorem lineCount_eq [Finite P] [Finite L] (p : P) : lineCount L p = order P L + 1 := by
  classical
  obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
  cases nonempty_fintype { l : L // q ∈ l }
  rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q, lineCount,
    Nat.card_eq_fintype_card, Nat.sub_add_cancel]
  exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

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