rpow_eq_top_iff_of_pos

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For x ∈ ENNReal and y ∈ ℝ with y>0, x^y = ∞ iff x = ∞.

Русский

Для x ∈ ENNReal и y ∈ ℝ, y>0: x^y = ∞ тогда и только тогда, когда x = ∞.

LaTeX

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

Lean4

theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = ⊤ ↔ x = ⊤ := by
  simp [rpow_eq_top_iff, hy, asymm hy]

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

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

Разделы

Аффилиация

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