Configuration.HasPoints.card_le
theorem Configuration.HasPoints.card_le :
∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst : Configuration.HasPoints P L] [inst : Fintype P]
[inst_1 : Fintype L], Fintype.card L ≤ Fintype.card P
This theorem states that for a nondegenerate configuration, if every pair of lines has a unique point of intersection, then the number of distinct lines (`|L|`) is less than or equal to the number of distinct points (`|P|`). Here, `P` and `L` represent the types of points and lines respectively. The `Configuration.HasPoints` instance asserts that there is a unique intersection point for every pair of lines in the configuration. The `Fintype` instances indicate that the sets of points and lines are finite.
More concisely: In a nondegenerate configuration of finite sets of points and lines where every pair of lines intersects in a unique point, the number of lines is less than or equal to the number of points.
|
Configuration.Nondegenerate.exists_injective_of_card_le
theorem Configuration.Nondegenerate.exists_injective_of_card_le :
∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [inst_1 : Configuration.Nondegenerate P L]
[inst_2 : Fintype P] [inst_3 : Fintype L],
Fintype.card L ≤ Fintype.card P → ∃ f, Function.Injective f ∧ ∀ (l : L), f l ∉ l
The theorem `Configuration.Nondegenerate.exists_injective_of_card_le` states that for any nondegenerate configuration (a mathematical setup involving points and lines), if the total number of points is equal to or exceeds the total number of lines, then there exists an injective function, denoted by `f`, from the set of lines to the set of points such that for any line `l`, the point `f(l)` does not lie on `l`. Here, an injective function is a function where distinct lines map to distinct points, ensuring that two different lines will not map to the same point. The nondegeneracy of the configuration ensures that each line contains at least two distinct points.
More concisely: In a nondegenerate configuration with at least as many points as lines, there exists an injective function from lines to distinct points not lying on the corresponding lines.
|
Configuration.HasLines.pointCount_le_lineCount
theorem Configuration.HasLines.pointCount_le_lineCount :
∀ {P : Type u_1} {L : Type u_2} [inst : Membership P L] [inst_1 : Configuration.HasLines P L] {p : P} {l : L},
p ∉ l → ∀ [inst_2 : Finite { l // p ∈ l }], Configuration.pointCount P l ≤ Configuration.lineCount L p
The theorem `Configuration.HasLines.pointCount_le_lineCount` states that for every set of points `P` and set of lines `L` with a membership relation, and given a configuration where every point is on at least one line (`Configuration.HasLines P L`), for any particular point `p` and line `l` such that the point `p` is not on the line `l`, as long as the set of lines passing through point `p` is finite, the number of points on line `l` (given by `Configuration.pointCount P l`) is less than or equal to the number of lines through point `p` (given by `Configuration.lineCount L p`). In simple terms, the number of points on any line not passing through a given point is always less than or equal to the number of lines passing through the given point.
More concisely: For any set of points and lines with a membership relation in a configuration where every point is on at least one line, the number of points on any line not passing through a given point is less than or equal to the number of lines passing through that point.
|
Configuration.HasLines.card_le
theorem Configuration.HasLines.card_le :
∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst : Configuration.HasLines P L] [inst : Fintype P]
[inst_1 : Fintype L], Fintype.card P ≤ Fintype.card L
This theorem states that for any types `P` and `L` that represent sets of points and lines in a configuration respectively, if the configuration is such that it has a unique line through any two points (which we refer to as being a 'nondegenerate' configuration), then the cardinality (or number of elements) of the set of points `P` is less than or equal to the cardinality of the set of lines `L`. This is formalized in Lean 4 using the fintype.card function, which gives the number of elements in a finite type. In mathematical terms, this could be written as `|P| ≤ |L|`.
More concisely: In a nondegenerate configuration of points and lines, the number of points is less than or equal to the number of lines.
|