α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.77663
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖)
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.77663
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
rw [uniformContinuous_iff]
no goals
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.77663
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖)
exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq