set.sigma ?

Stream: general

[Peter Nelson]

Is there a reason finset.sigma is defined in mathlib but set.sigma isn't?

https://leanprover-community.github.io/mathlib_docs/data/finset/basic.html#finset.sigma

[Yury G. Kudryashov]

Nobody needed it? def set.sigma {α : Type*} {β : α → Type*} (s : set α) (t : α → set β) := {x : Σ a, β a | x.1 ∈ s ∧ x.2 ∈ t x.1}

[Peter Nelson]

yup - that's what I've been using. With finsum it will likely be useful for lemmas like finsum_in_sigma that reverse the order of summation.

[Peter Nelson]

Was just making sure there isn't a better reason

[Yaël Dillies]

#12305

[Kevin Buzzard]

@Wrenna Robson you're not the only person using finsum -- the matroid people like it too.

[Wrenna Robson]

I don't know what a matroid is but great! Would be good to compare notes.

[Kevin Buzzard]

Come to London Learning Lean on 2022-03-03T16:00:00Z and @Alena Gusakov will tell you!

[Wrenna Robson]

Ah, it's hybrid - interesting.