lt_max_of_sq_lt_mul

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

If a^2 < b · c, then a < max(b,c).

Русский

Если a^2 < b · c, то a < max(b,c).

LaTeX

$$$a^2 < b c \Rightarrow a < \max(b,c)$$$

Lean4

@[to_additive lt_max_of_two_nsmul_lt_add]
theorem lt_max_of_sq_lt_mul {a b c : M} (h : a ^ 2 < b * c) : a < max b c := by
  simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)

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

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

Разделы

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

Аффилиация

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