Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 07:17 0544641d

View on Github →

chore(analysis/special_functions/pow): review lemmas about measurability of cpow/rpow (#6209)

  • prove that complex.cpow is measurable;
  • deduce measurability of real.rpow from definition, not continuity.

Estimated changes

added theorem measurable.cpow
modified theorem measurable.ennreal_rpow
modified theorem measurable.nnreal_rpow
deleted theorem nnreal.measurable_rpow
deleted theorem real.measurable_rpow