circleIntegrable' — Mathlib

English

If f is continuous on the circle { z : |z − c| = |R| }, then f is circle-integrable on that circle.

Русский

Если функция f непрерывна на окружности { z : |z − c| = |R| }, то она кругово интегрируема вдоль этой окружности.

LaTeX

$$$\\text{ContinuousOn}(f,\\mathrm{sphere}\\;c\\;|R|) \\Rightarrow CircleIntegrable f c R$$$

Lean4

theorem circleIntegrable' {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ContinuousOn f (sphere c |R|)) : CircleIntegrable f c R :=
  (hf.comp_continuous (continuous_circleMap _ _) (circleMap_mem_sphere' _ _)).intervalIntegrable _ _

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