circleIntegral_def_Icc — Mathlib

English

If the circle has zero radius, the circle integral vanishes: ∮ z in C(c,0), f z = 0 for any f.

Русский

Если радиус окружности нулевой, круговой интеграл равен нулю: ∮ z in C(c,0), f(z) = 0 для любой f.

LaTeX

$$$\\oint z\\in C(c,0),\\;f(z) = 0$$$

Lean4

theorem circleIntegral_def_Icc (f : ℂ → E) (c : ℂ) (R : ℝ) :
    (∮ z in C(c, R), f z) = ∫ θ in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ) := by
  rw [circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le, Measure.restrict_congr_set Ioc_ae_eq_Icc]

Похожие утверждения