[Merged by Bors] - chore(analysis/special_functions/trigonometric): review, golf #5392
Conversation
urkud
commented
Dec 16, 2020
urkud
commented
| @@ -1068,15 +1067,16 @@ lemma cos_eq_one_iff (x : ℝ) : cos x = 1 ↔ ∃ n : ℤ, (n : ℝ) * (2 * π) | |||
| exact absurd h (by norm_num))⟩, | |||
| λ ⟨n, hn⟩, hn ▸ cos_int_mul_two_pi _⟩ | |||
|
|
|||
| lemma cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x < 2 * π) : cos x = 1 ↔ x = 0 := | |||
| ⟨λ h, let ⟨n, hn⟩ := (cos_eq_one_iff x).1 h in | |||
| lemma cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -(2 * π) < x) (hx₂ : x < 2 * π) : | |||
There was a problem hiding this comment.
Is this one worth stating in terms of Ioo too?
There was a problem hiding this comment.
Do we often have x ∈ Ioo (-(2 * π)) (2 * π) as an assumption?
There was a problem hiding this comment.
No, but presumably if there's an assumption about a smaller range then there is api to expand it to this larger one?
There was a problem hiding this comment.
There is set.Ioo_subset_Ioo, but I'm not sure it's so useful, because checking that an interval is contained in another interval itself reduces to checking inequalities. We can leave it for now, and add variants for specific numeric intervals if anyone ever uses this fact there.
There was a problem hiding this comment.
This looks good to me, @eric-wieser are you happy to leave out the variant lemma?
|
I don't really care, just curious if someone else did |
|
bors r+ |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
