map_singletonSubgraph — Mathlib

English

Let f: G →g G' be a graph homomorphism. Then the image under Subgraph.map of the singleton subgraph at vertex v equals the singleton subgraph at f(v).

Русский

Пусть f: G →g G' — гомоморфизм графов. Тогда образ подграфа-одиночки в вершине v равен одиночному подграфу в f(v).

LaTeX

$$$\\mathrm{Subgraph.map}(f, G.\\mathrm{singletonSubgraph}(v)) = G'.\\mathrm{singletonSubgraph}(f(v))$$$

Lean4

@[simp]
theorem map_singletonSubgraph (f : G →g G') {v : V} :
    Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v) :=
  by
  ext <;>
    simp only [Relation.Map, Subgraph.map_adj, singletonSubgraph_adj, Pi.bot_apply, exists_and_left,
      and_iff_left_iff_imp, Subgraph.map_verts, singletonSubgraph_verts, Set.image_singleton]
  exact False.elim

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