mul_le_of_le_one_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If b ≥ 0 and a ≤ 1, then a b ≤ b.

Русский

Если b ≥ 0 и a ≤ 1, то a b ≤ b.

LaTeX

$$$\\\\forall a,b \\\\in \\\\alpha, \\\\ 0 \\\\le b \\\\land a \\\\le 1 \\\\Rightarrow a b \\\\le b.$$$

Lean4

theorem mul_le_of_le_one_left [MulPosMono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := by
  simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb

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

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

Разделы

Аффилиация

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