not_isLoopAt

Mathlib.Combinatorics.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Graph.IsNonloopAt.not_isLoopAt

English

If e is nonloop at x, then e cannot be a loop at any vertex y.

Русский

Если e некольцевое по отношению к x, то e не может быть петлей ни при одной вершине y.

LaTeX

$$$\\forall y, \\neg G.IsLoopAt\\ e\\ y \\;\\text{(given } G.IsNonloopAt\\ e\\ x\\))$$$

Lean4

theorem not_isLoopAt (h : G.IsNonloopAt e x) (y : α) : ¬G.IsLoopAt e y := fun h' ↦ h'.not_isNonloopAt x h

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

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

Разделы

Аффилиация

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