Theorem Filter.EventuallyConst.of_monotone_of_lt_cof

Modification history

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