iUnion is compatible with product of types

Stream: Is there code for X?

[Michael Rothgang]

lemma iUnion_product {X Y Z : Type*} (f : X × Y → Set Z) :
  ⋃ (x : X) (y : Y), (f ⟨x, y⟩) = ⋃ t : X × Y, (f t) := by sorry

I have a proof locally, but also the nagging feeling this should exist somewhere...

None of exact?, apply?, rw? and aesop find this; this isn't listed on docs#Data.Set.Lattice either (where #find_home says it belongs).

[Anatole Dedecker]

docs#iSup_prod but I don’t think we have the set spelling

[Michael Rothgang]

Thanks - so I'll send a PR then.

[Michael Rothgang]

#7528