definition of tan

Stream: new members

[Benjamin Davidson]

Hi everyone, I wanted to solicit your advice on some ideas I had regarding improving the definition of the tan function, which can essentially be broken down into 3 parts:
1) Proving ∀ (x:ℝ), cos x = 0 ↔ (∃ (n:ℕ), x = n*π + π/2)
2) Improve the precision of statements that currently use {x // cos x ≠ 0} (i.e. the continuity of tan) so that they instead use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ
3) Write a proof for the derivative of tan using the lemma described in (1)
What do you think about this? I would appreciate any critiques or suggestions.
Thanks!

[Kevin Buzzard]

We have cos_eq_zero_iff in analysis.special_functions.trigonometric.

[Kevin Buzzard]

n needs to be an integer, not a natural. Note that you're not improving the definition of tan, indeed you're not changing the definition of tan at all, you're proving theorems about the definition.

[Heather Macbeth]

The current lemma for continuity of tan has the statement

lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x)

and I think Ben is asking, would it be an improvement to change this statement to use {x // ∃ (n:ℕ), x = n*π + π/2}ᶜ instead of {x // cos x ≠ 0} ?

[Eric Wieser]

Presumably there is already a lemma which can translate one .property into the other?

[Kevin Buzzard]

cos_eq_zero_iff