bddBelow_smul_iff_of_neg

Mathlib.Algebra.Order.Module.Pointwise

URI: https://scilib.ai/kg/mathlib#bddBelow_smul_iff_of_neg

English

For a negative scalar a, BddBelow(a • s) ↔ BddAbove s.

Русский

При отрицательном a выполняется BddBelow(a • s) ⇔ BddAbove s.

LaTeX

$$$$ BddBelow(a \\cdot s) \\iff BddAbove(s) \\quad (a<0). $$$$

Lean4

@[simp]
theorem bddBelow_smul_iff_of_neg (ha : a < 0) : BddBelow (a • s) ↔ BddAbove s :=
  (OrderIso.smulRightDual β ha).bddAbove_image

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru