strictAnti_smul_left

Mathlib.Algebra.Order.Module.Defs

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

English

The same strict anti-monotone behavior holds for the left smul when a < 0.

Русский

Строгое антимонотное поведение сохраняется слева для умножения на ноль и ниже.

LaTeX

$$$a<0 \Rightarrow (x_1 < x_2 \Rightarrow a\cdot x_1 > a\cdot x_2)$$$

Lean4

theorem strictAnti_smul_left (ha : a < 0) : StrictAnti ((a • ·) : β → β) := fun _ _ h ↦ smul_lt_smul_of_neg_left h ha

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

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

Разделы

Аффилиация

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