top

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.IsInduced.top

English

The top subgraph is an induced subgraph of G.

Русский

Верхний подграф является индуцированным подграфом графа G.

LaTeX

$$$ \\mathrm{IsInduced}(\\top_G) $$$

Lean4

@[simp]
theorem top : (⊤ : G.Subgraph).IsInduced := fun _ _ _ _ ↦ id

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

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

Разделы

Аффилиация

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