rpow_eq_zero_iff_of_pos

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_eq_zero_iff_of_pos

English

If y > 0, x^y equals infinity only when x is infinity.

Русский

Если y > 0, x^y бесконечность достигается только для x = ∞.

LaTeX

$$$y>0 \\Rightarrow x^y = \\infty \\iff x = \\infty$$$

Lean4

theorem rpow_eq_zero_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = 0 ↔ x = 0 := by simp [hy, hy.not_gt]

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

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

Разделы

Аффилиация

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