Theorems · Theorem · global analysis

hasDerivAt_of_tendstoLocallyUniformlyOn

∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g : 𝕜 → G} {f' : ι → 𝕜 → G} {g' : 𝕜 → G}
  {x : 𝕜} [IsRCLikeNormedField 𝕜] [l.NeBot] {s : Set 𝕜},
  IsOpen s →
    TendstoLocallyUniformlyOn f' g' l s →
      (∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x

Defined in

Mathlib.Analysis.Calculus.UniformLimitsDeriv

Cited by

3 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceIsRCLikeNormedFieldFilter.NeBot