feat: Topological properties of order-connected sets in ℝⁿ (#10565)

Partially forward-port leanprover-community/mathlib3#16976

Mathlib.lean

@@ -4216,6 +4216,7 @@ import Mathlib.Topology.NoetherianSpace
 import Mathlib.Topology.OmegaCompletePartialOrder
 import Mathlib.Topology.Order
 import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.Order.Bornology
 import Mathlib.Topology.Order.Bounded
 import Mathlib.Topology.Order.Category.AlexDisc
 import Mathlib.Topology.Order.Category.FrameAdjunction

Mathlib/Analysis/Normed/Order/UpperLower.lean

@@ -4,12 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Field.Pi
+import Mathlib.Algebra.Order.UpperLower
 import Mathlib.Analysis.Normed.Group.Pointwise
 import Mathlib.Analysis.Normed.Order.Basic
-import Mathlib.Algebra.Order.UpperLower
 import Mathlib.Data.Real.Sqrt
+import Mathlib.Topology.Algebra.Order.UpperLower
+import Mathlib.Topology.MetricSpace.Sequences
 
-#align_import analysis.normed.order.upper_lower from "leanprover-community/mathlib"@"992efbda6f85a5c9074375d3c7cb9764c64d8f72"
+#align_import analysis.normed.order.upper_lower from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
 
 /-!
 # Upper/lower/order-connected sets in normed groups
@@ -20,15 +22,21 @@ set).
 
 We also prove lemmas specific to `ℝⁿ`. Those are helpful to prove that order-connected sets in `ℝⁿ`
 are measurable.
--/
 
+## TODO
+
+Is there a way to generalise `IsClosed.upperClosure_pi`/`IsClosed.lowerClosure_pi` so that they also
+apply to `ℝ`, `ℝ × ℝ`, `EuclideanSpace ι ℝ`? `_pi` has been appended to their names to disambiguate
+from the other possible lemmas, but we will want there to be a single set of lemmas for all
+situations.
+-/
 
-open Function Metric Set
+open Bornology Function Metric Set
+open scoped Pointwise
 
 variable {α ι : Type*}
 
-section MetricSpace
-
+section NormedOrderedGroup
 variable [NormedOrderedGroup α] {s : Set α}
 
 @[to_additive IsUpperSet.thickening]
@@ -63,14 +71,25 @@ protected theorem IsLowerSet.cthickening' (hs : IsLowerSet s) (ε : ℝ) :
 #align is_lower_set.cthickening' IsLowerSet.cthickening'
 #align is_lower_set.cthickening IsLowerSet.cthickening
 
-end MetricSpace
+@[to_additive upperClosure_interior_subset] lemma upperClosure_interior_subset' (s : Set α) :
+    (upperClosure (interior s) : Set α) ⊆ interior (upperClosure s) :=
+  upperClosure_min (interior_mono subset_upperClosure) (upperClosure s).upper.interior
+#align upper_closure_interior_subset' upperClosure_interior_subset'
+#align upper_closure_interior_subset upperClosure_interior_subset
+
+@[to_additive lowerClosure_interior_subset] lemma lowerClosure_interior_subset' (s : Set α) :
+    (lowerClosure (interior s) : Set α) ⊆ interior (lowerClosure s) :=
+  lowerClosure_min (interior_mono subset_lowerClosure) (lowerClosure s).lower.interior
+#align lower_closure_interior_subset' lowerClosure_interior_subset'
+#align lower_closure_interior_subset lowerClosure_interior_subset
+
+end NormedOrderedGroup
 
 /-! ### `ℝⁿ` -/
 
 
 section Finite
