toSubgraph_map — Mathlib

English

If p is a walk and f is a graph homomorphism between G and G', then the subgraph of the mapped walk equals the mapped subgraph of the original walk.

Русский

Если p — обход, а f — гомоморфизм графов G → G', тогда подграф обхода после отображения совпадает с отображённым подграфом исходного обхода.

LaTeX

$$$ (p.map f).toSubgraph = p.toSubgraph.map f $$$

Lean4

@[simp]
theorem toSubgraph_map (f : G →g G') (p : G.Walk u v) : (p.map f).toSubgraph = p.toSubgraph.map f := by
  induction p <;> simp [*, Subgraph.map_sup]

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