const_mul'

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#MonotoneOn.const_mul'

← MathLib Explorer

English

If f is monotone on a set s, then x ↦ a · f(x) is monotone on s.

Русский

Если f монотонна на множестве s, то x ↦ a · f(x) монотонна на s.

LaTeX

$$$MonotoneOn f s \\\\Rightarrow MonotoneOn (\\\\lambda x. a \\\\cdot f(x)) s$$$

Lean4

@[to_additive const_add]
theorem const_mul' [MulLeftMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => a * f x) s :=
  mul_right_mono.comp_monotoneOn hf

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

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

Разделы

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

Аффилиация

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