toDeleteEdges — Mathlib

English

Given a walk p, and a set of edges s that p avoids, toDeleteEdges produces a walk in the graph with edges s removed that corresponds to p.

Русский

Дано обход p и множество ребер s, которых p избегает; toDeleteEdges дает обход в графе без ребер s, соответствующий p.

LaTeX

$$toDeleteEdges (s) {v w} (p : G.Walk v w) (hp : ∀ e, e ∈ p.edges → e ∉ s) : (G.deleteEdges s).Walk v w$$

Lean4

/-- Given a walk that avoids a set of edges, produce a walk in the graph
with those edges deleted. -/
abbrev toDeleteEdges (s : Set (Sym2 V)) {v w : V} (p : G.Walk v w) (hp : ∀ e, e ∈ p.edges → e ∉ s) :
    (G.deleteEdges s).Walk v w :=
  p.transfer _ <| by
    simp only [edgeSet_deleteEdges, Set.mem_diff]
    exact fun e ep => ⟨edges_subset_edgeSet p ep, hp e ep⟩

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