smul_of_nonneg — Mathlib

English

If s is bounded below and a is nonnegative, then the set a · s is also bounded below.

Русский

Если множество s ограничено снизу, и коэффициент a неотрицателен, то множество a · s также ограничено снизу.

LaTeX

$$$\\operatorname{BddBelow}(s) \\rightarrow 0 \\le a \\rightarrow \\operatorname{BddBelow}(a \\cdot s)$$$

Lean4

theorem smul_of_nonneg (hs : BddBelow s) (ha : 0 ≤ a) : BddBelow (a • s) :=
  (monotone_smul_left_of_nonneg ha).map_bddBelow hs

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