Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 05:51 cc32876d

View on Github →

chore(analysis/normed_space/basic): add continuous_at.inv', continuous.div etc (#4667) Also add continuous_on_(cos/sin).

Estimated changes

added theorem continuous.div
added theorem continuous.inv'
added theorem continuous_at.inv'
added theorem continuous_on.div
added theorem continuous_on.inv'
added theorem real.continuous_on_cos