degree_le — Mathlib

English

For a subgraph G' of G, the degree at any vertex is not greater than the degree in G.

Русский

Степень вершины в подграфе не превосходит степени в исходном графе.

LaTeX

$$$\forall {G' : Subgraph G} (v : V) [Fintype (G'.neighborSet v)] [Fintype (G.neighborSet v)] : G'.degree v \le G.degree v$$$

Lean4

theorem degree_le (G' : Subgraph G) (v : V) [Fintype (G'.neighborSet v)] [Fintype (G.neighborSet v)] :
    G'.degree v ≤ G.degree v := by
  rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card (G'.neighborSet_subset v)

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