const_mul' — Mathlib

English

Let α be a preordered set with a multiplication that is compatible with the order. If f is strictly monotone on a set s, then for every constant c, the map x ↦ c · f(x) is strictly monotone on s.

Русский

Пусть α упорядоченное множество с умножением совместимо с порядком. Если f строго мономорна на множество s, то для любого константного элемента c отображение x ↦ c · f(x) строго мономорно на s.

LaTeX

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

Lean4

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

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