coe_compl — Mathlib

English

The underlying set of the complement of a finite subgraph equals the complement subgraph in the ambient graph.

Русский

Множество, лежащее в комплементе конечного подграфа, совпадает с комплементом соответствующего подграфа в графе-окружении.

LaTeX

$$$↑(G'^{c}) = (G'^{c} : G.Subgraph)$$$

Lean4

@[simp, norm_cast]
theorem coe_compl (G' : G.Finsubgraph) : ↑(G'ᶜ) = (G'ᶜ : G.Subgraph) :=
  rfl

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