Union BigOperator

Stream: Is there code for X?

[Ralf Stephan]

I would like to state something like

example (S : Finset (Finset ℕ)) (T : Finset ℕ) : ∪ s ∈ S = T := by sorry

Does it exist under another name?

[Ralf Stephan]

Or maybe indexed if the outer set is a list?

[Ira Fesefeldt]

Finset.biUnion where t is id, maybe?

[Ira Fesefeldt]

Forget that and use Finset.sup

[Ralf Stephan]

Thanks.

[Malvin Gattinger]

I ran into this just now and want to leave this here for anyone searching for Finset.join or Finset.sUnion.

import Mathlib.Data.Finset.Lattice

set_option diagnostics true

def Finset.join_via_sup (s : Finset (Finset α)) : Finset α := s.sup id -- failed to synthesize `SemilatticeSup (Finset α)`

def Finset.join_via_biUnion (s : Finset (Finset α)) : Finset α := s.biUnion id -- failed to synthesisze `DecidableEq α`

-- But note that adding `[DecidableEq α]` fixes both of them!

def Finset.join3 [DecidableEq α] (s : Finset (Finset α)) : Finset α := s.biUnion id

def Finset.join4 [DecidableEq α] (s : Finset (Finset α)) : Finset α := s.sup id

And I am still wondering: Why is using sup id preferred/recommended instead of biUnion id ? Is there a more minimal way to get SemilatticeSup (Finset α) instead of via DecidableEq α?

[Yaël Dillies]

No, it really is necessary. Assume SemilatticeSup (Finset alpha). Then you can compute ({a} union {b}).card. If it is 1, then a = b. If it is 2, then a != b. Congratulations, you have proved DecidableEq alpha.

[Eric Wieser]

If you don't have decidable equality but know the sets are disjoint, you can use docs#Finset.disjUnion and docs#Finset.disjiUnion