of_isEmpty

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsIndContained.of_isEmpty

English

If the vertex type is empty, then any G is inducedly contained in any H.

Русский

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

LaTeX

$$$[IsEmpty V] \Rightarrow G \subseteq_{\mathrm{ind}} H$$$

Lean4

theorem of_isEmpty [IsEmpty V] : G ⊴ H :=
  ⟨{  toFun := isEmptyElim
      inj' := isEmptyElim
      map_rel_iff' := fun {a} ↦ isEmptyElim a }⟩

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

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

Разделы

Аффилиация

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