Commit 2024-02-22 12:56 d824f0fb

View on Github →

feat(Topology/Order): generalize disjoint_nhds_atTop (#10580) Generalize to a Preorder, add an Iff version.

Estimated changes

modified theorem Filter.OrderTop.atTop_eq
added theorem IsBot.atBot_eq
added theorem IsTop.atTop_eq
deleted theorem disjoint_nhds_atBot
deleted theorem disjoint_nhds_atTop
deleted theorem inf_nhds_atBot
deleted theorem inf_nhds_atTop
added theorem disjoint_nhds_atBot
added theorem disjoint_nhds_atTop
modified theorem ge_of_tendsto'
modified theorem ge_of_tendsto
modified theorem ge_of_tendsto_of_frequently
added theorem inf_nhds_atBot
added theorem inf_nhds_atTop
modified theorem isClosed_Iic
modified theorem le_of_tendsto'
modified theorem le_of_tendsto
modified theorem le_of_tendsto_of_frequently