mono

Mathlib.Topology.EMetricSpace.BoundedVariation

URI: https://scilib.ai/kg/mathlib#eVariationOn.mono

← MathLib Explorer

English

If t ⊆ s then eVariationOn f t ≤ eVariationOn f s.

Русский

Если t ⊆ s, то eVariationOn f t ≤ eVariationOn f s.

LaTeX

$$$\forall f:α\to E,\;\forall s,t\subset α,\; t\subset s\Rightarrow eVariationOn f t \le eVariationOn f s$$

Lean4

theorem mono (f : α → E) {s t : Set α} (hst : t ⊆ s) : eVariationOn f t ≤ eVariationOn f s :=
  by
  apply iSup_le _
  rintro ⟨n, ⟨u, hu, ut⟩⟩
  exact sum_le f n hu fun i => hst (ut i)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru