Commit 2026-06-23 12:20 eac05c61

feat(Combinatorics/SimpleGraph/Finite): some minDegree/maxDegree lemmas (#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