Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ordinal.is_closed_iff_bsup

Modification history

2022-05-26 15:16
src/set_theory/ordinal/topology.lean
chore(set_theory/ordinal/topology): add `variables` block (#14369) …
Modified ordinal.is_closed_iff_bsupView on Github →
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_closed_iff_bsupView on Github →