feat(Combinatorics/SimpleGraph/Finite): some minDegree/maxDegree lemmas (leanprover-community#40622)

- `G.minDegree = 0 ∧ G.maxDegree = 0` given `Subsingleton V` (we have these for `IsEmpty V`)
- `G.maxDegree = 0 ↔ G = ⊥`
- `G.minDegree = 0 ↔ ∃ v, G.IsIsolated v`
- `G.minDegree = 0 ↔ G.support ≠ .univ`
- For a set `s` that contains the support we have
  - `G.minDegree ≤ (G.induce s).minDegree`
  - `(G.induce s).maxDegree = G.maxDegree`

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -341,7 +341,8 @@ lemma maxDegree_mono {H : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] [Decid
 theorem Copy.minDegree_mono [Fintype V] [Fintype W] [DecidableRel G.Adj] [DecidableRel H.Adj]
     {f : Copy G H} (hf : Function.Surjective f) : G.minDegree ≤ H.minDegree := by
   cases isEmpty_or_nonempty W
-  · simp [Function.isEmpty f]
+  · have := Function.isEmpty f
+    simp
   refine H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_
   obtain ⟨v, rfl⟩ := hf w
   grw [← f.degree_le, ← minDegree_le_degree]
@@ -354,6 +355,15 @@ theorem Hom.minDegree_mono [Fintype V] [Fintype W] [DecidableRel G.Adj] [Decidab
 
 @[deprecated (since := "2026-05-20")] alias Hom.minDegree_le := Hom.minDegree_mono
 
+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.maxDegree_mono <| 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/Finite.lean

@@ -385,10 +385,8 @@ theorem exists_minimal_degree_vertex [DecidableRel G.Adj] [Nonempty V] :
   grind [minDegree, WithTop.untopD_coe, min_mem_image_coe <| univ_nonempty.image (G.degree ·)]
 
 /-- The minimum degree in the graph is at most the degree of any particular vertex. -/
-theorem minDegree_le_degree [DecidableRel G.Adj] (v : V) : G.minDegree ≤ G.degree v := by
-  obtain ⟨t, ht⟩ := Finset.min_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))
-  have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht
-  rwa [minDegree, ht]
+theorem minDegree_le_degree [DecidableRel G.Adj] (v : V) : G.minDegree ≤ G.degree v :=
+  WithTop.untopD_le <| Finset.min_le <| mem_image_of_mem (G.degree ·) <| mem_univ v
 
 /-- In a nonempty graph, if `k` is at most the degree of every vertex, it is at most the minimum
 degree. Note the assumption that the graph is nonempty is necessary as long as `G.minDegree` is
@@ -399,14 +397,16 @@ theorem le_minDegree_of_forall_le_degree [DecidableRel G.Adj] [Nonempty V] (k :
   rw [hv]
   apply h
 
-/-- If there are no vertices then the `minDegree` is zero. -/
 @[simp]
-lemma minDegree_of_isEmpty [DecidableRel G.Adj] [IsEmpty V] : G.minDegree = 0 := by
-  rw [minDegree, WithTop.untopD_eq_self_iff]
-  simp
+lemma minDegree_of_subsingleton [DecidableRel G.Adj] [Subsingleton V] : G.minDegree = 0 := by
+  cases isEmpty_or_nonempty V <;>
+    simp [minDegree, Finset.image_const]
+
+@[deprecated (since := "2026-06-15")] alias minDegree_of_isEmpty := minDegree_of_subsingleton
 
 variable {G} in
 /-- If `G` is a subgraph of `H` then `G.minDegree ≤ H.minDegree`. -/
+@[gcongr]
 lemma minDegree_le_minDegree {H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj]
     (hle : G ≤ H) : G.minDegree ≤ H.minDegree := by
   cases isEmpty_or_nonempty V
@@ -438,8 +438,11 @@ theorem degree_le_maxDegree [DecidableRel G.Adj] (v : V) : G.degree v ≤ G.maxD
   WithBot.le_unbotD <| Finset.le_max <| mem_image_of_mem (G.degree ·) <| mem_univ v
 
 @[simp]
-lemma maxDegree_of_isEmpty [DecidableRel G.Adj] [IsEmpty V] : G.maxDegree = 0 := by
-  rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]
+lemma maxDegree_of_subsingleton [DecidableRel G.Adj] [Subsingleton V] : G.maxDegree = 0 := by
+  cases isEmpty_or_nonempty V <;>
+    simp [maxDegree, Finset.image_const]
+
+@[deprecated (since := "2026-06-15")] alias maxDegree_of_isEmpty := maxDegree_of_subsingleton
 
 /-- In a graph, if `k` is at least the degree of every vertex, then it is at least the maximum
 degree. -/
@@ -458,6 +461,16 @@ theorem IsRegularOfDegree.maxDegree_eq [Nonempty V] [DecidableRel G.Adj] {d : 
 lemma maxDegree_bot_eq_zero : (⊥ : SimpleGraph V).maxDegree = 0 :=
   Nat.le_zero.1 <| maxDegree_le_of_forall_degree_le _ _ (by simp)
 
+variable {G} in
+@[simp]
+theorem maxDegree_eq_zero_iff [DecidableRel G.Adj] : G.maxDegree = 0 ↔ G = ⊥ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [eq_bot_iff_isIsolated]
+    intro v
+    grind [degree_eq_zero, G.degree_le_maxDegree v]
+  · convert maxDegree_bot_eq_zero
+    assumption
+
 @[simp]
 lemma maxDegree_top [DecidableEq V] : (⊤ : SimpleGraph V).maxDegree = Fintype.card V - 1 := by
   cases isEmpty_or_nonempty V
@@ -478,6 +491,18 @@ theorem IsRegularOfDegree.minDegree_eq [Nonempty V] [DecidableRel G.Adj] {d : 
 lemma minDegree_bot_eq_zero : (⊥ : SimpleGraph V).minDegree = 0 :=
   Nat.le_zero.1 <| (minDegree_le_maxDegree _).trans (by simp)
 
+variable {G} in
+theorem minDegree_eq_zero_iff [DecidableRel G.Adj] [Nonempty V] :
+    G.minDegree = 0 ↔ ∃ v, G.IsIsolated v := by
+  refine ⟨fun h ↦ ?_, fun ⟨v, hv⟩ ↦ ?_⟩
+  · grind [G.exists_minimal_degree_vertex, degree_eq_zero]
+  · grind [G.minDegree_le_degree v, degree_eq_zero]
+
+variable {G} in
+theorem minDegree_eq_zero_iff_support_ne [DecidableRel G.Adj] [Nonempty V] :
+    G.minDegree = 0 ↔ G.support ≠ .univ := by
+  simp [Set.ne_univ_iff_exists_notMem, minDegree_eq_zero_iff]
+
 @[simp]
 lemma minDegree_top [DecidableEq V] : (⊤ : SimpleGraph V).minDegree = Fintype.card V - 1 := by
   cases isEmpty_or_nonempty V
@@ -613,6 +638,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