mul_lt_of_lt_one_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If a > 0 and a < 1 then a b < b for b > 0.

Русский

Если a > 0 и a < 1, то a b < b при b > 0.

LaTeX

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

Lean4

theorem mul_lt_of_lt_one_left [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b := by
  simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

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

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

Разделы

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

Аффилиация

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