bot_degree

Mathlib.Combinatorics.SimpleGraph.Finite

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

← MathLib Explorer

English

The bottom graph has no edges, hence every vertex has degree 0.

Русский

Нижний граф не имеет ребер, следовательно, каждая вершина имеет степень 0.

LaTeX

$$∀ v, deg_⊥(v) = 0$$

Lean4

@[simp]
theorem bot_degree (v : V) : (⊥ : SimpleGraph V).degree v = 0 :=
  by
  simp_rw [degree, neighborFinset_eq_filter, bot_adj, filter_false]
  exact Finset.card_empty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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