edgeSet_nil

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.edgeSet_nil

English

The edgeSet of the nil walk from u to u is empty.

Русский

EdgeSet нулевого хода от u к u пуст.

LaTeX

$$$ (\text{nil} : G.Walk\,u\,u).edgeSet = \emptyset $$$

Lean4

@[simp]
theorem edgeSet_nil (u : V) : (nil : G.Walk u u).edgeSet = ∅ := by ext; simp

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

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

Разделы

Аффилиация

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