`bigcup_bigcup` naming

[affeldt-aist]

analysis/classical/classical_sets.v

Lines 1797 to 1799 in 7da8655

	Lemma bigcup_bigcup {J : Type} (F : I -> J -> set T) (P : set I) (Q : set J) :
	\bigcup_(i in P) \bigcup_(j in Q) F i j =
	\bigcup_(k in P `*` Q) F k.1 k.2.

Wouldn't it better to call this bigcup_bigcup_setM to keep bigcup_bigcup for the nesting of bigcup as in

Lemma bigcup_bigcup (I : Type) T1 T2 (F : I -> set T1) (G : T1 -> set T2) :
  \bigcup_(i in \bigcup_n F n) G i = \bigcup_n \bigcup_(i in F n) G i.

[CohenCyril]

Indeed, and we could rather have

Lemma bigcup_setM {J : Type} (F : I -> J -> set T) (P : set I) (Q : set J) : 
   \bigcup_(k in P `*` Q) F k.1 k.2 = \bigcup_(i in P) \bigcup_(j in Q) F i j.

instead.

[CohenCyril]

More generally, I'm also wondering about the naming convention that would allow to distinguish \bigcup_(x in ~` P) F x from bigcup_(A in P) ~` F A.