# Zulip Chat Archive

## Stream: maths

### Topic: I don't get all these types of union

#### Kevin Buzzard (Feb 28 2020 at 16:24):

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 (Feb 28 2020 at 16:26):

Is this now a bUnion or something? Aah bingo, `apply subset_bUnion_of_mem`

works. I find all this very confusing.

#### Mario Carneiro (Feb 28 2020 at 23:21):

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 (Feb 29 2020 at 08:06):

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

#### Mario Carneiro (Feb 29 2020 at 08:47):

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 (Feb 29 2020 at 09:36):

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 (Feb 29 2020 at 09:38):

that's correct

#### Mario Carneiro (Feb 29 2020 at 09:38):

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

Last updated: May 18 2021 at 06:15 UTC