bump to nightly-2023-09-20-06

mathlib commit leanprover-community/mathlib@ce64cd3

Archive/Imo/Imo1959Q1.lean

@@ -36,7 +36,7 @@ end imo1959_q1
 
 open imo1959_q1
 
-theorem imo1959_q1 : ∀ n : ℕ, coprime (21 * n + 4) (14 * n + 3) := fun n =>
+theorem imo1959_q1 : ∀ n : ℕ, Coprime (21 * n + 4) (14 * n + 3) := fun n =>
   coprime_of_dvd' fun k hp h1 h2 => calculation n k h1 h2
 #align imo1959_q1 imo1959_q1
 

Archive/Imo/Imo2005Q4.lean

@@ -89,7 +89,7 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime
     exact (id (h 2 one_le_two) : IsCoprime (8 * 6 : ℤ) k).of_mul_left_right
   -- In particular `p` is coprime to `2` (we record the `nat.coprime` version since that's what's
   -- needed later).
-  have hp₂ : Nat.coprime 2 p := by
+  have hp₂ : Nat.Coprime 2 p := by
     rw [← Nat.isCoprime_iff_coprime]
     exact (id hp₆ : IsCoprime (3 * 2 : ℤ) p).of_mul_left_right
   -- Suppose for the sake of contradiction that `k ≠ 1`.  Then `p` is genuinely a prime factor of

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -96,7 +96,7 @@ theorem eq_two_pow_hMul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n)
   rw [Nat.perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
     is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm,
     sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf 
-  rcases Nat.coprime.dvd_of_dvd_mul_left
+  rcases Nat.Coprime.dvd_of_dvd_mul_left
       (nat.prime_two.coprime_pow_of_not_dvd (odd_mersenne_succ _)) (Dvd.intro _ perf) with
     ⟨j, rfl⟩
   rw [← mul_assoc, mul_comm _ (mersenne _), mul_assoc] at perf 

Mathbin/Algebra/Category/Group/Injective.lean

@@ -34,7 +34,6 @@ variable (A : Type u) [AddCommGroup A]
 
 namespace AddCommGroupCat
 
-#print AddCommGroupCat.injective_of_injective_as_module /-
 theorem injective_of_injective_as_module [Injective (⟨A⟩ : ModuleCat ℤ)] :
     CategoryTheory.Injective (⟨A⟩ : AddCommGroupCat) :=
   {
@@ -58,9 +57,7 @@ theorem injective_of_injective_as_module [Injective (⟨A⟩ : ModuleCat ℤ)] :
       refine' ⟨(injective.factor_thru G F).toAddMonoidHom, _⟩
       ext; convert FunLike.congr_fun (injective.comp_factor_thru G F) x }
 #align AddCommGroup.injective_of_injective_as_module AddCommGroupCat.injective_of_injective_as_module
--/
 
-#print AddCommGroupCat.injective_as_module_of_injective_as_Ab /-
 theorem injective_as_module_of_injective_as_Ab [Injective (⟨A⟩ : AddCommGroupCat)] :
     Injective (⟨A⟩ : ModuleCat ℤ) :=
   {
@@ -80,7 +77,6 @@ theorem injective_as_module_of_injective_as_Ab [Injective (⟨A⟩ : AddCommGrou
         · simp only [sub_smul, map_sub, hn, one_smul]
       ext; convert FunLike.congr_fun (injective.comp_factor_thru G F) x }
 #align AddCommGroup.injective_as_module_of_injective_as_Ab AddCommGroupCat.injective_as_module_of_injective_as_Ab
--/
 
 #print AddCommGroupCat.injective_of_divisible /-
 instance injective_of_divisible [DivisibleBy A ℤ] :

Mathbin/Algebra/Group/UniqueProds.lean

@@ -86,7 +86,6 @@ theorem set_subsingleton (A B : Finset G) (a0 b0 : G) (h : UniqueMul A B a0 b0)
 
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (ab «expr ∈ » [finset.product/multiset.product/set.prod/list.product](A, B)) -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print UniqueMul.iff_existsUnique /-
 @[to_additive]
 theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
     UniqueMul A B a0 b0 ↔ ∃! (ab : _) (_ : ab ∈ A ×ˢ B), ab.1 * ab.2 = a0 * b0 :=
@@ -96,13 +95,11 @@ theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) :
         rintro ⟨x1, x2⟩ _ _ J x y hx hy l
         rcases prod.mk.inj_iff.mp (J (a0, b0) (Finset.mk_mem_product aA bB) rfl) with ⟨rfl, rfl⟩
         exact prod.mk.inj_iff.mp (J (x, y) (Finset.mk_mem_product hx hy) l))⟩
-#align unique_mul.iff_exists_unique UniqueMul.iff_existsUnique
-#align unique_add.iff_exists_unique UniqueAdd.iff_existsUnique
--/
+#align unique_mul.iff_exists_unique UniqueMul.iff_existsUniqueₓ
+#align unique_add.iff_exists_unique UniqueAdd.iff_existsUniqueₓ
 
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (ab «expr ∈ » [finset.product/multiset.product/set.prod/list.product](A, B)) -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print UniqueMul.exists_iff_exists_existsUnique /-
 @[to_additive]
 theorem exists_iff_exists_existsUnique :
     (∃ a0 b0 : G, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔
@@ -113,9 +110,8 @@ theorem exists_iff_exists_existsUnique :
     rcases h' with ⟨⟨a, b⟩, ⟨hab, rfl, -⟩, -⟩
     cases' finset.mem_product.mp hab with ha hb
     exact ⟨a, b, ha, hb, (iff_exists_unique ha hb).mpr h⟩⟩
-#align unique_mul.exists_iff_exists_exists_unique UniqueMul.exists_iff_exists_existsUnique
-#align unique_add.exists_iff_exists_exists_unique UniqueAdd.exists_iff_exists_existsUnique
--/
+#align unique_mul.exists_iff_exists_exists_unique UniqueMul.exists_iff_exists_existsUniqueₓ
+#align unique_add.exists_iff_exists_exists_unique UniqueAdd.exists_iff_exists_existsUniqueₓ
 
 #print UniqueMul.mulHom_preimage /-
 /-- `unique_mul` is preserved by inverse images under injective, multiplicative maps. -/

Mathbin/Algebra/IsPrimePow.lean

@@ -140,7 +140,7 @@ theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m
 -/
 
 #print Nat.disjoint_divisors_filter_isPrimePow /-
-theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.coprime b) :
+theorem Nat.disjoint_divisors_filter_isPrimePow {a b : ℕ} (hab : a.Coprime b) :
     Disjoint (a.divisors.filterₓ IsPrimePow) (b.divisors.filterₓ IsPrimePow) :=
   by
   simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]

