Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC