finset bUnion

Stream: general

[Kenny Lau]

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

[Kenny Lau]

should I use finset.sup?

[Kenny Lau]

@Chris Hughes what do you think?

[Chris Hughes]

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

[Kenny Lau]

but that would require subtypes?

[Chris Hughes]

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

[Kenny Lau]

that's implicitly two Unions, aka bUnion

[Chris Hughes]

One way might be to make iota a fintype actually.

[Chris Hughes]

That's probably the most sensible.

[Kenny Lau]

but then you can't do induction

[Kenny Lau]

finset.sup is the easiest to destruct

[Chris Hughes]

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

[Patrick Massot]

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?