α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
⊢ IsClosed (⋂ (i : α → Prop), {x | (¬∀ᶠ (x : α) in 𝓝 x, i x) ∨ ∃ᶠ (x : α) in f, i x})
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
⊢ IsClosed {x | ClusterPt x f}
simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or]
case refine'_1
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets (𝓝 x) {x | (fun x => p x) x}

case refine'_2
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets f {x | (fun x => ¬(fun x => p x) x) x}
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
⊢ IsClosed (⋂ (i : α → Prop), {x | (¬∀ᶠ (x : α) in 𝓝 x, i x) ∨ ∃ᶠ (x : α) in f, i x})
refine' isClosed_iInter fun p => IsClosed.union _ _ <;> apply isClosed_compl_iff.2
no goals
case refine'_1
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets (𝓝 x) {x | (fun x => p x) x}

case refine'_2
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
p : α → Prop
⊢ IsOpen fun x => sets f {x | (fun x => ¬(fun x => p x) x) x}
exacts [isOpen_setOf_eventually_nhds, isOpen_const]