α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
⊢ IsCompact (insert b (range f))
intro l hne hle
case pos
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ClusterPt b l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l

case neg
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ¬ClusterPt b l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
by_cases hb : ClusterPt b l
case neg
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ∃ x h x_1 h, Disjoint x x_1
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
case neg
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ¬ClusterPt b l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
simp only [clusterPt_iff, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hb
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
case neg
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ∃ x h x_1 h, Disjoint x x_1
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
rcases hb with ⟨s, hsb, t, htl, hd⟩
case neg.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
rcases mem_cocompact.1 (hf hsb) with ⟨K, hKc, hKs⟩
case neg.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
case neg.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
have : f '' K ∈ l := by
  filter_upwards [htl, le_principal_iff.1 hle]with y hyt hyf
  rcases hyf with (rfl | ⟨x, rfl⟩)
  exacts [(hd.le_bot ⟨mem_of_mem_nhds hsb, hyt⟩).elim,
    mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : β
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
case neg.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
y : β
hy : y ∈ f '' K
hyl : ClusterPt y l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩
no goals
case pos
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
hb : ClusterPt b l
⊢ ∃ a, a ∈ insert b (range f) ∧ ClusterPt a l
exact ⟨b, Or.inl rfl, hb⟩
case h
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : β
hyt : y ∈ t
hyf : y ∈ insert b (range f)
⊢ y ∈ f '' K
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ f '' K ∈ l
filter_upwards [htl, le_principal_iff.1 hle]with y hyt hyf
case h.inl
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
hfc : Continuous f
l : Filter β
hne : NeBot l
s t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : β
hyt : y ∈ t
hf : Tendsto f (cocompact α) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsb : s ∈ 𝓝 y
⊢ y ∈ f '' K

case h.inr.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
x : α
hyt : f x ∈ t
⊢ f x ∈ f '' K
case h
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : β
hyt : y ∈ t
hyf : y ∈ insert b (range f)
⊢ y ∈ f '' K
rcases hyf with (rfl | ⟨x, rfl⟩)
no goals
case h.inl
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
hfc : Continuous f
l : Filter β
hne : NeBot l
s t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : β
hyt : y ∈ t
hf : Tendsto f (cocompact α) (𝓝 y)
hle : l ≤ 𝓟 (insert y (range f))
hsb : s ∈ 𝓝 y
⊢ y ∈ f '' K

case h.inr.intro
α : Type u
β : Type v
ι : Type ?u.47904
π : ι → Type ?u.47909
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
f : α → β
b : β
hf : Tendsto f (cocompact α) (𝓝 b)
hfc : Continuous f
l : Filter β
hne : NeBot l
hle : l ≤ 𝓟 (insert b (range f))
s : Set β
hsb : s ∈ 𝓝 b
t : Set β
htl : t ∈ l
hd : Disjoint s t
K : Set α
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
x : α
hyt : f x ∈ t
⊢ f x ∈ f '' K
exacts [(hd.le_bot ⟨mem_of_mem_nhds hsb, hyt⟩).elim,
  mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]