mul_lt_of_lt_of_lt_one

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

← MathLib Explorer

English

If b < c and a < 1, then b < c·a.

Русский

Если b < c и a < 1, тогда b < c·a.

LaTeX

$$$$\forall a,b,c \in \alpha:\; b < c \land a < 1 \Rightarrow b < c\,a.$$$$

Lean4

@[to_additive]
theorem mul_lt_of_lt_of_lt_one [MulLeftStrictMono α] {a b c : α} (hbc : b < c) (ha : a < 1) : b * a < c :=
  calc
    b * a < b * 1 := mul_lt_mul_left' ha b
    _ = b := (mul_one b)
    _ < c := hbc

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

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

Разделы

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

Аффилиация

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