refactor(Topology/MetricSpace): remove Metric.Bounded (#7240)

Use `Bornology.IsBounded` instead.

Mathlib/Algebra/Module/Zlattice.lean

@@ -44,7 +44,7 @@ noncomputable section
 
 namespace Zspan
 
-open MeasureTheory MeasurableSet Submodule
+open MeasureTheory MeasurableSet Submodule Bornology
 
 variable {E ι : Type*}
 
@@ -235,16 +235,13 @@ end Unique
 
 end Fintype
 
-theorem fundamentalDomain_bounded [Finite ι] [HasSolidNorm K] :
-    Metric.Bounded (fundamentalDomain b) := by
+theorem fundamentalDomain_isBounded [Finite ι] [HasSolidNorm K] :
+    IsBounded (fundamentalDomain b) := by
   cases nonempty_fintype ι
-  use 2 * ∑ j, ‖b j‖
-  intro x hx y hy
-  refine le_trans (dist_le_norm_add_norm x y) ?_
-  rw [← fract_eq_self.mpr hx, ← fract_eq_self.mpr hy]
-  refine (add_le_add (norm_fract_le b x) (norm_fract_le b y)).trans ?_
-  rw [← two_mul]
-#align zspan.fundamental_domain_bounded Zspan.fundamentalDomain_bounded
+  refine isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩
+  rw [← fract_eq_self.mpr hx]
+  apply norm_fract_le
+#align zspan.fundamental_domain_bounded Zspan.fundamentalDomain_isBounded
 
 theorem vadd_mem_fundamentalDomain [Fintype ι] (y : span ℤ (Set.range b)) (x : E) :
     y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x := by
@@ -372,7 +369,7 @@ theorem Zlattice.FG : AddSubgroup.FG L := by
     refine Set.Finite.of_finite_image (f := ((↑) : _ →  E) ∘ Zspan.quotientEquiv b) ?_
       (Function.Injective.injOn (Subtype.coe_injective.comp (Zspan.quotientEquiv b).injective) _)
     have : Set.Finite ((Zspan.fundamentalDomain b) ∩ L) :=
-      Metric.Finite_bounded_inter_isClosed (Zspan.fundamentalDomain_bounded b) inferInstance
+      Metric.finite_isBounded_inter_isClosed (Zspan.fundamentalDomain_isBounded b) inferInstance
     refine Set.Finite.subset this ?_
     rintro _ ⟨_, ⟨⟨x, ⟨h_mem, rfl⟩⟩, rfl⟩⟩
     rw [Function.comp_apply, mkQ_apply, Zspan.quotientEquiv_apply_mk, Zspan.fractRestrict_apply]
@@ -468,7 +465,7 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
         · exact zsmul_mem (subset_span (Set.diff_subset _ _ hv)) _
         · exact span_mono (by simp [ht_inc]) (coe_mem _)
     have h_finite : Set.Finite (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ (L : Set E)) :=
-      Metric.Finite_bounded_inter_isClosed Metric.bounded_closedBall inferInstance
+      Metric.finite_isBounded_inter_isClosed Metric.isBounded_closedBall inferInstance
     obtain ⟨n, -, m, -, h_neq, h_eq⟩ := Set.Infinite.exists_ne_map_eq_of_mapsTo
       Set.infinite_univ h_mapsto h_finite
     have h_nz : (-n + m : ℚ) ≠ 0 := by

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -111,7 +111,7 @@ theorem norm_volume_sub_integral_face_upper_sub_lower_smul_le {f : (Fin (n + 1)
       · intro y hy
         refine' (hε y hy).trans (mul_le_mul_of_nonneg_left _ h0.le)
         rw [← dist_eq_norm]
-        exact dist_le_diam_of_mem I.isCompact_Icc.bounded hy hxI
+        exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI
       rw [two_mul, add_mul]
       exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))
   calc

Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean

@@ -284,7 +284,7 @@ theorem IsSubordinate.diam_le [Fintype ι] {π : TaggedPrepartition I} (h : π.I
     (hJ : J ∈ π.boxes) : diam (Box.Icc J) ≤ 2 * r (π.tag J) :=
   calc
     diam (Box.Icc J) ≤ diam (closedBall (π.tag J) (r <| π.tag J)) :=
-      diam_mono (h J hJ) bounded_closedBall
+      diam_mono (h J hJ) isBounded_closedBall
     _ ≤ 2 * r (π.tag J) := diam_closedBall (le_of_lt (r _).2)
 #align box_integral.tagged_prepartition.is_subordinate.diam_le BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le
 

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -27,7 +27,7 @@ the indicator function of `closedBall 0 1` with a function as above with `s = ba
 noncomputable section
 
 open Set Metric TopologicalSpace Function Asymptotics MeasureTheory FiniteDimensional
-  ContinuousLinearMap Filter MeasureTheory.Measure
+  ContinuousLinearMap Filter MeasureTheory.Measure Bornology
 
 open scoped Pointwise Topology NNReal BigOperators Convolution
 
@@ -59,10 +59,9 @@ theorem exists_smooth_tsupport_subset {s : Set E} {x : E} (hs : s ∈ 𝓝 x) :
     rw [tsupport, ← Euclidean.closure_ball _ d_pos.ne']
     exact closure_mono f_supp
   refine' ⟨f, f_tsupp.trans hd, _, _, _, _⟩
-  · refine' isCompact_of_isClosed_bounded isClosed_closure _
-    have : Bounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.bounded
-    apply this.mono _
-    refine' (IsClosed.closure_subset_iff Euclidean.isClosed_closedBall).2 _
+  · refine' isCompact_of_isClosed_isBounded isClosed_closure _
+    have : IsBounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.isBounded
+    refine this.subset (Euclidean.isClosed_closedBall.closure_subset_iff.2 ?_)
     exact f_supp.trans Euclidean.ball_subset_closedBall
   · apply c.contDiff.comp
     exact ContinuousLinearEquiv.contDiff _

Mathlib/Analysis/Complex/AbsMax.lean

@@ -79,7 +79,7 @@ maximum modulus principle, complex analysis
 -/
 
 
-open TopologicalSpace Metric Set Filter Asymptotics Function MeasureTheory AffineMap
+open TopologicalSpace Metric Set Filter Asymptotics Function MeasureTheory AffineMap Bornology
 
 open scoped Topology Filter NNReal Real
 
@@ -367,7 +367,7 @@ variable [Nontrivial E]
 set `U` and is continuous on its closure, then there exists a point `z ∈ frontier U` such that
 `(‖f ·‖)` takes it maximum value on `closure U` at `z`. -/
 theorem exists_mem_frontier_isMaxOn_norm [FiniteDimensional ℂ E] {f : E → F} {U : Set E}
-    (hb : Bounded U) (hne : U.Nonempty) (hd : DiffContOnCl ℂ f U) :
+    (hb : IsBounded U) (hne : U.Nonempty) (hd : DiffContOnCl ℂ f U) :
     ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z := by
   have hc : IsCompact (closure U) := hb.isCompact_closure
   obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w
@@ -384,7 +384,7 @@ theorem exists_mem_frontier_isMaxOn_norm [FiniteDimensional ℂ E] {f : E → F}
 
 /-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a bounded set `U` and
 `‖f z‖ ≤ C` for any `z ∈ frontier U`, then the same is true for any `z ∈ closure U`. -/
-theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : Bounded U)
+theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : IsBounded U)
     (hd : DiffContOnCl ℂ f U) {C : ℝ} (hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C) {z : E}
     (hz : z ∈ closure U) : ‖f z‖ ≤ C := by
   rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz
@@ -399,7 +399,7 @@ theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : B
   replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
   exact hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
   have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [mem_preimage, lineMap_apply_zero]
-  rcases exists_mem_frontier_isMaxOn_norm (hL.bounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
+  rcases exists_mem_frontier_isMaxOn_norm (hL.isBounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
   calc
     ‖f z‖ = ‖f (e 0)‖ := by simp only [lineMap_apply_zero]
     _ ≤ ‖f (e ζ)‖ := (hζ (subset_closure h₀))
@@ -408,7 +408,7 @@ theorem norm_le_of_forall_mem_frontier_norm_le {f : E → F} {U : Set E} (hU : B
 
 /-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
 `U`, then they are equal on `closure U`. -/
-theorem eqOn_closure_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : Bounded U)
+theorem eqOn_closure_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : IsBounded U)
     (hf : DiffContOnCl ℂ f U) (hg : DiffContOnCl ℂ g U) (hfg : EqOn f g (frontier U)) :
     EqOn f g (closure U) := by
   suffices H : ∀ z ∈ closure U, ‖(f - g) z‖ ≤ 0; · simpa [sub_eq_zero] using H
@@ -418,7 +418,7 @@ theorem eqOn_closure_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : Bounded
 
 /-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
 `U`, then they are equal on `U`. -/
-theorem eqOn_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : Bounded U) (hf : DiffContOnCl ℂ f U)
+theorem eqOn_of_eqOn_frontier {f g : E → F} {U : Set E} (hU : IsBounded U) (hf : DiffContOnCl ℂ f U)
     (hg : DiffContOnCl ℂ g U) (hfg : EqOn f g (frontier U)) : EqOn f g U :=
   (eqOn_closure_of_eqOn_frontier hU hf hg hfg).mono subset_closure
 #align complex.eq_on_of_eq_on_frontier Complex.eqOn_of_eqOn_frontier

Mathlib/Analysis/Complex/Liouville.lean

@@ -25,7 +25,7 @@ The proof is based on the Cauchy integral formula for the derivative of an analy
 
 local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
 
-open TopologicalSpace Metric Set Filter Asymptotics Function MeasureTheory
+open TopologicalSpace Metric Set Filter Asymptotics Function MeasureTheory Bornology
 
 open scoped Topology Filter NNReal Real
 
@@ -88,12 +88,12 @@ theorem norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : 
 #align complex.norm_deriv_le_of_forall_mem_sphere_norm_le Complex.norm_deriv_le_of_forall_mem_sphere_norm_le
 
 /-- An auxiliary lemma for Liouville's theorem `Differentiable.apply_eq_apply_of_bounded`. -/
-theorem liouville_theorem_aux {f : ℂ → F} (hf : Differentiable ℂ f) (hb : Bounded (range f))
+theorem liouville_theorem_aux {f : ℂ → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f))
     (z w : ℂ) : f z = f w := by
   suffices : ∀ c, deriv f c = 0; exact is_const_of_deriv_eq_zero hf this z w
   clear z w; intro c
   obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C := by
-    rcases bounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
+    rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
     exact
       ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
         (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
@@ -111,24 +111,24 @@ namespace Differentiable
 open Complex
 
 /-- **Liouville's theorem**: a complex differentiable bounded function `f : E → F` is a constant. -/
-theorem apply_eq_apply_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : Bounded (range f))
+theorem apply_eq_apply_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : IsBounded (range f))
     (z w : E) : f z = f w := by
   set g : ℂ → F := f ∘ fun t : ℂ => t • (w - z) + z
   suffices g 0 = g 1 by simpa
   apply liouville_theorem_aux
   exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z),
-    hb.mono (range_comp_subset_range _ _)]
+    hb.subset (range_comp_subset_range _ _)]
 #align differentiable.apply_eq_apply_of_bounded Differentiable.apply_eq_apply_of_bounded
 
 /-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/
 theorem exists_const_forall_eq_of_bounded {f : E → F} (hf : Differentiable ℂ f)
-    (hb : Bounded (range f)) : ∃ c, ∀ z, f z = c :=
+    (hb : IsBounded (range f)) : ∃ c, ∀ z, f z = c :=
   ⟨f 0, fun _ => hf.apply_eq_apply_of_bounded hb _ _⟩
 #align differentiable.exists_const_forall_eq_of_bounded Differentiable.exists_const_forall_eq_of_bounded
 
 /-- **Liouville's theorem**: a complex differentiable bounded function is a constant. -/
-theorem exists_eq_const_of_bounded {f : E → F} (hf : Differentiable ℂ f) (hb : Bounded (range f)) :
-    ∃ c, f = const E c :=
+theorem exists_eq_const_of_bounded {f : E → F} (hf : Differentiable ℂ f)
+    (hb : IsBounded (range f)) : ∃ c, f = const E c :=
   (hf.exists_const_forall_eq_of_bounded hb).imp fun _ => funext
 #align differentiable.exists_eq_const_of_bounded Differentiable.exists_eq_const_of_bounded
 

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -214,8 +214,8 @@ theorem horizontal_strip (hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b))
             ((differentiable_id.sub_const _).const_mul _).neg.cexp).const_mul _).cexp
   replace hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
   exact (hgd.diffContOnCl.smul hfd).mono (inter_subset_right _ _)
-  convert norm_le_of_forall_mem_frontier_norm_le ((bounded_Ioo _ _).reProdIm (bounded_Ioo _ _)) hd
-    (fun w hw => _) _
+  convert norm_le_of_forall_mem_frontier_norm_le ((isBounded_Ioo _ _).reProdIm (isBounded_Ioo _ _))
+    hd (fun w hw => _) _
   · rw [frontier_reProdIm, closure_Ioo (neg_lt_self hR₀).ne, frontier_Ioo hab, closure_Ioo hab.ne,
       frontier_Ioo (neg_lt_self hR₀)] at hw
     by_cases him : w.im = a - b ∨ w.im = a + b

Mathlib/Analysis/Complex/Polynomial.lean

@@ -18,7 +18,7 @@ This file proves that every nonconstant complex polynomial has a root using Liou
 As a consequence, the complex numbers are algebraically closed.
 -/
 
-open Polynomial
+open Polynomial Bornology
 
 open scoped Polynomial
 
@@ -28,9 +28,9 @@ namespace Complex
   has a root -/
 theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z := by
   contrapose! hf
-  have : Metric.Bounded (Set.range (eval · f)⁻¹)
+  have : IsBounded (Set.range (eval · f)⁻¹)
   · obtain ⟨z₀, h₀⟩ := f.exists_forall_norm_le
-    simp only [Pi.inv_apply, bounded_iff_forall_norm_le, Set.forall_range_iff, norm_inv]
+    simp only [Pi.inv_apply, isBounded_iff_forall_norm_le, Set.forall_range_iff, norm_inv]
     exact ⟨‖eval z₀ f‖⁻¹, fun z => inv_le_inv_of_le (norm_pos_iff.2 <| hf z₀) (h₀ z)⟩
   obtain ⟨c, hc⟩ := (f.differentiable.inv hf).exists_const_forall_eq_of_bounded this
   · obtain rfl : f = C c⁻¹ := Polynomial.funext fun z => by rw [eval_C, ← hc z, inv_inv]

Mathlib/Analysis/Complex/ReImTopology.lean

@@ -210,6 +210,6 @@ theorem IsClosed.reProdIm (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ×
   (hs.preimage continuous_re).inter (ht.preimage continuous_im)
 #align is_closed.re_prod_im IsClosed.reProdIm
 
-theorem Metric.Bounded.reProdIm (hs : Bounded s) (ht : Bounded t) : Bounded (s ×ℂ t) :=
-  antilipschitz_equivRealProd.bounded_preimage (hs.prod ht)
-#align metric.bounded.re_prod_im Metric.Bounded.reProdIm
+theorem Bornology.IsBounded.reProdIm (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ×ℂ t) :=
+  antilipschitz_equivRealProd.isBounded_preimage (hs.prod ht)
+#align metric.bounded.re_prod_im Bornology.IsBounded.reProdIm

Mathlib/Analysis/Complex/Schwarz.lean

@@ -77,7 +77,7 @@ theorem schwarz_aux {f : ℂ → ℂ} (hd : DifferentiableOn ℂ f (ball c R₁)
     rw [closure_ball c hr₀.ne']
     exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
       (closedBall_subset_ball hr.2)
-  refine' norm_le_of_forall_mem_frontier_norm_le bounded_ball hd _ _
+  refine' norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd _ _
   · rw [frontier_ball c hr₀.ne']
     intro z hz
     have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'

Mathlib/Analysis/Convex/Body.lean

@@ -162,13 +162,13 @@ section SeminormedAddCommGroup
 
 variable [SeminormedAddCommGroup V] [NormedSpace ℝ V] (K L : ConvexBody V)
 
-protected theorem bounded : Metric.Bounded (K : Set V) :=
-  K.isCompact.bounded
-#align convex_body.bounded ConvexBody.bounded
+protected theorem isBounded : Bornology.IsBounded (K : Set V) :=
+  K.isCompact.isBounded
+#align convex_body.bounded ConvexBody.isBounded
 
 theorem hausdorffEdist_ne_top {K L : ConvexBody V} : EMetric.hausdorffEdist (K : Set V) L ≠ ⊤ := by
   apply_rules [Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty,
-    ConvexBody.bounded]
+    ConvexBody.isBounded]
 #align convex_body.Hausdorff_edist_ne_top ConvexBody.hausdorffEdist_ne_top
 
 /-- Convex bodies in a fixed seminormed space $V$ form a pseudo-metric space under the Hausdorff

Mathlib/Analysis/Convex/Measure.lean

@@ -18,7 +18,7 @@ convex set in `E`. Then the frontier of `s` has measure zero (see `Convex.addHaa
 -/
 
 
-open MeasureTheory MeasureTheory.Measure Set Metric Filter
+open MeasureTheory MeasureTheory.Measure Set Metric Filter Bornology
 
 open FiniteDimensional (finrank)
 
@@ -42,11 +42,11 @@ theorem addHaar_frontier (hs : Convex ℝ s) : μ (frontier s) = 0 := by
   /- Without loss of generality, `s` is bounded. Indeed, `∂s ⊆ ⋃ n, ∂(s ∩ ball x (n + 1))`, hence it
     suffices to prove that `∀ n, μ (s ∩ ball x (n + 1)) = 0`; the latter set is bounded.
     -/
-  suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → Bounded t → μ (frontier t) = 0
+  suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → IsBounded t → μ (frontier t) = 0
   · let B : ℕ → Set E := fun n => ball x (n + 1)
     have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
       refine' measure_iUnion_null fun n =>
-        H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
+        H _ (hs.inter (convex_ball _ _)) _ (isBounded_ball.subset (inter_subset_right _ _))
       rw [interior_inter, isOpen_ball.interior_eq]
       exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
     refine' measure_mono_null (fun y hy => _) this; clear this
@@ -59,17 +59,15 @@ theorem addHaar_frontier (hs : Convex ℝ s) : μ (frontier s) = 0 := by
   intro s hs hx hb
   /- Since `s` is bounded, we have `μ (interior s) ≠ ∞`, hence it suffices to prove
     `μ (closure s) ≤ μ (interior s)`. -/
-  replace hb : μ (interior s) ≠ ∞
-  exact (hb.mono interior_subset).measure_lt_top.ne
+  replace hb : μ (interior s) ≠ ∞ := (hb.subset interior_subset).measure_lt_top.ne
   suffices μ (closure s) ≤ μ (interior s) by
     rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb,
       tsub_eq_zero_iff_le]
   /- Due to `Convex.closure_subset_image_homothety_interior_of_one_lt`, for any `r > 1` we have
     `closure s ⊆ homothety x r '' interior s`, hence `μ (closure s) ≤ r ^ d * μ (interior s)`,
     where `d = finrank ℝ E`. -/
   set d : ℕ := FiniteDimensional.finrank ℝ E
-  have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := by
-    intro r hr
+  have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := fun r hr ↦ by
     refine' (measure_mono <|
       hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
     rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]

Mathlib/Analysis/Convex/Normed.lean

@@ -116,9 +116,10 @@ theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.di
 
 /-- Convex hull of `s` is bounded if and only if `s` is bounded. -/
 @[simp]
-theorem bounded_convexHull {s : Set E} : Metric.Bounded (convexHull ℝ s) ↔ Metric.Bounded s := by
-  simp only [Metric.bounded_iff_ediam_ne_top, convexHull_ediam]
-#align bounded_convex_hull bounded_convexHull
+theorem isBounded_convexHull {s : Set E} :
+    Bornology.IsBounded (convexHull ℝ s) ↔ Bornology.IsBounded s := by
+  simp only [Metric.isBounded_iff_ediam_ne_top, convexHull_ediam]
+#align bounded_convex_hull isBounded_convexHull
 
 instance (priority := 100) NormedSpace.instPathConnectedSpace : PathConnectedSpace E :=
   TopologicalAddGroup.pathConnectedSpace