Stream: general

Topic: union over a finset

Kenny Lau (Feb 28 2019 at 00:15):

for s : finset ι and f : ι → set α, what is the union of f over s? is it s.sup f or ⋃ i ∈ s, f i or ⋃ i ∈ (↑s : set ι), f i?

@Mario Carneiro

Chris Hughes (Feb 28 2019 at 00:39):

I like the second one. Aren't the last two defeq?

Kenny Lau (Feb 28 2019 at 00:42):

yes, but that special place (H : i \in s) is hard to reach by both rw and simp so one should be very careful there

Last updated: May 10 2021 at 00:31 UTC