concatRec_concat — Mathlib

English

If p.concat h = p'.concat h' for p, p' walks and h, h' edges, then there exists hv : v = v' such that p.copy rfl hv = p'.

Русский

Если p.concat h = p'.concat h' для путей p, p' и рёбер h, h', то существует hv: v = v', такое что p.copy rfl hv = p'.

LaTeX

$$$p.\concat h = p'.\concat h' \Rightarrow \exists hv: v = v',\ p.copy( rfl )\, hv = p'$$$

Lean4

@[simp]
theorem concatRec_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    @concatRec _ _ motive @Hnil @Hconcat _ _ (p.concat h) = Hconcat p h (concatRec (@Hnil) (@Hconcat) p) :=
  by
  simp only [concatRec]
  apply eq_of_heq
  apply rec_heq_of_heq
  trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)
  · congr
    simp
  · rw [concatRecAux, eqRec_heq_iff_heq]
    congr <;> simp

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