α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
⊢ Tendsto F p (𝓝 f)
rw [tendsto_iff_forall_compact_tendstoUniformlyOn]
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
⊢ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
intro K hK
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]
no goals
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
exact h.tendstoLocallyUniformlyOn