English
Let f be a bijection between the vertex sets V and W and let G be a simple graph on W. Then the inverse side of the isomorphism obtained by pulling back G along f coincides with the inverse map f^{-1} evaluated at w. In other words, for every w in W, the inverse isomorphism sends w to f^{-1}(w).
Русский
Пусть f — биекция между множествами вершин V и W, и G — граф на W. Тогда обратная часть изоморфизма, полученного переносом графа G по f, отобразит элемент w ∈ W в f^{-1}(w). То есть для каждого w выполнено (SimpleGraph.Iso.comap f G).symm(w) = f^{-1}(w).
LaTeX
$$$$(\\mathrm{SimpleGraph.Iso.comap}\\, f\, G)^{-1}(w) = f^{-1}(w)$$$$
Lean4
@[simp]
theorem comap_symm_apply (f : V ≃ W) (G : SimpleGraph W) (w : W) : (SimpleGraph.Iso.comap f G).symm w = f.symm w :=
rfl
