Structures · Combinatorics

Configuration.Nondegenerate

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.

Defined in

Mathlib.Combinatorics.Configuration

Shape

2 explicit arguments · adds exists_point, exists_line, eq_or_eq