coe_rpow_def — Mathlib

English

For x ≥ 0 and any real y, x^y in ENNReal equals ∞ if x=0 and y<0, otherwise equals ↑(x^y).

Русский

Для x ≥ 0 и любого y ∈ ℝ x^y в ENNReal равен ∞, если x=0 и y<0; иначе равен ↑(x^y).

LaTeX

$$$(x)^y = \\begin{cases} \\infty & (x=0 \\land y<0) \\\\ ↑(x^y) & \\text{otherwise} \\end{cases}$$$

Lean4

theorem coe_rpow_def (x : ℝ≥0) (y : ℝ) : (x : ℝ≥0∞) ^ y = if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y) :=
  rfl

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