Theorem GaloisConnection.u_ciInf_set_of_directedOn

Modification history

2026-02-16 16:43
Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean
feat: basic API for `ConditionallyCompletePartialOrder` (#35047) …
Added GaloisConnection.u_ciInf_set_of_directedOnView on Github →