## Stream: general

### Topic: finset bUnion

#### Kenny Lau (May 25 2019 at 07:36):

Given s : finset ι and f : ι → ideal R, what is the idiomatic way to write ⋃ i ∈ (↑s : set ι), f i?

#### Kenny Lau (May 25 2019 at 07:37):

should I use finset.sup?

#### Kenny Lau (May 25 2019 at 07:42):

@Chris Hughes what do you think?

#### Chris Hughes (May 25 2019 at 08:18):

I think Union is more readable. And then you have lemmas like mem_Union.

#### Kenny Lau (May 25 2019 at 08:32):

but that would require subtypes?

#### Chris Hughes (May 25 2019 at 08:37):

I don't see any subtypes. I mean the thing you wrote down. Is that Union?

#### Kenny Lau (May 25 2019 at 09:00):

that's implicitly two Unions, aka bUnion

#### Chris Hughes (May 25 2019 at 09:02):

One way might be to make iota a fintype actually.

#### Chris Hughes (May 25 2019 at 09:02):

That's probably the most sensible.

#### Kenny Lau (May 25 2019 at 12:44):

but then you can't do induction

#### Kenny Lau (May 25 2019 at 12:44):

finset.sup is the easiest to destruct

#### Chris Hughes (May 25 2019 at 12:46):

They're all very easily equivalent, so it probably depends on the use case.

#### Patrick Massot (May 26 2019 at 11:33):

Given s : finset ι and f : ι → ideal R, what is the idiomatic way to write ⋃ i ∈ (↑s : set ι), f i?

Welcome back Kenny! Are you done with exams? What are your current Lean projects?

Last updated: May 15 2021 at 22:14 UTC