nnrpow_nonneg

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

URI: https://scilib.ai/kg/mathlib#CFC.nnrpow_nonneg

English

For a, x, y ∈ ℝ≥0 and suitable topology, (a^x)^y = a^(x·y).

Русский

Для a, x, y ∈ ℝ≥0 выполняется (a^x)^y = a^(x·y).

LaTeX

$$(a^x)^y = a^(x*y)$$

Lean4

@[simp, grind]
theorem nnrpow_nonneg {a : A} {x : ℝ≥0} : 0 ≤ a ^ x :=
  cfcₙ_predicate _ a

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

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

Разделы

Аффилиация

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