instPowReal

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

There is a real-power operation on ENNReal (a Pow ENNReal Real instance).

Русский

Существует операция возведения в степень по вещественным степеням на ENNReal.

LaTeX

$$$\\text{There exists a real-power operation on } \\mathbb{R}_{\\ge 0}^{\\infty}$.$$

Lean4

noncomputable instance : Pow ℝ≥0∞ ℝ :=
  ⟨rpow⟩

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

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

Разделы

Аффилиация

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