Theorems · Theorem · combinatorics
Configuration.HasLines.card_le
∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.HasLines P L] [inst : Fintype P] [inst_1 : Fintype L], Fintype.card P ≤ Fintype.card L
If a nondegenerate configuration has a unique line through any two points, then |P| ≤ |L|.
- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- Fintype.cardstatement and proof · cited by 1,386
- Finset.mapproof · cited by 747
- zero_leproof · cited by 382
- Finset.mem_univproof · cited by 361
- Nat.card_eq_fintype_cardproof · cited by 200
- lt_irreflproof · cited by 190
- Finset.sum_le_sumproof · cited by 182
- Finset.sum_mapproof · cited by 115
Cited by2
Results whose statement or proof uses this declaration.
- Configuration.ProjectivePlane.card_points_eq_card_linesproof · cited by 2
- Configuration.HasPoints.card_leproof · cited by 1