α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n 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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
⊢ TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p t
intro u hu x hx
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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n 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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩
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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n 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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
have : g ⁻¹' a ∈ 𝓝[t] x :=
  (cg x hx).preimage_mem_nhdsWithin' (nhdsWithin_mono (g x) hg.image_subset ha)
no goals
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 α
inst✝ : TopologicalSpace γ
t : Set γ
h : TendstoLocallyUniformlyOn F f p s
g : γ → α
hg : MapsTo g t s
cg : ContinuousOn g t
u : Set (β × β)
hu : u ∈ 𝓤 β
x : γ
hx : x ∈ t
a : Set α
ha : a ∈ 𝓝[s] g x
H : ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ a → (f y, F n y) ∈ u
this : g ⁻¹' a ∈ 𝓝[t] x
⊢ ∃ t_1, t_1 ∈ 𝓝[t] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : γ), y ∈ t_1 → ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
exact ⟨g ⁻¹' a, this, H.mono fun n hn y hy => hn _ hy⟩