F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ ∀ (a : α →ᵇ β), 𝓝 a = comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) a))
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ Inducing (↑UniformFun.ofFun ∘ FunLike.coe)
rw [inducing_iff_nhds]
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) f))
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x : α
C : ℝ
⊢ ∀ (a : α →ᵇ β), 𝓝 a = comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) a))
refine' fun f => eq_of_forall_le_iff fun l => _
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i => ↑(id i)) (↑f) l ↔
    TendstoUniformly (↑UniformFun.ofFun ∘ FunLike.coe) ((↑UniformFun.ofFun ∘ FunLike.coe) f) l
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (↑UniformFun.ofFun ∘ FunLike.coe) (𝓝 ((↑UniformFun.ofFun ∘ FunLike.coe) f))
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
  UniformFun.tendsto_iff_tendstoUniformly]
no goals
F : Type ?u.310540
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i => ↑(id i)) (↑f) l ↔
    TendstoUniformly (↑UniformFun.ofFun ∘ FunLike.coe) ((↑UniformFun.ofFun ∘ FunLike.coe) f) l
rfl