α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s = 𝓝ˢ t ↔ s = t
simp_rw [le_antisymm_iff]
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s t : Set α
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s
exact and_congr nhdsSet_le_iff nhdsSet_le_iff