Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.is_normal_iff_strict_mono_and_continuous

Modification history

2022-03-14 13:59
src/set_theory/ordinal_topology.lean
feat(set_theory/ordinal_topology): Basic results on the order topology of ordinals (#11861) …
Added ordinal.is_normal_iff_strict_mono_and_continuousView on Github →