Commit 2026-06-21 22:46 2ddd05d8

View on Github →

feat: monotone function Cardinal → α is eventually constant (#37344)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Small/Basic.lean

Modified Mathlib/Order/Preorder/Chain.lean

added theorem Antitone.isChain_image

added theorem Antitone.isChain_range

added def IsChain.linearOrder

Created Mathlib/SetTheory/Cardinal/EventuallyConst.lean

added theorem Cardinal.eventuallyConst_of_antitone

added theorem Cardinal.eventuallyConst_of_monotone

added theorem Filter.EventuallyConst.of_antitone_of_lt_cof

added theorem Filter.EventuallyConst.of_monotone_of_lt_cof

added theorem Filter.EventuallyConst.of_not_isCofinal_rangeSplitting

added theorem Ordinal.eventuallyConst_of_antitone

added theorem Ordinal.eventuallyConst_of_monotone