rpow_inv_lt_iff

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_inv_lt_iff

English

For nonnegative NNReal numbers x, y and z > 0, x^{1/z} < y if and only if x < y^{z}.

Русский

Для NNReal: x^{1/z} < y эквивалентно x < y^{z}, при z > 0.

LaTeX

$$x ^ z⁻¹ < y ↔ x < y ^ z$$

Lean4

theorem rpow_inv_lt_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ < y ↔ x < y ^ z := by
  simp only [← not_le, le_rpow_inv_iff hz]

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

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

Разделы

Аффилиация

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