conj_conj — Mathlib

English

If f is differentiable at conj z, then conj ∘ f ∘ conj is differentiable at z.

Русский

Если f дифференцируема в conj z, то conj ∘ f ∘ conj дифференцируема в z.

LaTeX

$$theorem conj_conj {f : 𝕜 → 𝕜} (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (conj ∘ f ∘ conj) (conj x) := hf.star_star$$

Lean4

/-- If `f` is differentiable at `conj z`, then `conj ∘ f ∘ conj` is differentiable at `z`. -/
theorem conj_conj {f : 𝕜 → 𝕜} (hf : DifferentiableAt 𝕜 f x) : DifferentiableAt 𝕜 (conj ∘ f ∘ conj) (conj x) :=
  hf.star_star

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