Commit 2026-09-23 14:00 95c90ee2

View on Github →

feat(Order/ConditionallyCompleteLattice): antitone versions of sSup (f '' s) lemmas (#41273) f (sInf s) = sSup (f '' s) and f (sSup s) = sInf (f '' s) for an antitone function and a finite nonempty set. Matches the existing monotone lemmas.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem Antitone.csSup_image_le

added theorem Antitone.csSup_image_le_map_csInf

added theorem Antitone.le_csSup_image

modified theorem Monotone.csSup_image_le

modified theorem Monotone.csSup_image_le_map_csSup

modified theorem Monotone.le_csSup_image

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Set.Finite.map_sSup_of_antitone

added theorem Set.Finite.map_sSup_of_antitoneOn

modified theorem Set.Finite.map_sSup_of_monotone

added theorem Set.Finite.map_sSup_of_monotoneOn