Sup_eq_supr

Stream: general

[Peter Nelson]

Is there a reason that Sup_eq_supr is not called Sup_eq_bsupras per the naming conventions at the top of https://leanprover-community.github.io/mathlib_docs/order/complete_lattice.html?

[Yaël Dillies]

It's because this naming convention is loosely adhered, in the sense that we add b or ₂ only to disambiguate.