refl

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Reachable.refl

English

Every vertex is reachable from itself via the empty walk.

Русский

Каждая вершина достижима из самой себя через пустой ход.

LaTeX

$$$\forall u,\ G.Reachable u u.$$$

Lean4

@[refl]
protected theorem refl (u : V) : G.Reachable u u :=
  ⟨Walk.nil⟩

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

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

Разделы

Аффилиация

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