continuous_sinc — Mathlib

English

The sinc function is continuous on the real line.

Русский

Функция sinc непрерывна на всей вещественной прямой.

LaTeX

$$$\operatorname{sinc} \in C(\mathbb{R})$$$

Lean4

/-- The function `sinc` is continuous. -/
@[fun_prop]
theorem continuous_sinc : Continuous sinc :=
  by
  refine continuous_iff_continuousAt.mpr fun x ↦ ?_
  rw [sinc_eq_dslope]
  by_cases hx : x = 0
  · simp [hx]
  · rw [continuousAt_dslope_of_ne hx]
    fun_prop

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