analyticOnNhd_sin — Mathlib

English

sin is analytic on a neighborhood of every point, i.e., analytic on nhds neighborhoods.

Русский

sin аналитична в окрестности любой точки, то есть аналитична в окрестностях nhds.

LaTeX

$$$$\forall x, \; \text{AnalyticOnNhd}(\mathbb{C}, \sin, x).$$$$

Lean4

/-- The function `Complex.sin` is complex analytic. -/
theorem analyticOnNhd_sin {s : Set ℂ} : AnalyticOnNhd ℂ sin s := fun _ _ ↦ analyticAt_sin

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