min_le_of_mul_le_sq

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

If a^2 ≤ b · c, then min(a,b) ≤ c.

Русский

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

LaTeX

$$$a^2 \le bc \Rightarrow \min(a,b) \le c$$$

Lean4

@[to_additive min_le_of_add_le_two_nsmul]
theorem min_le_of_mul_le_sq {a b c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c := by
  simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)

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

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

Разделы

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

Аффилиация

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