Skip to content

Commit

Permalink
doc(Analysis.Complex.CauchyIntegral): add missing word (#9211)
Browse files Browse the repository at this point in the history
Replace "continuous the closed annulus" with " continuous on the closed annulus"
  • Loading branch information
faenuccio committed Dec 22, 2023
1 parent 623cc31 commit e885101
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions Mathlib/Analysis/Complex/CauchyIntegral.lean
Original file line number Diff line number Diff line change
Expand Up @@ -293,10 +293,10 @@ theorem integral_boundary_rect_eq_zero_of_differentiableOn (f : ℂ → E) (z w
inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)
#align complex.integral_boundary_rect_eq_zero_of_differentiable_on Complex.integral_boundary_rect_eq_zero_of_differentiableOn

/-- If `f : ℂ → E` is continuous the closed annulus `r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`, and is complex
differentiable at all but countably many points of its interior, then the integrals of
`f z / (z - c)` (formally, `(z - c)⁻¹ • f z`) over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are
equal to each other. -/
/-- If `f : ℂ → E` is continuous on the closed annulus `r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`,
and is complex differentiable at all but countably many points of its interior,
then the integrals of `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`)
over the circles `‖z - c‖ = r` and `‖z - c‖ = R` are equal to each other. -/
theorem circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable {c : ℂ}
{r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : Set ℂ} (hs : s.Countable)
(hc : ContinuousOn f (closedBall c R \ ball c r))
Expand Down

0 comments on commit e885101

Please sign in to comment.