isIndContained'

Mathlib.Combinatorics.SimpleGraph.Copy

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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