pathELength_mono — Mathlib

English

If a ≤ a' and b ≤ b', then the path length over [a,b] is no larger than the path length over [a',b'] for the same γ.

Русский

Если a ≤ a' и b ≤ b', то длина траектории по [a,b] не превышает длину по [a',b'] для одной и той же траектории.

LaTeX

$$pathELength I γ a b ≤ pathELength I γ a' b' whenever a' ≤ a and b ≤ b'.$$

Lean4

@[gcongr]
theorem pathELength_mono (h : a' ≤ a) (h' : b ≤ b') : pathELength I γ a b ≤ pathELength I γ a' b' := by
  simpa [pathELength_eq_lintegral_mfderiv_Icc] using lintegral_mono_set (Icc_subset_Icc h h')

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