minDegree_le_minDegree — Mathlib

English

If G ≤ H, then G.minDegree ≤ H.minDegree.

Русский

Если G ≤ H, то G.minDegree ≤ H.minDegree.

LaTeX

$$G.minDegree ≤ H.minDegree$$

Lean4

/-- If `G` is a subgraph of `H` then `G.minDegree ≤ H.minDegree`. -/
theorem minDegree_le_minDegree {H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (hle : G ≤ H) :
    G.minDegree ≤ H.minDegree := by
  by_cases hne : Nonempty V
  · apply le_minDegree_of_forall_le_degree
    exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)
  · push_neg at hne
    simp

Похожие утверждения