α : Type u
β : Type v
X : Type ?u.524771
ι : Type ?u.524774
inst✝¹ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bounded (f '' t)
α : Type u
β : Type v
X : Type ?u.524771
ι : Type ?u.524774
inst✝¹ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousAt f x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bounded (f '' t)
simp_rw [← continuousWithinAt_univ] at hf
no goals
α : Type u
β : Type v
X : Type ?u.524771
ι : Type ?u.524774
inst✝¹ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f univ x
⊢ ∃ t, k ⊆ t ∧ IsOpen t ∧ Bounded (f '' t)
simpa only [inter_univ] using
  exists_isOpen_bounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf