monotone_eapprox

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.monotone_eapprox

English

eapprox is monotone in f: if f ≤ g then eapprox f ≤ eapprox g.

Русский

eapprox монотонно в отношении f: если f ≤ g, то eapprox f ≤ eapprox g.

LaTeX

$$$ f \le g \Rightarrow eapprox f \le eapprox g $$$

Lean4

@[mono]
theorem monotone_eapprox (f : α → ℝ≥0∞) : Monotone (eapprox f) :=
  monotone_approx _ f

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

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

Разделы

Аффилиация

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