adj_toSubgraph_mapLe — Mathlib

English

If G is contained in G' (G ≤ G'), then for any walk p in G, adjacency at any vertices is preserved when passing to the mapped subgraph: an edge in p.toSubgraph corresponds to an edge in (p.mapLe h).toSubgraph and vice versa.

Русский

Если граф G является подграфом G' (G ≤ G'), то для любого обхода p в G смежности в его подграфе сохраняются при отображении в подграф p.mapLe h

LaTeX

$$$ (p.mapLe h).toSubgraph.Adj w x \iff p.toSubgraph.Adj w x $$$

Lean4

theorem adj_toSubgraph_mapLe {G' : SimpleGraph V} {w x : V} {p : G.Walk u v} (h : G ≤ G') :
    (p.mapLe h).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x := by simp

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