Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-20 09:21 50107383

View on Github →

feat(topology/algebra/ordered): continuity of abs (#5412)

Estimated changes

Modified src/analysis/special_functions/exp_log.lean

Modified src/topology/algebra/ordered.lean

added theorem continuous.abs

added theorem continuous_abs

added theorem continuous_at.abs

added theorem continuous_on.abs

added theorem continuous_within_at.abs

added theorem filter.tendsto.abs

added theorem tendsto_abs_nhds_within_zero

Modified src/topology/basic.lean

Modified src/topology/instances/real.lean

deleted theorem rat.continuous_abs

deleted theorem real.continuous_abs