symm — Mathlib

English

If f is absolutely continuous on [a,b], then it is absolutely continuous on [b,a].

Русский

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

LaTeX

$$$ \text{symm}(hf) :\; \text{AbsolutelyContinuousOnInterval } f b a $$$

Lean4

theorem symm (hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval f b a := by
  simp_all [AbsolutelyContinuousOnInterval, disjWithin_comm]

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