differentiable_circleMap — Mathlib

English

For every c ∈ ℂ and R ∈ ℝ, the function θ ↦ circleMap(c, R, θ) is differentiable for all θ ∈ ℝ.

Русский

Пусть c ∈ ℂ и R ∈ ℝ. Функция θ ↦ circleMap(c, R, θ) дифференцируема для всех θ ∈ ℝ.

LaTeX

$$$\forall \theta \in \mathbb{R},\; \text{the derivative of } circleMap(c,R,\theta) \text{ with respect to } \theta \text{ exists}. $$$

Lean4

theorem differentiable_circleMap (c : ℂ) (R : ℝ) : Differentiable ℝ (circleMap c R) := fun θ =>
  (hasDerivAt_circleMap c R θ).differentiableAt

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