Commit 2026-09-13 22:38 7f22e856

View on Github →

feat(Order/SuccPred/Limit): small theorems and generalizations (#42480) Generalizes IsSucc[Pre]limit.isLUB_Iio from LinearOrder to SemilatticeInf, and IsSuccLimit.sSup_Iio from ConditionallyCompleteLinearOrderBot to ConditionallyCompleteLattice.

Estimated changes

Modified Counterexamples/Omega1Space.lean

Modified Mathlib/Order/Cover.lean

added theorem CovBy.isLUB_Iio_of_linearOrder

added theorem WCovBy.of_isLUB_Iio

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.IsSuccLimit.lt_iff_exists_lt

added theorem Order.IsSuccLimit.lt_iff_nonempty_Ioo

deleted theorem Order.IsSuccPrelimit.lt_iff_exists_lt

added theorem Order.IsSuccPrelimit.lt_iff_nonempty_Ioo

added theorem Order.IsSuccPrelimit.nonempty_Ioo_of_lt

added theorem Order.isSuccPrelimit_iff_forall_lt_nonempty_Ioo

Modified Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean

Modified Mathlib/SetTheory/ZFC/VonNeumann.lean

Modified Mathlib/Topology/Order/AtTopBotIxx.lean

Modified Mathlib/Topology/Order/Completion.lean