instPowReal — Mathlib

English

The definition of rpow uses the continuous functional calculus with nonnegative exponents.

Русский

Определение rpow использует непрерывный функциональный расчёт с неотрицательными степенями.

LaTeX

$$rpow a y = cfc (fun x : ℝ≥0 => x^y) a$$

Lean4

/-- Enable `a ^ y` notation for `CFC.rpow`. This is a low-priority instance to make sure it does
not take priority over other instances when they are available (such as `Pow ℝ ℝ`). -/
noncomputable instance (priority := 100) : Pow A ℝ where pow a y := rpow a y

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