coe_rpow — Mathlib

English

Coercion from NNReal to Real commutes with real power: the Real value of x^y equals (x)^{y} for x ≥ 0.

Русский

Проведение из NNReal в Real сохраняет возведение в степень: вещественное значение x^y равно (x)^y при x ≥ 0.

LaTeX

$$$\\bigl((x^y : \\mathbb{R}_{\\ge 0}) : \\mathbb{R}\\bigr) = x^y$$$

Lean4

@[simp, norm_cast]
theorem coe_rpow (x : ℝ≥0) (y : ℝ) : ((x ^ y : ℝ≥0) : ℝ) = (x : ℝ) ^ y :=
  rfl

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