Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.compl_section_ord_separating_set_mem_nhds_within_Ici

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_IciView on Github →