Commit 2020-12-22 17:05 7c2f1663

chore(analysis/special_functions/trigonometric): review continuity of tan (#5429)

• prove that tan is discontinuous at x whenever cos x = 0;
• turn continuous_at_tan and differentiable_at_tan into iff lemmas;
• reformulate various lemmas in terms of cos x = 0 instead of ∃ k, x = ...;