symm_toHom_comp_toHom — Mathlib

English

Graph embeddings from G to H correspond to graph embeddings from the complement graphs G^c to H^c.

Русский

Встраивания графов от G к H эквивалентны вложениям графов-полнений графов G^c к H^c.

LaTeX

$$$ (G \hookrightarrow H) \simeq (G^{c} \hookrightarrow H^{c}) $$$

Lean4

@[simp]
theorem symm_toHom_comp_toHom : f.symm.toHom.comp f.toHom = Hom.id :=
  by
  ext v
  simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding, RelIso.symm_apply_apply,
    RelHom.id_apply]

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