α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
h : ∀ (a : α), a ∈ s → ¬ClusterPt a f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
h :
  ∀ {ι : Type u} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → (s ⊆ ⋃ (i : ι), U i) → ∃ t, s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
⊢ ∃ a, a ∈ s ∧ ClusterPt a f
contrapose! h
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
h : ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen i) ∧ iᶜ ∈ f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
h : ∀ (a : α), a ∈ s → ¬ClusterPt a f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
  (nhds_basis_opens _).disjoint_iff_left] at h
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
h : ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen i) ∧ iᶜ ∈ f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
choose U hU hUf using h
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ False
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
⊢ Exists fun {ι} =>
    ∃ U, (∀ (i : ι), IsOpen (U i)) ∧ (s ⊆ ⋃ (i : ι), U i) ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i
refine ⟨s, U, fun x => (hU x).2, fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1⟩, fun t ht => ?_⟩
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ sᶜ ∈ f
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ False
refine compl_not_mem (le_principal_iff.1 hfs) ?_
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ (⋂ (i : ↑s) (_ : i ∈ t), U iᶜ) ⊆ sᶜ
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ sᶜ ∈ f
refine mem_of_superset ((biInter_finset_mem t).2 fun x _ => hUf x) ?_
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U iᶜᶜ
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ (⋂ (i : ↑s) (_ : i ∈ t), U iᶜ) ⊆ sᶜ
rw [subset_compl_comm, compl_iInter₂]
no goals
α : Type u
β : Type v
ι : Type ?u.25315
π : ι → Type ?u.25320
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : Filter α
hf : NeBot f
hfs : f ≤ 𝓟 s
U : ↑s → Set α
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)
hUf : ∀ (x : ↑s), U xᶜ ∈ f
t : Finset ↑s
ht : s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U i
⊢ s ⊆ ⋃ (i : ↑s) (_ : i ∈ t), U iᶜᶜ
simpa only [compl_compl]