α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
hf : Tendsto f cofinite (𝓝 a)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert a (range f))
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
hf : Tendsto f cofinite (𝓝 a)
⊢ IsCompact (insert a (range f))
letI : TopologicalSpace ι := ⊥
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
hf : Tendsto f cofinite (𝓝 a)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ IsCompact (insert a (range f))
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
hf : Tendsto f cofinite (𝓝 a)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert a (range f))
haveI h : DiscreteTopology ι := ⟨rfl⟩
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 a)
h : DiscreteTopology ι
⊢ IsCompact (insert a (range f))
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
hf : Tendsto f cofinite (𝓝 a)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ IsCompact (insert a (range f))
rw [← cocompact_eq_cofinite ι] at hf
no goals
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.50005
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : ι → α
a : α
this : TopologicalSpace ι := ⊥
hf : Tendsto f (cocompact ι) (𝓝 a)
h : DiscreteTopology ι
⊢ IsCompact (insert a (range f))
exact hf.isCompact_insert_range_of_cocompact continuous_of_discreteTopology