isMatching_map — Mathlib

English

For any graph isomorphism f: G ≃g G', the mapped subgraph M.map f is a matching iff M is a matching.

Русский

Для любого изоморфизма графов f: G ≃g G' отображение M.map f является соответствием тогда и только тогда, когда M — соответствие.

LaTeX

$$$$ (M.map f.toHom).IsMatching \\iff M.IsMatching $$$$

Lean4

@[simp]
theorem isMatching_map {G' : SimpleGraph W} {M : Subgraph G} (f : G ≃g G') : (M.map f.toHom).IsMatching ↔ M.IsMatching
    where
  mp h := by simpa [← map_comp] using h.map f.symm.toHom f.symm.injective
  mpr := .map f.toHom f.injective

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