of_isEmpty

Mathlib.Combinatorics.SimpleGraph.Copy

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

← MathLib Explorer

English

A graph having no vertices is contained in any graph.

Русский

Граф без вершин содержится в любом графе.

LaTeX

$$A ⊑ B (when IsEmpty α)$$

Lean4

/-- A simple graph having no vertices is contained in any simple graph. -/
theorem of_isEmpty [IsEmpty α] : A ⊑ B :=
  ⟨⟨isEmptyElim, fun {a} ↦ isEmptyElim a⟩, isEmptyElim⟩

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

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

Разделы

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

Аффилиация

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