comp_boundedVariationOn — Mathlib

English

If f is C-Lipschitz on t, g maps s into t, and g has bounded variation on s, then f∘g has bounded variation on s.

Русский

Пусть f: E → F удовлетворяет условию C-Lipschitz на т, g: α → E отображает s в t, и g имеет ограниченную вариацию на s; тогда композиция f ∘ g имеет ограниченную вариацию на s.

LaTeX

$$$ (LipschitzOnWith\ C\ f\ t) \land (MapsTo\ g\ s\ t) \land (BoundedVariationOn\ g\ s) \Rightarrow BoundedVariationOn\ (f \circ g)\ s $$$

Lean4

theorem comp_boundedVariationOn {f : E → F} {C : ℝ≥0} {t : Set E} (hf : LipschitzOnWith C f t) {g : α → E} {s : Set α}
    (hg : MapsTo g s t) (h : BoundedVariationOn g s) : BoundedVariationOn (f ∘ g) s :=
  ne_top_of_le_ne_top (by finiteness) (hf.comp_eVariationOn_le hg)

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