trans — Mathlib

English

If p1 is a subwalk of p2 and p2 is a subwalk of p3, then p1 is a subwalk of p3.

Русский

Если p1 является подпрохожим к p2 и p2 к p3, то p1 является подпрохожим к p3.

LaTeX

$$$\forall G\;\forall p_1:p_1\in G.Walk\,u_1\,v_1\;\forall p_2:p_2\in G.Walk\,u_2\,v_2\;\forall p_3:p_3\in G.Walk\,u_3\,v_3,\ (IsSubwalk(p_1,p_2)\land IsSubwalk(p_2,p_3))\Rightarrow IsSubwalk(p_1,p_3).$$$

Lean4

theorem trans {u₁ v₁ u₂ v₂ u₃ v₃} {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} {p₃ : G.Walk u₃ v₃} (h₁ : p₁.IsSubwalk p₂)
    (h₂ : p₂.IsSubwalk p₃) : p₁.IsSubwalk p₃ :=
  by
  obtain ⟨q₁, r₁, rfl⟩ := h₁
  obtain ⟨q₂, r₂, rfl⟩ := h₂
  use q₂.append q₁, r₁.append r₂
  simp only [append_assoc]

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