English
The total number of incidences can be counted in two ways: summing lineCount over all points equals summing pointCount over all lines.
Русский
Общее число инцидентностей считается двумя способами: сумма lineCount по всем точкам равна сумме pointCount по всем прямым.
LaTeX
$$$\\sum_{p\\in P} \\text{lineCount}(L,p) = \\sum_{l\\in L} \\text{pointCount}(P,l)$$$
Lean4
theorem sum_lineCount_eq_sum_pointCount [Fintype P] [Fintype L] : ∑ p : P, lineCount L p = ∑ l : L, pointCount P l := by
classical
simp only [lineCount, pointCount, Nat.card_eq_fintype_card, ← Fintype.card_sigma]
apply Fintype.card_congr
calc
(Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } := (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
_ ≃ { x : L × P // x.2 ∈ x.1 } := ((Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl)
_ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l
