From 52f61fd940955a7e44236edfd1b70ab65a492140 Mon Sep 17 00:00:00 2001 From: sven-manthe Date: Thu, 4 Apr 2024 19:56:21 +0200 Subject: [PATCH 1/3] style: fixed references to DenselyOrdered --- Mathlib/Data/PSigma/Order.lean | 4 ++-- Mathlib/Order/CountableDenseLinearOrder.lean | 4 ++-- Mathlib/Order/Cover.lean | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/PSigma/Order.lean b/Mathlib/Data/PSigma/Order.lean index 9eba8a28ccf24..7c3c927903245 100644 --- a/Mathlib/Data/PSigma/Order.lean +++ b/Mathlib/Data/PSigma/Order.lean @@ -153,7 +153,7 @@ instance denselyOrdered_of_noMaxOrder [Preorder ι] [∀ i, Preorder (α i)] exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩ #align psigma.lex.densely_ordered_of_no_max_order PSigma.Lex.denselyOrdered_of_noMaxOrder -instance densely_ordered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] +instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] [∀ i, DenselyOrdered (α i)] [∀ i, NoMinOrder (α i)] : DenselyOrdered (Σₗ' i, α i) := ⟨by rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩) @@ -161,7 +161,7 @@ instance densely_ordered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)] exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩ · obtain ⟨c, ha, hb⟩ := exists_between h exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩ -#align psigma.lex.densely_ordered_of_no_min_order PSigma.Lex.densely_ordered_of_noMinOrder +#align psigma.lex.densely_ordered_of_no_min_order PSigma.Lex.denselyOrdered_of_noMinOrder instance noMaxOrder_of_nonempty [Preorder ι] [∀ i, Preorder (α i)] [NoMaxOrder ι] [∀ i, Nonempty (α i)] : NoMaxOrder (Σₗ' i, α i) := diff --git a/Mathlib/Order/CountableDenseLinearOrder.lean b/Mathlib/Order/CountableDenseLinearOrder.lean index 519ed8556e285..0084e3c6964c5 100644 --- a/Mathlib/Order/CountableDenseLinearOrder.lean +++ b/Mathlib/Order/CountableDenseLinearOrder.lean @@ -46,7 +46,7 @@ theorem exists_between_finsets {α : Type*} [LinearOrder α] [DenselyOrdered α] ∃ m : α, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y := if nlo : lo.Nonempty then if nhi : hi.Nonempty then - -- both sets are nonempty, use densely_ordered + -- both sets are nonempty, use `DenselyOrdered` Exists.elim (exists_between (lo_lt_hi _ (Finset.max'_mem _ nlo) _ (Finset.min'_mem _ nhi))) fun m hm ↦ ⟨m, fun x hx ↦ lt_of_le_of_lt (Finset.le_max' lo x hx) hm.1, fun y hy ↦ @@ -61,7 +61,7 @@ theorem exists_between_finsets {α : Type*} [LinearOrder α] [DenselyOrdered α] Exists.elim (exists_lt (Finset.min' hi nhi)) fun m hm ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ lt_of_lt_of_le hm (Finset.min'_le hi y hy)⟩ - else-- both sets are empty, use nonempty + else-- both sets are empty, use `Nonempty` nonem.elim fun m ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩ #align order.exists_between_finsets Order.exists_between_finsets diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index a1798a554ed74..832756c4a3f20 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -245,10 +245,10 @@ theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h => h.2 hc.1 hc.2 #align not_covby not_covBy -theorem densely_ordered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b := +theorem denselyOrdered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b := ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h => ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩ -#align densely_ordered_iff_forall_not_covby densely_ordered_iff_forall_not_covBy +#align densely_ordered_iff_forall_not_covby denselyOrdered_iff_forall_not_covBy @[simp] theorem toDual_covBy_toDual_iff : toDual b ⋖ toDual a ↔ a ⋖ b := From 4d861b0a62bd07f6c88aa1816fea1d7bfffbb3ca Mon Sep 17 00:00:00 2001 From: sven-manthe <147848313+sven-manthe@users.noreply.github.com> Date: Thu, 4 Apr 2024 20:28:15 +0200 Subject: [PATCH 2/3] Update Mathlib/Order/CountableDenseLinearOrder.lean Co-authored-by: grunweg --- Mathlib/Order/CountableDenseLinearOrder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/CountableDenseLinearOrder.lean b/Mathlib/Order/CountableDenseLinearOrder.lean index 0084e3c6964c5..6b2beabcf0b55 100644 --- a/Mathlib/Order/CountableDenseLinearOrder.lean +++ b/Mathlib/Order/CountableDenseLinearOrder.lean @@ -61,7 +61,7 @@ theorem exists_between_finsets {α : Type*} [LinearOrder α] [DenselyOrdered α] Exists.elim (exists_lt (Finset.min' hi nhi)) fun m hm ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ lt_of_lt_of_le hm (Finset.min'_le hi y hy)⟩ - else-- both sets are empty, use `Nonempty` + else -- both sets are empty, use `Nonempty` nonem.elim fun m ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩ #align order.exists_between_finsets Order.exists_between_finsets From 9dce2f81ac11fd85d87959ce1204c332c0b65b3c Mon Sep 17 00:00:00 2001 From: sven-manthe Date: Thu, 4 Apr 2024 20:30:24 +0200 Subject: [PATCH 3/3] added deprecated theorem --- Mathlib/Order/Cover.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index 832756c4a3f20..b01895e11e61b 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -248,6 +248,8 @@ theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h => theorem denselyOrdered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b := ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h => ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩ +@[deprecated] alias densely_ordered_iff_forall_not_covBy := + denselyOrdered_iff_forall_not_covBy -- 2024-04-04 #align densely_ordered_iff_forall_not_covby denselyOrdered_iff_forall_not_covBy @[simp]