Theorem OrderIso.map_csInf_of_directedOn

Modification history

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 →