English
On an open disk, being conservative and continuous is equivalent to differentiability on the disk.
Русский
На открытом диске свойство консервативности и непрерывности эквивалентно дифференцируемости на диске.
LaTeX
$$$\\text{On an open disk } \\operatorname{IsConservativeOn}(f,U) \\land \\operatorname{ContinuousOn}(f,U) \\iff \\operatorname{DifferentiableOn}(\\mathbb{C},f,U).$$$
Lean4
theorem isConservativeOn_and_continuousOn_iff_isDifferentiableOn {U : Set ℂ} (hU : IsOpen U) :
IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U :=
by
refine ⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩
obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz
have : DifferentiableOn ℂ f (ball z r) :=
(IsConservativeOn.isExactOn_ball (hf'.mono h₁) (hf.mono h₁)).differentiableOn isOpen_ball
apply (this z (mem_ball_self h₀)).mono_of_mem_nhdsWithin
exact mem_nhdsWithin.mpr ⟨ball z r, isOpen_ball, mem_ball_self h₀, inter_subset_left⟩
