case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.85860
inst✝ : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure s ↔ (x, y) ∈ ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ s ○ V
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.85860
inst✝ : UniformSpace α
s : Set (α × α)
⊢ closure s = ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ s ○ V
ext ⟨x, y⟩
no goals
case h.mk
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.85860
inst✝ : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure s ↔ (x, y) ∈ ⋂ (V : Set (α × α)) (_ : V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}), V ○ s ○ V
simp (config := { contextual := true }) only
  [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
    and_imp, mem_comp_comp, exists_prop, ← mem_inter_iff, inter_comm, Set.Nonempty]