dart_fst_fiber_card_eq_degree

Mathlib.Combinatorics.SimpleGraph.DegreeSum

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

← MathLib Explorer

English

The number of darts with fst = v equals the degree of v.

Русский

Число стрел с fst = v равно степени вершины v.

LaTeX

$$$ #{d : G.Dart | d.fst = v} = G.degree v $$$

Lean4

theorem dart_fst_fiber_card_eq_degree [DecidableEq V] (v : V) : #{d : G.Dart | d.fst = v} = G.degree v := by
  simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
    card_image_of_injective univ (G.dartOfNeighborSet_injective v)

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

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

Разделы

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

Аффилиация

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