- Introduction
- Creating Sets
- The Formal Set Constructor
- The Enumerated Set Constructor
- { } : Null -> Set
- { U | } : Str -> Set
- { e1, e2, ..., en } : Elt, ..., Elt -> Set
- Example Set_Universe (H10E1)
- { U | e1, e2, ..., en } : Str, Elt, ..., Elt -> Set
- { e(x) : x in E | P(x) }
- { U | e(x) : x in E | P(x) }
- { e(x1,...,xk) : x1 in E1, ..., xkin Ek | P(x1, ..., xk) }
- { U | e(x1,...,xk) : x1 in E1, ...,xk in Ek | P(x1, ..., xk) }
- Example Set_AlmostFermat (H10E2)
- The Indexed Set Constructor
- {@ @} : Null -> SetIndx
- {@ U | @} : Str -> SetIndx
- {@ e1, e2, ..., en @} : Elt, ..., Elt -> SetIndx
- {@ U | e1, e2, ..., em @} : Str, Elt, ..., Elt -> SetIndx
- {@ e(x) : x in E | P(x) @}
- {@ U | e(x) : x in E | P(x) @}
- {@ e(x1,...,xk) : x1 in E1, ..., xkin Ek | P(x1, ..., xk) @}
- {@ U | e(x1,...,xk) : x1 in E1, ...,xk in Ek | P(x1, ..., xk)@}
- Example Set_AlmostFermatIndexed (H10E3)
- The Multiset Constructor
- {* *} : Null -> SetMulti
- {* U | *} : Str -> SetMulti
- {* e1, e2, ..., en *} : Elt, ..., Elt -> SetMulti
- {* U | e1, e2, ..., em *} : Str, Elt, ..., Elt -> SetMulti
- {* e(x) : x in E | P(x) *}
- {* U | e(x) : x in E | P(x) *}
- {* e(x1,...,xk) : x1 in E1, ..., xkin Ek | P(x1, ..., xk) *}
- {* U | e(x1,...,xk) : x1 in E1, ...,xk in Ek | P(x1, ..., xk) *}
- Example Set_Multiset (H10E4)
- The Arithmetic Progression Constructors
- Power Sets
- Sets from Structures
- Accessing and Modifying Sets
- Accessing Sets and their Associated Structures
- Selecting Elements of Sets
- Random(R) : SetIndx -> Elt
- random{ e(x) : x in E | P(x) }
- random{ e(x1, ..., xk) : x1 in E1,..., xk in Ek | P(x1, ..., xk) }
- Example Set_Random (H10E8)
- Representative(R) : SetIndx -> Elt
- ExtractRep(~R, ~r) : SetEnum, Elt ->
- rep{ e(x) : x in E | P(x) }
- rep{ e(x1, ..., xk) : x1 in E1, ...,xk in Ek | P(x1, ..., xk) }
- Example Set_ExtractRep (H10E9)
- Minimum(S) : SetIndx -> Elt, RngIntElt
- Maximum(S) : SetIndx -> Elt, RngIntElt
- Hash(x) : Elt -> RngIntElt
- Modifying Sets
- 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
- Other Set Operations
- Multiplicity(S, x) : SetMulti, Elt -> RngIntElt
- Multiplicities(S) : SetMulti -> SeqEnum
- Subsets(S) : SetEnum -> SetEnum
- Subsets(S, k) : SetEnum, RngIntElt -> SetEnum
- RandomSubset(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(x1, ..., xk): x1 in E1,..., xk in Ek | P(x1, ..., xk) }
- Example Set_Exists (H10E12)
- forall(t){ e(x) : x in E | P(x) }
- forall(t){ e(x1, ..., xk): x1 in E1,..., xk in Ek | P(x1, ..., xk) }
- Example Set_NestedExists (H10E13)
- Reduction and Iteration
V2.28, 13 July 2023