English
If every pair of points determines a unique line, then |P| ≤ |L|.
Русский
Если любая пара точек задает уникальную прямую, то число точек не превосходит число прямых.
LaTeX
$$$\\langle \\text{HasLines}\\ P\\ L \\rangle\\Rightarrow |P| \\le |L|$$$
Lean4
/-- If a nondegenerate configuration has a unique line through any two points, then `|P| ≤ |L|`. -/
theorem card_le [HasLines P L] [Fintype P] [Fintype L] : Fintype.card P ≤ Fintype.card L := by
classical
by_contra hc₂
obtain ⟨f, hf₁, hf₂⟩ := Nondegenerate.exists_injective_of_card_le (le_of_not_ge hc₂)
have :=
calc
∑ p, lineCount L p = ∑ l, pointCount P l := sum_lineCount_eq_sum_pointCount P L
_ ≤ ∑ l, lineCount L (f l) := (Finset.sum_le_sum fun l _ => HasLines.pointCount_le_lineCount (hf₂ l))
_ = ∑ p ∈ univ.map ⟨f, hf₁⟩, lineCount L p := by rw [sum_map]; dsimp
_ < ∑ p, lineCount L p :=
by
obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le _
· simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
· rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
obtain ⟨l, _⟩ := @exists_line P L _ _ p
exact
let this := not_exists.mp hp l
⟨⟨mkLine this, (mkLine_ax this).2⟩⟩
exact lt_irrefl _ this
