Commit 2025-04-24 06:28 6225383c

View on Github →

feat: generalize NoMaxOrder to NoTopOrder (#24203) Generalizes NoMaxOrder to NoTopOrder and NoMinOrder to NoBotOrder in some lemmas.

Estimated changes

modified theorem IsGLB.nonempty
modified theorem IsLUB.nonempty
modified theorem not_bddAbove_univ
modified theorem not_bddBelow_univ
modified theorem Filter.Iio_mem_atBot
modified theorem Filter.Ioi_mem_atTop
modified theorem Filter.eventually_gt_atTop
modified theorem Filter.eventually_lt_atBot
modified theorem Filter.eventually_ne_atBot
modified theorem Filter.eventually_ne_atTop
modified theorem Filter.disjoint_pure_atBot
modified theorem Filter.disjoint_pure_atTop
modified theorem Filter.atTop_le_cofinite