Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - style: fix references to DenselyOrdered #11897

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - style: fix references to DenselyOrdered #11897

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
52f61fd
style: fixed references to DenselyOrdered
sven-manthe Apr 4, 2024
4d861b0
Update Mathlib/Order/CountableDenseLinearOrder.lean
sven-manthe Apr 4, 2024
9dce2f8
added deprecated theorem
sven-manthe Apr 4, 2024
d1b7cc1
Merge remote-tracking branch 'refs/remotes/origin/sven-naming-densely…
sven-manthe Apr 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Data/PSigma/Order.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,15 +153,15 @@ 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)]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe the naming convention is that manual instance names should start with "inst", i.e.

Suggested change
instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)]
instance instDenselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)]

(I'm not 100% sure on the casing; you may want to compare with other names/wait for another pair of eyes.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If I do this, there will be many more examples of such instances in this file alone

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure; mathlib is not always consistent (and I think a fix for that would be welcome - to be sure, I'd ask on zulip first).

I'm not asking you to change any other instances! But when you're renaming this one, I'd rather rename it to a "right" than a "less wrong" name.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Personally, I would find the resulting inconsistency with e.g. denselyOrdered_of_noMaxOrder even more confusing

[∀ i, DenselyOrdered (α i)] [∀ i, NoMinOrder (α i)] : DenselyOrdered (Σₗ' i, α i) :=
⟨by
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
· obtain ⟨c, hb⟩ := exists_lt b
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) :=
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Order/CountableDenseLinearOrder.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ↦
Expand All @@ -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
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Order/Cover.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,10 +245,12 @@ 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 :=
sven-manthe marked this conversation as resolved.
Show resolved Hide resolved
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
@[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]
theorem toDual_covBy_toDual_iff : toDual b ⋖ toDual a ↔ a ⋖ b :=
Expand Down
Loading