map_toDeleteEdges_eq — Mathlib

English

Mapping via an LE-compatible map after toDeleteEdges recovers the original walk.

Русский

Отображение через совместимое LE отображение после toDeleteEdges восстанавливает исходный обход.

LaTeX

$$Walk.map (.ofLE (G.deleteEdges_le s)) (p.toDeleteEdges s hp) = p$$

Lean4

@[simp]
theorem map_toDeleteEdges_eq (s : Set (Sym2 V)) {p : G.Walk v w} (hp) :
    Walk.map (.ofLE (G.deleteEdges_le s)) (p.toDeleteEdges s hp) = p :=
  by
  rw [← transfer_eq_map_ofLE, transfer_transfer, transfer_self]
  intro e
  rw [edges_transfer]
  apply edges_subset_edgeSet p

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