transfer — Mathlib

English

If p is a G-Walk and H contains all edges of p, then transferring p to H is the same as mapping p by the LE inclusion f: G →≤ H.

Русский

Если p — обход в G, и H содержит все рёбра p, перенос p в H равен отображению p через вложение LE от G в H.

LaTeX

$$p.transfer H hp = p.map (SimpleGraph.Hom.ofLE GH)$$

Lean4

/-- The walk `p` transferred to lie in `H`, given that `H` contains its edges. -/
@[simp]
protected def transfer {u v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e, e ∈ p.edges → e ∈ H.edgeSet) :
    H.Walk u v :=
  match p with
  | nil => nil
  | cons' u v w _ p => cons (h s(u, v) (by simp)) (p.transfer H fun e he => h e (by simp [he]))

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