English
If f is absolutely continuous on [a,b], then it is uniformly continuous on the closed interval uIcc(a,b).
Русский
Если f абсолю́тно непрерывна на [a,b], то она равномерно непрерывна на замкнутом отрезке uIcc(a,b).
LaTeX
$$$\text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{UniformContinuousOn}(f, \; \mathrm{uIcc}(a,b))$$$
Lean4
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` is uniformly continuous on `uIcc a b`.
-/
theorem uniformlyContinuousOn (hf : AbsolutelyContinuousOnInterval f a b) : UniformContinuousOn f (uIcc a b) :=
by
simp only [UniformContinuousOn, Filter.tendsto_iff_comap, uniformity_eq_comap_totalLengthFilter]
simp only [AbsolutelyContinuousOnInterval, Filter.tendsto_iff_comap] at hf
convert Filter.comap_mono hf
· simp only [comap_inf, comap_principal]
congr
ext p
simp only [disjWithin, Finset.mem_range, preimage_setOf_eq, Nat.lt_one_iff, forall_eq, mem_setOf_eq, mem_prod]
simp
· simp only [totalLengthFilter, comap_comap]
congr 1
