le_max_of_sq_le_mul

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

URI: https://scilib.ai/kg/mathlib#le_max_of_sq_le_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 \le bc \Rightarrow a \le \max\{b,c\}$$$

Lean4

@[to_additive le_max_of_two_nsmul_le_add]
theorem le_max_of_sq_le_mul {a b c : M} (h : a ^ 2 ≤ b * c) : a ≤ max b c := by
  simpa using min_le_max_of_mul_le_mul ((pow_two _).symm.trans_le h)

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

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

Разделы

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

Аффилиация

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