lowerBounds_smul_of_pos — Mathlib

English

For a < 0, the lower bounds under smul by a correspond to the upper bounds via a transformation.

Русский

Если a < 0, нижние границы после умножения на a соответствуют верхним границам через соответствующее преобразование.

LaTeX

$$$ {\text{lowerBounds}}(a \cdot s) = a \cdot {\text{upperBounds}}(s) \quad \text{when } a < 0. $$$

Lean4

@[simp]
theorem lowerBounds_smul_of_pos (ha : 0 < a) : lowerBounds (a • s) = a • lowerBounds s :=
  (OrderIso.smulRight ha).lowerBounds_image

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