antitone_smul_left

Mathlib.Algebra.Order.Module.Defs

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

English

If a ≤ 0, then the map x ↦ a·x is antitone (order-reversing).

Русский

Если a ≤ 0, то отображение x ↦ a·x является антимонотонным (обращает порядок).

LaTeX

$$$x \mapsto a \cdot x \quad \text{антиномтонно при } a \le 0$$$

Lean4

theorem antitone_smul_left (ha : a ≤ 0) : Antitone ((a • ·) : β → β) := fun _ _ h ↦ smul_le_smul_of_nonpos_left h ha

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

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

Разделы

Аффилиация

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