α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
⊢ TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : Tendsto F p (𝓝 f)
⊢ TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
rw [tendsto_iff_forall_compact_tendstoUniformlyOn] at h
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (↑f y, (fun i a => ↑(F i) a) n y) ∈ V
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
⊢ TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p
intro V hV x
case intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (↑f y, (fun i a => ↑(F i) a) n y) ∈ V
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (↑f y, (fun i a => ↑(F i) a) n y) ∈ V
obtain ⟨n, hn₁, hn₂⟩ := hα x
no goals
case intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V✝ : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
hα : ∀ (x : α), ∃ n, IsCompact n ∧ n ∈ 𝓝 x
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (↑f y, (fun i a => ↑(F i) a) n y) ∈ V
exact ⟨n, hn₂, h n hn₁ V hV⟩