degree_pos_iff_exists_adj

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

The degree of v is positive iff there exists a neighbor of v.

Русский

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

LaTeX

$$$ 0 < G.degree v \iff \exists w, G.Adj v w $$$

Lean4

theorem degree_pos_iff_exists_adj : 0 < G.degree v ↔ ∃ w, G.Adj v w := by
  simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]

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

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

Разделы

Аффилиация

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