isLoopAt_iff_inc_not_isNonloopAt

Mathlib.Combinatorics.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Graph.isLoopAt_iff_inc_not_isNonloopAt

← MathLib Explorer

English

A loop at x is equivalent to inc e x and not IsNonloopAt e x.

Русский

Петля в x эквивалентна Inc e x и не IsNonloopAt e x.

LaTeX

$$$G.IsLoopAt\\ e\\ x\\Leftrightarrow G.Inc e x \\land \\neg G.IsNonloopAt e x$$$

Lean4

theorem isLoopAt_iff_inc_not_isNonloopAt : G.IsLoopAt e x ↔ G.Inc e x ∧ ¬G.IsNonloopAt e x := by
  simp +contextual [isNonloopAt_iff_inc_not_isLoopAt, iff_def, IsLoopAt.inc]

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

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

Разделы

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

Аффилиация

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