BoundedVariationOn — Mathlib

English

A function has bounded variation on a set s if its total variation on s is finite.

Русский

Функция имеет ограниченную вариацию на множестве s, если её общая вариация на s конечна.

LaTeX

$$BoundedVariationOn (f : α → E) (s : Set α) := eVariationOn f s ≠ ∞$$

Lean4

/-- A function has bounded variation on a set `s` if its total variation there is finite. -/
def BoundedVariationOn (f : α → E) (s : Set α) :=
  eVariationOn f s ≠ ∞

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