octalgo.third_party.bigop_aux

Section BigCupSeq.

Variables (T : finType) (I : eqType).
Implicit Types (P : pred I) (F : I → {set T}).

Lemma bigcup_seqP x P F l :
  reflect (exists2 i : I, i \in l & (x \in F i) && P i) (x \in \bigcup_(t <- l | P t) F t).

Lemma bigcups_seqP (U : pred T) (P : pred I) (F : I → {set T}) (r : seq I) :
  reflect (∀ i : I, i \in r → P i → F i \subset U)
          (\bigcup_(i <- r | P i) F i \subset U).

End BigCupSeq.

Open Scope fset_scope.

Notation "\bigcup_ ( i <- r | P ) F" :=
  (\big[@fsetU _/fset0]_(i <- r | P%fset) F%fset) : fset_scope.

Notation "\bigcup_ ( i <- r ) F" :=
  (\big[@fsetU _/fset0]_(i <- r) F%fset) : fset_scope.

Notation "\bigcup_ ( i | P ) F" :=
  (\big[@fsetU _/fset0]_(i | P) F%fset) : fset_scope.

Notation "\bigcup_ ( i 'in' A | P ) F" :=
  (\big[@fsetU _/fset0]_(i in A | P) F%fset) : fset_scope.

Notation "\bigcup_ ( i 'in' A ) F" :=
  (\big[@fsetU _/fset0]_(i in A) F%fset) : fset_scope.

Section FSetMonoids.

Import Monoid.
Variable (T : choiceType).


End FSetMonoids.

Section BigFOpsFin.

Variables (T : choiceType) (I : finType).
Implicit Types (P : pred I) (A B : {fset I}) (F : I → {fset T}).

End BigFOpsFin.

Section BigFOpsSeq.

Variables (T : choiceType) (I : eqType).
Implicit Types (l : seq I) (P : pred I) (U : {fset T}) (F : I → {fset T}).

Lemma bigfcup_seqP x F l :
  reflect (exists2 i : I, i \in l & x \in F i) (x \in \bigcup_(t <- l) F t).

Lemma bigfcups_seqP F U l :
  reflect (∀ i : I, i \in l → F i `<=` U) (\bigcup_(i <- l) F i `<=` U).

End BigFOpsSeq.

Close Scope fset_scope.