α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousAt f x
rw [← continuousWithinAt_univ]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ∀ (u : Set (β × β)),
    u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∃ F, ContinuousWithinAt F univ 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 α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x
apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
L : ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∃ t, t ∈ 𝓝 x ∧ ∃ F, ContinuousAt F x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
⊢ ∀ (u : Set (β × β)),
    u ∈ 𝓤 β → ∃ t, t ∈ 𝓝[univ] x ∧ ∃ F, ContinuousWithinAt F univ x ∧ ∀ (y : α), y ∈ t → (f y, F y) ∈ u
simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L