smul_nonpos_iff

Mathlib.Algebra.Order.Module.Defs

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

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_nonpos_iff : a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
  rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]

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

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

Разделы

Аффилиация

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