α : Type u
β : Type v
ι : Type ?u.93052
π : ι → Type ?u.93057
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
f : α → β
hf : Inducing f
s : Set α
hs : IsCompact (f '' s)
F : Filter α
F_ne_bot : NeBot F
F_le : F ≤ 𝓟 s
⊢ ∃ a, a ∈ s ∧ ClusterPt a F
α : Type u
β : Type v
ι : Type ?u.93052
π : ι → Type ?u.93057
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
f : α → β
hf : Inducing f
s : Set α
⊢ IsCompact (f '' s) ↔ IsCompact s
refine ⟨fun hs F F_ne_bot F_le => ?_, fun hs => hs.image hf.continuous⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.93052
π : ι → Type ?u.93057
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
f : α → β
hf : Inducing f
s : Set α
hs : IsCompact (f '' s)
F : Filter α
F_ne_bot : NeBot F
F_le : F ≤ 𝓟 s
x : α
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ a, a ∈ s ∧ ClusterPt a F
α : Type u
β : Type v
ι : Type ?u.93052
π : ι → Type ?u.93057
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
f : α → β
hf : Inducing f
s : Set α
hs : IsCompact (f '' s)
F : Filter α
F_ne_bot : NeBot F
F_le : F ≤ 𝓟 s
⊢ ∃ a, a ∈ s ∧ ClusterPt a F
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
  hs ((map_mono F_le).trans_eq map_principal)
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.93052
π : ι → Type ?u.93057
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
f : α → β
hf : Inducing f
s : Set α
hs : IsCompact (f '' s)
F : Filter α
F_ne_bot : NeBot F
F_le : F ≤ 𝓟 s
x : α
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ a, a ∈ s ∧ ClusterPt a F
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