transfer — Mathlib

English

If p is a path in G from u to v, then transferring p along H with a suitable hp yields a path in the transferred graph q.

Русский

Если p является путём в G от u к v, то перенос путей p через граф H с подходящим hp даёт путём в перенесённом графе q.

LaTeX

$$$\\\\forall {V} {G} {H} {u v} {p : G.Walk u v}, \\\\text{pp} : p.IsPath \\\\Rightarrow (p.transfer H hp).IsPath$$

Lean4

protected theorem transfer (hp) (pp : p.IsPath) : (p.transfer H hp).IsPath := by
  induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
    exact ⟨ih _ pp.1, pp.2⟩

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