continuousOn_tan — Mathlib

English

The function tan is continuous on the set of real numbers where cos x ≠ 0.

Русский

Функция tan непрерывна на множестве {x ∈ ℝ : cos x ≠ 0}.

LaTeX

$$$ \operatorname{ContinuousOn}(\tan, \{ x \mid \cos x \neq 0 \}) $$$

Lean4

theorem continuousOn_tan : ContinuousOn tan {x | cos x ≠ 0} :=
  by
  suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
    by
    have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
    rwa [h_eq] at this
  exact continuousOn_sin.div continuousOn_cos fun x => id

Похожие утверждения