English
If |P| = |L| and HasLines, then there exists a bijection f: L → P satisfying point/line incidence correspondence: ∀l, pointCount P l = lineCount L (f l).
Русский
При равности кардинальностей |P| = |L| существует биекция f: L → P, такая что для каждой прямой l число точек на l равно числу прямых через соответствующую точку f(l).
LaTeX
$$$\\exists f:\\, L\\to P,\\ \\text{Bijective}(f)\\ \\land\\ \\forall l,\\ \\text{pointCount}(P,l) = \\text{lineCount}(L,(f\\,l))$$$
Lean4
theorem exists_bijective_of_card_eq [HasLines P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) :
∃ f : L → P, Function.Bijective f ∧ ∀ l, pointCount P l = lineCount L (f l) := by
classical
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
exact
⟨f, hf3, fun l ↦
(sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <|
mem_univ _⟩
