Commit 2021-02-15 21:04 65fe78ae
View on Github →feat(analysis/special_functions/trigonometric): add missing continuity attributes (#6236)
I added continuity attributes to lemmas about the continuity of trigonometric functions, e.g. continuous_sin, continuous_cos, continuous_tan, etc. This came up in this Zulip conversation
I also added real.continuous_tan.