exact (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).symm
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ (∀ s ⊆ U,
      IsCompact s →
        TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) ∘ F)
          ((UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) f) l s) ↔
    TendstoLocallyUniformlyOn F f l U
no goals