smul_min_of_nonpos

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

If a ≤ 0, then a·max{b1,b2} = min{a·b1, a·b2}.

Русский

Если a ≤ 0, то a·max{b1,b2} = min{a·b1, a·b2}.

LaTeX

$$$a \le 0 \Rightarrow a \cdot \max\{b_{1}, b_{2}\} = \min\{a \cdot b_{1}, a \cdot b_{2}\}$$$

Lean4

theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : β) : a • min b₁ b₂ = max (a • b₁) (a • b₂) :=
  (antitone_smul_left ha : Antitone (_ : β → β)).map_min

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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