degree_le_of_le — Mathlib

English

If G is a subgraph of H, then for every vertex v, deg_G(v) ≤ deg_H(v).

Русский

Если G является подграфом H, то для любой вершины v deg_G(v) ≤ deg_H(v).

LaTeX

$$$G \le H \Rightarrow \deg_G(v) \le \deg_H(v)$$$

Lean4

/-- If `G ≤ H` then `G.degree v ≤ H.degree v` for any vertex `v`. -/
theorem degree_le_of_le {H : SimpleGraph V} [Fintype (H.neighborSet v)] (hle : G ≤ H) : G.degree v ≤ H.degree v :=
  by
  simp_rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card fun v hv => hle hv

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