smul_nonneg_iff

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

If a·b1 ≤ a·b2 and a < 0, then b2 ≤ b1.

Русский

Если a·b1 ≤ a·b2 и a < 0, тогда b2 ≤ b1.

LaTeX

$$$a\cdot b_{1} \le a\cdot b_{2} \land a<0 \Rightarrow b_{2} \le b_{1}$$$

Lean4

theorem smul_nonneg_iff : 0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg, fun h ↦
    h.elim (and_imp.2 smul_nonneg) (and_imp.2 smul_nonneg_of_nonpos_of_nonpos)⟩

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

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

Разделы

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

Аффилиация

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