contDiff_circleMap — Mathlib

English

For every c ∈ ℂ and R ∈ ℝ, circleMap c R is continuously differentiable of order n for any n (i.e., ContDiff ℝ n circleMap c R).

Русский

Для любых c ∈ ℂ и R ∈ ℝ отображение circleMap c R непрерывно дифференцируемо высших порядков (ContDiff).

LaTeX

$$$\forall n\,\ ContDiff\ _\mathbb{R}\ n\ (circleMap(c,R)). $$$

Lean4

/-- The circleMap is continuously differentiable. -/
theorem contDiff_circleMap (c : ℂ) (R : ℝ) {n : WithTop ℕ∞} : ContDiff ℝ n (circleMap c R) :=
  (analyticOnNhd_circleMap c R).contDiff

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