-
-variable [Finite ι] {s : Set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+variable [Finite ι] {s : Set (ι → ℝ)} {x y : ι → ℝ}
 
 theorem IsUpperSet.mem_interior_of_forall_lt (hs : IsUpperSet s) (hx : x ∈ closure s)
     (h : ∀ i, x i < y i) : y ∈ interior s := by
@@ -112,8 +131,42 @@ theorem IsLowerSet.mem_interior_of_forall_lt (hs : IsLowerSet s) (hx : x ∈ clo
 end Finite
 
 section Fintype
+variable [Fintype ι] {s t : Set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+-- TODO: Generalise those lemmas so that they also apply to `ℝ` and `EuclideanSpace ι ℝ`
+lemma dist_inf_sup_pi (x y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y := by
+  refine' congr_arg NNReal.toReal (Finset.sup_congr rfl fun i _ ↦ _)
+  simp only [Real.nndist_eq', sup_eq_max, inf_eq_min, max_sub_min_eq_abs, Pi.inf_apply,
+    Pi.sup_apply, Real.nnabs_of_nonneg, abs_nonneg, Real.toNNReal_abs]
+#align dist_inf_sup dist_inf_sup_pi
+
+lemma dist_mono_left_pi : MonotoneOn (dist · y) (Ici y) := by
+  refine' fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ _)
+  rw [Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
+    Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))]
+  exact Real.toNNReal_mono (sub_le_sub_right (hy _) _)
+#align dist_mono_left dist_mono_left_pi
+
+lemma dist_mono_right_pi : MonotoneOn (dist x) (Ici x) := by
+  simpa only [dist_comm _ x] using dist_mono_left_pi (y := x)
+#align dist_mono_right dist_mono_right_pi
 
-variable [Fintype ι] {s : Set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+lemma dist_anti_left_pi : AntitoneOn (dist · y) (Iic y) := by
+  refine' fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ _)
+  rw [Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
+    Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))]
+  exact Real.toNNReal_mono (sub_le_sub_left (hy _) _)
+#align dist_anti_left dist_anti_left_pi
+
+lemma dist_anti_right_pi : AntitoneOn (dist x) (Iic x) := by
+  simpa only [dist_comm] using dist_anti_left_pi (y := x)
+#align dist_anti_right dist_anti_right_pi
+
+lemma dist_le_dist_of_le_pi (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) :
+    dist a₁ b₁ ≤ dist a₂ b₂ :=
+  (dist_mono_right_pi h₁ (h₁.trans hb) hb).trans $
+    dist_anti_left_pi (ha.trans $ h₁.trans hb) (h₁.trans hb) ha
+#align dist_le_dist_of_le dist_le_dist_of_le_pi
 
 theorem IsUpperSet.exists_subset_ball (hs : IsUpperSet s) (hx : x ∈ closure s) (hδ : 0 < δ) :
     ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s := by
@@ -154,3 +207,63 @@ theorem IsLowerSet.exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s)
 #align is_lower_set.exists_subset_ball IsLowerSet.exists_subset_ball
 
 end Fintype
