Set.iUnion_inter_iUnion

Stream: Is there code for X?

[Alex Kontorovich]

I thought I needed these three little lemmata (to complement things like Set.iUnion_inter) but turns out I don't. Should I add them to a PR anyway - could they be useful for others?...

import Mathlib.Data.Set.Lattice

theorem Set.iUnion_inter_iUnion {α ι ι' : Type _} (A : ι → Set α) (B : ι' → Set α) :
    (⋃ (i : ι) (j : ι'), A i ∩ B j) = (⋃ (i : ι), A i) ∩ (⋃ (j : ι'), B j) := by
  rw [Set.iUnion_inter]
  apply Set.iUnion_congr
  intro i
  rw [Set.inter_iUnion]

theorem Set.iUnion_equiv {α ι ι' : Type _} (f : ι → Set α) (g : Equiv ι' ι) :
    (⋃ i, (f ∘ g) i) = ⋃ i, f i := Equiv.iSup_congr g (congrFun rfl)

theorem Set.iUnion_prod_dom {α ι ι' : Type _} (f : ι × ι' → Set α) :
    (⋃ (x : ι × ι'), f x) = (⋃ (i : ι) (j : ι'), f (i, j)) := iSup_prod (f := f)

[Eric Wieser]

That first one can be solved in one line with simp_rw, so probably isn't worth having.

[Eric Wieser]

The last one definitely should exist; every iSup lemma is fair game to copy to iUnion, though the name should be made to match

[Alex Kontorovich]

Ok great, thanks. For the name of the third one, there already exists iUnion_prod, but it assumes the function can also be decomposed as a product:

theorem Set.iUnion_prod{ι : Type u_11} {ι' : Type u_12} {α : Type u_13} {β : Type u_14} (s : ι → Set α) (t : ι' → Set β) :
⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i

Seems like both versions are useful? If so, do you have another suggestion for the name?...