Commit 2025-03-20 16:39 3a843e76
View on Github →chore(Algebra/Group): split iUnion
/iInter
from long file Pointwise/Set/Basic.lean
(#23152)
This PR splits up the long file Algebra.Group.Pointwise.Set.Basic
by taking out all results involving the complete lattice structure on Set: these now live in Pointwise.Set.Lattice
. We get a surprising reduction in downstream imports, since apparently we don't care much about order theory in that area of the library!