Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-26 20:38 ae60bb96

View on Github →

chore(topology/algebra/order): add continuous_on.surj_on_of_tendsto (#5502)

rename surjective_of_continuous to continuous.surjective and surjective_of_continuous' to continuous.surjective';
add continuous_on.surj_on_of_tendsto and continuous_on.surj_on_of_tendsto'

Estimated changes

Modified src/analysis/special_functions/exp_log.lean

Modified src/data/real/sqrt.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/topology/algebra/ordered.lean

added theorem continuous.surjective'

added theorem continuous.surjective

added theorem continuous_on.surj_on_of_tendsto'

added theorem continuous_on.surj_on_of_tendsto

deleted theorem surjective_of_continuous'

deleted theorem surjective_of_continuous