monotoneOn

Mathlib.Order.Monotone.Defs

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

English

If f is monotone, then its restriction to any subset s is monotone on s.

Русский

Если f монотонна, то её ограничение на произвольное множество s монотонно на s.

LaTeX

$$$\operatorname{Monotone}(f) \rightarrow \operatorname{MonotoneOn}(f,s)$$$

Lean4

protected theorem monotoneOn (hf : Monotone f) (s : Set α) : MonotoneOn f s := fun _ _ _ _ ↦ hf.imp

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

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

Разделы

Аффилиация

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