Sets
- Introduction
- Creating Sets
- The Enumerated Set Constructor
{ }: Null → Set{ U | }: Str → Set{ e₁, e₂, ..., eₙ }: Elt, ..., Elt → SetExample: Universe{ U | e₁, e₂, ..., eₙ }: Str, Elt, ..., Elt → Set{ e(x) : x in E | P(x) }{ U | e(x) : x in E | P(x) }{ e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }{ U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }Example: Almost Fermat
- The Indexed Set Constructor
{ @ @}: Null → SetIndx{ @ U | @}: Str → SetIndx{ @ e₁, e₂, ..., eₙ @}: Elt, ..., Elt → SetIndx{ @ U | e₁, e₂, ..., eₘ @}: Str, Elt, ..., Elt → SetIndx{ @ e(x) : x in E | P(x) @}{ @ U | e(x) : x in E | P(x) @}{ @ e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) @}{ @ U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)@}Example: Almost Fermat Indexed
- The Multiset Constructor
{* *}: Null → SetMulti{* U | *}: Str → SetMulti{* e₁, e₂, ..., eₙ *}: Elt, ..., Elt → SetMulti{* U | e₁, e₂, ..., eₘ *}: Str, Elt, ..., Elt → SetMulti{* e(x) : x in E | P(x) *}{* U | e(x) : x in E | P(x) *}{* e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) *}{* U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) *}Example: Multiset
- 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 → EltRandom(R): SetEnum → Eltrandom{ e(x) : x in E | P(x) }random{ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }Example: RandomRepresentative(R): SetIndx → EltRep(R): SetIndx → EltRepresentative(R): SetEnum → EltRep(R): SetEnum → EltExtractRep(~R, ~r): SetEnum, Eltrep{ e(x) : x in E | P(x) }rep{ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }Example: Extract RepMinimum(S): SetIndx → Elt, RngIntEltMin(S): SetIndx → Elt, RngIntEltMinimum(S): SetEnum → EltMin(S): SetEnum → EltMinimum(S): SetMulti → EltMin(S): SetMulti → EltMaximum(S): SetIndx → Elt, RngIntEltMax(S): SetIndx → Elt, RngIntEltMaximum(S): SetEnum → EltMax(S): SetEnum → EltMaximum(S): SetMulti → EltMax(S): SetMulti → EltHash(x): Elt → RngIntElt
- Modifying Sets
Include(~S, x): SetEnum, EltInclude(S, x): SetEnum, Elt → SetEnumInclude(~S, x): SetIndx, EltInclude(S, x): SetIndx, Elt → SetIndxInclude(~S, x): SetMulti, EltInclude(S, x): SetMulti, Elt → SetMultiExclude(~S, x): SetEnum, EltExclude(S, x): SetEnum, Elt → SetEnumExclude(~S, x): SetMulti, EltExclude(S, x): SetMulti, Elt → SetMultiChangeUniverse(~S, V): SetEnum, StrChangeUniverse(S, V): SetEnum, Str → SetEnumChangeUniverse(~S, V): SetIndx, StrChangeUniverse(S, V): SetIndx, Str → SetIndxChangeUniverse(~S, V): SetMulti, StrChangeUniverse(S, V): SetMulti, Str → SetMultiCanChangeUniverse(S, V): SetEnum, Str → Bool, SeqEnumCanChangeUniverse(S, V): SetIndx, Str → Bool, SeqEnumCanChangeUniverse(S, V): SetMulti, Str → Bool, SeqEnumExample: IncludeSetToIndexedSet(E): SetEnum → SetIndxIndexedSetToSet(S): SetIndx → SetEnumIsetset(S): SetIndx → SetEnumIndexedSetToSequence(S): SetIndx → SeqEnumIsetseq(S): SetIndx → SeqEnumMultisetToSet(S): SetMulti → SetEnumSetToMultiset(E): SetEnum → SetMultiSequenceToMultiset(Q): SeqEnum → SetMulti
- Operations on Sets
- Boolean Functions and Operators
IsNull(R): SetEnum → BoolEltIsNull(R): SetIndx → BoolEltIsNull(R): SetMulti → BoolEltIsEmpty(R): SetEnum → BoolEltIsEmpty(R): SetIndx → BoolEltIsEmpty(R): SetMulti → BoolEltx eq y: Elt, Elt → BoolEltx ne y: Elt, Elt → BoolEltx in R: Elt, Set → BoolEltx notin R: Elt, Set → BoolEltR subset S: SetEnum, Set → BoolEltR subset S: SetIndx, Set → BoolEltR subset S: SetMulti, Set → BoolEltR notsubset S: SetEnum, Set → BoolEltR notsubset S: SetIndx, Set → BoolEltR notsubset S: SetMulti, Set → BoolEltR eq S: Set, Set → BoolEltR ne S: Set, Set → BoolEltIsDisjoint(R, S): SetEnum, SetEnum → BoolEltIsDisjoint(R, S): SetIndx, SetIndx → BoolEltIsDisjoint(R, S): SetMulti, SetMulti → BoolElt
- Binary Set Operators
R join S: SetEnum, SetEnum → SetEnumR join S: SetIndx, SetIndx → SetIndxR join S: SetMulti, SetMulti → SetMultiR meet S: SetEnum, SetEnum → SetEnumR meet S: SetIndx, SetIndx → SetIndxR meet S: SetMulti, SetMulti → SetMultiR diff S: SetEnum, SetEnum → SetEnumR diff S: SetIndx, SetIndx → SetIndxR diff S: SetMulti, SetMulti → SetMultiR sdiff S: SetEnum, SetEnum → SetEnumR sdiff S: SetIndx, SetIndx → SetIndxR sdiff S: SetMulti, SetMulti → SetMultiExample: Join
- Other Set Operations
Multiplicity(S, x): SetMulti, Elt → RngIntEltMultiplicities(S): SetMulti → SeqEnumSubsets(S): SetEnum → SetEnumSubsets(S, k): SetEnum, RngIntElt → SetEnumRandomSubset(S, k): SetEnum, RngIntElt → SetEnumMultisets(S, k): SetEnum, RngIntElt → SetEnumSubsequences(S, k): SetEnum, RngIntElt → SetEnumPermutations(S): SetEnum → SetEnum;Permutations(S, k): SetEnum, RngIntElt → SetEnum;
- Quantifiers
exists(t){ e(x): x in E | P(x) }exists(t₁, ..., tᵣ){ e(x) : x in E | P(x) }exists(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}exists(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }Example: Existsforall(t){ e(x) : x in E | P(x) }forall(t₁, ..., tᵣ){ e(x) : x in E | P(x) }forall(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}forall(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }Example: Nested Exists
- Reduction and Iteration
