English
A real-differentiable function f: C → E is complex-differentiable at z iff it is real-differentiable at z and the derivative satisfies the CR relation.
Русский
Функция f: C → E комплексно дифференцируема в z тогда и только тогда, когда она вещественно дифференцируема в z и производная удовлетворяет CR-отношению.
LaTeX
$$DifferentiableAt ℂ f z \iff (DifferentiableAt Real f z) ∧ (fderiv Real f z I = I • fderiv Real f z 1)$$
Lean4
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals the real derivative.
-/
theorem complexOfReal_derivWithin (h₁ : DifferentiableWithinAt ℝ f s x)
(h₂ : fderivWithin ℝ f s x I = I • fderivWithin ℝ f s x 1) (hs : UniqueDiffWithinAt ℂ s x) :
derivWithin f s x = fderivWithin ℝ f s x 1 :=
HasDerivWithinAt.derivWithin (complexOfReal_hasDerivWithinAt h₁ h₂) hs
