Mathlib Map

Theorems · Definition · functional analysis

NNReal.nnrpow

NNReal → NNReal → NNReal

Taking a nonnegative power of a nonnegative number. This is defined as a standalone definition in order to speed up automation such as cfc_cont_tac.

Defined in
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Cited by
19 results in Mathlib
Foundations
Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CFC.sqrt_eq_nnrpow · cited by 8CFC.sqrt_eq_nnrpowCFC.nnrpow · cited by 6CFC.nnrpowCFC.nnrpow_eq_rpow · cited by 6CFC.nnrpow_eq_rpowCFC.nnrpow_one · cited by 6CFC.nnrpow_oneCFC.nnrpow_nnrpow · cited by 5CFC.nnrpow_nnrpowCFC.nnrpow_zero · cited by 4CFC.nnrpow_zeroCFC.nnnorm_nnrpow · cited by 3CFC.nnnorm_nnrpowCFC.nnrpow_def · cited by 3CFC.nnrpow_defCFC.nnrpow_two · cited by 3CFC.nnrpow_twoCFC.nnrpow_map_pi · cited by 2CFC.nnrpow_map_piCFC.nnrpow_map_prod · cited by 2CFC.nnrpow_map_prodCFC.nnrpow_eq_cfcₙ_real · cited by 1CFC.nnrpow_eq_cfcₙ_realNNReal.continuous_nnrpow_const · cited by 1NNReal.continuous_nnrpow_…NNReal.monotone_nnrpow_const · cited by 1NNReal.monotone_nnrpow_co…NNReal.nnrpow_def · cited by 0NNReal.nnrpow_defNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealNNReal.nnrpowCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by20

Results whose statement or proof uses this declaration.