Commit 2025-12-25 22:00 74bdd8de

chore(MeasureTheory/Measure/Stieltjes): use CompactIccSpace instead of ConditionallyCompleteLinearOrder (#33158) In #32482, the definitions in this file were generalized in a way that allows the space R to be empty. However, this generalization isn't actually usable, because most of the file assumes ConditionallyCompleteLinearOrder R, which implies Nonempty R (because of the junk value of sSup). This PR fixes this by switching to [LinearOrder R] [CompactIccSpace R].