smul_lowerBounds_subset_upperBounds_smul

English

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

Русский

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

LaTeX

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

Lean4

theorem smul_lowerBounds_subset_upperBounds_smul (ha : a ≤ 0) : a • lowerBounds s ⊆ upperBounds (a • s) :=
  (antitone_smul_left ha).image_lowerBounds_subset_upperBounds_image

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