compl_isIndContained_compl — Mathlib

English

Induced containment is preserved under graph complementation: Gᶜ is inducingly contained in Hᶜ iff G is inducingly contained in H.

Русский

Индуцированное вложение сохраняется при взятии дополнения графа: Gᶜ ⊴ Hᶜ тогда и только тогда, когда G ⊴ H.

LaTeX

$$$G^{\!c} \subseteq_{\mathrm{ind}} H^{\!c} \iff G \subseteq_{\mathrm{ind}} H$$$

Lean4

@[simp]
theorem compl_isIndContained_compl : Gᶜ ⊴ Hᶜ ↔ G ⊴ H :=
  Embedding.complEquiv.symm.nonempty_congr

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