Theorem Monotone.map_csInf_le_csInf_image

Modification history

2026-08-10 08:17
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
chore(order/ConditionallyCompleteLattice): use `to_dual` more (#41558) …
Deleted Monotone.map_csInf_le_csInf_imageView on Github →
2026-07-01 03:09
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(Order/ConditionallyCompleteLattice): `sSup (f '' s) ≤ f (sSup s)` (#35822)
Added Monotone.map_csInf_le_csInf_imageView on Github →