comp_le_of_monotoneOn — Mathlib

English

If φ is antitone on t and maps t into s, then the variation of f∘φ on t is bounded by the variation of f on s.

Русский

Если φ антитонна на t и отображает t в s, вариация f∘φ на t ограничена вариацией f на s.

LaTeX

$$$\forall f:α\to E,\; φ:β\to α,\; AntitoneOn φ t\;\Rightarrow\; MapsTo φ t s\;\Rightarrow eVariationOn (f\circ φ) t \le eVariationOn f s$$

Lean4

theorem comp_le_of_monotoneOn (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t)
    (φst : MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s :=
  iSup_le fun ⟨n, u, hu, ut⟩ =>
    le_iSup_of_le ⟨n, φ ∘ u, fun x y xy => hφ (ut x) (ut y) (hu xy), fun i => φst (ut i)⟩ le_rfl

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