integral_congr — Mathlib

English

If f1 and f2 are codiscretely equivalent on the circle and R ≠ 0, then their circle integrals around C(c,R) are equal.

Русский

Если f1 и f2 эквипернимы по окружности в смысле codiscreteWithin и R ≠ 0, то их круговые интегралы вокруг C(c,R) равны.

LaTeX

$$$(f_1 =\\!\\!\\!\\!_{codiscreteWithin (\\mathrm{sphere}\\;c\\;|R|)} f_2) \\land (R \\neq 0) \\Rightarrow (\\oint z in C(c,R), f_1 z) = (\\oint z in C(c,R), f_2 z)$$$

Lean4

theorem integral_congr {f g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : EqOn f g (sphere c R)) :
    (∮ z in C(c, R), f z) = ∮ z in C(c, R), g z :=
  intervalIntegral.integral_congr fun θ _ => by simp only [h (circleMap_mem_sphere _ hR _)]

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