transfer_transfer — Mathlib

English

For p, the map of toDeleteEdges by a suitable LE morphism returns the original walk.

Русский

Для обхода p отображение через toDeleteEdges возвращает исходный обход через соответствующее отображение.

LaTeX

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

Lean4

@[simp]
theorem transfer_transfer (hp) {K : SimpleGraph V} (hp') :
    (p.transfer H hp).transfer K hp' = p.transfer K (p.edges_transfer hp ▸ hp') := by
  induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons.injEq, heq_eq_eq, true_and]
    apply ih

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