English
If S and T are compact subsets of ℝ, then the product S ×ℂ T is compact in ℂ.
Русский
Если S и T — компактные подмножества ℝ, то S ×ℂ T компактно в ℂ.
LaTeX
$$IsCompact(S) -> IsCompact(T) -> IsCompact(S \\times_{\\mathbb{C}} T)$$
Lean4
/-- Suppose that a function `f : ℂ → E` is *real* differentiable on a closed rectangle with opposite
corners at `z w : ℂ` and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then
the integral of `f` over the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle. -/
theorem integral_boundary_rect_of_differentiableOn_real (f : ℂ → E) (z w : ℂ)
(Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
(Hi : IntegrableOn (fun z => I • fderiv ℝ f z 1 - fderiv ℝ f z I) ([[z.re, w.re]] ×ℂ [[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)) =
∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • fderiv ℝ f (x + y * I) 1 - fderiv ℝ f (x + y * I) I :=
integral_boundary_rect_of_hasFDerivAt_real_off_countable f (fderiv ℝ f) z w ∅ countable_empty Hd.continuousOn
(fun x hx =>
Hd.hasFDerivAt <| by simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1)
Hi
