mono — Mathlib

English

If f is absolutely continuous on [a,b] and [c,d] ⊆ [a,b], then f is absolutely continuous on [c,d].

Русский

Если f абсолютно непрерывна на [a,b] и [c,d] ⊆ [a,b], то f абсолютно непрерывна на [c,d].

LaTeX

$$$ \text{mono}(hf,habcd) :\; \text{AbsolutelyContinuousOnInterval } f c d $$$

Lean4

theorem mono (hf : AbsolutelyContinuousOnInterval f a b) (habcd : uIcc c d ⊆ uIcc a b) :
    AbsolutelyContinuousOnInterval f c d :=
  by
  simp only [AbsolutelyContinuousOnInterval, Tendsto] at *
  refine le_trans (Filter.map_mono ?_) hf
  gcongr; exact disjWithin_mono habcd

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