isIndContained

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Iso.isIndContained

English

If G is isomorphic to H, then G is inducingly contained in H.

Русский

Если графы G и H изоморфны, то G индуцированно вложен в H.

LaTeX

$$$G \cong H \Rightarrow G \subseteq_{\mathrm{ind}} H$$$

Lean4

/-- If `G` is isomorphic to `H`, then `G` is inducingly contained in `H`. -/
protected theorem isIndContained (e : G ≃g H) : G ⊴ H :=
  ⟨e⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru