Theorem ciSup_mem_iInter_Icc_of_antitone_Icc

Modification history

2024-10-22 14:55

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

refactor(Order/ConditionallyCompleteLattice): split large file (#18029)

Modified ciSup_mem_iInter_Icc_of_antitone_Icc View on Github →

2023-10-06 15:59

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

chore: clean up names with iUnion instead of Union (#7550)

Added ciSup_mem_iInter_Icc_of_antitone_Icc View on Github →