degree_pos_iff_mem_support

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.degree_pos_iff_mem_support

English

The degree is positive iff the vertex belongs to the support of the graph.

Русский

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

LaTeX

$$$ 0 < G.degree v \iff v \in G.support $$$

Lean4

theorem degree_pos_iff_mem_support : 0 < G.degree v ↔ v ∈ G.support := by
  rw [G.degree_pos_iff_exists_adj v, mem_support]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru