pathELength_congr — Mathlib

English

If γ and γ' are equal on the closed interval Icc(a,b), then their path lengths from a to b coincide.

Русский

Если γ и γ' совпадают на отрезке Icc(a,b), их длины траекторий между a и b совпадают.

LaTeX

$$pathELength I γ a b = pathELength I γ' a b, если EqOn γ γ' (Icc a b).$$

Lean4

theorem pathELength_congr (h : EqOn γ γ' (Icc a b)) : pathELength I γ a b = pathELength I γ' a b :=
  pathELength_congr_Ioo (fun _ hx ↦ h ⟨hx.1.le, hx.2.le⟩)

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