Commit 2025-02-17 19:20 bd789b88

View on Github →

chore(SetTheory/Ordinal/Topology): generalize theorems to SuccOrder (#20491) This takes care of some easy targets, though other theorems in this file should generalize as well.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Topology.lean

modified theorem Ordinal.nhdsLE_eq_nhds

modified theorem Ordinal.nhdsLT_eq_nhdsNE

Modified Mathlib/Topology/Order/Basic.lean

added theorem PredOrder.hasBasis_nhds_Ioc

added theorem PredOrder.hasBasis_nhds_Ioc_of_exists_gt

added theorem SuccOrder.hasBasis_nhds_Ioc

added theorem SuccOrder.hasBasis_nhds_Ioc_of_exists_lt

Modified Mathlib/Topology/Order/OrderClosed.lean

added theorem PredOrder.nhdsGE_eq_nhds

added theorem PredOrder.nhdsGT_eq_nhdsNE

added theorem SuccOrder.nhdsLE_eq_nhds

added theorem SuccOrder.nhdsLT_eq_nhdsNE