English
Let f1,f2: ℂ → E be functions and suppose f1 and f2 are equal on the circle { z : |z − c| = |R| } in the codiscreteWithin sense. Then CircleIntegrable f1 c R holds if and only if CircleIntegrable f2 c R holds.
Русский
Пусть f1,f2: ℂ → E. Если они равны на окружности $\\{ z : |z-c|=|R| \\}$ в смысле codiscreteWithin, то CircleIntegrable f1 c R эквивалентно CircleIntegrable f2 c R.
LaTeX
$$$(f_1 =\\!\\!\\!\\!_{codiscreteWithin(\\mathrm{sphere}\\;c\\;|R|)} f_2) \\Longrightarrow (CircleIntegrable f_1 c R \\;\\Leftrightarrow\\; CircleIntegrable f_2 c R)$$$
Lean4
/-- Circle integrability is invariant when functions change along discrete sets. -/
theorem circleIntegrable_congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E}
(hf : f₁ =ᶠ[codiscreteWithin (Metric.sphere c |R|)] f₂) : CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R :=
⟨(CircleIntegrable.congr_codiscreteWithin hf ·), (CircleIntegrable.congr_codiscreteWithin hf.symm ·)⟩
