Commit 2024-04-24 06:52 e1f6f66b
View on Github →feat: add theorem about order preservation of Real.toNNReal (#12369)
Add following theorem: if r and p are real and r.toNNReal < p.toNNReal, then r < p without any assumptions needed.
feat: add theorem about order preservation of Real.toNNReal (#12369)
Add following theorem: if r and p are real and r.toNNReal < p.toNNReal, then r < p without any assumptions needed.