Theorem OrderIso.map_csInf_of_directedOn'

Modification history

2026-07-17 22:50
Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
chore(Order/ConditionallyCompletePartialOrder/Indexed): use `to_dual` more to kill `TODO` (#41589) …
Deleted OrderIso.map_csInf_of_directedOn'View on Github →
2026-02-16 16:43
Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
feat: basic API for `ConditionallyCompletePartialOrder` (#35047) …
Added OrderIso.map_csInf_of_directedOn'View on Github →