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`.

src/combinatorics/simple_graph/basic.lean

@@ -483,6 +483,49 @@ vertex and the set of vertices adjacent to the vertex.
 
 end incidence
 
+/-! ## Edge deletion -/
+
+/-- Given a set of vertex pairs, remove all of the corresponding edges from the edge set.
+It is fine to delete edges outside the edge set. -/
+def delete_edges (s : set (sym2 V)) : simple_graph V :=
+{ adj := G.adj \ sym2.to_rel s,
+  symm := λ a b, by simp [adj_comm, sym2.eq_swap] }
+
+@[simp] lemma delete_edges_adj (s : set (sym2 V)) (v w : V) :
+  (G.delete_edges s).adj v w ↔ G.adj v w ∧ ¬ ⟦(v, w)⟧ ∈ s := iff.rfl
+
+lemma sdiff_eq_delete_edges (G G' : simple_graph V) :
+  G \ G' = G.delete_edges G'.edge_set :=
+by { ext, simp }
+
+lemma compl_eq_delete_edges :
+  Gᶜ = (⊤ : simple_graph V).delete_edges G.edge_set :=
+by { ext, simp }
+
+@[simp] lemma delete_edges_delete_edges (s s' : set (sym2 V)) :
+  (G.delete_edges s).delete_edges s' = G.delete_edges (s ∪ s') :=
+by { ext, simp [and_assoc, not_or_distrib] }
+
+@[simp] lemma delete_edges_empty_eq : G.delete_edges ∅ = G :=
+by { ext, simp }
+
+@[simp] lemma delete_edges_univ_eq : G.delete_edges set.univ = ⊥ :=
+by { ext, simp }
+
+lemma delete_edges_le (s : set (sym2 V)) : G.delete_edges s ≤ G :=
+by { intro, simp { contextual := tt } }
+
+lemma delete_edges_le_of_le {s s' : set (sym2 V)} (h : s ⊆ s') :
+  G.delete_edges s' ≤ G.delete_edges s :=
+λ v w, begin
+  simp only [delete_edges_adj, and_imp, true_and] { contextual := tt },
+  exact λ ha hn hs, hn (h hs),
+end
+
+lemma delete_edges_eq_inter_edge_set (s : set (sym2 V)) :
+  G.delete_edges s = G.delete_edges (s ∩ G.edge_set) :=
+by { ext, simp [imp_false] { contextual := tt } }
+
 section finite_at
 
 /-!

src/combinatorics/simple_graph/subgraph.lean

@@ -279,7 +279,7 @@ rel.dom_mono h.2
 lemma _root_.simple_graph.to_subgraph.is_spanning (H : simple_graph V) (h : H ≤ G) :
   (H.to_subgraph h).is_spanning := set.mem_univ
 
-lemma spanning_coe.is_subgraph_of_is_subgraph {H H' : subgraph G} (h : H ≤ H') :
+lemma spanning_coe_le_of_le {H H' : subgraph G} (h : H ≤ H') :
   H.spanning_coe ≤ H'.spanning_coe := h.2
 
 /-- The top of the `subgraph G` lattice is equivalent to the graph itself. -/

src/data/sym/sym2.lean

@@ -304,6 +304,19 @@ instance from_rel.decidable_pred (sym : symmetric r) [h : decidable_rel r] :
   decidable_pred (∈ sym2.from_rel sym) :=
 λ z, quotient.rec_on_subsingleton z (λ x, h _ _)
 
+/-- The inverse to `sym2.from_rel`. Given a set on `sym2 α`, give a symmetric relation on `α`
+(see `sym2.to_rel_symmetric`). -/
+def to_rel (s : set (sym2 α)) (x y : α) : Prop := ⟦(x, y)⟧ ∈ s
+
+@[simp] lemma to_rel_prop (s : set (sym2 α)) (x y : α) : to_rel s x y ↔ ⟦(x, y)⟧ ∈ s := iff.rfl
+
+lemma to_rel_symmetric (s : set (sym2 α)) : symmetric (to_rel s) := λ x y, by simp [eq_swap]
+
+lemma to_rel_from_rel (sym : symmetric r) : to_rel (from_rel sym) = r := rfl
+
+lemma from_rel_to_rel (s : set (sym2 α)) : from_rel (to_rel_symmetric s) = s :=
+set.ext (λ z, sym2.ind (λ x y, iff.rfl) z)
+
 end relations
 
 section sym_equiv