Commit 2023-01-05 13:18 ed005a8c

View on Github →

feat(topology/order/basic): replace partial_order by preorder (#18064) It turns out nearly all partial_order hypotheses can be generalized to preorder in this file.

Estimated changes

Modified src/topology/order/basic.lean

modified theorem is_open_gt'

modified theorem is_open_lt'

modified theorem nhds_bot_order

modified theorem nhds_top_order

modified theorem nhds_within_Ici_eq''

modified theorem nhds_within_Ici_eq'

modified theorem nhds_within_Iic_eq''

modified theorem nhds_within_Iic_eq'

modified theorem tendsto_nhds_bot_mono'

modified theorem tendsto_nhds_bot_mono

modified theorem tendsto_nhds_top_mono'

modified theorem tendsto_nhds_top_mono