α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ uniformSpace α β ≤ UniformSpace.comap (fun g => ↑ofFun (g ∘ f)) (uniformSpace γ β)
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ UniformContinuous fun g => ↑ofFun (g ∘ f)
rw [uniformContinuous_iff]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ 𝓤 (α →ᵤ β) ≤ comap (Prod.map (fun g => g ∘ f) fun g => g ∘ f) (𝓤 (γ →ᵤ β))
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ uniformSpace α β ≤ UniformSpace.comap (fun g => ↑ofFun (g ∘ f)) (uniformSpace γ β)
change
  𝓤 (α →ᵤ β) ≤ (𝓤 (γ →ᵤ β)).comap (Prod.map (fun g : α →ᵤ β => g ∘ f) fun g : α →ᵤ β => g ∘ f)
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i, i ∈ 𝓤 β ∧ UniformFun.gen α β i ⊆ (Prod.map (fun g => g ∘ f) fun g => g ∘ f) ⁻¹' UniformFun.gen γ β i'
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ 𝓤 (α →ᵤ β) ≤ comap (Prod.map (fun g => g ∘ f) fun g => g ∘ f) (𝓤 (γ →ᵤ β))
rw [(UniformFun.hasBasis_uniformity α β).le_basis_iff
    ((UniformFun.hasBasis_uniformity γ β).comap _)]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.43134
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i, i ∈ 𝓤 β ∧ UniformFun.gen α β i ⊆ (Prod.map (fun g => g ∘ f) fun g => g ∘ f) ⁻¹' UniformFun.gen γ β i'
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