mul_const' — Mathlib

English

If f is strictly monotone on s, then for every c the map x ↦ f(x) · c is strictly monotone on s.

Русский

Если f строго монотонна на s, то для любого c отображение x ↦ f(x) · c строго монотонно на s.

LaTeX

$$$StrictMonoOn(f,s) \Rightarrow \forall c \in \alpha,\; StrictMonoOn(\lambda x. f(x) \cdot c, s)$$$

Lean4

@[to_additive add_const]
theorem mul_const' (hf : StrictMonoOn f s) (c : α) : StrictMonoOn (fun x => f x * c) s := fun _ ha _ hb ab =>
  mul_lt_mul_right' (hf ha hb ab) c

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