locallyBoundedVariationOn — Mathlib

English

Bounded variation on s implies locally bounded variation on s.

Русский

Пусть для множества s вариация ограничена; тогда на каждом локальном участке сохраняется ограниченность вариации.

LaTeX

$$$\forall f:α\to E,\; h:BoundedVariationOn f s\Rightarrow LocallyBoundedVariationOn f s$$

Lean4

theorem _root_.BoundedVariationOn.locallyBoundedVariationOn {f : α → E} {s : Set α} (h : BoundedVariationOn f s) :
    LocallyBoundedVariationOn f s := fun _ _ _ _ => h.mono inter_subset_left

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