Commit 2023-02-06 15:54 4583a042

View on Github →

feat: port Topology.Algebra.Order.T5 (#2102)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Order/T5.lean

added theorem Set.compl_section_ordSeparatingSet_mem_nhds

added theorem Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Ici

added theorem Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Iic

added theorem Set.ordConnectedComponent_mem_nhds

added theorem Set.ordT5Nhd_mem_nhdsSet