le_rpow_of_log_le

Mathlib.Analysis.SpecialFunctions.Pow.Real

URI: https://scilib.ai/kg/mathlib#Real.le_rpow_of_log_le

← MathLib Explorer

English

For n ∈ Z, if log x ≤ n log y and y>0, then x ≤ y^n.

Русский

Для n ∈ Z, если log x ≤ n log y и y>0, тогда x ≤ y^n.

LaTeX

$$$n \in \mathbb{Z} \land y > 0 \land \log x \le n \log y \Rightarrow x \le y^{n}$$$

Lean4

theorem le_rpow_of_log_le (hy : 0 < y) (h : log x ≤ z * log y) : x ≤ y ^ z :=
  by
  obtain hx | hx := le_or_gt x 0
  · exact hx.trans (rpow_pos_of_pos hy _).le
  · exact (le_rpow_iff_log_le hx hy).2 h

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

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

Разделы

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

Аффилиация

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