smul_upperBounds_subset_lowerBounds_smul

English

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

Русский

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

LaTeX

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

Lean4

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

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