Compendium of Predicates
  • 🌐Orientation
    • ⭐Welcome
    • ✒️Notation
    • 😅An Example
  • 🧰Definitions
    • Relation Taxonomy
    • Order Taxonomy
    • Algebra
      • Magma
      • Semigroup
      • Monoid
      • Group
      • Ringoid
      • Semiring
      • Ring
      • Unit Ring
      • Boolean Ring
      • Boolean Group
    • Bandler and Kohout Products of Relations
    • Closed
    • Complement
    • De Baets and Kerre Products of Relations
    • Extremal Elements
    • Galois Connection
    • Images of a set under a relation
    • Indexed Union and Intersection
    • Monoidal Preorder
    • Monotone Map
    • Natural Projection
    • Non-Preservation of Extrema
    • Over and Under
    • Power Set
    • Preorder
    • Preservation of Extrema
    • Product
    • Relation Inclusion
    • Row Constant Relations
    • Semilattice
    • Set Inclusion
    • Symmetric Monoidal Preorder
    • Upper Set
  • 🔬Checks
    • 🎙️A few words about the checks
    • Indirect Equality and Inclusion
    • Below
    • Extremal Elements
    • Relation Division
    • Algebra
      • Ring
      • Boolean Ring
      • Boolean Group
Powered by GitBook
On this page
  • Warning
  • Indexed Union
  • Indexed Intersection
  1. Definitions

Indexed Union and Intersection

Families of relations and sets

Warning

Please pay attention to the type of the FFF 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]) \;\}CupIABF:={x∈A,y∈B:∃(i∈I::(x,y)∈F[i])}

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

F∈(A→B)IF \in (A \to B)^IF∈(A→B)I

Notation.

  1. Cup  I  A  B  F\textbf{Cup} \; I \; A \; B \; FCupIABF can be written as Cup  I  F\textbf{Cup} \; I \; FCupIF when AAA and BBB are clear from the context.

  2. Cup  I  F\textbf{Cup} \; I \; FCupIF is written with symbols as ⋃i∈IFi\bigcup_{i \in I} F_i⋃i∈I​Fi​

  3. ⋃i∈IFi\bigcup_{i \in I} F_i⋃i∈I​Fi​ can be written as ⋃(i:i∈I:F.i)\bigcup( i : i \in I: F.i)⋃(i:i∈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]) \;\}CupIAF:={x∈A:∃(i∈I::x∈F[i])}

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

F∈I→AF \in I \to AF∈I→A

Notation.

  1. Cup  I  A  F\textbf{Cup} \; I \; A \; F CupIAF can be written as Cup  I  F\textbf{Cup} \; I \; FCupIF when AAA is clear from the context.

  2. Cup  I  F\textbf{Cup} \; I \; FCupIF is written with symbols as ⋃i∈IFi\bigcup_{i \in I} F_i⋃i∈I​Fi​

  3. ⋃i∈IFi\bigcup_{i \in I} F_i⋃i∈I​Fi​ can be written as ⋃(i:i∈I:F.i)\bigcup( i : i \in I: F.i)⋃(i:i∈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]) \;\}CapIABF:={x∈A,y∈B:∀(i∈I::(x,y)∈F[i])}

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

F∈(A→B)IF \in (A \to B)^IF∈(A→B)I

Notation.

  1. Cap  I  A  B  F\textbf{Cap} \; I \; A \; B \; FCapIABF can be written as Cap  I  F\textbf{Cap} \; I \; FCapIF when AAA and BBB are clear from the context.

  2. Cap  I  F\textbf{Cap} \; I \; FCapIF is written with symbols as ⋂i∈IFi\bigcap_{i \in I} F_i⋂i∈I​Fi​

  3. ⋂i∈IFi\bigcap_{i \in I} F_i⋂i∈I​Fi​ can be written as ⋂(i:i∈I:F.i)\bigcap( i : i \in I: F.i)⋂(i:i∈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]) \;\}CapIAF:={x∈A:∀(i∈I::x∈F[i])}

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

F∈I→AF \in I \to AF∈I→A

Notation.

  1. Cap  I  A  F\textbf{Cap} \; I \; A \; FCapIAF can be written as Cap  I  F\textbf{Cap} \; I \; FCapIF when AAA is clear from the context.

  2. Cap  I  F\textbf{Cap} \; I \; FCapIF is written with symbols as ⋂i∈IFi\bigcap_{i \in I} F_i⋂i∈I​Fi​

  3. ⋂i∈IFi\bigcap_{i \in I} F_i⋂i∈I​Fi​ can be written as ⋂(i:i∈I:F.i)\bigcap( i : i \in I: F.i)⋂(i:i∈I:F.i)

fun Cap(I,A: set univ, F: I->A) : set A {
  { x: A | all i: I | x in i.F }
}
PreviousImages of a set under a relationNextMonoidal Preorder

Last updated 1 year ago

🧰