this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atBot atBot
rw [tendsto_comp_coe_Ioo_atBot this]
no goals
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
exact tendsto_tan_neg_pi_div_two
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atTop atTop
rw [tendsto_comp_coe_Ioo_atTop this]
no goals
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
exact tendsto_tan_pi_div_two