Finset iUnion

Stream: Is there code for X?

[Gareth Ma]

Hi, is there a notion for Finset / Multiset indexed union, at least over a finite set? I want to express that a Finset is the union of a few smaller disjoint Finsets ("classes"), and I want to keep it as Finset so that I can perform cardinality calculations later.

[Floris van Doorn]

docs#Finset.biUnion

[Gareth Ma]

Thanks! Also, is there a way to state {a : Fin k | P a} as a Finset ? Currently I write it as (univ : Finset (Fin k)).filter P but that's very long...

[Gareth Ma]

(deleted)

[Gareth Ma]

For example,

#check ({a : Fin 10 | a > 0} : Finset (Fin 10))
/-
▶ 26:8-26:48: error:
type mismatch
  {a | a > 0}
has type
  Set (Fin 10) : Type
but is expected to have type
  Finset (Fin 10) : Type
-/

[Floris van Doorn]

I'm afraid not, and you have to write univ.filter P (potentially with more typing information).

[Gareth Ma]

I see, that's very annoying for doing anything combinatorial :/ Thanks

[Yaël Dillies]

Also see docs#Finset.sigma

[Yaël Dillies]

Your suggested syntax is one of the things @Kyle Miller is working on.

[Kyle Miller]

@Gareth Ma You should be able to do Set.toFinset {a : Fin k | P a} (maybe even {a : Fin k | P a}.toFinset). The docs#Set.toFinset API is meant to be able to help you construct finsets using set notations, to the extent that typeclass inference can apply.

[Gareth Ma]

Thanks a lot!! I will try it out in a second.

[Gareth Ma]

I guess everyone in this thread learns something :D