continuous — Mathlib

English

For every natural k with k ≠ 1, the periodized Bernoulli function of order k is a continuous function on the unit circle.

Русский

Для каждого натурального k, отличного от 1, функция периодизированной Бернулли порядка k непрерывна на единичной окружности.

LaTeX

$$$\forall k \in \mathbb{N}, k \neq 1 \Rightarrow periodizedBernoulli(k) \in C(\mathbb{U}, \mathbb{C}).$$$

Lean4

theorem continuous {k : ℕ} (hk : k ≠ 1) : Continuous (periodizedBernoulli k) :=
  AddCircle.liftIco_zero_continuous (mod_cast (bernoulliFun_endpoints_eq_of_ne_one hk).symm)
    (Polynomial.continuous _).continuousOn

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