English
If f has constant speed on Icc(x,y) and on Icc(y,z) with the same l, then f has constant speed on Icc(x,z).
Русский
Если функция имеет постоянную скорость на Icc(x,y) и на Icc(y,z) с одинаковой скоростью l, то она имеет скорость l на Icc(x,z).
LaTeX
$$HasConstantSpeedOnWith f (Icc x y) l → HasConstantSpeedOnWith f (Icc y z) l → HasConstantSpeedOnWith f (Icc x z) l$$
Lean4
theorem Icc_Icc {x y z : ℝ} (hfs : HasConstantSpeedOnWith f (Icc x y) l) (hft : HasConstantSpeedOnWith f (Icc y z) l) :
HasConstantSpeedOnWith f (Icc x z) l :=
by
rcases le_total x y with (xy | yx)
· rcases le_total y z with (yz | zy)
· rw [← Set.Icc_union_Icc_eq_Icc xy yz]
exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)
· rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ← hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩,
Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right (vz.trans zy)]
· rintro u ⟨xu, uz⟩ v ⟨xv, vz⟩
rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ← hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc,
sup_of_le_right (yx.trans xu), inf_of_le_right vz]
