smul_upperBounds_subset_upperBounds_smul_of_nonneg

English

If a ≥ 0, then a • upperBounds(s) ⊆ upperBounds(a • s).

Русский

Если a ≥ 0, то a • верхние границы s ⊆ верхние границы (a • s).

LaTeX

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

Lean4

theorem smul_upperBounds_subset_upperBounds_smul_of_nonneg (ha : 0 ≤ a) : a • upperBounds s ⊆ upperBounds (a • s) :=
  (monotone_smul_left_of_nonneg ha).image_upperBounds_subset_upperBounds_image

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