Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-12-08 16:34
b5ab2f77
View on Github →
feat(topology/algebra/ordered): add lemmas about
map coe at_top/at_bot
(
#5238
)
Estimated changes
Modified
src/topology/algebra/ordered.lean
deleted
theorem
Ioo_at_bot_eq_nhds_within
deleted
theorem
Ioo_at_top_eq_nhds_within
added
theorem
comap_coe_Iio_nhds_within_Iio
added
theorem
comap_coe_Ioi_nhds_within_Ioi
added
theorem
comap_coe_Ioo_nhds_within_Iio
added
theorem
comap_coe_Ioo_nhds_within_Ioi
added
theorem
comap_coe_nhds_within_Iio_of_Ioo_subset
added
theorem
comap_coe_nhds_within_Ioi_of_Ioo_subset
added
theorem
map_coe_Iio_at_top
added
theorem
map_coe_Ioi_at_bot
added
theorem
map_coe_Ioo_at_bot
added
theorem
map_coe_Ioo_at_top
added
theorem
map_coe_at_bot_of_Ioo_subset
added
theorem
map_coe_at_top_of_Ioo_subset