[Merged by Bors] - feat: Small sets of games/surreals are bounded

Mathlib/Analysis/Normed/Order/UpperLower.lean

@@ -8,8 +8,10 @@
 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
@@ -22,13 +24,12 @@
 are measurable.
 -/
 
-
-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 +64,25 @@
 #align is_lower_set.cthickening' IsLowerSet.cthickening'
 #align is_lower_set.cthickening IsLowerSet.cthickening
 
-end MetricSpace
+@[to_additive upper_closure_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 upper_closure_interior_subset
+
+@[to_additive lower_closure_interior_subset] lemma lower_closure_interior_subset' (s : Set α) :
+    (upperClosure (interior s) : Set α) ⊆ interior (upperClosure s) :=
+  upperClosure_min (interior_mono subset_upperClosure) (upperClosure s).upper.interior
+#align lower_closure_interior_subset' lower_closure_interior_subset'
+#align lower_closure_interior_subset lower_closure_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 +124,82 @@
 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 (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
+
+lemma dist_mono_left : 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
+
+lemma dist_mono_right : MonotoneOn (dist x) (Ici x) := by
+  simpa only [dist_comm _ x] using dist_mono_left (y := x)
+#align dist_mono_right dist_mono_right
+
+lemma dist_anti_left : 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
+
+lemma dist_anti_right : AntitoneOn (dist x) (Iic x) := by
+  simpa only [dist_comm] using dist_anti_left (y := x)
+#align dist_anti_right dist_anti_right
+
+lemma dist_le_dist_of_le (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂ :=
+  (dist_mono_right h₁ (h₁.trans hb) hb).trans $
+    dist_anti_left (ha.trans $ h₁.trans hb) (h₁.trans hb) ha
+#align dist_le_dist_of_le dist_le_dist_of_le
+
+protected lemma Bornology.IsBounded.bddBelow : IsBounded s → BddBelow s := by
+  rw [isBounded_iff]
+  rintro ⟨r, hr⟩
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
+  · exact bddBelow_empty
+  · exact ⟨(x · - r), fun y hy i ↦
+      sub_le_comm.1 (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr hx hy).1⟩
+#align metric.bounded.bdd_below Bornology.IsBounded.bddBelow
+
+protected lemma Bornology.IsBounded.bddAbove : IsBounded s → BddAbove s := by
+  rw [isBounded_iff]
+  rintro ⟨r, hr⟩
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
+  · exact bddAbove_empty
+  · exact ⟨(x · + r), fun y hy i ↦
+      sub_le_iff_le_add'.1 $ (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr hx hy).2⟩
+#align metric.bounded.bdd_above Bornology.IsBounded.bddAbove
+
+protected lemma BddBelow.isBounded : BddBelow s → BddAbove s → IsBounded s := by
+  rintro ⟨a, ha⟩ ⟨b, hb⟩
+  refine isBounded_iff.2 ⟨dist a b, fun x hx y hy ↦ ?_⟩
+  rw [← dist_inf_sup]
+  exact dist_le_dist_of_le (le_inf (ha hx) $ ha hy) inf_le_sup (sup_le (hb hx) $ hb hy)
+#align bdd_below.bounded BddBelow.isBounded
+
+protected lemma BddAbove.isBounded : BddAbove s → BddBelow s → IsBounded s :=
+  flip BddBelow.isBounded
+#align bdd_above.bounded BddAbove.isBounded
+
+lemma isBounded_iff_bddBelow_bddAbove : IsBounded s ↔ BddBelow s ∧ BddAbove s :=
+  ⟨fun h ↦ ⟨h.bddBelow, h.bddAbove⟩, fun h ↦ h.1.isBounded h.2⟩
+#align bounded_iff_bdd_below_bdd_above isBounded_iff_bddBelow_bddAbove
+
+lemma BddBelow.isBounded_inter (hs : BddBelow s) (ht : BddAbove t) : IsBounded (s ∩ t) :=
+  (hs.mono $ inter_subset_left _ _).isBounded $ ht.mono $ inter_subset_right _ _
+#align bdd_below.bounded_inter BddBelow.isBounded_inter
 
-variable [Fintype ι] {s : Set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+lemma BddAbove.isBounded_inter (hs : BddAbove s) (ht : BddBelow t) : IsBounded (s ∩ t) :=
+  (hs.mono $ inter_subset_left _ _).isBounded $ ht.mono $ inter_subset_right _ _
+#align bdd_above.bounded_inter BddAbove.isBounded_inter
 
 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 +240,64 @@
 #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 theorem IsClosed.upperClosure (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
+
+protected lemma IsClosed.lowerClosure (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
+
+protected lemma IsClopen.upperClosure (hs : IsClopen s) (hs' : BddBelow s) :
+    IsClopen (upperClosure s : Set (ι → ℝ)) := ⟨hs.1.upperClosure hs', hs.2.upperClosure⟩
+#align is_clopen.upper_closure IsClopen.upperClosure
+
+protected lemma IsClopen.lowerClosure (hs : IsClopen s) (hs' : BddAbove s) :
+    IsClopen (lowerClosure s : Set (ι → ℝ)) := ⟨hs.1.lowerClosure hs', hs.2.lowerClosure⟩
+#align is_clopen.lower_closure IsClopen.lowerClosure
+
+lemma closure_upperClosure_comm (hs : BddBelow s) :
+    closure (upperClosure s : Set (ι → ℝ)) = upperClosure (closure s) :=
+  (closure_minimal (upperClosure_anti subset_closure) $
+      isClosed_closure.upperClosure hs.closure).antisymm $
+    upperClosure_min (closure_mono subset_upperClosure) (upperClosure s).upper.closure
+#align closure_upper_closure_comm closure_upperClosure_comm
+
+lemma closure_lowerClosure_comm (hs : BddAbove s) :
+    closure (lowerClosure s : Set (ι → ℝ)) = lowerClosure (closure s) :=
+  (closure_minimal (lowerClosure_mono subset_closure) $
+        isClosed_closure.lowerClosure hs.closure).antisymm $
+    lowerClosure_min (closure_mono subset_lowerClosure) (lowerClosure s).lower.closure
+#align closure_lower_closure_comm closure_lowerClosure_comm
+
+end Finite

Mathlib/Data/Real/NNReal.lean

@@ -12,7 +12,7 @@
 import Mathlib.Order.ConditionallyCompleteLattice.Group
 import Mathlib.Tactic.GCongr.Core
 
-#align_import data.real.nnreal from "leanprover-community/mathlib"@"de29c328903507bb7aff506af9135f4bdaf1849c"
+#align_import data.real.nnreal from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
 
 /-!
 # Nonnegative real numbers
@@ -1181,6 +1181,9 @@
   max_le (le_abs_self _) (abs_nonneg _)
 #align real.coe_to_nnreal_le Real.coe_toNNReal_le
 
+@[simp] lemma toNNReal_abs (x : ℝ) : |x|.toNNReal = nnabs x := NNReal.coe_injective <| by simp
+#align real.to_nnreal_abs Real.toNNReal_abs
+
 theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n := by
   ext
   rw [NNReal.coe_nat_cast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]