Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-04-27 15:18
1e9efeea
View on Github →
feat: the intersection of a collection of sets is empty if one of them is empty (
#38535
)
Estimated changes
Modified
Mathlib/Data/Set/Lattice.lean
added
theorem
Set.iInter_eq_empty_of_eq_empty