Commit 2023-02-15 00:55 5fa083ff

View on Github →

feat: add lemmas about 𝓝[>] a = ⊥ and 𝓝[<] a = ⊥ (#2289)

Estimated changes

Modified Mathlib/Topology/Order/Basic.lean

added theorem Covby.nhdsWithin_Iio

added theorem Covby.nhdsWithin_Ioi

added theorem countable_setOf_isolated_left

added theorem countable_setOf_isolated_right

added theorem nhdsWithin_Iio_basis'

added theorem nhdsWithin_Iio_eq_bot_iff

added theorem nhdsWithin_Ioi_basis'

added theorem nhdsWithin_Ioi_eq_bot_iff