degree_eq_zero_iff_notMem_support

English

The degree is zero iff the vertex does not belong to the graph's support.

Русский

Степень вершины равна нулю тогда и только тогда, когда вершина не принадлежит поддержке графа.

LaTeX

$$$ G.degree v = 0 \iff v \notin G.support $$$

Lean4

theorem degree_eq_zero_iff_notMem_support : G.degree v = 0 ↔ v ∉ G.support := by
  rw [← G.degree_pos_iff_mem_support v, Nat.pos_iff_ne_zero, not_ne_iff]

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