smul_of_nonpos

Mathlib.Algebra.Order.Module.Pointwise

URI: https://scilib.ai/kg/mathlib#BddAbove.smul_of_nonpos

English

If M,N have OrderedSMul, then their product M × N has a natural OrderedSMul structure by 𝕜.

Русский

Если M и N имеют OrderedSMul, то произведение M × N имеет естественное OrderedSMul по 𝕜.

LaTeX

$$$ OrderedSMul 𝕜 (M \times N). $$$

Lean4

theorem smul_of_nonpos (ha : a ≤ 0) (hs : BddAbove s) : BddBelow (a • s) :=
  (antitone_smul_left ha).map_bddAbove hs

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

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

Разделы

Аффилиация

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