degree_le_card_edgeFinset — Mathlib

English

Let G be a finite simple graph and v a vertex. Then deg_G(v) ≤ |E(G)|, i.e., the degree of v is at most the number of edges.

Русский

Пусть G — конечный простой граф и вершина v. Тогда deg_G(v) ≤ |E(G)|, то есть степень вершины не превосходит число ребер графа.

LaTeX

$$$\deg_G(v) \le |E(G)|$$$

Lean4

/-- The degree of a vertex is at most the number of edges. -/
theorem degree_le_card_edgeFinset [Fintype G.edgeSet] : G.degree v ≤ #G.edgeFinset := by
  classical
  rw [← card_incidenceFinset_eq_degree]
  exact card_le_card (G.incidenceFinset_subset v)

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