Theorems · Theorem · combinatorics
Configuration.HasLines.mkLine_ax
∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.HasLines P L] {p₁ p₂ : P} (h : p₁ ≠ p₂),
p₁ ∈ Configuration.HasLines.mkLine h ∧ p₂ ∈ Configuration.HasLines.mkLine h- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- Configuration.HasLines
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Configuration.HasLinesstatement and proof · cited by 6
- Configuration.HasLines.mkLinestatement · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- Configuration.HasLines.pointCount_le_lineCountproof · cited by 4
- Configuration.HasLines.card_leproof · cited by 2