lt_pow_iff_log_lt

Mathlib.Analysis.SpecialFunctions.Pow.Real

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

English

For x>0,y>0 and n ∈ Nat, x < y^n iff log x < n log y.

Русский

Для x>0, y>0 и n ∈ Nat, x < y^n эквивалентно log x < n log y.

LaTeX

$$$x > 0 \land y > 0 \Rightarrow x < y^{n} \iff \log x < n \log y$$$

Lean4

theorem lt_pow_iff_log_lt (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ log x < n * log y :=
  rpow_natCast _ _ ▸ lt_rpow_iff_log_lt hx hy

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

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

Разделы

Аффилиация

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