Mathbin/Algebra/Lie/Nilpotent.lean

@@ -262,7 +262,6 @@ theorem exists_forall_pow_toEndomorphism_eq_zero [hM : IsNilpotent R L M] :
 #align lie_module.nilpotent_endo_of_nilpotent_module LieModule.exists_forall_pow_toEndomorphism_eq_zero
 -/
 
-#print LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent /-
 /-- For a nilpotent Lie module, the weight space of the 0 weight is the whole module.
 
 This result will be used downstream to show that weight spaces are Lie submodules, at which time
@@ -278,7 +277,6 @@ theorem iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent [IsNilpotent R L M] :
   use k; rw [hk]
   exact LinearMap.zero_apply m
 #align lie_module.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent
--/
 
 #print LieModule.nilpotentOfNilpotentQuotient /-
 /-- If the quotient of a Lie module `M` by a Lie submodule on which the Lie algebra acts trivially
@@ -645,13 +643,11 @@ theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra [IsNilpotent R L] :
 #align lie_algebra.nilpotent_ad_of_nilpotent_algebra LieAlgebra.nilpotent_ad_of_nilpotent_algebra
 -/
 
-#print LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent /-
 /-- See also `lie_algebra.zero_root_space_eq_top_of_nilpotent`. -/
 theorem LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent [IsNilpotent R L] :
     (⨅ x : L, (ad R L x).maximalGeneralizedEigenspace 0) = ⊤ :=
   LieModule.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent R L L
 #align lie_algebra.infi_max_gen_zero_eigenspace_eq_top_of_nilpotent LieAlgebra.iInf_max_gen_zero_eigenspace_eq_top_of_nilpotent
