Bounded vs BddAbove

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#Set.Bounded, docs#BddAbove, and docs#BddBelow. Should we reuse the former for the other two?

[Yaël Dillies]

No. Violeta Hernández added (a lot of API for) the former because she didn't know about the latter two, but in general we prefer predicates specialised to <=, >= for usability.

[Yury G. Kudryashov]

Should we drop the former then?

[Yury G. Kudryashov]

Or at least mention BddAbove/BddBelow in the docstring?

[Yaël Dillies]

What are the current uses of Set.Bounded? In principle, I'm happy to drop it.

[Yury G. Kudryashov]

It is used in Order/Bounded (a lot), in Order/RelClasses (def + 2 lemmas), Order/WellFounded (2 lemmas), Cardinal/Cofinality (2 theorems), and Ordinal/Arithmetic (once).

[Yury G. Kudryashov]

Do you know that Lean 4 extension can show all uses of a definition/lemma?

[Yury G. Kudryashov]

(not hidden ones like in by simp)

[Alex J. Best]

You can right click and click on "Find all references"

[Yaël Dillies]

Ah no I didn't!

[Violeta Hernández]

Hi, just found this again, and yes, docs#Set.Bounded and docs#Set.Unbounded should be deprecated

[Violeta Hernández]

The file Order/Bounded was made by me to be "basic API for bounded sets" while being unaware of all the API that had already been written for BddAbove / BddBelow

[Violeta Hernández]

Order/WellFounded uses it only to define WellFounded.sup, which in my opinion should also be deprecated, since we already have docs#WellFoundedLT.conditionallyCompleteLinearOrderBot

[Violeta Hernández]

Its use in Ordinal/Arithmetic as docs#Ordinal.bounded_singleton is really the same thing as saying Ordinal is a NoMaxOrder

[Violeta Hernández]

And the theorems in Cardinal/Cofinality should be rewritten in terms of a linear order, rather than an arbitrary well-order relation.

[Violeta Hernández]

It's worth pointing out that the use of Set.Unbounded in the cofinality file isn't even correct for partial orders. The correct spelling for a cofinal partial set is ∀ a, ∃ b ∈ S, r a b for r = (· ≤ ·), rather than ∀ a, ∃ b ∈ S, ¬ r b a for r = (· < ·).

[Violeta Hernández]

It'd be nice to introduce a Set.Cofinal predicate to supercede it.

[Violeta Hernández]

(Really it'd be nice to work with PartialOrder instead of talking about unbundled relations, but since Ordinal is defined as a quotient of IsWellOrder that would introduce other complications)

[Violeta Hernández]

Actually, I could register a LinearOrder instance on o.α for o : WellOrder. Then Order.cof can instead take a Preorder instance argument instead of an arbitrary relation.

[Violeta Hernández]

And likewise, we can define a Set.Cofinal predicate taking in a LE instance argument

[Violeta Hernández]

Violeta Hernández said:

Actually, I could register a LinearOrder instance on o.α for o : WellOrder. Then Order.cof can instead take a Preorder instance argument instead of an arbitrary relation.

#18174 is the first step towards this