Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-15 09:02 dd51529f

View on Github →

feat(combinatorics/simple_graph/subgraph): delete_edges (#13306) Construct a subgraph from another by deleting edges.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

Modified src/combinatorics/simple_graph/subgraph.lean

deleted def simple_graph.subgraph.coe

added theorem simple_graph.subgraph.coe_delete_edges_eq

added theorem simple_graph.subgraph.coe_delete_edges_le

added def simple_graph.subgraph.delete_edges

added theorem simple_graph.subgraph.delete_edges_adj

added theorem simple_graph.subgraph.delete_edges_coe_eq

added theorem simple_graph.subgraph.delete_edges_delete_edges

added theorem simple_graph.subgraph.delete_edges_empty_eq

added theorem simple_graph.subgraph.delete_edges_inter_edge_set_left_eq

added theorem simple_graph.subgraph.delete_edges_inter_edge_set_right_eq

added theorem simple_graph.subgraph.delete_edges_le

added theorem simple_graph.subgraph.delete_edges_le_of_le

added theorem simple_graph.subgraph.delete_edges_spanning_coe_eq

added theorem simple_graph.subgraph.delete_edges_verts

deleted def simple_graph.subgraph.spanning_coe

added theorem simple_graph.subgraph.spanning_coe_delete_edges_le