degree_lt_card_verts — Mathlib

English

For every vertex v in G, the degree of v is strictly less than the number of vertices, i.e., deg_G(v) < |V|.

Русский

Для каждой вершины v графа G выполняется deg_G(v) < |V|, то есть степень вершины строго меньше числа вершин.

LaTeX

$$$\\forall v,\\ deg_G(v) < \\lvert V \\rvert$$$

Lean4

theorem degree_lt_card_verts [DecidableRel G.Adj] (v : V) : G.degree v < Fintype.card V := by
  classical
  apply Finset.card_lt_card
  rw [Finset.ssubset_iff]
  exact ⟨v, by simp, Finset.subset_univ _⟩

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