mathlib documentation

combinatorics.configuration

Configurations of Points and lines #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file introduces abstract configurations of points and lines, and proves some basic properties.

Main definitions #

Main statements #

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[class]
structure configuration.nondegenerate (P : Type u_1) (L : Type u_2) [has_mem P L] :
Prop

A configuration is nondegenerate if:

  1. there does not exist a line that passes through all of the points,
  2. there does not exist a point that is on all of the lines,
  3. there is at most one line through any two points,
  4. any two lines have at most one intersection point. Conditions 3 and 4 are equivalent.
Instances of this typeclass
@[class]
structure configuration.has_points (P : Type u_1) (L : Type u_2) [has_mem P L] :
Type (max u_1 u_2)

A nondegenerate configuration in which every pair of lines has an intersection point.

Instances of this typeclass
Instances of other typeclasses for configuration.has_points
  • configuration.has_points.has_sizeof_inst
@[class]
structure configuration.has_lines (P : Type u_1) (L : Type u_2) [has_mem P L] :
Type (max u_1 u_2)

A nondegenerate configuration in which every pair of points has a line through them.

Instances of this typeclass
Instances of other typeclasses for configuration.has_lines
  • configuration.has_lines.has_sizeof_inst
theorem configuration.has_points.exists_unique_point (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_points P L] (l₁ l₂ : L) (hl : l₁ l₂) :
∃! (p : P), p l₁ p l₂
theorem configuration.has_lines.exists_unique_line (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.has_lines P L] (p₁ p₂ : P) (hp : p₁ p₂) :
∃! (l : L), p₁ l p₂ l

If a nondegenerate configuration has at least as many points as lines, then there exists an injective function f from lines to points, such that f l does not lie on l.

noncomputable def configuration.line_count {P : Type u_1} (L : Type u_2) [has_mem P L] (p : P) :

Number of points on a given line.

Equations
noncomputable def configuration.point_count (P : Type u_1) {L : Type u_2} [has_mem P L] (l : L) :

Number of lines through a given point.

Equations
theorem configuration.has_points.line_count_le_point_count {P : Type u_1} {L : Type u_2} [has_mem P L] [configuration.has_points P L] {p : P} {l : L} (h : p l) [hf : finite {p // p l}] :

If a nondegenerate configuration has a unique line through any two points, then |P| ≤ |L|.

If a nondegenerate configuration has a unique point on any two lines, then |L| ≤ |P|.

If a nondegenerate configuration has a unique line through any two points, and if |P| = |L|, then there is a unique point on any two lines.

Equations

If a nondegenerate configuration has a unique point on any two lines, and if |P| = |L|, then there is a unique line through any two points.

Equations
@[class]
structure configuration.projective_plane (P : Type u_1) (L : Type u_2) [has_mem P L] :
Type (max u_1 u_2)

A projective plane is a nondegenerate configuration in which every pair of lines has an intersection point, every pair of points has a line through them, and which has three points in general position.

Instances of this typeclass
Instances of other typeclasses for configuration.projective_plane
  • configuration.projective_plane.has_sizeof_inst
noncomputable def configuration.projective_plane.order (P : Type u_1) (L : Type u_2) [has_mem P L] [configuration.projective_plane P L] :

The order of a projective plane is one less than the number of lines through an arbitrary point. Equivalently, it is one less than the number of points on an arbitrary line.

Equations