+
+section Finite
+variable [Finite ι] {s t : Set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+/-!
+#### Note
+
+The closure and frontier of an antichain might not be antichains. Take for example the union
+of the open segments from `(0, 2)` to `(1, 1)` and from `(2, 1)` to `(3, 0)`. `(1, 1)` and `(2, 1)`
+are comparable and both in the closure/frontier.
+-/
+
+protected lemma IsClosed.upperClosure_pi (hs : IsClosed s) (hs' : BddBelow s) :
+    IsClosed (upperClosure s : Set (ι → ℝ)) := by
+  cases nonempty_fintype ι
+  refine' IsSeqClosed.isClosed fun f x hf hx ↦ _
+  choose g hg hgf using hf
+  obtain ⟨a, ha⟩ := hx.bddAbove_range
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddAbove_Iic) fun n ↦
+    ⟨hg n, (hgf _).trans <| ha <| mem_range_self _⟩
+  exact ⟨b, closure_minimal inter_subset_left hs hb,
+    le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_atTop) fun _ ↦ hgf _⟩
+#align is_closed.upper_closure IsClosed.upperClosure_pi
+
+protected lemma IsClosed.lowerClosure_pi (hs : IsClosed s) (hs' : BddAbove s) :
+    IsClosed (lowerClosure s : Set (ι → ℝ)) := by
+  cases nonempty_fintype ι
+  refine IsSeqClosed.isClosed fun f x hf hx ↦ ?_
+  choose g hg hfg using hf
+  haveI : BoundedGENhdsClass ℝ := by infer_instance
+  obtain ⟨a, ha⟩ := hx.bddBelow_range
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.isBounded_inter bddBelow_Ici) fun n ↦
+    ⟨hg n, (ha $ mem_range_self _).trans $ hfg _⟩
+  exact ⟨b, closure_minimal inter_subset_left hs hb,
+    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_atTop) hbf fun _ ↦ hfg _⟩
+#align is_closed.lower_closure IsClosed.lowerClosure_pi
+
+protected lemma IsClopen.upperClosure_pi (hs : IsClopen s) (hs' : BddBelow s) :
+    IsClopen (upperClosure s : Set (ι → ℝ)) := ⟨hs.1.upperClosure_pi hs', hs.2.upperClosure⟩
+#align is_clopen.upper_closure IsClopen.upperClosure_pi
+
+protected lemma IsClopen.lowerClosure_pi (hs : IsClopen s) (hs' : BddAbove s) :
+    IsClopen (lowerClosure s : Set (ι → ℝ)) := ⟨hs.1.lowerClosure_pi hs', hs.2.lowerClosure⟩
+#align is_clopen.lower_closure IsClopen.lowerClosure_pi
+
+lemma closure_upperClosure_comm_pi (hs : BddBelow s) :
+    closure (upperClosure s : Set (ι → ℝ)) = upperClosure (closure s) :=
+  (closure_minimal (upperClosure_anti subset_closure) $
+      isClosed_closure.upperClosure_pi hs.closure).antisymm $
+    upperClosure_min (closure_mono subset_upperClosure) (upperClosure s).upper.closure
+#align closure_upper_closure_comm closure_upperClosure_comm_pi
+
+lemma closure_lowerClosure_comm_pi (hs : BddAbove s) :
+    closure (lowerClosure s : Set (ι → ℝ)) = lowerClosure (closure s) :=
+  (closure_minimal (lowerClosure_mono subset_closure) $
+        isClosed_closure.lowerClosure_pi hs.closure).antisymm $
+    lowerClosure_min (closure_mono subset_lowerClosure) (lowerClosure s).lower.closure
+#align closure_lower_closure_comm closure_lowerClosure_comm_pi
+
+end Finite

Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
 import Mathlib.MeasureTheory.Integral.Bochner
-import Mathlib.Topology.Order.Bounded
 
 /-!
 # Integration of bounded continuous functions
@@ -148,10 +147,8 @@ lemma tendsto_integral_of_forall_limsup_integral_le_integral {ι : Type*} {L : F
   rcases eq_or_neBot L with rfl|hL
   · simp only [tendsto_bot]
   have obs := BoundedContinuousFunction.isBounded_range_integral μs f
-  have bdd_above : IsBoundedUnder (· ≤ ·) L (fun i ↦ ∫ x, f x ∂μs i) :=
-    isBounded_le_map_of_bounded_range _ obs
-  have bdd_below : IsBoundedUnder (· ≥ ·) L (fun i ↦ ∫ x, f x ∂μs i) :=
-    isBounded_ge_map_of_bounded_range _ obs
+  have bdd_above : IsBoundedUnder (· ≤ ·) L (fun i ↦ ∫ x, f x ∂μs i) := obs.bddAbove.isBoundedUnder
+  have bdd_below : IsBoundedUnder (· ≥ ·) L (fun i ↦ ∫ x, f x ∂μs i) := obs.bddBelow.isBoundedUnder
   apply tendsto_of_le_liminf_of_limsup_le _ _ bdd_above bdd_below
   · have key := h _ (f.norm_sub_nonneg)
     simp_rw [f.integral_const_sub ‖f‖] at key
@@ -172,10 +169,8 @@ lemma tendsto_integral_of_forall_integral_le_liminf_integral {ι : Type*} {L : F
   rcases eq_or_neBot L with rfl|hL
   · simp only [tendsto_bot]
   have obs := BoundedContinuousFunction.isBounded_range_integral μs f
-  have bdd_above : IsBoundedUnder (· ≤ ·) L (fun i ↦ ∫ x, f x ∂μs i) :=
-    isBounded_le_map_of_bounded_range _ obs
-  have bdd_below : IsBoundedUnder (· ≥ ·) L (fun i ↦ ∫ x, f x ∂μs i) :=
-    isBounded_ge_map_of_bounded_range _ obs
+  have bdd_above : IsBoundedUnder (· ≤ ·) L (fun i ↦ ∫ x, f x ∂μs i) := obs.bddAbove.isBoundedUnder
+  have bdd_below : IsBoundedUnder (· ≥ ·) L (fun i ↦ ∫ x, f x ∂μs i) := obs.bddBelow.isBoundedUnder
   apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂ (μs i)) (∫ x, f x ∂μ)
   · have key := h _ (f.add_norm_nonneg)
     simp_rw [f.integral_add_const ‖f‖] at key

Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

@@ -193,7 +193,7 @@ instance isFiniteMeasure_restrict_Ioo (x y : ℝ) : IsFiniteMeasure (volume.rest
 theorem volume_le_diam (s : Set ℝ) : volume s ≤ EMetric.diam s := by
   by_cases hs : Bornology.IsBounded s
   · rw [Real.ediam_eq hs, ← volume_Icc]
-    exact volume.mono (Real.subset_Icc_sInf_sSup_of_isBounded hs)
+    exact volume.mono hs.subset_Icc_sInf_sSup
   · rw [Metric.ediam_of_unbounded hs]; exact le_top
 #align real.volume_le_diam Real.volume_le_diam
 

Mathlib/Order/Bounds/Basic.lean

@@ -148,6 +148,15 @@ theorem not_bddBelow_iff {α : Type*} [LinearOrder α] {s : Set α} :
   @not_bddAbove_iff αᵒᵈ _ _
 #align not_bdd_below_iff not_bddBelow_iff
 
+@[simp] lemma bddBelow_preimage_ofDual {s : Set α} : BddBelow (ofDual ⁻¹' s) ↔ BddAbove s := Iff.rfl
+@[simp] lemma bddAbove_preimage_ofDual {s : Set α} : BddAbove (ofDual ⁻¹' s) ↔ BddBelow s := Iff.rfl
+
+@[simp] lemma bddBelow_preimage_toDual {s : Set αᵒᵈ} :
+    BddBelow (toDual ⁻¹' s) ↔ BddAbove s := Iff.rfl
+
+@[simp] lemma bddAbove_preimage_toDual {s : Set αᵒᵈ} :
+    BddAbove (toDual ⁻¹' s) ↔ BddBelow s := Iff.rfl
+
 theorem BddAbove.dual (h : BddAbove s) : BddBelow (ofDual ⁻¹' s) :=
   h
 #align bdd_above.dual BddAbove.dual
@@ -633,12 +642,10 @@ theorem isGLB_singleton : IsGLB {a} a :=
   isLeast_singleton.isGLB
 #align is_glb_singleton isGLB_singleton
 
-theorem bddAbove_singleton : BddAbove ({a} : Set α) :=
-  isLUB_singleton.bddAbove
+@[simp] lemma bddAbove_singleton : BddAbove ({a} : Set α) := isLUB_singleton.bddAbove
 #align bdd_above_singleton bddAbove_singleton
 
-theorem bddBelow_singleton : BddBelow ({a} : Set α) :=
-  isGLB_singleton.bddBelow
+@[simp] lemma bddBelow_singleton : BddBelow ({a} : Set α) := isGLB_singleton.bddBelow
 #align bdd_below_singleton bddBelow_singleton
 
 @[simp]

Mathlib/Order/LiminfLimsup.lean

@@ -124,6 +124,16 @@ theorem IsBoundedUnder.comp {l : Filter γ} {q : β → β → Prop} {u : γ →
     (hv : ∀ a₀ a₁, r a₀ a₁ → q (v a₀) (v a₁)) : l.IsBoundedUnder r u → l.IsBoundedUnder q (v ∘ u)
   | ⟨a, h⟩ => ⟨v a, show ∀ᶠ x in map u l, q (v x) (v a) from h.mono fun x => hv x a⟩
 
+/-- A bounded above function `u` is in particular eventually bounded above. -/
+lemma _root_.BddAbove.isBoundedUnder [Preorder α] {f : Filter β} {u : β → α} :
+    BddAbove (Set.range u) → f.IsBoundedUnder (· ≤ ·) u
+  | ⟨b, hb⟩ => isBoundedUnder_of ⟨b, by simpa [mem_upperBounds] using hb⟩
+
+/-- A bounded below function `u` is in particular eventually bounded below. -/
+lemma _root_.BddBelow.isBoundedUnder [Preorder α] {f : Filter β} {u : β → α} :
+    BddBelow (Set.range u) → f.IsBoundedUnder (· ≥ ·) u
+  | ⟨b, hb⟩ => isBoundedUnder_of ⟨b, by simpa [mem_lowerBounds] using hb⟩
+
 theorem _root_.Monotone.isBoundedUnder_le_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α}
     {v : α → β} (hv : Monotone v) (hl : l.IsBoundedUnder (· ≤ ·) u) :
     l.IsBoundedUnder (· ≤ ·) (v ∘ u) :=

Mathlib/Topology/Bornology/Basic.lean

@@ -371,3 +371,22 @@ theorem cobounded_eq_bot : cobounded α = ⊥ :=
 #align bornology.cobounded_eq_bot Bornology.cobounded_eq_bot
 
 end Bornology
+
+namespace OrderDual
+variable [Bornology α]
+
+instance instBornology : Bornology αᵒᵈ := ‹Bornology α›
+
+@[simp] lemma isCobounded_preimage_ofDual {s : Set α} :
+    IsCobounded (ofDual ⁻¹' s) ↔ IsCobounded s := Iff.rfl
+
+@[simp] lemma isCobounded_preimage_toDual {s : Set αᵒᵈ} :
+    IsCobounded (toDual ⁻¹' s) ↔ IsCobounded s := Iff.rfl
+
+@[simp] lemma isBounded_preimage_ofDual {s : Set α} :
+    IsBounded (ofDual ⁻¹' s) ↔ IsBounded s := Iff.rfl
+
+@[simp] lemma isBounded_preimage_toDual {s : Set αᵒᵈ} :
+    IsBounded (toDual ⁻¹' s) ↔ IsBounded s := Iff.rfl
+
+end OrderDual

Mathlib/Topology/ContinuousFunction/Bounded.lean

@@ -1000,7 +1000,7 @@ theorem norm_normComp : ‖f.normComp‖ = ‖f‖ := by
 #align bounded_continuous_function.norm_norm_comp BoundedContinuousFunction.norm_normComp
 
 theorem bddAbove_range_norm_comp : BddAbove <| Set.range <| norm ∘ f :=
-  (Real.isBounded_iff_bddBelow_bddAbove.mp <| @isBounded_range _ _ _ _ f.normComp).2
+  (@isBounded_range _ _ _ _ f.normComp).bddAbove
 #align bounded_continuous_function.bdd_above_range_norm_comp BoundedContinuousFunction.bddAbove_range_norm_comp
 
 theorem norm_eq_iSup_norm : ‖f‖ = ⨆ x : α, ‖f x‖ := by

Mathlib/Topology/Instances/ENNReal.lean

@@ -1525,21 +1525,18 @@ theorem ediam_eq {s : Set ℝ} (h : Bornology.IsBounded s) :
   rcases eq_empty_or_nonempty s with (rfl | hne)
   · simp
   refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
-  · have := Real.subset_Icc_sInf_sSup_of_isBounded h
-    exact Real.dist_le_of_mem_Icc (this hx) (this hy)
+  · exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)
   · apply ENNReal.ofReal_le_of_le_toReal
     rw [← Metric.diam, ← Metric.diam_closure]
-    have h' := Real.isBounded_iff_bddBelow_bddAbove.1 h
     calc sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
-    _ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h'.2)
-        (csInf_mem_closure hne h'.1)
+    _ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
+        (csInf_mem_closure hne h.bddBelow)
 #align real.ediam_eq Real.ediam_eq
 
 /-- For a bounded set `s : Set ℝ`, its `Metric.diam` is equal to `sSup s - sInf s`. -/
 theorem diam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.diam s = sSup s - sInf s := by
   rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]
-  rw [Real.isBounded_iff_bddBelow_bddAbove] at h
-  exact sub_nonneg.2 (Real.sInf_le_sSup s h.1 h.2)
+  exact sub_nonneg.2 (Real.sInf_le_sSup s h.bddBelow h.bddAbove)
 #align real.diam_eq Real.diam_eq
 
 @[simp]

Mathlib/Topology/Instances/Real.lean

@@ -9,6 +9,7 @@ import Mathlib.Topology.Algebra.Order.Field
 import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Instances.Int
+import Mathlib.Topology.Order.Bornology
 
 #align_import topology.instances.real from "leanprover-community/mathlib"@"9a59dcb7a2d06bf55da57b9030169219980660cd"
 
@@ -176,22 +177,16 @@ lemma closure_of_rat_image_le_le_eq {a b : ℚ} (hab : a ≤ b) :
     closure (of_rat '' {q:ℚ | a ≤ q ∧ q ≤ b}) = {r:ℝ | of_rat a ≤ r ∧ r ≤ of_rat b} :=
   _
 -/
-theorem Real.isBounded_iff_bddBelow_bddAbove {s : Set ℝ} : IsBounded s ↔ BddBelow s ∧ BddAbove s :=
-  ⟨fun bdd ↦ by
-    obtain ⟨r, hr⟩ : ∃ r : ℝ, s ⊆ Icc (-r) r := by
-      simpa [Real.closedBall_eq_Icc] using bdd.subset_closedBall 0
-    exact ⟨bddBelow_Icc.mono hr, bddAbove_Icc.mono hr⟩,
-    fun h => isBounded_of_bddAbove_of_bddBelow h.2 h.1⟩
-#align real.bounded_iff_bdd_below_bdd_above Real.isBounded_iff_bddBelow_bddAbove
-
-theorem Real.subset_Icc_sInf_sSup_of_isBounded {s : Set ℝ} (h : IsBounded s) :
-    s ⊆ Icc (sInf s) (sSup s) :=
-  subset_Icc_csInf_csSup (Real.isBounded_iff_bddBelow_bddAbove.1 h).1
-    (Real.isBounded_iff_bddBelow_bddAbove.1 h).2
-#align real.subset_Icc_Inf_Sup_of_bounded Real.subset_Icc_sInf_sSup_of_isBounded
 
 end
 
+instance instIsOrderBornology : IsOrderBornology ℝ where
+  isBounded_iff_bddBelow_bddAbove s := by
+    refine ⟨fun bdd ↦ ?_, fun h ↦ isBounded_of_bddAbove_of_bddBelow h.2 h.1⟩
+    obtain ⟨r, hr⟩ : ∃ r : ℝ, s ⊆ Icc (-r) r := by
+      simpa [Real.closedBall_eq_Icc] using bdd.subset_closedBall 0
+    exact ⟨bddBelow_Icc.mono hr, bddAbove_Icc.mono hr⟩
+
 section Periodic
 
 namespace Function