From d19a0cebe970698b6a03b17388112c6a66f28f88 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 11 Jun 2024 23:44:44 +0000 Subject: [PATCH] chore: fix junk value for `sInf` on `WithTop` (#13717) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit As pointed out in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Definition.20of.20.60WithTop.2EinstInfSet.60/near/443609808, the current choice of junk value for `sInf s` when `s : Set (WithTop α)` is not bounded below does not coincide with `sInf ∅`. This makes it impossible to get a `ConditionallyCompleteLinearOrder` structure on `WithTop α` as we require the junk values to coincide. This PR fixes the choice of junk value for `sInf s` when `s : Set (WithTop α)` is not bounded below, making it equal to `⊤ = sInf ∅`. --- Mathlib/Data/ENNReal/Basic.lean | 6 +- Mathlib/Data/ENat/Lattice.lean | 9 ++- .../ConditionallyCompleteLattice/Basic.lean | 76 +++++++++++-------- 3 files changed, 53 insertions(+), 38 deletions(-) diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index a49efb497e2d8..0edb8314a28f6 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -753,8 +753,8 @@ theorem coe_sSup {s : Set ℝ≥0} : BddAbove s → (↑(sSup s) : ℝ≥0∞) = WithTop.coe_sSup #align ennreal.coe_Sup ENNReal.coe_sSup -theorem coe_sInf {s : Set ℝ≥0} : s.Nonempty → (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a := - WithTop.coe_sInf +theorem coe_sInf {s : Set ℝ≥0} (hs : s.Nonempty) : (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a := + WithTop.coe_sInf hs (OrderBot.bddBelow s) #align ennreal.coe_Inf ENNReal.coe_sInf theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) : @@ -764,7 +764,7 @@ theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) : @[norm_cast] theorem coe_iInf {ι : Sort*} [Nonempty ι] (f : ι → ℝ≥0) : (↑(iInf f) : ℝ≥0∞) = ⨅ a, ↑(f a) := - WithTop.coe_iInf f + WithTop.coe_iInf (OrderBot.bddBelow _) #align ennreal.coe_infi ENNReal.coe_iInf theorem coe_mem_upperBounds {s : Set ℝ≥0} : diff --git a/Mathlib/Data/ENat/Lattice.lean b/Mathlib/Data/ENat/Lattice.lean index b26781573bdcc..7b44a65a49b36 100644 --- a/Mathlib/Data/ENat/Lattice.lean +++ b/Mathlib/Data/ENat/Lattice.lean @@ -36,8 +36,13 @@ lemma iInf_coe_ne_top : ⨅ i, (f i : ℕ∞) ≠ ⊤ ↔ Nonempty ι := by lemma iInf_coe_lt_top : ⨅ i, (f i : ℕ∞) < ⊤ ↔ Nonempty ι := WithTop.iInf_coe_lt_top lemma coe_sSup : BddAbove s → ↑(sSup s) = ⨆ a ∈ s, (a : ℕ∞) := WithTop.coe_sSup -lemma coe_sInf : s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞) := WithTop.coe_sInf + +lemma coe_sInf (hs : s.Nonempty) : ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞) := + WithTop.coe_sInf hs (OrderBot.bddBelow s) + lemma coe_iSup : BddAbove (range f) → ↑(⨆ i, f i) = ⨆ i, (f i : ℕ∞) := WithTop.coe_iSup _ -@[norm_cast] lemma coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) := WithTop.coe_iInf _ + +@[norm_cast] lemma coe_iInf [Nonempty ι] : ↑(⨅ i, f i) = ⨅ i, (f i : ℕ∞) := + WithTop.coe_iInf (OrderBot.bddBelow _) end ENat diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean index f98ecd6b52e1d..b92fd4a7cb472 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean @@ -42,61 +42,64 @@ section Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α` -/ +variable [Preorder α] open scoped Classical -noncomputable instance WithTop.instSupSet {α : Type*} [Preorder α] [SupSet α] : +noncomputable instance WithTop.instSupSet [SupSet α] : SupSet (WithTop α) := ⟨fun S => if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then ↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩ -noncomputable instance WithTop.instInfSet {α : Type*} [InfSet α] : InfSet (WithTop α) := - ⟨fun S => if S ⊆ {⊤} then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩ +noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) := + ⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩ -noncomputable instance WithBot.instSupSet {α : Type*} [SupSet α] : SupSet (WithBot α) := +noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) := ⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩ -noncomputable instance WithBot.instInfSet {α : Type*} [Preorder α] [InfSet α] : +noncomputable instance WithBot.instInfSet [InfSet α] : InfSet (WithBot α) := ⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩ -theorem WithTop.sSup_eq [Preorder α] [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) +theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) (hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) := (if_neg hs).trans <| if_pos hs' #align with_top.Sup_eq WithTop.sSup_eq -theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) : +theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α) := - if_neg hs + if_neg <| by simp [hs, h's] #align with_top.Inf_eq WithTop.sInf_eq -theorem WithBot.sInf_eq [Preorder α] [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) +theorem WithBot.sInf_eq [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) (hs' : BddBelow ((↑) ⁻¹' s : Set α)) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α) := (if_neg hs).trans <| if_pos hs' #align with_bot.Inf_eq WithBot.sInf_eq -theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) : +theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) := - if_neg hs + WithTop.sInf_eq (α := αᵒᵈ) hs h's #align with_bot.Sup_eq WithBot.sSup_eq @[simp] -theorem WithTop.sInf_empty {α : Type*} [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ := - if_pos <| Set.empty_subset _ +theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ := + if_pos <| by simp #align with_top.cInf_empty WithTop.sInf_empty @[simp] -theorem WithTop.iInf_empty {α : Type*} [IsEmpty ι] [InfSet α] (f : ι → WithTop α) : +theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) : ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty] #align with_top.cinfi_empty WithTop.iInf_empty -theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) : +theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by obtain ⟨x, hx⟩ := hs change _ = ite _ _ _ split_ifs with h - · cases h (mem_image_of_mem _ hx) + · rcases h with h1 | h2 + · cases h1 (mem_image_of_mem _ hx) + · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim · rw [preimage_image_eq] exact Option.some_injective _ #align with_top.coe_Inf' WithTop.coe_sInf' @@ -104,12 +107,13 @@ theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) : -- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and -- does not need `rfl`. @[norm_cast] -theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] (f : ι → α) : +theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by - rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f), ← range_comp]; rfl + rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp] + rfl #align with_top.coe_infi WithTop.coe_iInf -theorem WithTop.coe_sSup' [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove s) : +theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) : ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by change _ = ite _ _ _ rw [if_neg, preimage_image_eq, if_pos hs] @@ -120,42 +124,44 @@ theorem WithTop.coe_sSup' [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove -- Porting note: the mathlib3 proof uses `range_comp` in the opposite direction and -- does not need `rfl`. @[norm_cast] -theorem WithTop.coe_iSup [Preorder α] [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : +theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp]; rfl #align with_top.coe_supr WithTop.coe_iSup @[simp] -theorem WithBot.csSup_empty {α : Type*} [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ := - if_pos <| Set.empty_subset _ -#align with_bot.cSup_empty WithBot.csSup_empty +theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ := + WithTop.sInf_empty (α := αᵒᵈ) +#align with_bot.cSup_empty WithBot.sSup_empty + +@[deprecated (since := "2024-06-10")] alias WithBot.csSup_empty := WithBot.sSup_empty @[simp] -theorem WithBot.ciSup_empty {α : Type*} [IsEmpty ι] [SupSet α] (f : ι → WithBot α) : +theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) : ⨆ i, f i = ⊥ := WithTop.iInf_empty (α := αᵒᵈ) _ #align with_bot.csupr_empty WithBot.ciSup_empty @[norm_cast] -theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) : +theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) : ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) := - WithTop.coe_sInf' (α := αᵒᵈ) hs + WithTop.coe_sInf' (α := αᵒᵈ) hs h's #align with_bot.coe_Sup' WithBot.coe_sSup' @[norm_cast] -theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] (f : ι → α) : +theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) : ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) := - WithTop.coe_iInf (α := αᵒᵈ) _ + WithTop.coe_iInf (α := αᵒᵈ) hf #align with_bot.coe_supr WithBot.coe_iSup @[norm_cast] -theorem WithBot.coe_sInf' [Preorder α] [InfSet α] {s : Set α} (hs : BddBelow s) : +theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) : ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) := WithTop.coe_sSup' (α := αᵒᵈ) hs #align with_bot.coe_Inf' WithBot.coe_sInf' @[norm_cast] -theorem WithBot.coe_iInf [Preorder α] [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : +theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) := WithTop.coe_iSup (α := αᵒᵈ) _ h #align with_bot.coe_infi WithBot.coe_iInf @@ -1335,6 +1341,7 @@ theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (Wit (hs : BddBelow s) : IsGLB s (sInf s) := by constructor · show ite _ _ _ ∈ _ + simp only [hs, not_true_eq_false, or_false] split_ifs with h · intro a ha exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha)) @@ -1351,6 +1358,7 @@ theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (Wit intro c hc exact coe_le_coe.1 (hb hc) · show ite _ _ _ ∈ _ + simp only [hs, not_true_eq_false, or_false] split_ifs with h · intro _ _ exact le_top @@ -1397,8 +1405,9 @@ theorem coe_sSup {s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, /-- A version of `WithTop.coe_sInf'` with a more convenient but less general statement. -/ @[norm_cast] -theorem coe_sInf {s : Set α} (hs : s.Nonempty) : ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by - rw [coe_sInf' hs, sInf_image] +theorem coe_sInf {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : + ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by + rw [coe_sInf' hs h's, sInf_image] #align with_top.coe_Inf WithTop.coe_sInf end WithTop @@ -1658,7 +1667,7 @@ noncomputable instance WithTop.WithBot.completeLattice {α : Type*} -- Porting note: previous proof relied on convert unfolding -- the definition of ⊥ apply congr_arg - simp only [h, preimage_empty, WithBot.csSup_empty] + simp only [h, preimage_empty, WithBot.sSup_empty] · exfalso apply h₂ use ⊥ @@ -1667,6 +1676,7 @@ noncomputable instance WithTop.WithBot.completeLattice {α : Type*} · exact (WithTop.isLUB_sSup' h).2 ha sInf_le := fun S a haS => show ite _ _ _ ≤ a by + simp only [OrderBot.bddBelow, not_true_eq_false, or_false] split_ifs with h₁ · cases' a with a · exact le_rfl