(slight) terminological inconsistency in mem_Union, … ?

Stream: new members

[Antoine Chambert-Loir]

I was adapting for bUniona lemma already done for Union.
At one point, I noticed that set.mem_Union, set.mem_sUnion are propositions of the form iff.
On the other hand, the corresponding lemma for bUnionis (rightly) called set.mem_bUnion_iff, while set.mem_bUnion proves that something belongs to a bUnion.

Is there an inconsistency here ? Or what do I miss ?

[Yaël Dillies]

Unfortunately the naming convention is not quite uniform. If you want more shivers down your spine, compare set lemmas with their finset counterparts.

[Kyle Miller]

I wouldn't mind iff-ification of these, or some way to make the naming consistent -- this particular difference has tripped me up before.