continuousAt_tan — Mathlib

English

Let x be a complex number. The tangent function tan has a continuous at x exactly when cos x ≠ 0.

Русский

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

LaTeX

$$$$\forall x \in \mathbb{C}, \; \mathrm{ContinuousAt}(\tan, x) \iff \cos x \neq 0.$$$$

Lean4

@[simp]
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_norm_tan_of_cos_eq_zero h₀) _ (hc.norm.tendsto.mono_left inf_le_left)

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