English
The ball around 1 of radius 1 is contained in the slit plane (same as 47341).
Русский
Шар вокруг точки 1 радиуса 1 содержится в слитной плоскости.
LaTeX
$$Ball(1,1) \\subset \\text{slitPlane}$$
Lean4
/-- **Cauchy-Goursat theorem for a rectangle**: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if `f` is continuous on a closed
rectangle and is complex differentiable on the corresponding open rectangle, then its integral over
the boundary of the rectangle equals zero. -/
theorem integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn (f : ℂ → E) (z w : ℂ)
(Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
(Hd : DifferentiableOn ℂ f (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im))) :
(∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
I • (∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
I • (∫ y : ℝ in z.im..w.im, f (re z + y * I)) =
0 :=
integral_boundary_rect_eq_zero_of_differentiable_on_off_countable f z w ∅ countable_empty Hc fun _x hx =>
Hd.differentiableAt <| (isOpen_Ioo.reProdIm isOpen_Ioo).mem_nhds hx.1
