Theorem Ordinal.IsAcc.mono

Modification history

2024-10-25 20:32
Mathlib/SetTheory/Ordinal/Topology.lean
feat(SetTheory/Ordinal/Topology): define Ordinal.IsClosed and Ordinal.IsAcc (#16710) …
Added Ordinal.IsAcc.monoView on Github →