Commit 2025-01-14 14:39 456d19bb

View on Github →

feat(Order/PartialSups): allow general orders as domain (#20137) Currently PartialSups is only defined for Nat-indexed sequences. This generalises it to arbitrary preorders satisfying suitable typeclass assumptions.

Estimated changes

added theorem partialSups_add_one
modified theorem Monotone.partialSups_eq
modified theorem bddAbove_range_partialSups
added theorem ciSup_partialSups_eq'
modified theorem ciSup_partialSups_eq
modified theorem disjoint_partialSups_left
modified theorem disjoint_partialSups_right
modified theorem iSup_partialSups_eq
modified theorem le_partialSups
modified theorem le_partialSups_of_le
modified def partialSups.gi
modified def partialSups
modified theorem partialSups_apply
added theorem partialSups_bot
modified theorem partialSups_eq_biSup
modified theorem partialSups_eq_ciSup_Iic
modified theorem partialSups_eq_sup_range
modified theorem partialSups_iff_forall
modified theorem partialSups_le
modified theorem partialSups_le_iff
modified theorem partialSups_mono
modified theorem partialSups_monotone
modified theorem partialSups_succ