Theorem ciSup_mem_iInter_Icc_of_antitone_Icc
Modification history
2026-02-16 16:43
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat: basic API for `ConditionallyCompletePartialOrder` (#35047) …
Modified ciSup_mem_iInter_Icc_of_antitone_IccView on Github →