Commit 2023-05-31 09:29 0eaf85df

View on Github →

feat: add Real.iSup_nonneg etc (#4475) Forward-port of leanprover-community/mathlib#19096

Estimated changes

modified theorem Real.sSup_nonpos