ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : U ∈ 𝓝 (F i x₀)
⊢ U ∈ map (F i) (𝓝 x₀)
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
⊢ ContinuousAt (F i) x₀
intro U hU
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : ∃ V, V ∈ 𝓤 α ∧ ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : U ∈ 𝓝 (F i x₀)
⊢ U ∈ map (F i) (𝓝 x₀)
rw [UniformSpace.mem_nhds_iff] at hU
case intro.intro
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
V : Set (α × α)
hV₁ : V ∈ 𝓤 α
hV₂ : ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
hU : ∃ V, V ∈ 𝓤 α ∧ ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
rcases hU with ⟨V, hV₁, hV₂⟩
no goals
case intro.intro
ι : Type u_1
κ : Type ?u.28015
X : Type u_2
Y : Type ?u.28021
Z : Type ?u.28024
α : Type u_3
β : Type ?u.28030
γ : Type ?u.28033
𝓕 : Type ?u.28036
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
i : ι
U : Set α
V : Set (α × α)
hV₁ : V ∈ 𝓤 α
hV₂ : ball (F i x₀) V ⊆ U
⊢ U ∈ map (F i) (𝓝 x₀)
exact mem_map.mpr (mem_of_superset (h V hV₁) fun x hx => hV₂ (hx i))