mono

Mathlib.MeasureTheory.Measure.Stieltjes

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

English

Given a monotone real function f, the associated Stieltjes function is monotone.

Русский

Для монотонной функции f действует, что сопутствующая функция Стильтьеса монотонна.

LaTeX

$$$$\\text{Monotone } f \\Rightarrow \\text{Monotone } (\\text{StieltjesFunction}.mono).$$$$

Lean4

theorem mono : Monotone f :=
  f.mono'

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

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

Разделы

Аффилиация

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