Theorem Ordinal.accPt_subtype

Modification history

2026-10-10 09:42

Mathlib/SetTheory/Ordinal/Topology.lean

chore: delete deprecated declarations to March 2026 (#44240)

Deleted Ordinal.accPt_subtype View on Github →

2024-10-25 20:32

Mathlib/SetTheory/Ordinal/Topology.lean

feat(SetTheory/Ordinal/Topology): define Ordinal.IsClosed and Ordinal.IsAcc (#16710) …

Added Ordinal.accPt_subtype View on Github →