Structures · Combinatorics
Configuration.HasLines
A nondegenerate configuration in which every pair of points has a line through them.
- Defined in
- Mathlib.Combinatorics.Configuration
- Shape
- 2 explicit arguments · adds mkLine, mkLine_ax
Extends1
Extended by1
Concrete types that are instances1
- Configuration.Dual
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- Configuration.HasLines.pointCount_le_lineCount
- Configuration.HasLines.lineCount_eq_pointCount
- Configuration.HasLines.mkLine
- Configuration.HasLines.card_le
- Configuration.HasLines.mkLine_ax
- Configuration.HasLines.exists_bijective_of_card_eq
- Configuration.Dual.hasPoints
- Configuration.HasLines.toNondegenerate
- Configuration.HasLines.hasPoints
- Configuration.HasLines.existsUnique_line