Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 10:10 55c30c69

View on Github →

feat(topology/basic): interior of finite intersection is intersection of interiors (#9508) And likewise for finite unions and closures.

Estimated changes