Theorems · Theorem · combinatorics
SimpleGraph.eccent_le_one_iff
∀ {α : Type u_1} {G : SimpleGraph α} (u : α), G.eccent u ≤ 1 ↔ ∀ (v : α), u ≠ v → G.Adj u v- Defined in
- Mathlib.Combinatorics.SimpleGraph.Diam
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENatstatement · cited by 4,985
- LE.le.transproof · cited by 3,151
- SimpleGraphstatement and proof · cited by 3,072
- le_antisymmproof · cited by 2,068
- SimpleGraph.Adjstatement and proof · cited by 1,346
- SimpleGraph.edistproof · cited by 55
- SimpleGraph.eccentstatement and proof · cited by 28
- Order.one_le_iff_posproof · cited by 27
- SimpleGraph.edist_eq_one_iff_adjproof · cited by 5
- SimpleGraph.edist_le_eccentproof · cited by 4
- SimpleGraph.edist_pos_of_neproof · cited by 3
- SimpleGraph.eccent_le_iffproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- SimpleGraph.eccent_eq_one_iffproof · cited by 0