monotoneOn

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#StrictMonoOn.monotoneOn

English

If f is strictly monotone on s, then f is monotone on s.

Русский

Если функция строго монотонна на s, то она монотонна на s.

LaTeX

$$$$\\text{StrictMonoOn } f s \\Rightarrow \\text{MonotoneOn } f s.$$$$

Lean4

protected theorem monotoneOn (hf : StrictMonoOn f s) : MonotoneOn f s :=
  monotoneOn_iff_forall_lt.2 fun _ ha _ hb h ↦ (hf ha hb h).le

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

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

Разделы

Аффилиация

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