snd_mem_support_of_mem_edges

Mathlib.Combinatorics.SimpleGraph.Walk

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

← MathLib Explorer

English

If an edge s(t,u) lies in p.edges, then u belongs to p.support.

Русский

Если ребро s(t,u) лежит в p.edges, то u принадлежит p.support.

LaTeX

$$$ s(t,u) \in p.edges \Rightarrow u \in p.support $$$

Lean4

theorem snd_mem_support_of_mem_edges {t u v w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) : u ∈ p.support :=
  by
  rw [Sym2.eq_swap] at he
  exact p.fst_mem_support_of_mem_edges he

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

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

Разделы

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

Аффилиация

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