Theorem Set.biUnion_univ_pi

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) …
Added Set.biUnion_univ_piView on Github →