Commit 2022-11-17 18:59 8ab239e9

View on Github →

feat(combinatorics/simple_graph/basic): Graph construction from edges (#16691) This PR adds ways to construct a simple_graph from the set or finset of edges. It can further simplify the addition/deletion of edges from a graph. It also enables the induction on the edges of the graph using finset induction.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.delete_edges_eq_sdiff_from_edge_set

added theorem simple_graph.edge_set_from_edge_set

added def simple_graph.from_edge_set

added theorem simple_graph.from_edge_set_adj

added theorem simple_graph.from_edge_set_edge_set

added theorem simple_graph.from_edge_set_empty

added theorem simple_graph.from_edge_set_univ