const_mul' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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