isIndContained_iff_exists_iso_subgraph

English

A graph G is inducedly contained in H iff there exists an induced subgraph H' of H and an isomorphism G ≅ H'.coe.

Русский

Граф G индуцировано вложен в H тогда и только тогда, когда существует индуцированный подграф H' графа H и изоморфизм G ≅ H'.coe.

LaTeX

$$G \subseteq_{\mathrm{ind}} H \iff \exists H' : H.Subgraph, \; \exists e : G \cong_g H'.coe, \; H'.IsInduced$$

Lean4

theorem isIndContained_iff_exists_iso_subgraph : G ⊴ H ↔ ∃ (H' : H.Subgraph) (_e : G ≃g H'.coe), H'.IsInduced :=
  by
  constructor
  · rintro ⟨f⟩
    refine ⟨Subgraph.map f.toHom ⊤, f.toCopy.isoToSubgraph, ?_⟩
    simp [Subgraph.IsInduced, Relation.map_apply_apply, f.injective]
  · rintro ⟨H', e, hH'⟩
    exact e.isIndContained.trans hH'.isIndContained

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