mono — Mathlib

English

If h is a BV on s, then for any t ⊆ s, f has BV on t.

Русский

Если f имеет ограниченную вариацию на s, то на любом подмножестве t ⊆ s вариация также ограничена.

LaTeX

$$$\forall f:α\to E,\; h:BoundedVariationOn f s\Rightarrow \forall t\,(t\subset s)\; BoundedVariationOn f t$$

Lean4

theorem _root_.BoundedVariationOn.mono {f : α → E} {s : Set α} (h : BoundedVariationOn f s) {t : Set α} (ht : t ⊆ s) :
    BoundedVariationOn f t :=
  ne_top_of_le_ne_top h (eVariationOn.mono f ht)

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