Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-16 09:03 90fa510d

View on Github →

feat(analysis/special_functions/pow): rpow is measurable (#5008) Prove the measurability of rpow in two cases: real and nnreal.

Estimated changes

added theorem measurable.nnreal_rpow
added theorem measurable.rpow
added theorem measurable.rpow_const
added theorem nnreal.measurable_rpow
added theorem real.measurable_rpow