feat(Combinatorics/SimpleGraph): edges of an induced subgraph as a filter (#42135)

Add two lemmas describing the edges of a finite simple graph `G` whose vertices all lie in a finset `s`.

Author: mitchell-horner

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -715,6 +715,20 @@ theorem le_minDegree_induce_of_support_subset (h : G.support ⊆ s) :
   grw [G.minDegree_le_degree v, degree_induce_of_neighborSet_subset]
   grw [neighborSet_subset_support, h]
 
+theorem filter_edgeFinset_toFinset_subset [DecidableEq V] (s : Finset V) :
+    {e ∈ G.edgeFinset | e.toFinset ⊆ s} = G.edgeFinset ∩ s.sym2 := by
+  simp [subset_iff, ← mem_sym2_iff, filter_mem_eq_inter]
+
+/-- The edges whose vertices lie in `s` are in bijection with the edges of the induced
+subgraph `G.induce s`. -/
+theorem card_filter_edgeFinset_toFinset_subset [DecidableEq V] (s : Finset V) :
+    #{e ∈ G.edgeFinset | e.toFinset ⊆ s} = #(G.induce ↑s).edgeFinset := by
+  have h := congrArg Finset.card (map_edgeFinset_induce (s := (↑s : Set V)) (G := G))
+  rw [card_map, toFinset_coe] at h
+  rw [filter_edgeFinset_toFinset_subset]
+  convert h.symm using 1
+  congr!
+
 end Support
 
 section Map