pathELength_congr_Ioo — Mathlib

English

If two paths γ and γ' agree on the interior Ioo(a,b), then they have the same path length from a to b.

Русский

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

LaTeX

$$pathELength I γ a b = pathELength I γ' a b, если γ t = γ' t для всех t ∈ Ioo(a,b).$$

Lean4

theorem pathELength_congr_Ioo (h : EqOn γ γ' (Ioo a b)) : pathELength I γ a b = pathELength I γ' a b :=
  by
  simp only [pathELength_eq_lintegral_mfderiv_Ioo]
  apply setLIntegral_congr_fun measurableSet_Ioo (fun t ht ↦ ?_)
  have A : γ t = γ' t := h ht
  congr! 2
  apply Filter.EventuallyEq.mfderiv_eq
  filter_upwards [Ioo_mem_nhds ht.1 ht.2] with a ha using h ha

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