Indexed Union and Intersection

Families of relations and sets

Warning

Please pay attention to the type of the FF parameter in each definition.

The math notation (as is typical) hides the typing and leaves it for the reader to determine on their own. As such, it can be challenging to know whether you are indexing a family of sets or relations. Hopefully, this page will help clear that up.

Indexed Union

Family of Relations

Cupβ€…β€ŠIβ€…β€ŠAβ€…β€ŠBβ€…β€ŠF:={β€…β€Šx∈A,y∈B:βˆƒ(i∈I::(x,y)∈F[i])β€…β€Š}\textbf{Cup} \; I \; A \; B \; F := \{\; x \in A, y \in B : \exists(i \in I :: (x,y) \in F[i]) \;\}

I,A,B∈SetI, A, B \in \textbf{Set}

F∈(Aβ†’B)IF \in (A \to B)^I


Notation.

  1. Cupβ€…β€ŠIβ€…β€ŠAβ€…β€ŠBβ€…β€ŠF\textbf{Cup} \; I \; A \; B \; F can be written as Cupβ€…β€ŠIβ€…β€ŠF\textbf{Cup} \; I \; F when AA and BB are clear from the context.

  2. Cupβ€…β€ŠIβ€…β€ŠF\textbf{Cup} \; I \; F is written with symbols as ⋃i∈IFi\bigcup_{i \in I} F_i

  3. ⋃i∈IFi\bigcup_{i \in I} F_i can be written as ⋃(i:i∈I:F.i)\bigcup( i : i \in I: F.i)


fun Cup(I,A,B: set univ, F: I->A->B) : A->B {
  { x: A, y: B | some i: I | x->y in i.F }
}

Family of Sets

Cupβ€…β€ŠIβ€…β€ŠAβ€…β€ŠF:={β€…β€Šx∈A:βˆƒ(i∈I::x∈F[i])β€…β€Š}\textbf{Cup} \; I \; A \; F := \{\; x \in A : \exists(i \in I :: x \in F[i]) \;\}

I,A∈SetI, A \in \textbf{Set}

F∈Iβ†’AF \in I \to A


Notation.

  1. Cupβ€…β€ŠIβ€…β€ŠAβ€…β€ŠF\textbf{Cup} \; I \; A \; F can be written as Cupβ€…β€ŠIβ€…β€ŠF\textbf{Cup} \; I \; F when AA is clear from the context.

  2. Cupβ€…β€ŠIβ€…β€ŠF\textbf{Cup} \; I \; F is written with symbols as ⋃i∈IFi\bigcup_{i \in I} F_i

  3. ⋃i∈IFi\bigcup_{i \in I} F_i can be written as ⋃(i:i∈I:F.i)\bigcup( i : i \in I: F.i)


fun Cup(I,A: set univ, F: I->A) : set A {
  { x: A | some i: I | x in i.F }
}

Indexed Intersection

Family of Relations

Capβ€…β€ŠIβ€…β€ŠAβ€…β€ŠBβ€…β€ŠF:={β€…β€Šx∈A,y∈B:βˆ€(i∈I::(x,y)∈F[i])β€…β€Š}\textbf{Cap} \; I \; A \; B \; F := \{\; x \in A, y \in B : \forall(i \in I :: (x,y) \in F[i]) \;\}

I,A,B∈SetI, A, B \in \textbf{Set}

F∈(Aβ†’B)IF \in (A \to B)^I


Notation.

  1. Capβ€…β€ŠIβ€…β€ŠAβ€…β€ŠBβ€…β€ŠF\textbf{Cap} \; I \; A \; B \; F can be written as Capβ€…β€ŠIβ€…β€ŠF\textbf{Cap} \; I \; F when AA and BB are clear from the context.

  2. Capβ€…β€ŠIβ€…β€ŠF\textbf{Cap} \; I \; F is written with symbols as β‹‚i∈IFi\bigcap_{i \in I} F_i

  3. β‹‚i∈IFi\bigcap_{i \in I} F_i can be written as β‹‚(i:i∈I:F.i)\bigcap( i : i \in I: F.i)


fun Cap(I,A,B: set univ, F: I->A->B) : A->B {
  {x: A, y: B | all i: I | x->y in i.F }
}

Family of Sets

Capβ€…β€ŠIβ€…β€ŠAβ€…β€ŠF:={β€…β€Šx∈A:βˆ€(i∈I::x∈F[i])β€…β€Š}\textbf{Cap} \; I \; A \; F := \{\; x \in A : \forall(i \in I :: x \in F[i]) \;\}

I,A∈SetI, A \in \textbf{Set}

F∈Iβ†’AF \in I \to A


Notation.

  1. Capβ€…β€ŠIβ€…β€ŠAβ€…β€ŠF\textbf{Cap} \; I \; A \; F can be written as Capβ€…β€ŠIβ€…β€ŠF\textbf{Cap} \; I \; F when AA is clear from the context.

  2. Capβ€…β€ŠIβ€…β€ŠF\textbf{Cap} \; I \; F is written with symbols as β‹‚i∈IFi\bigcap_{i \in I} F_i

  3. β‹‚i∈IFi\bigcap_{i \in I} F_i can be written as β‹‚(i:i∈I:F.i)\bigcap( i : i \in I: F.i)


fun Cap(I,A: set univ, F: I->A) : set A {
  { x: A | all i: I | x in i.F }
}

Last updated