Commit 2026-01-28 14:02 85b15fe3
View on Github →feat: IsLUB versions of [c]sSup_image2_eq_[c]sSup_[c]sSup (#34104)
I find that sometimes it's more convenient to carry around IsLUB than a conditional sup + nonemptyness + boundedness.
This PR generalizes the family of lemmas like csSup_image2_eq_csSup_csSup to this setup.
I will use it to prove IsLUB.add, the IsLUB analog of csSup_add