comp_locallyBoundedVariationOn — Mathlib

English

If f is LipschitzWith on α, then composing with any g preserves local BV on the domain.

Русский

Если f — LipschitzWith на всей области, композиция с любой g сохраняет локальную BV на области определения.

LaTeX

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

Lean4

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

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