SETS

DETAILS

 
Introduction

      Enumerated Sets

      Formal Sets

      Indexed Sets

      Multisets

      Compatibility

      Notation

 
Creating Sets

      The Formal Set Constructor
            {! x in F | P(x) !}

      The Enumerated Set Constructor
            { } : Null -> Set
            { U | } : Struct -> Set
            { e_1, e_2, ..., e_n } : Elt, ..., Elt -> Set
            Example Set_Universe (H9E1)
            { U | e_1, e_2, ..., e_n } : Struct, Elt, ..., Elt -> Set
            { e(x) : x in E | P(x) }
            { U | e(x) : x in E | P(x) }
            { e(x_1,...,x_k) : x_1 in E_1, ..., x_kin E_k | P(x_1, ..., x_k) }
            { U | e(x_1,...,x_k) : x_1 in E_1, ...,x_k in E_k | P(x_1, ..., x_k) }
            Example Set_AlmostFermat (H9E2)

      The Indexed Set Constructor
            {@ @} : Null -> SetIndx
            {@ U | @} : Struct -> SetIndx
            {@ e_1, e_2, ..., e_n @} : Elt, ..., Elt -> SetIndx
            {@ U | e_1, e_2, ..., e_m @} : Struct, Elt, ..., Elt -> SetIndx
            {@ e(x) : x in E | P(x) @}
            {@ U | e(x) : x in E | P(x) @}
            {@ e(x_1,...,x_k) : x_1 in E_1, ..., x_kin E_k | P(x_1, ..., x_k) @}
            {@ U | e(x_1,...,x_k) : x_1 in E_1, ...,x_k in E_k | P(x_1, ..., x_k)@}
            Example Set_AlmostFermatIndexed (H9E3)

      The Multiset Constructor
            {* *} : Null -> SetMulti
            {* U | *} : Struct -> SetMulti
            {* e_1, e_2, ..., e_n *} : Elt, ..., Elt -> SetMulti
            {* U | e_1, e_2, ..., e_m *} : Struct, Elt, ..., Elt -> SetMulti
            {* e(x) : x in E | P(x) *}
            {* U | e(x) : x in E | P(x) *}
            {* e(x_1,...,x_k) : x_1 in E_1, ..., x_kin E_k | P(x_1, ..., x_k) *}
            {* U | e(x_1,...,x_k) : x_1 in E_1, ...,x_k in E_k | P(x_1, ..., x_k) *}
            Example Set_Multiset (H9E4)

      The Arithmetic Progression Constructors
            { i..j } : RngIntElt, RngIntElt -> Set
            { i .. j by k } : RngIntElt, RngIntElt, RngIntElt -> Set
            Example Set_Progression (H9E5)

 
Power Sets
      PowerSet(R) : Struct -> PowSetEnum
      PowerIndexedSet(R) : Struct -> PowSetIndx
      PowerMultiset(R) : Struct -> PowSetMulti
      S in P : SetEnum, PowSetEnum -> BoolElt
      PowerFormalSet(R) : Struct -> PowSetIndx
      S in P : SetIndx, PowSetIndx -> BoolElt
      S in P : SetMulti, PowSetMulti -> BoolElt
      P ! S : PowSetEnum, SetEnum -> SetEnum
      P ! S : PowSetIndx, SetIndx -> SetIndx
      P ! S : PowSetMulti, SetMulti -> SetMulti
      Example Set_PowerSet (H9E6)

      The Cartesian Product Constructors

 
Sets from Structures
      Set(M) : Struct -> SetEnum
      FormalSet(M) : Struct -> SetForm

 
