circleIntegrable — Mathlib

English

If R ≥ 0 and f is continuous on the circle, then f is circle-integrable on that circle.

Русский

Если R ≥ 0 и f непрерывна на окружности, то она кругово интегрируема вдоль этой окружности.

LaTeX

$$$R\\ge 0 \\;\\wedge\\; ContinuousOn(f,\\mathrm{sphere}\\;c\\;R) \\Rightarrow CircleIntegrable f c R$$$

Lean4

theorem circleIntegrable {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hf : ContinuousOn f (sphere c R)) :
    CircleIntegrable f c R :=
  ContinuousOn.circleIntegrable' <| (abs_of_nonneg hR).symm ▸ hf

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