Theorems · Theorem · global analysis

hasFDerivAt_of_tendstoLocallyUniformlyOn

∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {g : E → G} {f' : ι → E → E →L[𝕜] G}
  {g' : E → E →L[𝕜] G} {x : E} [l.NeBot] {s : Set E},
  IsOpen s →
    TendstoLocallyUniformlyOn f' g' l s →
      (∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasFDerivAt g (g' x) x

Defined in

Mathlib.Analysis.Calculus.UniformLimitsDeriv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNontriviallyNormedFieldIsRCLikeNormedFieldNormedSpaceNormedAddCommGroupNormedSpaceFilter.NeBot