Commit 2023-02-18 18:40 d8399fe7

View on Github →

feat: port SetTheory.Ordinal.Topology (#2342)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Ordinal/Topology.lean

added theorem Ordinal.enumOrd_isNormal_iff_isClosed

added theorem Ordinal.isClosed_iff_bsup

added theorem Ordinal.isClosed_iff_sup

added theorem Ordinal.isLimit_of_mem_frontier

added theorem Ordinal.isNormal_iff_strictMono_and_continuous

added theorem Ordinal.isOpen_iff

added theorem Ordinal.isOpen_singleton_iff

added theorem Ordinal.mem_closed_iff_bsup

added theorem Ordinal.mem_closed_iff_sup

added theorem Ordinal.mem_closure_iff_bsup

added theorem Ordinal.mem_closure_iff_sup

added theorem Ordinal.mem_closure_tfae

added theorem Ordinal.nhdsBasis_Ioc

added theorem Ordinal.nhds_eq_pure

added theorem Ordinal.nhds_left'_eq_nhds_ne

added theorem Ordinal.nhds_left_eq_nhds

added theorem Ordinal.nhds_right'