pathELength_add — Mathlib

English

If a ≤ b ≤ c, then the length from a to c equals the sum of the lengths from a to b and from b to c.

Русский

Если a ≤ b ≤ c, то длина от a до c равна сумме длин от a до b и от b до c.

LaTeX

$$pathELength I γ a b + pathELength I γ b c = pathELength I γ a c$$

Lean4

theorem pathELength_add (h : a ≤ b) (h' : b ≤ c) : pathELength I γ a b + pathELength I γ b c = pathELength I γ a c :=
  by
  symm
  have : Icc a c = Icc a b ∪ Ioc b c := (Icc_union_Ioc_eq_Icc h h').symm
  rw [pathELength, this, lintegral_union measurableSet_Ioc]; swap
  · exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)
  simp [restrict_Ioc_eq_restrict_Icc, pathELength]

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