Theorem Set.biUnion_prod

Modification history

2025-07-28 02:18
Mathlib/Data/Set/Lattice/Image.lean
feat: `⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ (⋃ x ∈ t, g x)` etc. (#27016) …
Added Set.biUnion_prodView on Github →