Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-02 12:12 f3746ea6

View on Github →

chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives (#9502) In a future PR, I want to split all files in the special_functions folder to avoid importing calculus when not needed (the goal is to avoid importing it in the definition of lp_space in measure_theory). This PR changes the proofs of continuity of trigonometric functions.

Estimated changes

modified theorem complex.continuous_cos
modified theorem complex.continuous_cosh
modified theorem complex.continuous_sin
modified theorem complex.continuous_sinh
modified theorem real.continuous_cos
modified theorem real.continuous_cosh
modified theorem real.continuous_sin
modified theorem real.continuous_sinh