map_subgraphOfAdj — Mathlib

English

Under a graph homomorphism f, the image of the subgraphOfAdj hvw equals the subgraphOfAdj of the mapped adjacency.

Русский

При гомоморфизме f образ подграфа G.subgraphOfAdj hvw равен подграфу G'.subgraphOfAdj (f.map_adj hvw).

LaTeX

$$$\\mathrm{Subgraph.map}\,f\\left(G.\\mathrm{subgraphOfAdj}(hvw)\\right) = G'.\\mathrm{subgraphOfAdj}(f.map\\_adj(hvw))$$$

Lean4

@[simp]
theorem map_subgraphOfAdj (f : G →g G') {v w : V} (hvw : G.Adj v w) :
    Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj (f.map_adj hvw) :=
  by
  ext
  · grind [Subgraph.map_verts, subgraphOfAdj_verts]
  · grind [Relation.Map, Subgraph.map_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff]

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