edist_anti — Mathlib

English

Supergraphs have not greater extended distances than subgraphs: adding edges cannot increase the edist to a given pair of vertices.

Русский

Суперграфы имеют не большие расстояния, чем их подграфы: добавление ребер не увеличивает edist между парами вершин.

LaTeX

$$$ G \le G' \Rightarrow G'.edist u v \le G.edist u v $$$

Lean4

/-- Supergraphs have smaller or equal extended distances to their subgraphs. -/
@[gcongr]
theorem edist_anti {G' : SimpleGraph V} (h : G ≤ G') : G'.edist u v ≤ G.edist u v :=
  by
  by_cases hr : G.Reachable u v
  · obtain ⟨_, hw⟩ := hr.exists_walk_length_eq_edist
    rw [← hw, ← Walk.length_map (.ofLE h)]
    apply edist_le
  · exact edist_eq_top_of_not_reachable hr ▸ le_top

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