weight_nil

Mathlib.Combinatorics.Quiver.Path.Weight

URI: https://scilib.ai/kg/mathlib#Quiver.Path.weight_nil

← MathLib Explorer

English

The weight of the nil path is 1 for any edge-weighting function w.

Русский

Вес нулевого пути равен 1 при любом задании весов на ребрах.

LaTeX

$$$\mathrm{weight} w (\mathrm{Path.nil}) = 1$$$

Lean4

@[to_additive (attr := simp) addWeight_nil]
theorem weight_nil (w : ∀ {i j : V}, (i ⟶ j) → R) (a : V) : weight w (Path.nil : Path a a) = 1 := by simp [weight]

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

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

Разделы

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

Аффилиация

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