Real coordinate slices of complex-domain functions

A real Fréchet derivative determines the derivatives of the horizontal and vertical slices.

theorem HasFDerivAt.hasDerivAt_re_slice {P : ℂ → ℝ} {L : ℂ →L[ℝ] ℝ} {z : ℂ} (hP : HasFDerivAt P L z) : HasDerivAt (fun (x : ℝ) => P { re := x, im := z.im }) (L 1) z.re

A real Fréchet derivative gives the derivative of the horizontal coordinate slice.

theorem HasFDerivAt.hasDerivAt_im_slice {P : ℂ → ℝ} {L : ℂ →L[ℝ] ℝ} {z : ℂ} (hP : HasFDerivAt P L z) : HasDerivAt (fun (y : ℝ) => P { re := z.re, im := y }) (L Complex.I) z.im

A real Fréchet derivative gives the derivative of the vertical coordinate slice.