α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58164
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α ↔ {p | p.snd = x → p.fst ∈ s} ∈ Prod.swap <$> 𝓤 α
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58164
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.snd = x → p.fst ∈ s} ∈ 𝓤 α
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58164
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.fst = x → p.snd ∈ s} ∈ 𝓤 α ↔ {p | p.snd = x → p.fst ∈ s} ∈ Prod.swap <$> 𝓤 α
rfl