dist_anti — Mathlib

English

If G is contained in a supergraph G′ and u,v are G-reachable, then the distance in G′ is at most the distance in G.

Русский

Если G содержится в суперграфе G′ и вершины u, v достижимы в G, то расстояние в G′ не превосходит расстояния в G.

LaTeX

$$$ G \le G' \land G.\mathrm{Reachable}(u,v) \Rightarrow \operatorname{dist}_{G'}(u,v) \le \operatorname{dist}_{G}(u,v) $$$

Lean4

/-- Supergraphs have smaller or equal distances to their subgraphs. -/
@[gcongr]
protected theorem dist_anti {G' : SimpleGraph V} (h : G ≤ G') (hr : G.Reachable u v) : G'.dist u v ≤ G.dist u v :=
  by
  obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_dist
  rw [← hw, ← Walk.length_map (.ofLE h)]
  apply dist_le

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