feat(topology/metric_space/basic): a continuous function is bounded o…

…n a neighborhood of a compact set (#17457)

src/topology/metric_space/basic.lean

@@ -561,6 +561,13 @@ theorem closed_ball_subset_ball (h : ε₁ < ε₂) :
   closed_ball x ε₁ ⊆ ball x ε₂ :=
 λ y (yh : dist y x ≤ ε₁), lt_of_le_of_lt yh h
 
+lemma closed_ball_subset_ball' (h : ε₁ + dist x y < ε₂) :
+  closed_ball x ε₁ ⊆ ball y ε₂ :=
+λ z hz, calc
+  dist z y ≤ dist z x + dist x y : dist_triangle _ _ _
+  ... ≤ ε₁ + dist x y : add_le_add_right hz _
+  ... < ε₂ : h
+
 lemma dist_le_add_of_nonempty_closed_ball_inter_closed_ball
   (h : (closed_ball x ε₁ ∩ closed_ball y ε₂).nonempty) :
   dist x y ≤ ε₁ + ε₂ :=
@@ -2275,6 +2282,44 @@ lemma bounded_range_of_tendsto (u : ℕ → α) {x : α} (hu : tendsto u at_top
   bounded (range u) :=
 hu.cauchy_seq.bounded_range
 
+/-- If a function is continuous at every point of a compact set `k`, then it is bounded on
+some open neighborhood of `k`. -/
+lemma exists_is_open_bounded_image_of_is_compact_of_forall_continuous_at
+  [topological_space β] {k : set β} {f : β → α}
+  (hk : is_compact k) (hf : ∀ x ∈ k, continuous_at f x) :
+  ∃ t, k ⊆ t ∧ is_open t ∧ bounded (f '' t) :=
+begin
+  apply hk.induction_on,
+  { refine ⟨∅, subset.refl _, is_open_empty, by simp only [image_empty, bounded_empty]⟩ },
+  { rintros s s' hss' ⟨t, s't, t_open, t_bounded⟩,
+    exact ⟨t, hss'.trans s't, t_open, t_bounded⟩ },
+  { rintros s s' ⟨t, st, t_open, t_bounded⟩ ⟨t', s't', t'_open, t'_bounded⟩,
+    refine ⟨t ∪ t', union_subset_union st s't', t_open.union t'_open, _⟩,
+    rw image_union,
+    exact t_bounded.union t'_bounded },
+  { assume x hx,
+    have A : ball (f x) 1 ∈ 𝓝 (f x), from ball_mem_nhds _ zero_lt_one,
+    have B : f ⁻¹' (ball (f x) 1) ∈ 𝓝 x, from hf x hx A,
+    obtain ⟨u, uf, u_open, xu⟩ : ∃ (u : set β) (H : u ⊆ f ⁻¹' ball (f x) 1), is_open u ∧ x ∈ u,
+      from _root_.mem_nhds_iff.1 B,
+    refine ⟨u, _, u, subset.refl _, u_open, _⟩,
+    { apply nhds_within_le_nhds,
+      exact u_open.mem_nhds xu },
+    { apply bounded.mono (image_subset _ uf),
+      exact bounded_ball.mono (image_preimage_subset _ _) } }
+end
+
+/-- If a function is continuous on a neighborhood of a compact set `k`, then it is bounded on
+some open neighborhood of `k`. -/
+lemma exists_is_open_bounded_image_of_is_compact_of_continuous_on
+  [topological_space β] {k s : set β} {f : β → α}
+  (hk : is_compact k) (hs : is_open s) (hks : k ⊆ s) (hf : continuous_on f s) :
+  ∃ t, k ⊆ t ∧ is_open t ∧ bounded (f '' t) :=
+begin
+  apply exists_is_open_bounded_image_of_is_compact_of_forall_continuous_at hk
+  (λ x hx, hf.continuous_at (hs.mem_nhds (hks hx))),
+end
+
 /-- The **Heine–Borel theorem**: In a proper space, a closed bounded set is compact. -/
 lemma is_compact_of_is_closed_bounded [proper_space α] (hc : is_closed s) (hb : bounded s) :
   is_compact s :=