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