mathlib
cb425931 - feat(data/real/basic): add `real.supr_nonneg` etc (#19096)

Commit
2 years ago
feat(data/real/basic): add `real.supr_nonneg` etc (#19096) Motivated by lemmas from the sphere eversion project
Author
Parents
Loading