Theorem Set.iInter_eq_empty_of_eq_empty

Modification history

2026-08-24 10:14
Mathlib/Data/Set/Lattice.lean
refactor(Data/Set): split long file Lattice.lean (#43030) …
Modified Set.iInter_eq_empty_of_eq_emptyView on Github →
2026-04-27 15:18
Mathlib/Data/Set/Lattice.lean
feat: the intersection of a collection of sets is empty if one of them is empty (#38535)
Added Set.iInter_eq_empty_of_eq_emptyView on Github →