comp_boundedVariationOn — Mathlib

English

If f is LipschitzWith with constant C, then BV of g on s implies BV of f∘g on s.

Русский

Если f — липшицева с константой C, то BV функции g на s влечёт BV композиции f∘g на s.

LaTeX

$$$ (LipschitzWith\ C\ f) \Rightarrow (BoundedVariationOn\ g\ s) \Rightarrow BoundedVariationOn\ (f \circ g)\ s $$$

Lean4

theorem comp_boundedVariationOn {f : E → F} {C : ℝ≥0} (hf : LipschitzWith C f) {g : α → E} {s : Set α}
    (h : BoundedVariationOn g s) : BoundedVariationOn (f ∘ g) s :=
  hf.lipschitzOnWith.comp_boundedVariationOn (mapsTo_univ _ _) h

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