English
The tangent function is continuous on the open interval (-π/2, π/2).
Русский
Тангенс непрерывен на открытом интервале (-π/2, π/2).
LaTeX
$$$ \operatorname{ContinuousOn}(\tan, \mathrm{Ioo}\left(-\frac{\pi}{2}, \frac{\pi}{2}\right)) $$$
Lean4
theorem continuousOn_tan_Ioo : ContinuousOn tan (Ioo (-(π / 2)) (π / 2)) :=
by
refine ContinuousOn.mono continuousOn_tan fun x => ?_
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne]
rw [cos_eq_zero_iff]
rintro hx_gt hx_lt ⟨r, hxr_eq⟩
rcases le_or_gt 0 r with h | h
· rw [lt_iff_not_ge] at hx_lt
refine hx_lt ?_
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_left₀ (half_pos pi_pos)]
simp [h]
· rw [lt_iff_not_ge] at hx_gt
refine hx_gt ?_
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, neg_mul_eq_neg_mul, mul_le_mul_iff_left₀ (half_pos pi_pos)]
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]
· norm_num
assumption_mod_cast
· exact zero_lt_two
