notMem_edges_of_loop — Mathlib

English

A path p from v to v has no edges in its corresponding walk; i.e., no edge e lies in p.edges.

Русский

Путь p от вершины v к самой вершине v не содержит ребер в соответствующем обходе; то есть ни одно ребро e не принадлежит p.edges.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v}, e \notin (p : G.Walk v v).edges$$$

Lean4

theorem notMem_edges_of_loop {v : V} {e : Sym2 V} {p : G.Path v v} : e ∉ (p : G.Walk v v).edges := by simp [p.loop_eq]

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