Commit 2023-05-25 13:41 8916ee44

View on Github →

feat: port Analysis.SpecialFunctions.Pow.Continuity (#4336)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

added theorem Complex.continuousAt_cpow_const_of_re_pos

added theorem Complex.continuousAt_cpow_of_re_pos

added theorem Complex.continuousAt_cpow_zero_of_re_pos

added theorem Complex.continuousAt_of_real_cpow

added theorem Complex.continuousAt_of_real_cpow_const

added theorem Complex.continuous_of_real_cpow_const

added theorem Continuous.const_cpow

added theorem Continuous.cpow

added theorem Continuous.rpow

added theorem Continuous.rpow_const

added theorem ContinuousOn.const_cpow

added theorem ContinuousOn.cpow

added theorem ContinuousOn.cpow_const

added theorem ContinuousOn.rpow

added theorem ContinuousOn.rpow_const

added theorem ENNReal.continuous_rpow_const

added theorem ENNReal.eventually_pow_one_div_le

added theorem ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos

added theorem Filter.Tendsto.const_cpow

added theorem Filter.Tendsto.cpow

added theorem Filter.Tendsto.ennrpow_const

added theorem Filter.Tendsto.nnrpow

added theorem Filter.Tendsto.rpow

added theorem Filter.Tendsto.rpow_const

added theorem NNReal.continuousAt_rpow

added theorem NNReal.continuousAt_rpow_const

added theorem NNReal.continuous_rpow_const

added theorem NNReal.eventually_pow_one_div_le

added theorem Real.continuousAt_const_rpow'

added theorem Real.continuousAt_const_rpow

added theorem Real.continuousAt_rpow

added theorem Real.continuousAt_rpow_const

added theorem Real.continuousAt_rpow_of_ne

added theorem Real.continuousAt_rpow_of_pos

added theorem Real.rpow_eq_nhds_of_neg

added theorem Real.rpow_eq_nhds_of_pos

added theorem continuousAt_const_cpow'

added theorem continuousAt_const_cpow

added theorem continuousAt_cpow

added theorem continuousAt_cpow_const

added theorem cpow_eq_nhds'

added theorem cpow_eq_nhds

added theorem zero_cpow_eq_nhds