isIndContained — Mathlib

English

If G' is an induced subgraph of G, then G'.coe is an inducedly contained subgraph of G.

Русский

Если G' является индуцированным подграфом G, то G'.coe является индуцированно вложенным в G.

LaTeX

$$$\text{If } G' \text{ isInduced in } G, \; G'_{\mathrm{coe}} \subseteq_{\mathrm{ind}} G$$$

Lean4

protected theorem isIndContained {G' : G.Subgraph} (hG' : G'.IsInduced) : G'.coe ⊴ G :=
  ⟨{  toFun := (↑)
      inj' := Subtype.coe_injective
      map_rel_iff' := hG'.adj.symm }⟩

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