complEquiv — Mathlib

English

Graph embeddings from G to H correspond exactly to graph embeddings from the complements G^c to H^c.

Русский

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

LaTeX

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

Lean4

/-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`. -/
def complEquiv : G ↪g H ≃ Gᶜ ↪g Hᶜ where
  toFun f := ⟨f.toEmbedding, by simp⟩
  invFun
    f :=
    ⟨f.toEmbedding, fun {v w} ↦ by
      obtain rfl | hvw := eq_or_ne v w
      · simp
      · simpa [hvw, not_iff_not] using f.map_adj_iff (v := v) (w := w)⟩

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