--/
 
 -- TODO Generalise the below to Lie modules if / when we define morphisms, equivs of Lie modules
 -- covering a Lie algebra morphism of (possibly different) Lie algebras.

Mathbin/Algebra/Lie/Weights.lean

@@ -72,7 +72,6 @@ open scoped BigOperators
 
 open scoped TensorProduct
 
-#print LieModule.preWeightSpace /-
 /-- Given a Lie module `M` over a Lie algebra `L`, the pre-weight space of `M` with respect to a
 map `χ : L → R` is the simultaneous generalized eigenspace of the action of all `x : L` on `M`,
 with eigenvalues `χ x`.
@@ -81,26 +80,21 @@ See also `lie_module.weight_space`. -/
 def preWeightSpace (χ : L → R) : Submodule R M :=
   ⨅ x : L, (toEndomorphism R L M x).maximalGeneralizedEigenspace (χ x)
 #align lie_module.pre_weight_space LieModule.preWeightSpace
--/
 
-#print LieModule.mem_preWeightSpace /-
 theorem mem_preWeightSpace (χ : L → R) (m : M) :
     m ∈ preWeightSpace M χ ↔ ∀ x, ∃ k : ℕ, ((toEndomorphism R L M x - χ x • 1) ^ k) m = 0 := by
   simp [pre_weight_space, -LinearMap.pow_apply]
 #align lie_module.mem_pre_weight_space LieModule.mem_preWeightSpace
--/
 
 variable (R)
 
-#print LieModule.exists_preWeightSpace_zero_le_ker_of_isNoetherian /-
 theorem exists_preWeightSpace_zero_le_ker_of_isNoetherian [IsNoetherian R M] (x : L) :
     ∃ k : ℕ, preWeightSpace M (0 : L → R) ≤ (toEndomorphism R L M x ^ k).ker :=
   by
   use(to_endomorphism R L M x).maximalGeneralizedEigenspaceIndex 0
   simp only [← Module.End.generalizedEigenspace_zero, pre_weight_space, Pi.zero_apply, iInf_le, ←
     (to_endomorphism R L M x).maximalGeneralizedEigenspace_eq]
 #align lie_module.exists_pre_weight_space_zero_le_ker_of_is_noetherian LieModule.exists_preWeightSpace_zero_le_ker_of_isNoetherian
--/
 
 variable {R} (L)
 
