case a
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58422
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ comap (Prod.mk x) (𝓤 α)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58422
inst✝ : UniformSpace α
x : α
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α)
ext s
no goals
case a
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58422
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ comap (Prod.mk x) (𝓤 α)
rw [mem_nhds_uniformity_iff_right, mem_comap_prod_mk]