α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49429
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49429
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ Prod.swap <$> 𝓤 α
rw [map_swap_eq_comap_swap]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.49429
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
exact tendsto_swap_uniformity.le_comap