Commit 2026-07-01 03:09 9dcbf323

View on Github →

feat(Order/ConditionallyCompleteLattice): sSup (f '' s) ≤ f (sSup s) (#35822)

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem Monotone.csSup_image_le_map_csSup

added theorem Monotone.map_csInf_le_csInf_image

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Set.Finite.map_sInf_of_monotone

added theorem Set.Finite.map_sSup_of_monotone