Theorem Set.biInter_subset_biUnion

Modification history

2026-08-24 10:14
Mathlib/Data/Set/Lattice.lean
refactor(Data/Set): split long file Lattice.lean (#43030) …
Modified Set.biInter_subset_biUnionView on Github →
2025-01-10 13:20
Mathlib/Data/Set/Lattice.lean
feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) …
Added Set.biInter_subset_biUnionView on Github →