smul_of_nonpos

Mathlib.Algebra.Order.Module.Pointwise

URI: https://scilib.ai/kg/mathlib#BddBelow.smul_of_nonpos

English

If a ≤ 0 and s is bounded below, then a • s is bounded above.

Русский

Если a ≤ 0 и s ограничено снизу, то a • s ограничено сверху.

LaTeX

$$$ (ha : a \le 0) \Rightarrow (\operatorname{BddBelow} s) \Rightarrow \operatorname{BddAbove}(a \cdot s). $$$

Lean4

theorem smul_of_nonpos (ha : a ≤ 0) (hs : BddBelow s) : BddAbove (a • s) :=
  (antitone_smul_left ha).map_bddBelow hs

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

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

Разделы

Аффилиация

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