min_lt_of_mul_lt_sq

Mathlib.Algebra.Order.Monoid.Unbundled.Pow

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

← MathLib Explorer

English

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

Русский

Если произведение a · b меньше c^2, тогда min(a,b) < c.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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