union over a finset

Stream: general

[Kenny Lau]

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?

[Kenny Lau]

@Mario Carneiro

[Chris Hughes]

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

[Kenny Lau]

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