Theorem Monotone.csSup_image_le_map_csSup

Modification history

2026-07-01 03:09
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(Order/ConditionallyCompleteLattice): `sSup (f '' s) ≤ f (sSup s)` (#35822)
Added Monotone.csSup_image_le_map_csSupView on Github →