English
If there is a bijection f as above, then for any line l, lineCount L p summed over all p equals pointCount P l summed over all l with the matching correspondence; consequently, lineCount and pointCount agree along the matching.
Русский
При существовании биекции f соответствия считывается равенство сумм lineCount и pointCount по перегруппировке инцидентностей.
LaTeX
$$$\\sum_{l\\in L} \\text{lineCount}(L, f(l)) = \\sum_{p\\in P} \\text{pointCount}(P, p)$$$
Lean4
theorem lineCount_eq_pointCount [HasLines P L] [Fintype P] [Fintype L] (hPL : Fintype.card P = Fintype.card L) {p : P}
{l : L} (hpl : p ∉ l) : lineCount L p = pointCount P l := by
classical
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL
let s : Finset (P × L) := Set.toFinset {i | i.1 ∈ i.2}
have step1 : ∑ i : P × L, lineCount L i.1 = ∑ i : P × L, pointCount P i.2 :=
by
rw [← Finset.univ_product_univ, Finset.sum_product_right, Finset.sum_product]
simp_rw [Finset.sum_const, Finset.card_univ, hPL, sum_lineCount_eq_sum_pointCount]
have step2 : ∑ i ∈ s, lineCount L i.1 = ∑ i ∈ s, pointCount P i.2 :=
by
rw [s.sum_finset_product Finset.univ fun p => Set.toFinset {l | p ∈ l}]
on_goal 1 =>
rw [s.sum_finset_product_right Finset.univ fun l => Set.toFinset {p | p ∈ l}, eq_comm]
· refine sum_bijective _ hf1 (by simp) fun l _ ↦ ?_
simp_rw [hf2, sum_const, Set.toFinset_card, ← Nat.card_eq_fintype_card]
change pointCount P l • _ = lineCount L (f l) • _
rw [hf2]
all_goals simp_rw [s, Finset.mem_univ, true_and, Set.mem_toFinset]; exact fun p => Iff.rfl
have step3 : ∑ i ∈ sᶜ, lineCount L i.1 = ∑ i ∈ sᶜ, pointCount P i.2 := by
rwa [← s.sum_add_sum_compl, ← s.sum_add_sum_compl, step2, add_left_cancel_iff] at step1
rw [← Set.toFinset_compl] at step3
exact
((Finset.sum_eq_sum_iff_of_le fun i hi => HasLines.pointCount_le_lineCount (by exact Set.mem_toFinset.mp hi)).mp
step3.symm (p, l) (Set.mem_toFinset.mpr hpl)).symm
