# Sets

- [Introduction](introduction.md)

  - [Enumerated Sets](introduction.md#enumerated-sets)

  - [Indexed Sets](introduction.md#indexed-sets)

  - [Multisets](introduction.md#multisets)

  - [Compatibility](introduction.md#compatibility)

  - [Notation](introduction.md#notation)

- [Creating Sets](creation.md)

  - [The Enumerated Set Constructor](creation.md#the-enumerated-set-constructor)

    - [`{ }: Null → Set`](creation.md#literal-literal-null-set)

    - [`{ U | }: Str → Set`](creation.md#literal-literal-u-str-set)

    - [`{ e₁, e₂, ..., eₙ }: Elt, ..., Elt → Set`](creation.md#literal-literal-e1-e2-en-elt-elt-set)

    - [`Example: Universe`](creation.md#example-ex-4076ed)

    - [`{ U | e₁, e₂, ..., eₙ }: Str, Elt, ..., Elt → Set`](creation.md#literal-literal-u-e1-e2-en-str-elt-elt-set)

    - [`{ e(x) : x in E | P(x) }`](creation.md#literal-literal-lbrace-rbrace-e-x-x-in-e-p-x)

    - [`{ U | e(x) : x in E | P(x) }`](creation.md#literal-literal-lbrace-rbrace-u-e-x-x-in-e-p-x)

    - [`{ e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }`](creation.md#literal-literal-lbrace-rbrace-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`{ U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }`](creation.md#literal-literal-lbrace-rbrace-u-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`Example: Almost Fermat`](creation.md#example-ex-8d723f)

  - [The Indexed Set Constructor](creation.md#the-indexed-set-constructor)

    - [`{ @ @}: Null → SetIndx`](creation.md#literal-literal-null-setindx)

    - [`{ @ U | @}: Str → SetIndx`](creation.md#literal-literal-u-str-setindx)

    - [`{ @ e₁, e₂, ..., eₙ @}: Elt, ..., Elt → SetIndx`](creation.md#literal-literal-e1-e2-en-elt-elt-setindx)

    - [`{ @ U |  e₁, e₂, ..., eₘ @}: Str, Elt, ..., Elt → SetIndx`](creation.md#literal-literal-u-e1-e2-em-str-elt-elt-setindx)

    - [`{ @ e(x) : x in E | P(x) @}`](creation.md#literal-literal-lbrace-rbrace-e-x-x-in-e-p-x-2)

    - [`{ @ U |  e(x) : x in E | P(x) @}`](creation.md#literal-literal-lbrace-rbrace-u-e-x-x-in-e-p-x-2)

    - [`{ @ e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) @}`](creation.md#literal-literal-lbrace-rbrace-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk-2)

    - [`{ @ U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)@}`](creation.md#literal-literal-lbrace-rbrace-u-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk-2)

    - [`Example: Almost Fermat Indexed`](creation.md#example-ex-c67e42)

  - [The Multiset Constructor](creation.md#the-multiset-constructor)

    - [`{* *}: Null → SetMulti`](creation.md#literal-literal-null-setmulti)

    - [`{* U | *}: Str → SetMulti`](creation.md#literal-literal-u-str-setmulti)

    - [`{* e₁, e₂, ..., eₙ *}: Elt, ..., Elt → SetMulti`](creation.md#literal-literal-e1-e2-en-elt-elt-setmulti)

    - [`{* U |  e₁, e₂, ..., eₘ *}: Str, Elt, ..., Elt → SetMulti`](creation.md#literal-literal-u-e1-e2-em-str-elt-elt-setmulti)

    - [`{* e(x) : x in E | P(x) *}`](creation.md#literal-literal-bracestar-starbrace-e-x-x-in-e-p-x)

    - [`{* U |  e(x) : x in E | P(x) *}`](creation.md#literal-literal-bracestar-starbrace-u-e-x-x-in-e-p-x)

    - [`{* e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) *}`](creation.md#literal-literal-bracestar-starbrace-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`{* U | e(x₁,...,xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) *}`](creation.md#literal-literal-bracestar-starbrace-u-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`Example: Multiset`](creation.md#example-ex-ca72ec)

  - [The Arithmetic Progression Constructors](creation.md#the-arithmetic-progression-constructors)

    - [`{  i..j }: RngIntElt, RngIntElt → Set`](creation.md#literal-literal-i-j-rngintelt-rngintelt-set)

    - [`{ U | i..j }: Str, RngIntElt, RngIntElt → SetIndx`](creation.md#literal-literal-u-i-j-str-rngintelt-rngintelt-setindx)

    - [`{ i .. j by k }: RngIntElt, RngIntElt, RngIntElt → Set`](creation.md#literal-literal-i-j-by-k-rngintelt-rngintelt-rngintelt-set)

    - [`{ U | i .. j by k }: Str, RngIntElt, RngIntElt, RngIntElt → Set`](creation.md#literal-literal-u-i-j-by-k-str-rngintelt-rngintelt-rngintelt-set)

    - [`Example: Progression`](creation.md#example-ex-91fc28)

- [Power Sets](power-set.md)

  - [`PowerSet(R): Str → PowSetEnum`](power-set.md#function-powerset-str)

  - [`PowerIndexedSet(R): Str → PowSetIndx`](power-set.md#function-powerindexedset-str)

  - [`PowerMultiset(R): Str → PowSetMulti`](power-set.md#function-powermultiset-str)

  - [`S in P: SetEnum, PowSetEnum → BoolElt`](power-set.md#operation-op-in-setenum-powsetenum)

  - [`S in P: SetIndx, PowSetIndx → BoolElt`](power-set.md#operation-op-in-setindx-powsetindx)

  - [`S in P: SetMulti, PowSetMulti → BoolElt`](power-set.md#operation-op-in-setmulti-powsetmulti)

  - [`P ! S: PowSetEnum, SetEnum → SetEnum`](power-set.md#operation-op-powsetenum-setenum)

  - [`P ! S: PowSetIndx, SetIndx → SetIndx`](power-set.md#operation-op-powsetindx-setindx)

  - [`P ! S: PowSetMulti, SetMulti → SetMulti`](power-set.md#operation-op-powsetmulti-setmulti)

  - [`Example: Power Set`](power-set.md#example-ex-0340bf)

  - [The Cartesian Product Constructors](power-set.md#the-cartesian-product-constructors)

- [Sets from Structures](conversion.md)

  - [`Set(M): Str → SetEnum`](conversion.md#function-set-str)

- [Accessing and Modifying Sets](access-modification.md)

  - [Accessing Sets and their Associated Structures](access-modification.md#accessing-sets-and-their-associated-structures)

    - [`# R: SetIndx → RngIntElt`](access-modification.md#operation-operation-setindx-rngintelt)

    - [`# R: SetEnum → RngIntElt`](access-modification.md#operation-operation-setenum-rngintelt)

    - [`# R: SetMulti → RngIntElt`](access-modification.md#operation-operation-setmulti-rngintelt)

    - [`Category(S): Any → Cat`](access-modification.md#function-category-any)

    - [`Type(S): Any → Cat`](access-modification.md#function-type-any)

    - [`Parent(R): Set → Str`](access-modification.md#function-parent-set)

    - [`Universe(R): Set → Str`](access-modification.md#function-universe-set)

    - [`Index(S, x): SetIndx, Elt → RngIntElt`](access-modification.md#function-index-setindx-elt)

    - [`Position(S, x): SetIndx, Elt → RngIntElt`](access-modification.md#function-position-setindx-elt)

    - [`S[i]: SetIndx, RngIntElt → Elt`](access-modification.md#literal-literal-s-i-setindx-rngintelt-elt)

    - [`S[I]: SetIndx, [RngIntElt] → SetIndx`](access-modification.md#literal-literal-s-i-setindx-rngintelt-setindx)

    - [`Example: Miscellaneous`](access-modification.md#example-ex-3d41ac)

  - [Selecting Elements of Sets](access-modification.md#selecting-elements-of-sets)

    - [`Random(R): SetIndx → Elt`](access-modification.md#function-random-setindx)

    - [`Random(R): SetEnum → Elt`](access-modification.md#function-random-setenum)

    - [`random{ e(x) : x in E | P(x) }`](access-modification.md#literal-literal-random-random-e-x-x-in-e-p-x)

    - [`random{ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }`](access-modification.md#literal-literal-random-random-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`Example: Random`](access-modification.md#example-ex-1b553f)

    - [`Representative(R): SetIndx → Elt`](access-modification.md#function-representative-setindx)

    - [`Rep(R): SetIndx → Elt`](access-modification.md#function-rep-setindx)

    - [`Representative(R): SetEnum → Elt`](access-modification.md#function-representative-setenum)

    - [`Rep(R): SetEnum → Elt`](access-modification.md#function-rep-setenum)

    - [`ExtractRep(~R, ~r): SetEnum, Elt`](access-modification.md#function-extractrep-setenum-elt-ref)

    - [`rep{ e(x) : x in E | P(x) }`](access-modification.md#literal-literal-rep-rep-e-x-x-in-e-p-x)

    - [`rep{ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ) }`](access-modification.md#literal-literal-rep-rep-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

    - [`Example: Extract Rep`](access-modification.md#example-ex-e07b22)

    - [`Minimum(S): SetIndx → Elt, RngIntElt`](access-modification.md#function-minimum-setindx)

    - [`Min(S): SetIndx → Elt, RngIntElt`](access-modification.md#function-min-setindx)

    - [`Minimum(S): SetEnum → Elt`](access-modification.md#function-minimum-setenum)

    - [`Min(S): SetEnum → Elt`](access-modification.md#function-min-setenum)

    - [`Minimum(S): SetMulti → Elt`](access-modification.md#function-minimum-setmulti)

    - [`Min(S): SetMulti → Elt`](access-modification.md#function-min-setmulti)

    - [`Maximum(S): SetIndx → Elt, RngIntElt`](access-modification.md#function-maximum-setindx)

    - [`Max(S): SetIndx → Elt, RngIntElt`](access-modification.md#function-max-setindx)

    - [`Maximum(S): SetEnum → Elt`](access-modification.md#function-maximum-setenum)

    - [`Max(S): SetEnum → Elt`](access-modification.md#function-max-setenum)

    - [`Maximum(S): SetMulti → Elt`](access-modification.md#function-maximum-setmulti)

    - [`Max(S): SetMulti → Elt`](access-modification.md#function-max-setmulti)

    - [`Hash(x): Elt → RngIntElt`](access-modification.md#function-hash-elt)

  - [Modifying Sets](access-modification.md#modifying-sets)

    - [`Include(~S, x): SetEnum, Elt`](access-modification.md#function-include-setenum-elt-ref)

    - [`Include(S, x): SetEnum, Elt → SetEnum`](access-modification.md#function-include-setenum-elt)

    - [`Include(~S, x): SetIndx, Elt`](access-modification.md#function-include-setindx-elt-ref)

    - [`Include(S, x): SetIndx, Elt → SetIndx`](access-modification.md#function-include-setindx-elt)

    - [`Include(~S, x): SetMulti, Elt`](access-modification.md#function-include-setmulti-elt-ref)

    - [`Include(S, x): SetMulti, Elt → SetMulti`](access-modification.md#function-include-setmulti-elt)

    - [`Exclude(~S, x): SetEnum, Elt`](access-modification.md#function-exclude-setenum-elt-ref)

    - [`Exclude(S, x): SetEnum, Elt → SetEnum`](access-modification.md#function-exclude-setenum-elt)

    - [`Exclude(~S, x): SetMulti, Elt`](access-modification.md#function-exclude-setmulti-elt-ref)

    - [`Exclude(S, x): SetMulti, Elt → SetMulti`](access-modification.md#function-exclude-setmulti-elt)

    - [`ChangeUniverse(~S, V): SetEnum, Str`](access-modification.md#function-changeuniverse-setenum-str-ref)

    - [`ChangeUniverse(S, V): SetEnum, Str → SetEnum`](access-modification.md#function-changeuniverse-setenum-str)

    - [`ChangeUniverse(~S, V): SetIndx, Str`](access-modification.md#function-changeuniverse-setindx-str-ref)

    - [`ChangeUniverse(S, V): SetIndx, Str → SetIndx`](access-modification.md#function-changeuniverse-setindx-str)

    - [`ChangeUniverse(~S, V): SetMulti, Str`](access-modification.md#function-changeuniverse-setmulti-str-ref)

    - [`ChangeUniverse(S, V): SetMulti, Str → SetMulti`](access-modification.md#function-changeuniverse-setmulti-str)

    - [`CanChangeUniverse(S, V): SetEnum, Str → Bool, SeqEnum`](access-modification.md#function-canchangeuniverse-setenum-str)

    - [`CanChangeUniverse(S, V): SetIndx, Str → Bool, SeqEnum`](access-modification.md#function-canchangeuniverse-setindx-str)

    - [`CanChangeUniverse(S, V): SetMulti, Str → Bool, SeqEnum`](access-modification.md#function-canchangeuniverse-setmulti-str)

    - [`Example: Include`](access-modification.md#example-ex-708b1a)

    - [`SetToIndexedSet(E): SetEnum → SetIndx`](access-modification.md#function-settoindexedset-setenum)

    - [`IndexedSetToSet(S): SetIndx → SetEnum`](access-modification.md#function-indexedsettoset-setindx)

    - [`Isetset(S): SetIndx → SetEnum`](access-modification.md#function-isetset-setindx)

    - [`IndexedSetToSequence(S): SetIndx → SeqEnum`](access-modification.md#function-indexedsettosequence-setindx)

    - [`Isetseq(S): SetIndx → SeqEnum`](access-modification.md#function-isetseq-setindx)

    - [`MultisetToSet(S): SetMulti → SetEnum`](access-modification.md#function-multisettoset-setmulti)

    - [`SetToMultiset(E): SetEnum → SetMulti`](access-modification.md#function-settomultiset-setenum)

    - [`SequenceToMultiset(Q): SeqEnum → SetMulti`](access-modification.md#function-sequencetomultiset-seqenum)

- [Operations on Sets](operation.md)

  - [Boolean Functions and Operators](operation.md#boolean-functions-and-operators)

    - [`IsNull(R): SetEnum → BoolElt`](operation.md#function-isnull-setenum)

    - [`IsNull(R): SetIndx → BoolElt`](operation.md#function-isnull-setindx)

    - [`IsNull(R): SetMulti → BoolElt`](operation.md#function-isnull-setmulti)

    - [`IsEmpty(R): SetEnum → BoolElt`](operation.md#function-isempty-setenum)

    - [`IsEmpty(R): SetIndx → BoolElt`](operation.md#function-isempty-setindx)

    - [`IsEmpty(R): SetMulti → BoolElt`](operation.md#function-isempty-setmulti)

    - [`x eq y: Elt, Elt → BoolElt`](operation.md#operation-op-eq-elt-elt)

    - [`x ne y: Elt, Elt → BoolElt`](operation.md#operation-op-ne-elt-elt)

    - [`x in R: Elt, Set → BoolElt`](operation.md#operation-op-in-elt-set)

    - [`x notin R: Elt, Set → BoolElt`](operation.md#operation-op-notin-elt-set)

    - [`R subset S: SetEnum, Set → BoolElt`](operation.md#operation-op-subset-setenum-set)

    - [`R subset S: SetIndx, Set → BoolElt`](operation.md#operation-op-subset-setindx-set)

    - [`R subset S: SetMulti, Set → BoolElt`](operation.md#operation-op-subset-setmulti-set)

    - [`R notsubset S: SetEnum, Set → BoolElt`](operation.md#operation-operation-notsubset-setenum-set-boolelt)

    - [`R notsubset S: SetIndx, Set → BoolElt`](operation.md#operation-operation-notsubset-setindx-set-boolelt)

    - [`R notsubset S: SetMulti, Set → BoolElt`](operation.md#operation-operation-notsubset-setmulti-set-boolelt)

    - [`R eq S: Set, Set → BoolElt`](operation.md#operation-op-eq-set-set)

    - [`R ne S: Set, Set → BoolElt`](operation.md#operation-op-ne-set-set)

    - [`IsDisjoint(R, S): SetEnum, SetEnum → BoolElt`](operation.md#function-isdisjoint-setenum-setenum)

    - [`IsDisjoint(R, S): SetIndx, SetIndx → BoolElt`](operation.md#function-isdisjoint-setindx-setindx)

    - [`IsDisjoint(R, S): SetMulti, SetMulti → BoolElt`](operation.md#function-isdisjoint-setmulti-setmulti)

  - [Binary Set Operators](operation.md#binary-set-operators)

    - [`R join S: SetEnum, SetEnum → SetEnum`](operation.md#operation-op-join-setenum-setenum)

    - [`R join S: SetIndx, SetIndx → SetIndx`](operation.md#operation-op-join-setindx-setindx)

    - [`R join S: SetMulti, SetMulti → SetMulti`](operation.md#operation-op-join-setmulti-setmulti)

    - [`R meet S: SetEnum, SetEnum → SetEnum`](operation.md#operation-op-meet-setenum-setenum)

    - [`R meet S: SetIndx, SetIndx → SetIndx`](operation.md#operation-op-meet-setindx-setindx)

    - [`R meet S: SetMulti, SetMulti → SetMulti`](operation.md#operation-op-meet-setmulti-setmulti)

    - [`R diff S: SetEnum, SetEnum → SetEnum`](operation.md#operation-operation-diff-setenum-setenum-setenum)

    - [`R diff S: SetIndx, SetIndx → SetIndx`](operation.md#operation-operation-diff-setindx-setindx-setindx)

    - [`R diff S: SetMulti, SetMulti → SetMulti`](operation.md#operation-operation-diff-setmulti-setmulti-setmulti)

    - [`R sdiff S: SetEnum, SetEnum → SetEnum`](operation.md#operation-operation-sdiff-setenum-setenum-setenum)

    - [`R sdiff S: SetIndx, SetIndx → SetIndx`](operation.md#operation-operation-sdiff-setindx-setindx-setindx)

    - [`R sdiff S: SetMulti, SetMulti → SetMulti`](operation.md#operation-operation-sdiff-setmulti-setmulti-setmulti)

    - [`Example: Join`](operation.md#example-ex-527afc)

  - [Other Set Operations](operation.md#other-set-operations)

    - [`Multiplicity(S, x): SetMulti, Elt → RngIntElt`](operation.md#function-multiplicity-setmulti-elt)

    - [`Multiplicities(S): SetMulti → SeqEnum`](operation.md#function-multiplicities-setmulti)

    - [`Subsets(S): SetEnum → SetEnum`](operation.md#function-subsets-setenum)

    - [`Subsets(S, k): SetEnum, RngIntElt → SetEnum`](operation.md#function-subsets-setenum-rngintelt)

    - [`RandomSubset(S, k): SetEnum, RngIntElt → SetEnum`](operation.md#function-randomsubset-setenum-rngintelt)

    - [`Multisets(S, k): SetEnum, RngIntElt → SetEnum`](operation.md#function-multisets-setenum-rngintelt)

    - [`Subsequences(S, k): SetEnum, RngIntElt → SetEnum`](operation.md#function-subsequences-setenum-rngintelt)

    - [`Permutations(S): SetEnum → SetEnum;`](operation.md#function-permutations-setenum)

    - [`Permutations(S, k): SetEnum, RngIntElt → SetEnum;`](operation.md#function-permutations-setenum-rngintelt)

- [Quantifiers](quantifier.md)

  - [`exists(t){ e(x): x in E | P(x) }`](quantifier.md#literal-literal-exists-exists-t-e-x-x-in-e-p-x)

  - [`exists(t₁, ..., tᵣ){ e(x) : x in E | P(x) }`](quantifier.md#literal-literal-exists-exists-t1-tr-e-x-x-in-e-p-x)

  - [`exists(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}`](quantifier.md#literal-literal-exists-exists-t-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

  - [`exists(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }`](quantifier.md#literal-literal-exists-exists-t1-tr-e-x1-xk-x1-in-e1-xk-in-ek-p)

  - [`Example: Exists`](quantifier.md#example-ex-eb9af3)

  - [`forall(t){ e(x) : x in E | P(x) }`](quantifier.md#literal-literal-forall-forall-t-e-x-x-in-e-p-x)

  - [`forall(t₁, ..., tᵣ){ e(x) : x in E | P(x) }`](quantifier.md#literal-literal-forall-forall-t1-tr-e-x-x-in-e-p-x)

  - [`forall(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}`](quantifier.md#literal-literal-forall-forall-t-e-x1-xk-x1-in-e1-xk-in-ek-p-x1-xk)

  - [`forall(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }`](quantifier.md#literal-literal-forall-forall-t1-tr-e-x1-xk-x1-in-e1-xk-in-ek-p)

  - [`Example: Nested Exists`](quantifier.md#example-ex-8bbcd9)

- [Reduction and Iteration](reduction-iteration.md)

  - [Reduction](reduction-iteration.md#reduction)

    - [`& o S: Op, SetEnum → Elt`](reduction-iteration.md#operation-operation-op-setenum-elt)

    - [`& o S: Op, SetIndx → Elt`](reduction-iteration.md#operation-operation-op-setindx-elt)

    - [`& o S: Op, SetMulti → Elt`](reduction-iteration.md#operation-operation-op-setmulti-elt)

    - [`Example: Reduction`](reduction-iteration.md#example-ex-50129c)

  - [Iteration](reduction-iteration.md#iteration)

    - [`x in S`](reduction-iteration.md#literal-literal-in-x-in-s)

    - [`i -> x in S`](reduction-iteration.md#literal-literal-in-i-x-in-s)

    - [`x -> v in M`](reduction-iteration.md#literal-literal-in-x-v-in-m)

    - [`Example: Iteration`](reduction-iteration.md#example-ex-00bab7)