I don't get all these types of union

Stream: maths

[Kevin Buzzard]

I noticed recently that I often make a real meal of arguments involving arbitrary unions. I am beginning to wonder whether I'm missing some tips and tricks.

I have a goal

f : Y -> X
I : set (set X),
⊢ f ⁻¹' ⋃₀ I ∈ F.sets

and if I rw preimage_sUnion I get

⊢ (⋃ (t : set X) (H : t ∈ I), f ⁻¹' t) ∈ F.sets

Later on the goal gets reduced to

⊢ f ⁻¹' U ⊆ ⋃ (t : set X) (H : t ∈ I), f ⁻¹' t

and I have a proof that U \in I but now the sUnion appears to be a Union and apply subset_Union fails. Am I already in some kind of trouble when I have ⋃ (t : set X) (H : t ∈ I), ...? I don't know where to learn about how to control all these unions sensibly.

[Kevin Buzzard]

Is this now a bUnion or something? Aah bingo, apply subset_bUnion_of_mem works. I find all this very confusing.

[Mario Carneiro]

There are three kinds of arbitrary union. sUnion is ⋃₀ S, which applies when S is a set of sets and takes the union of all of them. Union is ⋃ i:I, f i which applies when f : I -> set A and is in some sense the most type theoretically natural union of a family. bUnion is written ⋃ t ∈ S, f t and works when f : I -> set A and S : set I, that is, it is a union bounded by a set in the index. However, because of the way the lean parser works on relations in the binders, this is just a double Union, with the second one ranging over proofs that t ∈ S, that is, ⋃ (t : I), ⋃ (H : t ∈ S), f t. So you can usually apply Union theorems to these expressions, and in that sense bUnion is just a shortcut for this special case.

[Kevin Buzzard]

Can we have unions over two or more predicates on a type? Are these also called bUnion? Should they be avoided?

[Mario Carneiro]

Like I said, bUnion is really just a special case of Union. You can iterate the Union construction as many times as you like

[Kevin Buzzard]

The problem I run into is that I find myself taking a union over all proofs that s is in S, for example. That can't be right

[Mario Carneiro]

that's correct

[Mario Carneiro]

Notice that a union over proofs is equal to the body, if the proposition is true, and is empty otherwise