Accessing and Modifying Sets

      Accessing Sets and their Associated Structures
            # R : SetIndx -> RngIntElt
            Category(S) : Obj -> Cat
            Parent(R) : Set -> Struct
            Universe(R) : Set -> Struct
            Index(S, x) : SetIndx, Elt -> RngIntElt
            S[i] : SetIndx, RngIntElt -> Elt
            S[I] : SetIndx, [RngIntElt] -> SetIndx
            Example Set_Miscellaneous (H9E7)

      Selecting Elements of Sets
            Random(R) : SetIndx -> Elt
            random{ e(x) : x in E | P(x) }
            random{ e(x_1, ..., x_k) : x_1 in E_1,..., x_k in E_k | P(x_1, ..., x_k) }
            Example Set_Random (H9E8)
            Representative(R) : SetIndx -> Elt
            ExtractRep(~R, ~r) : SetEnum, Elt ->
            rep{ e(x) : x in E | P(x) }
            rep{ e(x_1, ..., x_k) : x_1 in E_1, ...,x_k in E_k | P(x_1, ..., x_k) }
            Example Set_ExtractRep (H9E9)
            Minimum(S) : SetIndx -> Elt, RngIntElt
            Maximum(S) : SetIndx -> Elt, RngIntElt
            Hash(x) : Elt -> RngIntElt

      Modifying Sets
            Include(~S, x) : SetEnum, Elt ->
            Exclude(~S, x) : SetEnum, Elt ->
            ChangeUniverse(~S, V) : SetEnum, Str ->
            CanChangeUniverse(S, V) : SetEnum, Str -> Bool, SeqEnum
            Example Set_Include (H9E10)
            SetToIndexedSet(E) : SetEnum -> SetIndx
            IndexedSetToSet(S) : SetIndx -> SetEnum
            IndexedSetToSequence(S) : SetIndx -> SeqEnum
            MultisetToSet(S) : SetMulti -> SetEnum
            SetToMultiset(E) : SetEnum -> SetMulti
            SequenceToMultiset(Q) : SeqEnum -> SetMulti

 
Operations on Sets

      Boolean Functions and Operators
            IsNull(R) : SetEnum -> BoolElt
            IsEmpty(R) : SetEnum -> BoolElt
            x eq y : Elt, Elt -> BoolElt
            x ne y : Elt, Elt -> BoolElt
            x in R : Elt, Set -> BoolElt
            x notin R : Elt, Set -> BoolElt
            R subset S : SetEnum, Set -> BoolElt
            R notsubset S : SetEnum, Set -> BoolElt
            R eq S : Set, Set -> BoolElt
            R ne S : Set, Set -> BoolElt
            IsDisjoint(R, S) : SetEnum, SetEnum -> BoolElt

      Binary Set Operators
            R join S : SetEnum, SetEnum -> SetEnum
            R meet S : SetEnum, SetEnum -> SetEnum
            R diff S : SetEnum, SetEnum -> SetEnum
            R sdiff S : SetEnum, SetEnum -> SetEnum
            Example Set_Join (H9E11)

      Other Set Operations
            Multiplicity(S, x) : SetMulti, Elt -> RngIntElt
            Multiplicities(S) : SetMulti -> SeqEnum
            Subsets(S) : SetEnum -> SetEnum
            Subsets(S, k) : SetEnum, RngIntElt -> SetEnum
            Multisets(S, k) : SetEnum, RngIntElt -> SetEnum
            Subsequences(S, k) : SetEnum, RngIntElt -> SetEnum
            Permutations(S) : SetEnum -> SetEnum;
            Permutations(S, k) : SetEnum, RngIntElt -> SetEnum;

 
Quantifiers
      exists(t){ e(x): x in E | P(x) }
      exists(t){ e(x_1, ..., x_k): x_1 in E_1,..., x_k in E_k | P(x_1, ..., x_k) }
      Example Set_Exists (H9E12)
      forall(t){ e(x) : x in E | P(x) }
      forall(t){ e(x_1, ..., x_k): x_1 in E_1,..., x_k in E_k | P(x_1, ..., x_k) }
      Example Set_NestedExists (H9E13)

 
Reduction and Iteration over Sets
      x in S
      & o S : Op, SetIndx -> Elt
      Example Set_Reduction (H9E14)