Commit 2021-12-27 16:46 d67c4697

View on Github →

feat(combinatorics/simple_graph/basic): edge deletion (#11054) Function to delete edges from a simple graph, and some associated lemmas. Also defines sym2.to_rel as an inverse to sym2.from_rel.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.compl_eq_delete_edges

added def simple_graph.delete_edges

added theorem simple_graph.delete_edges_adj

added theorem simple_graph.delete_edges_delete_edges

added theorem simple_graph.delete_edges_empty_eq

added theorem simple_graph.delete_edges_eq_inter_edge_set

added theorem simple_graph.delete_edges_le

added theorem simple_graph.delete_edges_le_of_le

added theorem simple_graph.delete_edges_univ_eq

added theorem simple_graph.sdiff_eq_delete_edges

Modified src/combinatorics/simple_graph/subgraph.lean

deleted theorem simple_graph.subgraph.spanning_coe.is_subgraph_of_is_subgraph

added theorem simple_graph.subgraph.spanning_coe_le_of_le

Modified src/data/sym/sym2.lean

added theorem sym2.from_rel_to_rel

added def sym2.to_rel

added theorem sym2.to_rel_from_rel

added theorem sym2.to_rel_prop

added theorem sym2.to_rel_symmetric