From cf1e03a54821e7ef4681be769106449f7baf100a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 14 Feb 2024 16:27:09 -0600 Subject: [PATCH 1/4] =?UTF-8?q?feat:=20Topological=20properties=20of=20ord?= =?UTF-8?q?er-connected=20sets=20in=20=E2=84=9D=E2=81=BF?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib.lean | 1 + Mathlib/Analysis/Normed/Order/UpperLower.lean | 132 ++++++++++++++++-- .../Integral/BoundedContinuousFunction.lean | 13 +- .../MeasureTheory/Measure/Lebesgue/Basic.lean | 2 +- Mathlib/Order/Bounds/Basic.lean | 15 +- Mathlib/Order/LiminfLimsup.lean | 10 ++ Mathlib/Topology/Bornology/Basic.lean | 19 +++ .../Topology/ContinuousFunction/Bounded.lean | 2 +- Mathlib/Topology/Instances/ENNReal.lean | 11 +- Mathlib/Topology/Instances/Real.lean | 21 ++- .../MetricSpace/GromovHausdorffRealized.lean | 16 +-- Mathlib/Topology/Order/Bornology.lean | 111 +++++++++++++++ Mathlib/Topology/Order/Bounded.lean | 8 +- Mathlib/Topology/TietzeExtension.lean | 6 +- 14 files changed, 306 insertions(+), 61 deletions(-) create mode 100644 Mathlib/Topology/Order/Bornology.lean diff --git a/Mathlib.lean b/Mathlib.lean index 17a7109539c1b..d33d4402c95cc 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4214,6 +4214,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 diff --git a/Mathlib/Analysis/Normed/Order/UpperLower.lean b/Mathlib/Analysis/Normed/Order/UpperLower.lean index 657e67f4755d7..028c3c902db38 100644 --- a/Mathlib/Analysis/Normed/Order/UpperLower.lean +++ b/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,41 @@ 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 (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 -variable [Fintype ι] {s : Set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ} +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 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 +206,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 diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean index 42f95e9afb434..21d319b98f6c2 100644 --- a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean index 5794cf805b9e9..617562ed14940 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean +++ b/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 diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index 86dc6fa05bdaa..198293037c37c 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/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] diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean index ce8b03b4a5587..2a193f7d5ec6e 100644 --- a/Mathlib/Order/LiminfLimsup.lean +++ b/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) := diff --git a/Mathlib/Topology/Bornology/Basic.lean b/Mathlib/Topology/Bornology/Basic.lean index bf366eb2e0a91..a4fc7d2fef2a1 100644 --- a/Mathlib/Topology/Bornology/Basic.lean +++ b/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 diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean index 1cb193a5f4391..29f86cf839a2c 100644 --- a/Mathlib/Topology/ContinuousFunction/Bounded.lean +++ b/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 diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 13d98bae1073d..6932fc5646cec 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/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] diff --git a/Mathlib/Topology/Instances/Real.lean b/Mathlib/Topology/Instances/Real.lean index ef6ead6af20c5..961480d80a12d 100644 --- a/Mathlib/Topology/Instances/Real.lean +++ b/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 diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean index 5e5dff37511bb..590496607a3f5 100644 --- a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean +++ b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean @@ -292,13 +292,13 @@ to check that the defining sets are bounded below or above. This is done in the technical lemmas. -/ theorem HD_below_aux1 {f : Cb X Y} (C : ℝ) {x : X} : BddBelow (range fun y : Y => f (inl x, inr y) + C) := - let ⟨cf, hcf⟩ := (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1 + let ⟨cf, hcf⟩ := f.isBounded_range.bddBelow ⟨cf + C, forall_mem_range.2 fun _ => add_le_add_right ((fun x => hcf (mem_range_self x)) _) _⟩ #align Gromov_Hausdorff.HD_below_aux1 GromovHausdorff.HD_below_aux1 private theorem HD_bound_aux1 (f : Cb X Y) (C : ℝ) : BddAbove (range fun x : X => ⨅ y, f (inl x, inr y) + C) := by - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).2 with ⟨Cf, hCf⟩ + obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩ calc ⨅ y, f (inl x, inr y) + C ≤ f (inl x, inr default) + C := ciInf_le (HD_below_aux1 C) default @@ -306,13 +306,13 @@ private theorem HD_bound_aux1 (f : Cb X Y) (C : ℝ) : theorem HD_below_aux2 {f : Cb X Y} (C : ℝ) {y : Y} : BddBelow (range fun x : X => f (inl x, inr y) + C) := - let ⟨cf, hcf⟩ := (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1 + let ⟨cf, hcf⟩ := f.isBounded_range.bddBelow ⟨cf + C, forall_mem_range.2 fun _ => add_le_add_right ((fun x => hcf (mem_range_self x)) _) _⟩ #align Gromov_Hausdorff.HD_below_aux2 GromovHausdorff.HD_below_aux2 private theorem HD_bound_aux2 (f : Cb X Y) (C : ℝ) : BddAbove (range fun y : Y => ⨅ x, f (inl x, inr y) + C) := by - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).2 with ⟨Cf, hCf⟩ + obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩ calc ⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default @@ -347,9 +347,9 @@ theorem HD_candidatesBDist_le : prove separately inequalities controlling the two terms (relying too heavily on copy-paste...) -/ private theorem HD_lipschitz_aux1 (f g : Cb X Y) : (⨆ x, ⨅ y, f (inl x, inr y)) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g := by - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 g.isBounded_range).1 with ⟨cg, hcg⟩ + obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x) - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1 with ⟨cf, hcf⟩ + obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x) -- prove the inequality but with `dist f g` inside, by using inequalities comparing -- iSup to iSup and iInf to iInf @@ -375,9 +375,9 @@ private theorem HD_lipschitz_aux1 (f g : Cb X Y) : private theorem HD_lipschitz_aux2 (f g : Cb X Y) : (⨆ y, ⨅ x, f (inl x, inr y)) ≤ (⨆ y, ⨅ x, g (inl x, inr y)) + dist f g := by - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 g.isBounded_range).1 with ⟨cg, hcg⟩ + obtain ⟨cg, hcg⟩ := g.isBounded_range.bddBelow have Hcg : ∀ x, cg ≤ g x := fun x => hcg (mem_range_self x) - rcases (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1 with ⟨cf, hcf⟩ + obtain ⟨cf, hcf⟩ := f.isBounded_range.bddBelow have Hcf : ∀ x, cf ≤ f x := fun x => hcf (mem_range_self x) -- prove the inequality but with `dist f g` inside, by using inequalities comparing -- iSup to iSup and iInf to iInf diff --git a/Mathlib/Topology/Order/Bornology.lean b/Mathlib/Topology/Order/Bornology.lean new file mode 100644 index 0000000000000..910f20c47c0a3 --- /dev/null +++ b/Mathlib/Topology/Order/Bornology.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2024 Yaël Dillies. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies +-/ +import Mathlib.Topology.Bornology.Constructions + +/-! +# Bornology of order-bounded sets + +This file relates the notion of bornology-boundedness (sets that lie in a bornology) to the notion +of order-boundedness (sets that are bounded above and below). + +## Main declarations + +* `orderBornology`: The bornology of order-bounded sets of a nonempty lattice. +* `IsOrderBornology`: Typeclass predicate for a preorder to be equipped with its order-bornology. +-/ + +open Bornology Set + +variable {α : Type*} [Bornology α] {s t : Set α} + +section Lattice +variable [Lattice α] [Nonempty α] + +/-- Order-bornology on a nonempty lattice. The bounded sets are the sets that are bounded both above +and below. -/ +def orderBornology : Bornology α := .ofBounded + {s | BddBelow s ∧ BddAbove s} + (by simp) + (fun s hs t hst ↦ ⟨hs.1.mono hst, hs.2.mono hst⟩) + (fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩) + (by simp) + +@[simp] lemma orderBornology_isBounded : orderBornology.IsBounded s ↔ BddBelow s ∧ BddAbove s := by + simp [IsBounded, IsCobounded, -isCobounded_compl_iff] + +end Lattice + +variable (α) [Preorder α] in +/-- Predicate for a preorder to be equipped with its order-bornology, namely for its bounded sets +to be the ones that are bounded both above and below. -/ +class IsOrderBornology : Prop where + protected isBounded_iff_bddBelow_bddAbove (s : Set α) : IsBounded s ↔ BddBelow s ∧ BddAbove s + +lemma isOrderBornology_iff_eq_orderBornology [Lattice α] [Nonempty α] : + IsOrderBornology α ↔ ‹Bornology α› = orderBornology := by + refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩ + ext s + exact isBounded_compl_iff.symm.trans (h.1 _) + +section Preorder +variable [Preorder α] [IsOrderBornology α] + +lemma isBounded_iff_bddBelow_bddAbove : IsBounded s ↔ BddBelow s ∧ BddAbove s := + IsOrderBornology.isBounded_iff_bddBelow_bddAbove _ +#align bounded_iff_bdd_below_bdd_above isBounded_iff_bddBelow_bddAbove +#align real.bounded_iff_bdd_below_bdd_above isBounded_iff_bddBelow_bddAbove + +protected lemma Bornology.IsBounded.bddBelow (hs : IsBounded s) : BddBelow s := + (isBounded_iff_bddBelow_bddAbove.1 hs).1 +#align metric.bounded.bdd_below Bornology.IsBounded.bddBelow + +protected lemma Bornology.IsBounded.bddAbove (hs : IsBounded s) : BddAbove s := + (isBounded_iff_bddBelow_bddAbove.1 hs).2 +#align metric.bounded.bdd_above Bornology.IsBounded.bddAbove + +protected lemma BddBelow.isBounded (hs₀ : BddBelow s) (hs₁ : BddAbove s) : IsBounded s := + isBounded_iff_bddBelow_bddAbove.2 ⟨hs₀, hs₁⟩ +#align bdd_below.bounded BddBelow.isBounded + +protected lemma BddAbove.isBounded (hs₀ : BddAbove s) (hs₁ : BddBelow s) : IsBounded s := + isBounded_iff_bddBelow_bddAbove.2 ⟨hs₁, hs₀⟩ +#align bdd_above.bounded BddAbove.isBounded + +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 + +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 + +instance OrderDual.instIsOrderBornology : IsOrderBornology αᵒᵈ where + isBounded_iff_bddBelow_bddAbove s := by + rw [← isBounded_preimage_toDual, ← bddBelow_preimage_toDual, ← bddAbove_preimage_toDual, + isBounded_iff_bddBelow_bddAbove, and_comm] + +instance Prod.instIsOrderBornology {β : Type*} [Preorder β] [Bornology β] [IsOrderBornology β] : + IsOrderBornology (α × β) where + isBounded_iff_bddBelow_bddAbove s := by + rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm, + isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove] + +instance Pi.instIsOrderBornology {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] + [∀ i, Bornology (α i)] [∀ i, IsOrderBornology (α i)] : IsOrderBornology (∀ i, α i) where + isBounded_iff_bddBelow_bddAbove s := by + simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and, + isBounded_iff_bddBelow_bddAbove] + +end Preorder + +section ConditionallyCompleteLattice +variable [ConditionallyCompleteLattice α] [IsOrderBornology α] {s : Set α} + +protected lemma Bornology.IsBounded.subset_Icc_sInf_sSup (hs : IsBounded s) : + s ⊆ Icc (sInf s) (sSup s) := subset_Icc_csInf_csSup hs.bddBelow hs.bddAbove +#align real.subset_Icc_Inf_Sup_of_bounded Bornology.IsBounded.subset_Icc_sInf_sSup + +end ConditionallyCompleteLattice diff --git a/Mathlib/Topology/Order/Bounded.lean b/Mathlib/Topology/Order/Bounded.lean index 6230f50c07b87..9d7a19e970c6f 100644 --- a/Mathlib/Topology/Order/Bounded.lean +++ b/Mathlib/Topology/Order/Bounded.lean @@ -23,18 +23,18 @@ open Set Filter section Real +@[deprecated isBoundedUnder_of (since := "2024-06-07")] lemma Filter.isBounded_le_map_of_bounded_range {ι : Type*} (F : Filter ι) {f : ι → ℝ} (h : Bornology.IsBounded (Set.range f)) : (F.map f).IsBounded (· ≤ ·) := by - rw [Real.isBounded_iff_bddBelow_bddAbove] at h - obtain ⟨c, hc⟩ := h.2 + obtain ⟨c, hc⟩ := h.bddAbove exact isBoundedUnder_of ⟨c, by simpa [mem_upperBounds] using hc⟩ +@[deprecated isBoundedUnder_of (since := "2024-06-07")] lemma Filter.isBounded_ge_map_of_bounded_range {ι : Type*} (F : Filter ι) {f : ι → ℝ} (h : Bornology.IsBounded (Set.range f)) : (F.map f).IsBounded (· ≥ ·) := by - rw [Real.isBounded_iff_bddBelow_bddAbove] at h - obtain ⟨c, hc⟩ := h.1 + obtain ⟨c, hc⟩ := h.bddBelow apply isBoundedUnder_of ⟨c, by simpa [mem_lowerBounds] using hc⟩ end Real diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index c4c4edc176bb0..1e967a295d1f1 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/Mathlib/Topology/TietzeExtension.lean @@ -316,10 +316,8 @@ theorem exists_extension_forall_exists_le_ge_of_closedEmbedding [Nonempty X] (f ∃ g : Y →ᵇ ℝ, (∀ y, ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ g ∘ e = f := by inhabit X -- Put `a = ⨅ x, f x` and `b = ⨆ x, f x` - obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := - ⟨_, isGLB_ciInf (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).1⟩ - obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b := - ⟨_, isLUB_ciSup (Real.isBounded_iff_bddBelow_bddAbove.1 f.isBounded_range).2⟩ + obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := ⟨_, isGLB_ciInf f.isBounded_range.bddBelow⟩ + obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b := ⟨_, isLUB_ciSup f.isBounded_range.bddAbove⟩ -- Then `f x ∈ [a, b]` for all `x` have hmem : ∀ x, f x ∈ Icc a b := fun x => ⟨ha.1 ⟨x, rfl⟩, hb.1 ⟨x, rfl⟩⟩ -- Rule out the trivial case `a = b` From bf28fbf5f0bd634c8aa7c60825942447d354a4f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 7 Jun 2024 09:21:42 +0000 Subject: [PATCH 2/4] fix --- Mathlib/Analysis/Normed/Order/UpperLower.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Normed/Order/UpperLower.lean b/Mathlib/Analysis/Normed/Order/UpperLower.lean index 028c3c902db38..1ab44af4d54c8 100644 --- a/Mathlib/Analysis/Normed/Order/UpperLower.lean +++ b/Mathlib/Analysis/Normed/Order/UpperLower.lean @@ -226,7 +226,7 @@ protected lemma IsClosed.upperClosure_pi (hs : IsClosed s) (hs' : BddBelow s) : 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, + 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 @@ -239,7 +239,7 @@ protected lemma IsClosed.lowerClosure_pi (hs : IsClosed s) (hs' : BddAbove s) : 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, + 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 From 30e64649aac9170af51852fcca5a5349f9062f8c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 7 Jun 2024 18:09:08 +0000 Subject: [PATCH 3/4] add more `_pi` --- Mathlib/Analysis/Normed/Order/UpperLower.lean | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/Mathlib/Analysis/Normed/Order/UpperLower.lean b/Mathlib/Analysis/Normed/Order/UpperLower.lean index 1ab44af4d54c8..92b9715245a27 100644 --- a/Mathlib/Analysis/Normed/Order/UpperLower.lean +++ b/Mathlib/Analysis/Normed/Order/UpperLower.lean @@ -134,38 +134,38 @@ 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 +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 +#align dist_inf_sup dist_inf_sup_pi -lemma dist_mono_left : MonotoneOn (dist · y) (Ici y) := by +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 +#align dist_mono_left dist_mono_left_pi -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_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 -lemma dist_anti_left : AntitoneOn (dist · y) (Iic y) := by +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 +#align dist_anti_left dist_anti_left_pi -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_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 (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 +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 From 5c9503d04cc6099666f42237101052a55d319e36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 7 Jun 2024 18:15:53 +0000 Subject: [PATCH 4/4] long line --- Mathlib/Analysis/Normed/Order/UpperLower.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Normed/Order/UpperLower.lean b/Mathlib/Analysis/Normed/Order/UpperLower.lean index 92b9715245a27..0a73b0807d7e5 100644 --- a/Mathlib/Analysis/Normed/Order/UpperLower.lean +++ b/Mathlib/Analysis/Normed/Order/UpperLower.lean @@ -162,7 +162,8 @@ 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₂ := +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