Theorem Set.iUnion₂_comm

Modification history

2025-07-28 02:18
Mathlib/Data/Set/Lattice.lean
feat: `⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ (⋃ x ∈ t, g x)` etc. (#27016) …
Modified Set.iUnion₂_commView on Github →
2023-05-14 07:05
Mathlib/Data/Set/Lattice.lean
chore: Rename to `sSup`/`iSup` (#3938) …
Added Set.iUnion₂_commView on Github →