Zulip Chat Archive

Stream: general

Topic: finset bUnion


view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 25 2019 at 07:37):

should I use finset.sup?

view this post on Zulip Kenny Lau (May 25 2019 at 07:42):

@Chris Hughes what do you think?

view this post on Zulip Chris Hughes (May 25 2019 at 08:18):

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

view this post on Zulip Kenny Lau (May 25 2019 at 08:32):

but that would require subtypes?

view this post on Zulip Chris Hughes (May 25 2019 at 08:37):

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

view this post on Zulip Kenny Lau (May 25 2019 at 09:00):

that's implicitly two Unions, aka bUnion

view this post on Zulip Chris Hughes (May 25 2019 at 09:02):

One way might be to make iota a fintype actually.

view this post on Zulip Chris Hughes (May 25 2019 at 09:02):

That's probably the most sensible.

view this post on Zulip Kenny Lau (May 25 2019 at 12:44):

but then you can't do induction

view this post on Zulip Kenny Lau (May 25 2019 at 12:44):

finset.sup is the easiest to destruct

view this post on Zulip Chris Hughes (May 25 2019 at 12:46):

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

view this post on Zulip 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