edist_ne_top_iff_reachable

Mathlib.Combinatorics.SimpleGraph.Metric

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

← MathLib Explorer

English

edist u v ≠ ⊤ iff G.Reachable u v.

Русский

edist u v ≠ ⊤ тогда и только тогда, когда G.Reachable u v.

LaTeX

$$$ G.edist u v \neq \top \iff G.Reachable u v $$$

Lean4

theorem edist_ne_top_iff_reachable : G.edist u v ≠ ⊤ ↔ G.Reachable u v :=
  by
  refine ⟨reachable_of_edist_ne_top, fun h ↦ ?_⟩
  by_contra hx
  simp only [edist, iInf_eq_top, ENat.coe_ne_top] at hx
  exact h.elim hx

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

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

Разделы

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

Аффилиация

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