α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
⊢ ContinuousOn f s
refine continuousOn_of_locally_uniform_approx_of_continuousWithinAt fun x hx u hu => ?_
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
rcases h u hu x hx with ⟨t, ht, H⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
rcases (hc.and H).exists with ⟨n, hFc, hF⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝¹ : TopologicalSpace α
h : TendstoLocallyUniformlyOn F f p s
hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s
inst✝ : NeBot p
x : α
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set α
ht : t ∈ 𝓝[s] x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
n : ι
hFc : ContinuousOn (F n) s
hF : ∀ (y : α), y ∈ t → (f y, F n y) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ F, ContinuousWithinAt F s x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
exact ⟨t, ht, ⟨F n, hFc.continuousWithinAt hx, hF⟩⟩