top_rpow_of_neg

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

If y < 0, (⊤)^y = 0.

Русский

Если y < 0, (⊤)^y = 0.

LaTeX

$$$y < 0 \\Rightarrow (\\top)^{y} = 0$$$

Lean4

@[simp]
theorem top_rpow_of_neg {y : ℝ} (h : y < 0) : (⊤ : ℝ≥0∞) ^ y = 0 := by simp [top_rpow_def, asymm h, ne_of_lt h]

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

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

Разделы

Аффилиация

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