mul_const'

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive add_const]
theorem mul_const' [MulRightMono α] (hf : MonotoneOn f s) (a : α) : MonotoneOn (fun x => f x * a) s :=
  mul_left_mono.comp_monotoneOn hf

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

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

Разделы

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

Аффилиация

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