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] - feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty #15944

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty #15944

Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
eb3c183
feat(Order/SuccPred): `BddAbove.exists_isGreatest_of_nonempty`
pechersky Aug 18, 2024
5dd72ee
Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ…
pechersky Aug 27, 2024
7642ea1
linear order now necessary
pechersky Aug 27, 2024
4310bdc
Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ…
pechersky Sep 8, 2024
bed7cd9
Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ…
pechersky Sep 17, 2024
9a9e559
Update Mathlib/Order/SuccPred/Archimedean.lean
pechersky Oct 8, 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
32 changes: 32 additions & 0 deletions Mathlib/Order/SuccPred/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1401,3 +1401,35 @@ lemma SuccOrder.forall_ne_bot_iff
rw [← Nat.succ_pred_eq_of_pos hj]
simp only [Function.iterate_succ', Function.comp_apply]
apply h

section IsLeast

lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [LinearOrder X] [SuccOrder X]
[IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
∃ x, IsGreatest S x := by
Copy link
Member

Choose a reason for hiding this comment

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

@YaelDillies Are these the right typeclass assumptions?

Copy link
Collaborator

Choose a reason for hiding this comment

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

I guess the right assumption is something like "locally cowell-founded", meaning "Iic x is cowell-founded for all x". We don't have that in mathlib, so the current generality seems okay.

Note however that LinearOrder shouldn't be necessary since the recent refactor on SuccOrder

Suggested change
∃ x, IsGreatest S x := by
lemma BddAbove.exists_isGreatest_of_nonempty {X : Type*} [Preorder X] [SuccOrder X]
[IsSuccArchimedean X] {S : Set X} (hS : BddAbove S) (hS' : S.Nonempty) :
∃ x, IsGreatest S x := by

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I can't generalize to Preorder because I use Order.le_succ_iff_eq_or_le in the inductive step proof of Succ.rec.

Copy link
Collaborator

Choose a reason for hiding this comment

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

The end result is still true, though (although I've noticed you also need to assume that the set is directed). Can you try using another lemma?

Copy link
Collaborator

Choose a reason for hiding this comment

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

@Command-Master, didn't you prove that the assumptions above imply SemilatticeSup X?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, I now see the results got split

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've left a TODO to come back to this after that PR.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Sorry, I won't merge this for now because I suspect you don't even need the lemmas in the current PR. Please first coordinate with @Command-Master to get #16272 (or rather the preliminary part) merged.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Can you take a look at https://github.com/leanprover-community/mathlib4/pull/16619/files#diff-e9c6f03b09ef6fa37d4bb4f98167c69a8165fcbbd8f189451b15fafbf798f65cR113 please? It's the point of use.

Copy link
Collaborator Author

@pechersky pechersky Sep 17, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

I tried to bring in the relevant lemmas from that PR, but I still don't have a proof. I also can't assume that my set is OrdConnected. I need help with this if the blocker is generalization.

obtain ⟨m, hm⟩ := hS
obtain ⟨n, hn⟩ := hS'
by_cases hm' : m ∈ S
· exact ⟨_, hm', hm⟩
have hn' := hm hn
revert hn hm hm'
refine Succ.rec ?_ ?_ hn'
· simp (config := {contextual := true})
intro m _ IH hm hn hm'
rw [mem_upperBounds] at IH hm
simp_rw [Order.le_succ_iff_eq_or_le] at hm
replace hm : ∀ x ∈ S, x ≤ m := by
intro x hx
refine (hm x hx).resolve_left ?_
rintro rfl
exact hm' hx
by_cases hmS : m ∈ S
· exact ⟨m, hmS, hm⟩
· exact IH hm hn hmS

lemma BddBelow.exists_isLeast_of_nonempty {X : Type*} [LinearOrder X] [PredOrder X]
[IsPredArchimedean X] {S : Set X} (hS : BddBelow S) (hS' : S.Nonempty) :
∃ x, IsLeast S x :=
BddAbove.exists_isGreatest_of_nonempty (X := Xᵒᵈ) hS hS'

end IsLeast
Loading