continuousAt_tan — Mathlib

English

The tangent function is continuous at x if and only if cos x ≠ 0.

Русский

Функция тангенс непрерывна в точке x тогда и только тогда, когда cos x ≠ 0.

LaTeX

$$$ \text{ContinuousAt } \tan x \ iff \ cos x \neq 0. $$$

Lean4

theorem continuousAt_tan {x : ℝ} : ContinuousAt tan x ↔ cos x ≠ 0 :=
  by
  refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩
  exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _ (hc.norm.tendsto.mono_left inf_le_left)

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