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

[pechersky]

when IsSuccArchimedean

---

[github-actions]

PR summary 9a9e559fd9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ BddAbove.exists_isGreatest_of_nonempty
+ BddBelow.exists_isLeast_of_nonempty

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[urkud]

@YaelDillies Are these the right typeclass assumptions?

[YaelDillies]

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

[pechersky]

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

[YaelDillies]

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?

[YaelDillies]

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

[pechersky]

Yes, I now see the results got split

[pechersky]

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

[YaelDillies]

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.

[pechersky]

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

[pechersky]

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.

[urkud]

LGTM but I'm not sure if it can be generalized to some other *Order class we have, so delegating to @YaelDillies .
bors d=@YaelDillies

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

I am not super happy with the generality of this PR, but since @Command-Master's PRs that would unlock the greater generality are currently stalled, let's press on.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style