feat(combinatorics/simple_graph): adding simple_graph.support and mem…

…_support / support_mono lemmas (#10176)




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/combinatorics/simple_graph/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark, Kyle Miller, Alena Gusakov, Hunter Monroe
 -/
 import data.fintype.basic
+import data.rel
 import data.set.finite
 import data.sym.sym2
 
@@ -228,6 +229,14 @@ end decidable
 
 end order
 
+/-- `G.support` is the set of vertices that form edges in `G`. -/
+def support : set V := rel.dom G.adj
+
+lemma mem_support {v : V} : v ∈ G.support ↔ ∃ w, G.adj v w := iff.rfl
+
+lemma support_mono {G G' : simple_graph V} (h : G ≤ G') : G.support ⊆ G'.support :=
+rel.dom_mono h
+
 /-- `G.neighbor_set v` is the set of vertices adjacent to `v` in `G`. -/
 def neighbor_set (v : V) : set V := set_of (G.adj v)
 

src/data/rel.lean

@@ -48,6 +48,9 @@ lemma inv_inv : inv (inv r) = r := by { ext x y, reflexivity }
 /-- Domain of a relation -/
 def dom := {x | ∃ y, r x y}
 
+lemma dom_mono {r s : rel α β} (h : r ≤ s) : dom r ⊆ dom s :=
+λ a ⟨b, hx⟩, ⟨b, h a b hx⟩
+
 /-- Codomain aka range of a relation -/
 def codom := {y | ∃ x, r x y}