α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s ⊆ s ↔ ∀ (x : α), (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsClosed s ↔ ∀ (x : α), (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
rw [← closure_subset_iff_isClosed]
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ closure s ⊆ s ↔ ∀ (x : α), (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
refine' forall_congr' fun x => _
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : α) in 𝓝 x, y ∈ s) → x ∈ s
rw [mem_closure_iff_frequently]