α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K) ↔
    TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p univ
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => ↑(F i) a) (↑f) p
rw [tendsto_iff_forall_compact_tendstoUniformlyOn, ← tendstoUniformlyOn_univ]
no goals
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst✝ : CompactSpace α
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K) ↔
    TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p univ
exact ⟨fun h => h univ isCompact_univ, fun h K _hK => h.mono (subset_univ K)⟩