smul_nonneg_iff_pos_imp_nonneg

Mathlib.Algebra.Order.Module.Defs

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

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_nonneg_iff_pos_imp_nonneg : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) :=
  smul_nonneg_iff.trans <| by grind

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

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

Разделы

Аффилиация

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