set.sigma

Stream: Is there code for X?

[Yaël Dillies]

We have docs#finset.sigma, but do we not have set.sigma?

[Eric Rodriguez]

maybe you're meant to write it with the bind operation (like multiset.sigma does in the end)? not sure, really not a monad person at all

[Eric Wieser]

I assume a correct implementation would be:

def set.sigma {α : Type*} {σ : α → Type*} (s : set α) (t : Π a, set (σ a)) :
  set (Σ a, σ a) := {x | x.1 ∈ s ∧ x.2 ∈ t x.1}

[Mario Carneiro]

LGTM

[Eric Wieser]

or ⋃ i ∈ s, sigma.mk i '' t i

[Yaël Dillies]

Will open the PR :rofl:

[Eric Wieser]

Or even ⋃₀ ((λ i, sigma.mk i '' t i) '' s), but that is definitionally way more annoying

[Yaël Dillies]

#12305