edist_eq_top_of_not_reachable

Mathlib.Combinatorics.SimpleGraph.Metric

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

English

If u and v are not reachable, then edist u v = ⊤.

Русский

Если вершины u и v не достижимы, то edist u v = ⊤.

LaTeX

$$$ \neg G.Reachable u v \Rightarrow G.edist u v = \top $$$

Lean4

theorem edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) : G.edist u v = ⊤ := by
  simp [edist, not_reachable_iff_isEmpty_walk.mp h]

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

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

Разделы

Аффилиация

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