Commit 2022-11-18 21:43 b0768801

View on Github →

feat(combinatorics/simple_graph/acyclic): acyclic graphs and trees (#17213) Defines the notions of acyclic graphs and trees and proves some characterizations, for example uniqueness of paths. From the walks_and_trees branch.

Estimated changes

Created src/combinatorics/simple_graph/acyclic.lean

added theorem simple_graph.is_acyclic.path_unique

added def simple_graph.is_acyclic

added theorem simple_graph.is_acyclic_iff_forall_adj_is_bridge

added theorem simple_graph.is_acyclic_iff_forall_edge_is_bridge

added theorem simple_graph.is_acyclic_iff_path_unique

added theorem simple_graph.is_acyclic_of_path_unique

added structure simple_graph.is_tree

added theorem simple_graph.is_tree_iff_exists_unique_path

Modified src/combinatorics/simple_graph/connectivity.lean

modified theorem simple_graph.walk.is_path.nil

added theorem simple_graph.walk.is_path_iff_eq_nil