loopless

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

Every subgraph of a simple graph is loopless; no vertex has a loop in any subgraph.

Русский

Каждый подграф простого графа не имеет петель; в любом подграфе петля отсутствует.

LaTeX

$$For every subgraph $H$ of a simple graph $G$, $\forall v, \neg H.Adj\,v\,v$.$$

Lean4

protected theorem loopless (G' : Subgraph G) : Irreflexive G'.Adj := fun v h ↦ G.loopless v (G'.adj_sub h)

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

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

Разделы

Аффилиация

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