isExactOn_ball — Mathlib

English

If a function is differentiable on a disk, then it has a primitive on that disk.

Русский

Если функция дифференцируема на диске, то она имеет примитив на этом диске.

LaTeX

$$$\\text{If } f \\text{ is differentiable on } \\mathrm{ball}(c,r) \\text{ then } IsExactOn(f, \\mathrm{ball}(c,r)).$$$

Lean4

/-- **Morera's theorem for a disk** On a disk, a holomorphic function has primitives. -/
theorem _root_.DifferentiableOn.isExactOn_ball (hf : DifferentiableOn ℂ f (ball c r)) : IsExactOn f (ball c r) :=
  hf.isConservativeOn.isExactOn_ball hf.continuousOn

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