α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58600
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (a : α), a ∈ s → s ∈ comap (Prod.mk a) (𝓤 α)) ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58600
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity]
no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.58600
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (a : α), a ∈ s → s ∈ comap (Prod.mk a) (𝓤 α)) ↔ ∀ (x : α), x ∈ s → ∃ V, V ∈ 𝓤 α ∧ ball x V ⊆ s
rfl