From cef1b6c38e62c0b5ae2a979fbeb66e095ddfc50b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 5 Jan 2025 22:04:38 -0600 Subject: [PATCH 1/5] generalize --- Mathlib/Order/SuccPred/CompleteLinearOrder.lean | 16 +++++++++------- Mathlib/Order/SuccPred/Limit.lean | 11 +++++++++++ 2 files changed, 20 insertions(+), 7 deletions(-) diff --git a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean index 748703d2d7787..66aaec8417a91 100644 --- a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean +++ b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean @@ -123,17 +123,17 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit' @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")] alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit' -lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := by - obtain rfl | hs' := s.eq_empty_or_nonempty - · simp [show x = ⊥ by simpa using hs, isSuccPrelimit_bot] at hx - · exact hs.mem_of_nonempty_of_not_isSuccPrelimit hs' hx +@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")] +lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := + hx.imp_symm hs.isSuccPrelimit_of_not_mem @[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")] alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit +@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")] lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) : ∃ i, f i = x := - hf.mem_of_not_isSuccPrelimit hx + hx.imp_symm hf.isSuccPrelimit_of_not_mem @[deprecated IsLUB.exists_of_not_isSuccPrelimit (since := "2024-09-05")] alias IsLUB.exists_of_not_isSuccLimit := IsLUB.exists_of_not_isSuccPrelimit @@ -199,15 +199,17 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i)) @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")] alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit +@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")] lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s := - hs.sInf_eq ▸ sInf_mem_of_not_isPredPrelimit (hs.sInf_eq ▸ hx) + hx.imp_symm hs.isPredPrelimit_of_not_mem @[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")] alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit +@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")] lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : ∃ i, f i = x := - hf.mem_of_not_isPredPrelimit hx + hx.imp_symm hf.isPredPrelimit_of_not_mem @[deprecated IsGLB.exists_of_not_isPredPrelimit (since := "2024-09-05")] alias IsGLB.exists_of_not_isPredLimit := IsGLB.exists_of_not_isPredPrelimit diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean index 2497ef7e19efd..bf5648f907a72 100644 --- a/Mathlib/Order/SuccPred/Limit.lean +++ b/Mathlib/Order/SuccPred/Limit.lean @@ -324,6 +324,13 @@ theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c theorem IsSuccLimit.lt_iff_exists_lt (h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c := h.isSuccPrelimit.lt_iff_exists_lt +lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hx : a ∉ s) : + IsSuccPrelimit a := by + intro b hb + obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt + obtain rfl := (hb.ge_of_gt hbc).antisymm hca + contradiction + variable [SuccOrder α] theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a := @@ -620,6 +627,10 @@ theorem IsPredPrelimit.lt_iff_exists_lt (h : IsPredPrelimit b) : b < a ↔ ∃ c theorem IsPredLimit.lt_iff_exists_lt (h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a := h.dual.lt_iff_exists_lt +lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hx : a ∉ s) : + IsPredPrelimit a := by + simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem hx + variable [PredOrder α] theorem IsPredPrelimit.pred_le_iff (hb : IsPredPrelimit b) : pred a ≤ b ↔ a ≤ b := From 3c69b335e7b710abcf9767c07da0fd31096240ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 5 Jan 2025 22:24:51 -0600 Subject: [PATCH 2/5] add other aux lemma --- Mathlib/Order/SuccPred/Limit.lean | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean index bf5648f907a72..6afdc5770dc8d 100644 --- a/Mathlib/Order/SuccPred/Limit.lean +++ b/Mathlib/Order/SuccPred/Limit.lean @@ -324,13 +324,21 @@ theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c theorem IsSuccLimit.lt_iff_exists_lt (h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c := h.isSuccPrelimit.lt_iff_exists_lt -lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hx : a ∉ s) : +lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) : IsSuccPrelimit a := by intro b hb obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt obtain rfl := (hb.ge_of_gt hbc).antisymm hca contradiction +lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) + (ha : a ∉ s) : IsSuccLimit a := by + refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩ + obtain ⟨b, hb⟩ := hs' + obtain rfl | hb := (hs.1 hb).eq_or_lt + · contradiction + · exact hb.not_isMin + variable [SuccOrder α] theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a := @@ -627,9 +635,13 @@ theorem IsPredPrelimit.lt_iff_exists_lt (h : IsPredPrelimit b) : b < a ↔ ∃ c theorem IsPredLimit.lt_iff_exists_lt (h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a := h.dual.lt_iff_exists_lt -lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hx : a ∉ s) : +lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) : IsPredPrelimit a := by - simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem hx + simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha + +lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) + (ha : a ∉ s) : IsPredLimit a := by + simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha variable [PredOrder α] From 1db78830827834bc1b9791d56eb0fae8787ec9a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 5 Jan 2025 23:18:03 -0600 Subject: [PATCH 3/5] fix --- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index e2bee0bf6130e..f6b74712c151e 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1098,7 +1098,7 @@ lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit (hω : ¬ IsSuccPrelimit ω) (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by subst h - refine (isLUB_csSup' ?_).exists_of_not_isSuccPrelimit hω + refine hω.imp_symm (isLUB_csSup' (s := range f) ?_).isSuccPrelimit_of_not_mem contrapose! hω with hf rw [iSup, csSup_of_not_bddAbove hf, csSup_empty] exact isSuccPrelimit_bot From a6da15221741db056f9db45a518cdc6d1d488247 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 19 Jan 2025 16:52:22 -0600 Subject: [PATCH 4/5] apply suggestions --- .../Order/SuccPred/CompleteLinearOrder.lean | 18 +++++------------- Mathlib/Order/SuccPred/Limit.lean | 16 ++++++++++++++++ Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- 3 files changed, 22 insertions(+), 14 deletions(-) diff --git a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean index a2e951b0b7d14..e09d531cbd364 100644 --- a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean +++ b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean @@ -124,17 +124,13 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit' @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")] alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit' -@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")] -lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := - hx.imp_symm hs.isSuccPrelimit_of_not_mem - @[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")] alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit -@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")] +@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2025-01-05")] lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) : ∃ i, f i = x := - hx.imp_symm hf.isSuccPrelimit_of_not_mem + hf.mem_of_not_isSuccPrelimit hx @[deprecated IsLUB.exists_of_not_isSuccPrelimit (since := "2024-09-05")] alias IsLUB.exists_of_not_isSuccLimit := IsLUB.exists_of_not_isSuccPrelimit @@ -209,17 +205,13 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i)) @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")] alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit -@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")] -lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s := - hx.imp_symm hs.isPredPrelimit_of_not_mem - @[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")] alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit -@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")] -lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : +@[deprecated IsGLB.mem_of_not_isPredLimit (since := "2025-01-05")] +lemma IsGLB.isPredPrelimit_of_not_mem (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : ∃ i, f i = x := - hx.imp_symm hf.isPredPrelimit_of_not_mem + hf.mem_of_not_isPredLimit hx @[deprecated IsGLB.exists_of_not_isPredPrelimit (since := "2024-09-05")] alias IsGLB.exists_of_not_isPredLimit := IsGLB.exists_of_not_isPredPrelimit diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean index 6afdc5770dc8d..08b7d01f42dbf 100644 --- a/Mathlib/Order/SuccPred/Limit.lean +++ b/Mathlib/Order/SuccPred/Limit.lean @@ -331,6 +331,10 @@ lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : obtain rfl := (hb.ge_of_gt hbc).antisymm hca contradiction +lemma _root_.IsLUB.mem_of_not_isSuccPrelimit {s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) : + a ∈ s := + ha.imp_symm hs.isSuccPrelimit_of_not_mem + lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) : IsSuccLimit a := by refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩ @@ -339,6 +343,10 @@ lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s · contradiction · exact hb.not_isMin +lemma _root_.IsLUB.mem_of_not_isSuccLimit {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) + (ha : ¬IsSuccLimit a) : a ∈ s := + ha.imp_symm <| hs.isSuccLimit_of_not_mem hs' + variable [SuccOrder α] theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a := @@ -639,10 +647,18 @@ lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : IsPredPrelimit a := by simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha +lemma _root_.IsGLB.mem_of_not_isPredPrelimit {s : Set α} (hs : IsGLB s a) (ha : ¬IsPredPrelimit a) : + a ∈ s := + ha.imp_symm hs.isPredPrelimit_of_not_mem + lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : a ∉ s) : IsPredLimit a := by simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha +lemma _root_.IsGLB.mem_of_not_isPredLimit {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) + (ha : ¬IsPredLimit a) : a ∈ s := + ha.imp_symm <| hs.isPredLimit_of_not_mem hs' + variable [PredOrder α] theorem IsPredPrelimit.pred_le_iff (hb : IsPredPrelimit b) : pred a ≤ b ↔ a ≤ b := diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index e6242074f1143..ca3df047a7bdc 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1098,7 +1098,7 @@ lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit (hω : ¬ IsSuccPrelimit ω) (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by subst h - refine hω.imp_symm (isLUB_csSup' (s := range f) ?_).isSuccPrelimit_of_not_mem + refine (isLUB_csSup' ?_).exists_of_not_isSuccPrelimit hω contrapose! hω with hf rw [iSup, csSup_of_not_bddAbove hf, csSup_empty] exact isSuccPrelimit_bot From b6f79adc75ed6f385b32ca53186fc7599f7e11d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 19 Jan 2025 17:10:08 -0600 Subject: [PATCH 5/5] fix --- Mathlib/Order/SuccPred/CompleteLinearOrder.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean index bb3dcff44f861..c48128f1fe298 100644 --- a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean +++ b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean @@ -124,9 +124,6 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit' @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")] alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit' -@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")] -alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit - @[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2025-01-05")] lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) : ∃ i, f i = x := @@ -202,13 +199,10 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i)) @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")] alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit -@[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")] -alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit - @[deprecated IsGLB.mem_of_not_isPredLimit (since := "2025-01-05")] -lemma IsGLB.isPredPrelimit_of_not_mem (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : +lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) : ∃ i, f i = x := - hf.mem_of_not_isPredLimit hx + hf.mem_of_not_isPredPrelimit hx @[deprecated IsGLB.exists_of_not_isPredPrelimit (since := "2024-09-05")] alias IsGLB.exists_of_not_isPredLimit := IsGLB.exists_of_not_isPredPrelimit