α : Type u_1
β : Type u_2
γ : Type ?u.27728
ι : Type ?u.27731
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β
α : Type u_1
β : Type u_2
γ : Type ?u.27728
ι : Type ?u.27731
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ↑toFun)
change _ ≤ _
α : Type u_1
β : Type u_2
γ : Type ?u.27728
ι : Type ?u.27731
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i,
        i ∈ 𝓤 β ∧
          UniformFun.gen α β i ⊆
            (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) ⁻¹' id i'
α : Type u_1
β : Type u_2
γ : Type ?u.27728
ι : Type ?u.27731
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β
rw [map_le_iff_le_comap,
  (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.27728
ι : Type ?u.27731
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i,
        i ∈ 𝓤 β ∧
          UniformFun.gen α β i ⊆
            (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) ⁻¹' id i'
exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