Structures · Combinatorics
Configuration.HasPoints
A nondegenerate configuration in which every pair of lines has an intersection point.
- Defined in
- Mathlib.Combinatorics.Configuration
- Shape
- 2 explicit arguments · adds mkPoint, mkPoint_ax
Extends1
Extended by1
Concrete types that are instances1
- Configuration.Dual
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- Configuration.HasPoints.mkPoint
- Configuration.HasPoints.mkPoint_ax
- Configuration.HasPoints.existsUnique_point
- Configuration.HasPoints.card_le
- Configuration.HasPoints.lineCount_le_pointCount
- Configuration.HasPoints.lineCount_eq_pointCount
- Configuration.HasPoints.hasLines
- Configuration.HasPoints.toNondegenerate
- Configuration.Dual.hasLines