smul_lowerBounds_subset_lowerBounds_smul_of_nonneg

English

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

Русский

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

LaTeX

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

Lean4

theorem smul_lowerBounds_subset_lowerBounds_smul_of_nonneg (ha : 0 ≤ a) : a • lowerBounds s ⊆ lowerBounds (a • s) :=
  (monotone_smul_left_of_nonneg ha).image_lowerBounds_subset_lowerBounds_image

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