Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 13:59 c1edbec8

View on Github →

feat(set_theory/ordinal_topology): Basic results on the order topology of ordinals (#11861) We link together various notions about ordinals to their topological counterparts.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

modified theorem ordinal.is_normal.sup

Created src/set_theory/ordinal_topology.lean

added theorem ordinal.enum_ord_is_normal_iff_is_closed

added theorem ordinal.is_closed_iff_bsup

added theorem ordinal.is_closed_iff_sup

added theorem ordinal.is_limit_of_mem_frontier

added theorem ordinal.is_normal_iff_strict_mono_and_continuous

added theorem ordinal.is_open_iff

added theorem ordinal.is_open_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