length_comp — Mathlib

English

The length of the composite path p ∘ q equals the sum of lengths: length(p ∘ q) = length(p) + length(q).

Русский

Длина композиции путей p ∘ q равна сумме длин: length(p ∘ q) = length(p) + length(q).

LaTeX

$$$\\forall p:\\; \\mathrm{Path}(a,b),\\; q:\\; \\mathrm{Path}(b,c):\\; \\mathrm{length}(p\\circ q) = \\mathrm{length}(p) + \\mathrm{length}(q).$$$

Lean4

@[simp]
theorem length_comp (p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).length = p.length + q.length
  | _, nil => rfl
  | _, cons _ _ => congr_arg Nat.succ (length_comp _ _)

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