comap — Mathlib

English

Given a bijection f : V ≃ W and a graph G on W, the comapped graph SimpleGraph.Iso.comap f G is isomorphic to G.

Русский

Для биекции f : V ≃ W и графа G на W граф-комапация Graph имеет изоморфизм с G.

LaTeX

$$$ G^{\mathrm{comap}} f \simeq_g G $$$

Lean4

/-- Given a bijection, there is an embedding from the comapped graph into the original
graph. -/
-- Porting note: `@[simps]` does not work here anymore since `f` is not a constructor application.
-- `@[simps toEmbedding]` could work, but Floris suggested writing `comap_apply` for now.

protected def comap (f : V ≃ W) (G : SimpleGraph W) : G.comap f.toEmbedding ≃g G :=
  { f with map_rel_iff' := by simp }

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