Commit 2025-02-15 11:39 64142846

View on Github →

feat: add Set.bi{Union,Inter}_{le,ge} (#21884) From sphere-eversion

Estimated changes

added theorem Set.biInter_ge
added theorem Set.biInter_le
added theorem Set.biUnion_ge
added theorem Set.biUnion_le
added theorem biInf_ge_eq_inf
added theorem biInf_le_eq_inf
added theorem biSup_ge_eq_sup
added theorem biSup_le_eq_sup