Order/Bounded

Stream: mathlib4

[Violeta Hernández]

Just came across https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Bounded.html, an old file I made about two years ago about results for Bounded (· < ·) and Unbounded (· < ·).

[Violeta Hernández]

As I understand now, the preferred spelling for this predicate is BddAbove or ¬ BddAbove.

[Violeta Hernández]

Should deprecating this file be something we work towards?

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

I tend to agree, yes. This file is only used on Cardinal and Ordinal, where BddAbove is equivalent and more idiomatic.

[Violeta Hernández]

Yes, that's also my fault. I'm working on redefining docs#Ordinal.enumIso to use the BddAbove hypothesis, which should get rid of those usages.