α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
⊢ IsCompact (s ∩ t)
intro f hnf hstf
case intro.intro
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
a : α
hsa : a ∈ s
ha : ClusterPt a f
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
obtain ⟨a, hsa, ha⟩ : ∃ a ∈ s, ClusterPt a f :=
  hs (le_trans hstf (le_principal_iff.2 (inter_subset_left _ _)))
case intro.intro
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
a : α
hsa : a ∈ s
ha : ClusterPt a f
this : a ∈ t
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
case intro.intro
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
a : α
hsa : a ∈ s
ha : ClusterPt a f
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
have : a ∈ t := ht.mem_of_nhdsWithin_neBot <|
  ha.mono <| le_trans hstf (le_principal_iff.2 (inter_subset_right _ _))
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.6738
π : ι → Type ?u.6743
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsClosed t
f : Filter α
hnf : NeBot f
hstf : f ≤ 𝓟 (s ∩ t)
a : α
hsa : a ∈ s
ha : ClusterPt a f
this : a ∈ t
⊢ ∃ a, a ∈ s ∩ t ∧ ClusterPt a f
exact ⟨a, ⟨hsa, this⟩, ha⟩