smul_max_of_nonpos

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

0 ≤ a·b iff (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a).

Русский

0 ≤ a·b эквивалентно (0 < a ⇒ 0 ≤ b) и (0 < b ⇒ 0 ≤ a).

LaTeX

$$$0 \le a \cdot b \iff (0 < a \rightarrow 0 \le b) \land (0 < b \rightarrow 0 \le a)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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