Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
set.compl_section_ord_separating_set_mem_nhds_within_Iic
Modification history
2022-09-21 06:16
src/topology/algebra/order/t5.lean
feat(topology/algebra/order): a linear order is Tâ (#16540)
Added
set.compl_section_ord_separating_set_mem_nhds_within_Iic
View on Github â