Theorem Ordinal.eventuallyConst_of_antitone

Modification history

2026-06-21 22:46
Mathlib/SetTheory/Cardinal/EventuallyConst.lean
feat: monotone function `Cardinal → α` is eventually constant (#37344)
Added Ordinal.eventuallyConst_of_antitoneView on Github →