Commit 2025-08-29 11:44 9925c676

View on Github →

feat: IsOrderBornology instances for ℕ and ℤ (#28575) ... using a new constructor assuming IsCompactIcc. As a result, I could make all existing instances on concrete types into one-liners.

Estimated changes

modified theorem bddAbove_Icc
modified theorem bddAbove_Ico
modified theorem bddAbove_Ioc
modified theorem bddAbove_Ioo
modified theorem bddBelow_Icc
modified theorem bddBelow_Ico
modified theorem bddBelow_Ioc
modified theorem bddBelow_Ioo