le_of_forall_one_lt_le_mul

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

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

← MathLib Explorer

English

If ∀ ε > 1, a ≤ b·ε, then a ≤ b.

Русский

Если для всех ε > 1 верно a ≤ b·ε, тогда a ≤ b.

LaTeX

$$$\forall \varepsilon>1:\ a \le b\varepsilon \Rightarrow a \le b$.$$

Lean4

@[to_additive]
theorem le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
  le_of_forall_gt_imp_ge_of_dense fun x hxb =>
    by
    obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
    exact h _ (one_lt_of_lt_mul_right hxb)

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

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

Разделы

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

Аффилиация

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