Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-21 06:16 236a0af4

View on Github →

feat(topology/algebra/order): a linear order is T₅ (#16540)

Estimated changes

Created src/data/set/intervals/ord_connected_component.lean

added theorem set.disjoint_left_ord_separating_set

added theorem set.disjoint_ord_t5_nhd

added theorem set.disjoint_right_ord_separating_set

added theorem set.dual_ord_connected_component

added theorem set.dual_ord_connected_section

added theorem set.dual_ord_separating_set

added theorem set.eq_of_mem_ord_connected_section_of_interval_subset

added theorem set.mem_ord_connected_component

added theorem set.mem_ord_connected_component_comm

added theorem set.mem_ord_connected_component_ord_connected_proj

added theorem set.mem_ord_connected_component_trans

added theorem set.nonempty_ord_connected_component

added def set.ord_connected_component

added theorem set.ord_connected_component_empty

added theorem set.ord_connected_component_eq

added theorem set.ord_connected_component_eq_empty

added theorem set.ord_connected_component_inter

added theorem set.ord_connected_component_ord_connected_proj

added theorem set.ord_connected_component_subset

added theorem set.ord_connected_component_univ

added theorem set.ord_connected_proj_eq

added theorem set.ord_connected_proj_mem_ord_connected_component

added def set.ord_connected_section

added theorem set.ord_connected_section_subset

added def set.ord_separating_set

added theorem set.ord_separating_set_comm

added def set.ord_t5_nhd

added theorem set.self_mem_ord_connected_component

added theorem set.subset_ord_connected_component

Modified src/topology/algebra/order/basic.lean

Created src/topology/algebra/order/t5.lean

added theorem set.compl_section_ord_separating_set_mem_nhds

added theorem set.compl_section_ord_separating_set_mem_nhds_within_Ici

added theorem set.compl_section_ord_separating_set_mem_nhds_within_Iic

added theorem set.ord_connected_component_mem_nhds

added theorem set.ord_t5_nhd_mem_nhds_set