LocallyBoundedVariationOn — Mathlib

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)

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