div_const — Mathlib

English

If f is strictly monotone and c > 0, then x ↦ f(x) / c is strictly monotone.

Русский

Если f строго монотонна и c > 0, то x ↦ f(x)/c строго монотонна.

LaTeX

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

Lean4

theorem div_const {β : Type*} [Preorder β] {f : β → α} (hf : StrictMono f) {c : α} (hc : 0 < c) :
    StrictMono fun x => f x / c := by
  simpa only [div_eq_mul_inv] using
    hf.mul_const
      (inv_pos.2 hc)
        -- see Note [lower instance priority]

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