uniformCauchySeqOnFilter_of_deriv

English

If a sequence of differentiable maps on a ball has uniform Cauchy behaviour for derivatives, then the maps form a uniform Cauchy sequence on that ball.

Русский

Если последовательность отображений на шаре имеет равномерно сходящуюся производную, то сами отображения образуют равномерно сходящуюся последовательность на шаре.

LaTeX

$$$\\forall r>0, \\; \\text{UniformCauchySeqOnBallOfFDeriv}(f', l, \\mathrm{Ball}(x,r)) \\Rightarrow \\cdots$$$

Lean4

theorem uniformCauchySeqOnFilter_of_deriv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
    (hf : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2) (hfg : Cauchy (map (fun n => f n x) l)) :
    UniformCauchySeqOnFilter f l (𝓝 x) :=
  by
  simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
  exact uniformCauchySeqOnFilter_of_fderiv hf'.one_smulRight hf hfg

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