adj_of_mem_edges

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.adj_of_mem_edges

English

If an edge s(x,y) is in the walk's edges, then x and y are adjacent.

Русский

Если ребро s(x,y) принадлежит ребрам обхода, то x смежен с y.

LaTeX

$$$\forall p:\\ G.Walk u v,\\ h:\\ Sym2 V,\\ s(x,y) \in p.\\edges \Rightarrow G.Adj x y$$$

Lean4

theorem adj_of_mem_edges {u v x y : V} (p : G.Walk u v) (h : s(x, y) ∈ p.edges) : G.Adj x y :=
  edges_subset_edgeSet p h

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

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

Разделы

Аффилиация

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