Commit 2024-10-22 22:22 c823b5f7

View on Github →

feat: biSup, biInf, biUnion and biInter in NoMaxOrder (#17762)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.biInter_ge_eq_iInf

added theorem Set.biInter_gt_eq_iInf

added theorem Set.biInter_le_eq_iInter

added theorem Set.biInter_lt_eq_iInter

added theorem Set.biUnion_ge_eq_iUnion

added theorem Set.biUnion_gt_eq_iUnion

added theorem Set.biUnion_le_eq_iUnion

added theorem Set.biUnion_lt_eq_iUnion

Modified Mathlib/Order/CompleteLattice.lean

added theorem biInf_ge_eq_iInf

added theorem biInf_gt_eq_iInf

added theorem biInf_le_eq_iInf

added theorem biInf_lt_eq_iInf

added theorem biSup_ge_eq_iSup

added theorem biSup_gt_eq_iSup

added theorem biSup_le_eq_iSup

added theorem biSup_lt_eq_iSup