map_symm_apply

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Iso.map_symm_apply

English

The inverse of the mapped graph along f, evaluated at w ∈ W, is f^{-1}(w).

Русский

Обратная к графу, полученному из графа по f, на элементе w ∈ W даёт f^{-1}(w).

LaTeX

$$$$ (\\mathrm{SimpleGraph.Iso.map}\\, f\\, G)^{-1}(w) = f^{-1}(w) $$$$

Lean4

@[simp]
theorem map_symm_apply (f : V ≃ W) (G : SimpleGraph V) (w : W) : (SimpleGraph.Iso.map f G).symm w = f.symm w :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru