Commit 2025-01-10 13:20 12958ea9

View on Github →

feat: ⨅ i, f i ≤ ⨆ i, f i (#20573) From my PhD (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.biInter_subset_biUnion

added theorem Set.iInter_subset_iUnion

Modified Mathlib/Order/CompleteLattice.lean

modified theorem biInf_le

added theorem biInf_le_biSup

added theorem iInf_le_iSup

modified theorem le_biSup

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciInf_le_ciSup