Theorems · Definition · combinatorics
SimpleGraph.IsAcyclic
{V : Type u_1} → SimpleGraph V → PropA graph is acyclic (or a forest) if it has no cycles.
- Cited by
- 67 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Walkproof · cited by 915
- SimpleGraph.Walk.IsCycleproof · cited by 91
Cited by71
Results whose statement or proof uses this declaration.
- SimpleGraph.IsTree.isAcyclicstatement · cited by 5
- SimpleGraph.IsAcyclic.comapstatement and proof · cited by 4
- SimpleGraph.IsAcyclic.sup_edge_of_not_reachablestatement and proof · cited by 4
- SimpleGraph.egirth_eq_topstatement · cited by 4
- SimpleGraph.isAcyclic_iff_forall_isBridgestatement and proof · cited by 4
- SimpleGraph.IsAcyclic.antistatement and proof · cited by 3
- SimpleGraph.IsAcyclic.embeddingstatement and proof · cited by 3
- SimpleGraph.isAcyclic_iff_subsingleton_pathstatement and proof · cited by 3
- SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclicstatement and proof · cited by 3
- SimpleGraph.IsAcyclic.colorable_twostatement and proof · cited by 2
- SimpleGraph.IsAcyclic.eq_snd_of_adj_startstatement and proof · cited by 2
- SimpleGraph.IsAcyclic.of_subsingletonstatement · cited by 2