Commit 2026-05-01 13:07 c9663a5f

View on Github →

feat: interactions between IsSuccLimit and WithTop (#38244)

Estimated changes

Modified Mathlib/Order/BoundedOrder/Basic.lean

added theorem not_top_covBy

Modified Mathlib/Order/Cover.lean

added theorem WithTop.covBy_top_iff

added theorem WithTop.not_covBy_top

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.withTopCoe

added theorem Order.IsSuccLimit.withTopCoe

added theorem Order.IsSuccPrelimit.withTopCoe

added theorem WithTop.isPredPrelimit_iff

added theorem WithTop.isSuccLimit_iff

added theorem WithTop.isSuccLimit_top

added theorem WithTop.isSuccPrelimit_iff

added theorem WithTop.isSuccPrelimit_top