upperBounds_smul_of_neg — Mathlib

English

If a < 0, then the upper bounds of a • s correspond to the lower bounds of s via a duality.

Русский

Если a < 0, верхние границы a • s соответствуют нижним границам s через двойственность.

LaTeX

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

Lean4

@[simp]
theorem upperBounds_smul_of_neg (ha : a < 0) : upperBounds (a • s) = a • lowerBounds s :=
  (OrderIso.smulRightDual β ha).lowerBounds_image

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