Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-15 21:24 6aefa38d

View on Github →

chore(topology/algebra/*,analysis/specific_limits): continuity of fpow (#8665)

  • add more API lemmas about continuity of x ^ n for natural and integer n;
  • prove that x⁻¹ and x ^ n, n < 0, are discontinuous at zero.

Estimated changes

added theorem inv_surjective
modified theorem continuous.fpow
modified theorem continuous_at.fpow
modified theorem continuous_at_fpow
added theorem continuous_on.fpow
modified theorem filter.tendsto.fpow
deleted theorem tendsto_fpow
added theorem continuous_at.pow
added theorem continuous_at_pow
added theorem continuous_on.pow
added theorem filter.tendsto.pow