Commit 2025-01-31 14:18 2c451907

View on Github →

feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) From discussion in #21172

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.insert_iInter

added theorem Set.insert_iUnion