@@ -182,7 +176,6 @@ protected theorem weight_vector_multiplication (M₁ : Type w₁) (M₂ : Type w
 
 variable {L M}
 
-#print LieModule.lie_mem_preWeightSpace_of_mem_preWeightSpace /-
 theorem lie_mem_preWeightSpace_of_mem_preWeightSpace {χ₁ χ₂ : L → R} {x : L} {m : M}
     (hx : x ∈ preWeightSpace L χ₁) (hm : m ∈ preWeightSpace M χ₂) :
     ⁅x, m⁆ ∈ preWeightSpace M (χ₁ + χ₂) :=
@@ -194,7 +187,6 @@ theorem lie_mem_preWeightSpace_of_mem_preWeightSpace {χ₁ χ₂ : L → R} {x
   simp only [Submodule.subtype_apply, to_module_hom_apply, TensorProduct.map_tmul]
   rfl
 #align lie_module.lie_mem_pre_weight_space_of_mem_pre_weight_space LieModule.lie_mem_preWeightSpace_of_mem_preWeightSpace
--/
 
 variable (M)
 
@@ -575,7 +567,6 @@ open LieAlgebra
 
 variable {R L H}
 
-#print LieModule.weightSpace' /-
 /-- A priori, weight spaces are Lie submodules over the Lie subalgebra `H` used to define them.
 However they are naturally Lie submodules over the (in general larger) Lie subalgebra
 `zero_root_subalgebra R L H`. Even though it is often the case that
@@ -590,14 +581,11 @@ def weightSpace' (χ : H → R) : LieSubmodule R (zeroRootSubalgebra R L H) M :=
       rw [← zero_add χ]
       exact lie_mem_weight_space_of_mem_weight_space hx hm }
 #align lie_module.weight_space' LieModule.weightSpace'
--/
 
-#print LieModule.coe_weightSpace' /-
 @[simp]
 theorem coe_weightSpace' (χ : H → R) : (weightSpace' M χ : Submodule R M) = weightSpace M χ :=
   rfl
 #align lie_module.coe_weight_space' LieModule.coe_weightSpace'
--/
 
 end LieModule
 

Mathbin/Algebra/Module/Zlattice.lean

@@ -247,9 +247,9 @@ end Unique
 
 end Fintype
 
-#print Zspan.fundamentalDomain_bounded /-
-theorem fundamentalDomain_bounded [Finite ι] [HasSolidNorm K] :
-    Metric.Bounded (fundamentalDomain b) :=
+#print Zspan.fundamentalDomain_isBounded /-
+theorem fundamentalDomain_isBounded [Finite ι] [HasSolidNorm K] :
+    Bornology.IsBounded (fundamentalDomain b) :=
   by
   cases nonempty_fintype ι
   use 2 * ∑ j, ‖b j‖
@@ -258,7 +258,7 @@ theorem fundamentalDomain_bounded [Finite ι] [HasSolidNorm K] :
   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
+#align zspan.fundamental_domain_bounded Zspan.fundamentalDomain_isBounded
 -/
 
 #print Zspan.vadd_mem_fundamentalDomain /-

Mathbin/Analysis/BoxIntegral/Partition/Tagged.lean

