Theorems · Theorem · functional analysis

Summable.multipliableLocallyUniformlyOn_nat_one_add

∀ {α : Type u_1} {K : Set α} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R] [CompleteSpace R]
  [inst_3 : TopologicalSpace α] [LocallyCompactSpace α] {f : ℕ → α → R},
  IsOpen K →
    ∀ {u : ℕ → ℝ},
      Summable u →
        (∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) →
          (∀ (n : ℕ), ContinuousOn (f n) K) → MultipliableLocallyUniformlyOn (fun n x => 1 + f n x) K

Defined in

Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedCommRingNormOneClassCompleteSpaceTopologicalSpaceLocallyCompactSpace