div_const

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

If f is monotone and c ≥ 0, then x ↦ f(x) / c is monotone in x.

Русский

Если f монотонна и c ≥ 0, то x ↦ f(x)/c монотонна по x.

LaTeX

$$$\text{Monotone}(f) \land (0 \le c) \Rightarrow \text{Monotone}\left(x \mapsto \frac{f(x)}{c}\right)$$$

Lean4

theorem div_const {β : Type*} [Preorder β] {f : β → α} (hf : Monotone f) {c : α} (hc : 0 ≤ c) :
    Monotone fun x => f x / c :=
  (monotone_div_right_of_nonneg hc).comp hf

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

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

Разделы

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

Аффилиация

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