English
A function has locally bounded variation on a set s if, for any interval [a,b] with endpoints in s, the function has finite variation on s ∩ [a,b].
Русский
Функция имеет локально ограниченную вариацию на s, если для любого интервала [a,b] с концами в s её вариация на s ∩ [a,b] конечна.
LaTeX
$$LocallyBoundedVariationOn (f : α → E) (s : Set α) := ∀ a b, a ∈ s → b ∈ s → BoundedVariationOn f (s ∩ Icc a b)$$
Lean4
/-- A function has locally bounded variation on a set `s` if, given any interval `[a, b]` with
endpoints in `s`, then the function has finite variation on `s ∩ [a, b]`. -/
def LocallyBoundedVariationOn (f : α → E) (s : Set α) :=
∀ a b, a ∈ s → b ∈ s → BoundedVariationOn f (s ∩ Icc a b)