rpow_ne_top_of_nonneg'

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_ne_top_of_nonneg'

← MathLib Explorer

English

If x is finite and nonzero, then x^y ≠ ∞ for any y.

Русский

Если x конечен и не равен нулю, то x^y не бесконечна для любого y.

LaTeX

$$For 0 < x < ∞, x^y ≠ ∞ for any y$$

Lean4

@[aesop (rule_sets := [finiteness]) unsafe apply]
theorem rpow_ne_top_of_nonneg' {y : ℝ} {x : ℝ≥0∞} (hx : 0 < x) (hx' : x ≠ ⊤) : x ^ y ≠ ⊤ := fun h ↦ by
  simp [rpow_eq_top_iff, hx.ne', hx'] at h

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

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

Разделы

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

Аффилиация

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