Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-15 13:26 136e67a6

View on Github →

refactor(topology): change continuous_at_within to continuous_within_at (#1034)

Estimated changes

Modified src/analysis/normed_space/deriv.lean

deleted theorem differentiable_within_at.continuous_at_within

added theorem differentiable_within_at.continuous_within_at

deleted theorem has_fderiv_within_at.continuous_at_within

added theorem has_fderiv_within_at.continuous_within_at

Modified src/topology/basic.lean

deleted def continuous_at_within

modified def continuous_on

added def continuous_within_at

Modified src/topology/constructions.lean

deleted theorem continuous_at_within.prod

added theorem continuous_within_at.prod

Modified src/topology/order.lean

deleted theorem continuous_at.continuous_at_within

added theorem continuous_at.continuous_within_at

deleted theorem continuous_at_within.mono

deleted theorem continuous_at_within.tendsto_nhds_within_image

deleted theorem continuous_at_within_iff_continuous_at_restrict

deleted theorem continuous_at_within_iff_ptendsto_res

deleted theorem continuous_at_within_univ

added theorem continuous_within_at.mono

added theorem continuous_within_at.tendsto_nhds_within_image

added theorem continuous_within_at_iff_continuous_at_restrict

added theorem continuous_within_at_iff_ptendsto_res

added theorem continuous_within_at_univ

modified theorem nhds_within_le_comap