@@ -362,7 +362,8 @@ theorem IsSubordinate.mono [Fintype ι] {π : TaggedPrepartition I} (hr₁ : π.
 theorem IsSubordinate.diam_le [Fintype ι] {π : TaggedPrepartition I} (h : π.IsSubordinate r)
     (hJ : J ∈ π.boxes) : diam J.Icc ≤ 2 * r (π.Tag J) :=
   calc
-    diam J.Icc ≤ diam (closedBall (π.Tag J) (r <| π.Tag J)) := diam_mono (h J hJ) bounded_closedBall
+    diam J.Icc ≤ diam (closedBall (π.Tag J) (r <| π.Tag J)) :=
+      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
 -/

Mathbin/Analysis/Complex/Liouville.lean

@@ -102,7 +102,7 @@ theorem liouville_theorem_aux {f : ℂ → F} (hf : Differentiable ℂ f) (hb :
   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 _ _)⟩

Mathbin/Analysis/Complex/Polynomial.lean

@@ -36,7 +36,7 @@ theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z :
   · obtain rfl : f = C c⁻¹ := Polynomial.funext fun z => by rw [eval_C, ← hc z, inv_inv]
     exact degree_C_le
   · obtain ⟨z₀, h₀⟩ := f.exists_forall_norm_le
-    simp only [bounded_iff_forall_norm_le, Set.forall_range_iff, norm_inv]
+    simp only [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)⟩
 #align complex.exists_root Complex.exists_root
 -/

Mathbin/Analysis/Complex/ReImTopology.lean

@@ -283,9 +283,9 @@ theorem IsClosed.reProdIm (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ×
 #align is_closed.re_prod_im IsClosed.reProdIm
 -/
 
-#print Metric.Bounded.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
+#print Bornology.IsBounded.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
 -/
 

Mathbin/Analysis/Convex/Body.lean

@@ -178,16 +178,16 @@ section SeminormedAddCommGroup
 
 variable [SeminormedAddCommGroup V] [NormedSpace ℝ V] (K L : ConvexBody V)
 
-#print ConvexBody.bounded /-
-protected theorem bounded : Metric.Bounded (K : Set V) :=
+#print ConvexBody.isBounded /-
+protected theorem isBounded : Bornology.IsBounded (K : Set V) :=
   K.IsCompact.Bounded
-#align convex_body.bounded ConvexBody.bounded
+#align convex_body.bounded ConvexBody.isBounded
 -/
 
 #print ConvexBody.hausdorffEdist_ne_top /-
 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
 -/
 

Mathbin/Analysis/Convex/Normed.lean

@@ -145,12 +145,13 @@ theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.di
 #align convex_hull_diam convexHull_diam
 -/
 
-#print bounded_convexHull /-
+#print isBounded_convexHull /-
 /-- 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
 -/
 
 #print NormedSpace.instPathConnectedSpace /-

Mathbin/Analysis/Convex/Topology.lean

@@ -66,8 +66,8 @@ variable (ι)
 
 #print bounded_stdSimplex /-
 /-- `std_simplex ℝ ι` is bounded. -/
-theorem bounded_stdSimplex : Metric.Bounded (stdSimplex ℝ ι) :=
-  (Metric.bounded_iff_subset_ball 0).2 ⟨1, stdSimplex_subset_closedBall⟩
+theorem bounded_stdSimplex : Bornology.IsBounded (stdSimplex ℝ ι) :=
+  (Metric.isBounded_iff_subset_closedBall 0).2 ⟨1, stdSimplex_subset_closedBall⟩
 #align bounded_std_simplex bounded_stdSimplex
 -/
 

Mathbin/Analysis/LocallyConvex/Bounded.lean

@@ -328,7 +328,7 @@ theorem isVonNBounded_closedBall (r : ℝ) :
 #print NormedSpace.isVonNBounded_iff /-
 theorem isVonNBounded_iff (s : Set E) : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s :=
   by
-  rw [← Metric.bounded_iff_isBounded, Metric.bounded_iff_subset_ball (0 : E)]
+  rw [← Metric.isBounded_iff_isBounded, Metric.isBounded_iff_subset_closedBall (0 : E)]
   constructor
   · intro h
     rcases h (Metric.ball_mem_nhds 0 zero_lt_one) with ⟨ρ, hρ, hρball⟩
@@ -344,7 +344,7 @@ theorem isVonNBounded_iff (s : Set E) : Bornology.IsVonNBounded 𝕜 s ↔ Borno
 #print NormedSpace.isVonNBounded_iff' /-
 theorem isVonNBounded_iff' (s : Set E) :
     Bornology.IsVonNBounded 𝕜 s ↔ ∃ r : ℝ, ∀ (x : E) (hx : x ∈ s), ‖x‖ ≤ r := by
-  rw [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded, bounded_iff_forall_norm_le]
+  rw [NormedSpace.isVonNBounded_iff, ← Metric.isBounded_iff_isBounded, isBounded_iff_forall_norm_le]
 #align normed_space.is_vonN_bounded_iff' NormedSpace.isVonNBounded_iff'
 -/
 

Mathbin/Analysis/Normed/Group/Basic.lean

@@ -768,29 +768,30 @@ theorem norm_div_sub_norm_div_le_norm_div (u v w : E) : ‖u / w‖ - ‖v / w
 #align norm_sub_sub_norm_sub_le_norm_sub norm_sub_sub_norm_sub_le_norm_sub
 -/
 
-#print bounded_iff_forall_norm_le' /-
-@[to_additive bounded_iff_forall_norm_le]
-theorem bounded_iff_forall_norm_le' : Bounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
+#print isBounded_iff_forall_norm_le' /-
+@[to_additive isBounded_iff_forall_norm_le]
+theorem isBounded_iff_forall_norm_le' : IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
   simpa only [Set.subset_def, mem_closedBall_one_iff] using bounded_iff_subset_ball (1 : E)
-#align bounded_iff_forall_norm_le' bounded_iff_forall_norm_le'
-#align bounded_iff_forall_norm_le bounded_iff_forall_norm_le
+#align bounded_iff_forall_norm_le' isBounded_iff_forall_norm_le'
+#align bounded_iff_forall_norm_le isBounded_iff_forall_norm_le
 -/
 
-alias ⟨Metric.Bounded.exists_norm_le', _⟩ := bounded_iff_forall_norm_le'
-#align metric.bounded.exists_norm_le' Metric.Bounded.exists_norm_le'
+alias ⟨Bornology.IsBounded.exists_norm_le', _⟩ := isBounded_iff_forall_norm_le'
+#align metric.bounded.exists_norm_le' Bornology.IsBounded.exists_norm_le'
 
-alias ⟨Metric.Bounded.exists_norm_le, _⟩ := bounded_iff_forall_norm_le
-#align metric.bounded.exists_norm_le Metric.Bounded.exists_norm_le
+alias ⟨Bornology.IsBounded.exists_norm_le, _⟩ := isBounded_iff_forall_norm_le
+#align metric.bounded.exists_norm_le Bornology.IsBounded.exists_norm_le
 
-attribute [to_additive Metric.Bounded.exists_norm_le] Metric.Bounded.exists_norm_le'
+attribute [to_additive Bornology.IsBounded.exists_norm_le] Bornology.IsBounded.exists_norm_le'
 
-#print Metric.Bounded.exists_pos_norm_le' /-
-@[to_additive Metric.Bounded.exists_pos_norm_le]
-theorem Metric.Bounded.exists_pos_norm_le' (hs : Metric.Bounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R :=
+#print Bornology.IsBounded.exists_pos_norm_le' /-
+@[to_additive Bornology.IsBounded.exists_pos_norm_le]
+theorem Bornology.IsBounded.exists_pos_norm_le' (hs : Bornology.IsBounded s) :
+    ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R :=
   let ⟨R₀, hR₀⟩ := hs.exists_norm_le'
   ⟨max R₀ 1, by positivity, fun x hx => (hR₀ x hx).trans <| le_max_left _ _⟩
-#align metric.bounded.exists_pos_norm_le' Metric.Bounded.exists_pos_norm_le'
-#align metric.bounded.exists_pos_norm_le Metric.Bounded.exists_pos_norm_le
+#align metric.bounded.exists_pos_norm_le' Bornology.IsBounded.exists_pos_norm_le'
+#align metric.bounded.exists_pos_norm_le Bornology.IsBounded.exists_pos_norm_le
 -/
 
 #print mem_sphere_iff_norm' /-
@@ -992,7 +993,7 @@ theorem MonoidHomClass.uniformContinuous_of_bound [MonoidHomClass 𝓕 E F] (f :
 @[to_additive IsCompact.exists_bound_of_continuousOn]
 theorem IsCompact.exists_bound_of_continuousOn' [TopologicalSpace α] {s : Set α} (hs : IsCompact s)
     {f : α → E} (hf : ContinuousOn f s) : ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C :=
-  (bounded_iff_forall_norm_le'.1 (hs.image_of_continuousOn hf).Bounded).imp fun C hC x hx =>
+  (isBounded_iff_forall_norm_le'.1 (hs.image_of_continuousOn hf).Bounded).imp fun C hC x hx =>
     hC _ <| Set.mem_image_of_mem _ hx
 #align is_compact.exists_bound_of_continuous_on' IsCompact.exists_bound_of_continuousOn'
 #align is_compact.exists_bound_of_continuous_on IsCompact.exists_bound_of_continuousOn