English
In a finite projective plane, all points have the same number of incident lines; equivalently, the lineCount is constant across P.
Русский
Во всей конечной проективной плоскости у всех точек одинаковое число инцидентных прямых.
LaTeX
$$$\\forall p,q\\in P, \\text{lineCount}(L,p) = \\text{lineCount}(L,q)$$$
Lean4
theorem lineCount_eq_lineCount [Finite P] [Finite L] (p q : P) : lineCount L p = lineCount L q :=
by
cases nonempty_fintype P
cases nonempty_fintype L
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, h₁₂, h₁₃, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
have h := card_points_eq_card_lines P L
let n := lineCount L p₂
have hp₂ : lineCount L p₂ = n := rfl
have hl₁ : pointCount P l₁ = n := (HasLines.lineCount_eq_pointCount h h₂₁).symm.trans hp₂
have hp₃ : lineCount L p₃ = n := (HasLines.lineCount_eq_pointCount h h₃₁).trans hl₁
have hl₃ : pointCount P l₃ = n := (HasLines.lineCount_eq_pointCount h h₃₃).symm.trans hp₃
have hp₁ : lineCount L p₁ = n := (HasLines.lineCount_eq_pointCount h h₁₃).trans hl₃
have hl₂ : pointCount P l₂ = n := (HasLines.lineCount_eq_pointCount h h₁₂).symm.trans hp₁
suffices ∀ p : P, lineCount L p = n by exact (this p).trans (this q).symm
refine fun p => or_not.elim (fun h₂ => ?_) fun h₂ => (HasLines.lineCount_eq_pointCount h h₂).trans hl₂
refine or_not.elim (fun h₃ => ?_) fun h₃ => (HasLines.lineCount_eq_pointCount h h₃).trans hl₃
rw [(eq_or_eq h₂ h₂₂ h₃ h₂₃).resolve_right fun h => h₃₃ ((congr_arg (p₃ ∈ ·) h).mp h₃₂)]
