lowerBounds_smul_of_neg — Mathlib

English

For a negative scalar, the lower bounds of the image under smul correspond to the image of the upper bounds.

Русский

Для отрицательного скаляра нижние границы образа смул соотносятся с образом верхних границ.

LaTeX

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

Lean4

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

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