From 87fa060ceb16e3f07f81fe91016a7eb0c6ad2035 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 23 Dec 2021 16:32:59 +0000 Subject: [PATCH] feat(combinatorics/configuration): Define `line_count` and `point_count` (#10884) Adds definitions for the number of lines through a given point and the number of points through a given line. Co-authored-by: tb65536 --- src/combinatorics/configuration.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/configuration.lean b/src/combinatorics/configuration.lean index aa7bc87ef4c22..d0ba31ec84a69 100644 --- a/src/combinatorics/configuration.lean +++ b/src/combinatorics/configuration.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Browning -/ import combinatorics.hall.basic -import data.fintype.card +import set_theory.fincard /-! # Configurations of Points and lines @@ -17,6 +17,8 @@ This file introduces abstract configurations of points and lines, and proves som every pair of lines has an intersection point. * `configuration.has_lines`: A nondegenerate configuration in which every pair of points has a line through them. +* `configuration.line_count`: The number of lines through a given point. +* `configuration.point_count`: The number of lines through a given line. ## Todo * Abstract projective planes. @@ -81,4 +83,14 @@ lemma has_lines.exists_unique_line [has_lines P L] (p₁ p₂ : P) (hp : p₁ ∃! l : L, p₁ ∈ l ∧ p₂ ∈ l := has_points.exists_unique_point (dual L) (dual P) p₁ p₂ hp +variables {P} (L) + +/-- Number of points on a given line. -/ +noncomputable def line_count (p : P) : ℕ := nat.card {l : L // p ∈ l} + +variables (P) {L} + +/-- Number of lines through a given point. -/ +noncomputable def point_count (l : L) : ℕ := nat.card {p : P // p ∈ l} + end configuration