mem_incidenceSet

Mathlib.Combinatorics.Graph.Basic

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

English

For any vertex x and edge e, e ∈ incidenceSet(x) if and only if G.Inc e x.

Русский

Для любого x и e выполняется e ∈ incidenceSet(x) тогда и только тогда, когда G.Inc e x.

LaTeX

$$$e\\in G.incidenceSet(x)\\iff G.Inc e x$$$

Lean4

@[simp]
theorem mem_incidenceSet (x : α) (e : β) : e ∈ G.incidenceSet x ↔ G.Inc e x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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