English
If a point p is not on a line l, then pointCount(P,l) ≤ lineCount(L,p) (under appropriate finiteness assumptions).
Русский
Если точка p не лежит на прямой l, то число точек на l не превышает число прямых через p (при определенных условия конечности).
LaTeX
$$$p\\notin l \\implies \\text{pointCount}(P,l) \\le \\text{lineCount}(L,p)$$$
Lean4
theorem pointCount_le_lineCount [HasLines P L] {p : P} {l : L} (h : p ∉ l) [Finite { l : L // p ∈ l }] :
pointCount P l ≤ lineCount L p := by
by_cases hf : Infinite { p : P // p ∈ l }
· exact (le_of_eq Nat.card_eq_zero_of_infinite).trans (zero_le (lineCount L p))
haveI := fintypeOfNotInfinite hf
cases nonempty_fintype { l : L // p ∈ l }
rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
have : ∀ p' : { p // p ∈ l }, p ≠ p' := fun p' hp' => h ((congr_arg (· ∈ l) hp').mpr p'.2)
exact
Fintype.card_le_of_injective (fun p' => ⟨mkLine (this p'), (mkLine_ax (this p')).1⟩) fun p₁ p₂ hp =>
Subtype.ext
((eq_or_eq p₁.2 p₂.2 (mkLine_ax (this p₁)).2
((congr_arg (_ ∈ ·) (Subtype.ext_iff.mp hp)).mpr (mkLine_ax (this p₂)).2)).resolve_right
fun h' => (congr_arg (p ∉ ·) h').mp h (mkLine_ax (this p₁)).1)
