English
A subset s of the sphere of radius r is contained in slitPlane iff -r is not in s.
Русский
Подмножество s сферы радиуса r входит в слитную плоскость тогда и только тогда, когда -r не принадлежит s.
LaTeX
$$s ⊆ \\text{sphere}(0,r) → (s ⊆ \\text{slitPlane} \\iff -r \\notin s)$$
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 at all but countably many points of the corresponding open
rectangle, then its integral over the boundary of the rectangle equals zero. -/
theorem integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ → E) (z w : ℂ) (s : Set ℂ)
(hs : s.Countable) (Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
(Hd :
∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x) :
(∫ 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 :=
by
refine
(integral_boundary_rect_of_hasFDerivAt_real_off_countable f (fun z => (fderiv ℂ f z).restrictScalars ℝ) z w s hs
Hc (fun x hx => (Hd x hx).hasFDerivAt.restrictScalars ℝ) ?_).trans
?_ <;>
simp
