Commit 2026-04-16 18:27 064f569d

View on Github →

chore: generalize cardinal supremum theorems to conditionally complete lattices (#38024)

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

added theorem csSup_mem_of_not_isSuccLimit

modified theorem csSup_mem_of_not_isSuccPrelimit'

added theorem exists_eq_ciSup_of_not_isSuccLimit

modified theorem exists_eq_ciSup_of_not_isSuccPrelimit'

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean