Theorems · Theorem · combinatorics
Configuration.ProjectivePlane.exists_config
∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.ProjectivePlane P L],
∃ p₁ p₂ p₃ l₁ l₂ l₃, p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Configuration.ProjectivePlanestatement and proof · cited by 14
Cited by6
Results whose statement or proof uses this declaration.
- Configuration.ProjectivePlane.orderproof · cited by 6
- Configuration.ProjectivePlane.lineCount_eqproof · cited by 3
- Configuration.ProjectivePlane.lineCount_eq_lineCountproof · cited by 3
- Configuration.ProjectivePlane.one_lt_orderproof · cited by 2
- Configuration.ProjectivePlane.Dual.orderproof · cited by 2
- Configuration.ProjectivePlane.card_pointsproof · cited by 1