Theorem Filter.EventuallyConst.of_not_isCofinal_rangeSplitting

Modification history

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