Theorems · Theorem · functional analysis

TendstoUniformlyOn.comp_cexp

∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ},
  TendstoUniformlyOn f g p K →
    BddAbove ((fun x => (g x).re) '' K) → TendstoUniformlyOn (fun x => Complex.exp ∘ f x) (Complex.exp ∘ g) p K

Defined in

Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Cited by

1 results in Mathlib

Foundations

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