bddAbove_smul_iff_of_neg

Mathlib.Algebra.Order.Module.Pointwise

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

English

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

Русский

Для отрицательного a: BddAbove(a • s) ⇔ BddBelow s.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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