Theorems · Inductive type · combinatorics
Configuration.ProjectivePlane
(P : Type u_1) → (L : Type u_2) → [Membership 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.
- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Membership
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by22
Results whose statement or proof uses this declaration.
- Configuration.ProjectivePlane.orderstatement and proof · cited by 6
- Configuration.ProjectivePlane.exists_configstatement and proof · cited by 5
- Configuration.ProjectivePlane.lineCount_eqstatement and proof · cited by 3
- Configuration.ProjectivePlane.lineCount_eq_lineCountstatement and proof · cited by 3
- Configuration.ProjectivePlane.pointCount_eqstatement and proof · cited by 3
- Configuration.ProjectivePlane.Dual.orderstatement and proof · cited by 2
- Configuration.ProjectivePlane.card_points_eq_card_linesstatement and proof · cited by 2
- Configuration.ProjectivePlane.mkLinestatement and proof · cited by 2
- Configuration.ProjectivePlane.one_lt_orderstatement and proof · cited by 2
- Configuration.ProjectivePlane.card_pointsstatement and proof · cited by 1
- Configuration.ProjectivePlane.lineCount_eq_pointCountstatement and proof · cited by 1
- Configuration.ProjectivePlane.mkLine_axstatement and proof · cited by 1