integral_radius_zero — Mathlib

English

If f and g agree almost everywhere on the circle { z : |z-c|=|R| }, then their circle integrals around C(c,R) are equal.

Русский

Если f и g согласованы почти всюду на окружности { z : |z-c|=|R| }, то их круговые интегралы вокруг C(c,R) равны.

LaTeX

$$$\\text{EqOn}(f,g,\\mathrm{sphere}\\;c\\;|R|) \\Rightarrow (\\oint z in C(c,R), f(z)) = (\\oint z in C(c,R), g(z))$$$

Lean4

@[simp]
theorem integral_radius_zero (f : ℂ → E) (c : ℂ) : (∮ z in C(c, 0), f z) = 0 := by
  simp +unfoldPartialApp [circleIntegral, const]

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