mono

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Preconnected.mono

English

If u is reachable from v, there exists a path from u to v.

Русский

Если из v можно дойти до u, существует путь от u до v.

LaTeX

$$$\forall {u v} (hr : G.Reachable u v), \exists p: G.Walk u v, p.IsPath.$$$

Lean4

@[mono]
protected theorem mono {G G' : SimpleGraph V} (h : G ≤ G') (hG : G.Preconnected) : G'.Preconnected := fun u v =>
  (hG u v).mono h

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

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

Разделы

Аффилиация

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