Commit 2024-11-11 05:16 cfe7adec

feat(Topology/Order): add more CovBy.nhdsWithin... lemmas (#18567)

• Add lemmas about 𝓝[<] a and 𝓝[≤] a in a PredOrder.
• Add lemmas about 𝓝[>] a and 𝓝[≥] a in a SuccOrder.
• Add CovBy.nhdsWithin_Ici and CovBy.nhdsWithin_Iic.
• Prove that an OrderClosedTopology on a linear order which is a PredOrder and a SuccOrder is discrete.
• Cleanup theorems about OrderTopology vs DiscreteTopology.