degrees of G.induce s

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -345,6 +345,15 @@ theorem Hom.minDegree_le [Fintype V] [Fintype W] [DecidableRel G.Adj] [Decidable
     {f : G →g H} (hf : Function.Bijective f) : G.minDegree ≤ H.minDegree :=
   Copy.minDegree_le (f := ⟨f, hf.injective⟩) hf.surjective
 
+theorem maxDegree_induce_of_support_subset [Fintype V] [DecidableRel G.Adj] {s : Set V}
+    [DecidablePred (· ∈ s)] (h : G.support ⊆ s) : (G.induce s).maxDegree = G.maxDegree := by
+  apply le_antisymm <| Copy.max_degree_le <| Embedding.induce s |>.toCopy
+  refine G.maxDegree_le_of_forall_degree_le _ fun v ↦ ?_
+  by_cases hv : G.IsIsolated v
+  · simp [hv]
+  grw [← degree_le_maxDegree _ ⟨v, h <| G.mem_support_iff_not_isIsolated.mpr hv⟩,
+    degree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h]
+
 end IsContained
 
 section Free

Mathlib/Combinatorics/SimpleGraph/Degree.lean

@@ -180,17 +180,19 @@ theorem edegree_le_maxEDegree : G.edegree v ≤ G.maxEDegree :=
 theorem minEDegree_le_edegree : G.minEDegree ≤ G.edegree v :=
   iInf_le G.edegree v
 
-variable {v} in
+variable {G v} in
 theorem maxEDegree_eq_top_of_edegree_eq_top (h : G.edegree v = ⊤) : G.maxEDegree = ⊤ :=
   eq_top_iff.mpr <| G.edegree_le_maxEDegree v |>.trans_eq' h
 
-variable {v} in
+variable {G v} in
 theorem minEDegree_eq_zero_of_edegree_eq_zero (h : G.edegree v = 0) : G.minEDegree = 0 :=
   nonpos_iff_eq_zero.mp <| G.minEDegree_le_edegree v |>.trans_eq h
 
+variable {G} in
 theorem maxEDegree_le_of_forall_edegree_le {n : ℕ∞} (h : ∀ v, G.edegree v ≤ n) : G.maxEDegree ≤ n :=
   iSup_le h
 
+variable {G} in
 theorem le_minEDegree_of_forall_le_edegree {n : ℕ∞} (h : ∀ v, n ≤ G.edegree v) : n ≤ G.minEDegree :=
   le_iInf h
 
@@ -323,7 +325,7 @@ theorem minEDegree_le_encard_edgeSet [Nonempty V] (G : SimpleGraph V) :
   exact hv ▸ G.edegree_le_encard_edgeSet v
 
 theorem maxEDegree_le_encard_edgeSet : G.maxEDegree ≤ G.edgeSet.encard :=
-  maxEDegree_le_of_forall_edegree_le _ G.edegree_le_encard_edgeSet
+  maxEDegree_le_of_forall_edegree_le G.edegree_le_encard_edgeSet
 
 theorem minEDegree_le_maxEDegree [Nonempty V] (G : SimpleGraph V) :
     G.minEDegree ≤ G.maxEDegree := by
@@ -358,4 +360,33 @@ theorem IsRegularOfDegree.minEDegree_eq [Nonempty V] [G.LocallyFinite] {d : ℕ}
     (h : G.IsRegularOfDegree d) : G.minEDegree = d := by
   simp [minEDegree_eq_iInf, h.edegree_eq]
 
+section Induce
+
+variable {s : Set V}
+
+variable {G} in
+theorem edegree_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
+    (G.induce s).edegree v = G.edegree v := by
+  rw [← encard_neighborSet, ← encard_neighborSet, neighborSet_induce,
+    Set.encard_preimage_of_injective_subset_range Subtype.val_injective <| by simpa]
+
+variable {G} in
+theorem maxEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    (G.induce s).maxEDegree = G.maxEDegree := by
+  apply le_antisymm <| Embedding.induce s |>.isContained.maxEDegree_le
+  refine G.maxEDegree_le_of_forall_edegree_le fun v ↦ ?_
+  by_cases hv : G.IsIsolated v
+  · simp [hv]
+  grw [← edegree_le_maxEDegree _ ⟨v, h <| G.mem_support_iff_not_isIsolated.mpr hv⟩,
+    edegree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h]
+
+variable {G} in
+theorem le_minEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    G.minEDegree ≤ (G.induce s).minEDegree := by
+  refine le_minEDegree_of_forall_le_edegree fun v ↦ ?_
+  grw [G.minEDegree_le_edegree v, edegree_induce_of_neighborSet_subset]
+  grw [neighborSet_subset_support, h]
+
+end Induce
+
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -652,6 +652,17 @@ theorem degree_induce_support (v : G.support) :
     (G.induce G.support).degree v = G.degree v :=
   degree_induce_of_support_subset subset_rfl v
 
+theorem le_minDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    G.minDegree ≤ (G.induce s).minDegree := by
+  cases isEmpty_or_nonempty V
+  · simp
+  rcases s.eq_empty_or_nonempty with (rfl | hs)
+  · simp [minDegree_eq_zero_iff_support_ne, Set.subset_empty_iff.mp h, Set.empty_ne_univ]
+  have := hs.to_subtype
+  refine le_minDegree_of_forall_le_degree _ _ fun v ↦ ?_
+  grw [G.minDegree_le_degree v, degree_induce_of_neighborSet_subset]
+  grw [neighborSet_subset_support, h]
+
 end Support
 
 section Map