upperBounds_smul_of_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem upperBounds_smul_of_pos (ha : 0 < a) : upperBounds (a • s) = a • upperBounds s :=
  (OrderIso.smulRight ha).upperBounds_image

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