nonneg_of_le

Mathlib.Topology.EMetricSpace.BoundedVariation

URI: https://scilib.ai/kg/mathlib#variationOnFromTo.nonneg_of_le

← MathLib Explorer

English

If a ≤ b, then variationOnFromTo f s a b ≥ 0.

Русский

Если a ≤ b, то variationOnFromTo f s a b ≥ 0.

LaTeX

$$0 ≤ variationOnFromTo f s a b$$

Lean4

protected theorem nonneg_of_le {a b : α} (h : a ≤ b) : 0 ≤ variationOnFromTo f s a b := by
  simp only [variationOnFromTo, if_pos h, ENNReal.toReal_nonneg]

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

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

Разделы

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

Аффилиация

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