instPowNNReal — Mathlib

English

For any a and y ∈ ℝ≥0, nnrpow a y equals the standard power a^y in the ambient structure, i.e., nnrpow a y = a^y.

Русский

Для любых a и y ∈ ℝ≥0 nnrpow a y совпадает с обычной степенью a^y.

LaTeX

$$nnrpow a y = a ^ y$$

Lean4

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

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