Commit 2023-08-14 19:43 d1cd996f
View on Github →feat: use junk value in the definition of conditionally complete linear order (#6571) Currently, in a conditionally complete linear order, the supremum of an unbounded set hasn't any specific property. However, in all instances in mathlib, all unbounded sets have the same supremum. This PR adds this requirement in mathlib. This will be convenient to remove boundedness assumptions in measurability statements.