Theorems · Inductive type · combinatorics

Configuration.Nondegenerate

(P : Type u_1) → (L : Type u_2) → [Membership 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.

Defined in

Mathlib.Combinatorics.Configuration

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Membership