loopSet

Mathlib.Combinatorics.Graph.Basic

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

English

Definition: loopSet x is the set of edges e such that G.IsLoopAt e x.

Русский

Определение: loopSet x — множество ребер e, для которых G.IsLoopAt e x.

LaTeX

$$$\\text{loopSet}(x) = \\{e\\mid G.IsLoopAt e x\\}$$$

Lean4

/-- `G.loopSet x` is the set of loops at `x` in `G`. -/
def loopSet (x : α) : Set β :=
  {e | G.IsLoopAt e x}

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

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

Разделы

Аффилиация

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