Equiv.asEmbeddingdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $e$ be an equivalence from $x_{1}$ to $\SubtypeSet {x_{2}}{p (x_{2})}$. Then $\operatorname{asEmbedding}$ applied to $e$ is an embedding of $x_{1}$ and $x$ defined as the composition of the embedding of $e$ and the subtype of $p$.
Equiv.embeddingCongrdefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding congruence of h and #2 (from the name)
English
Let $h$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{h'}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the embedding congruence of $h$ and $\mathrm{h'}$ is an equivalence from the set of embeddings of $x$ and $x_{2}$ to the set of embeddings of $x_{1}$ and $x_{3}$.
Equiv.embeddingSurjectiveEquivdefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding surjective equivalence (from the name)
English
The embedding surjective equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{Surjective} (\operatorname{coe} (f))})}{(\EquivMACRoAE {x}{x_{1}})}$.
Equiv.subtypeInjectiveEquivEmbeddingdefMathlib.Logic.Embedding.Basic, function or constantWording
the subtype injective equivalence embedding of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the subtype injective equivalence embedding of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{Injective} (f)})}{\operatorname{Embedding} (x , x_{1})}$.
Equiv.toEmbeddingdefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding of f (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Then the embedding of $f$ is an embedding of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{injective}$ applied to $f$.
Function.EmbeddingstructureMathlib.Logic.Embedding.Basic, typeWording
embedding of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the embeddings of $x$ and $x_{1}$ are a basic type.
Function.Embedding.arrowCongrLeftdefMathlib.Logic.Embedding.Basic, function or constantWording
the left arrow congruence of e (from the name)
English
Let $e$ be an embedding of $x$ and $x_{1}$. Then the left arrow congruence of $e$ is an embedding of the set of functions from elements of $x$ to elements of $x_{2}$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$.
Function.Embedding.arrowCongrRightdefMathlib.Logic.Embedding.Basic, function or constantWording
the right arrow congruence of e (from the name)
English
Let $e$ be an embedding of $x$ and $x_{1}$. Then the right arrow congruence of $e$ is an embedding of the set of functions from elements of $x_{2}$ to elements of $x$ and the set of functions from elements of $x_{2}$ to elements of $x_{1}$ defined as the right product congruence of the function that maps $x_{3}$ to $e$.
Function.Embedding.congrdefMathlib.Logic.Embedding.Basic, function or constantWording
the congruence of x5 and f (from the name)
English
Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{5}$ be an equivalence from $x_{2}$ to $x_{3}$. Let $f$ be an embedding of $x$ and $x_{2}$. Then the congruence of $x_{5}$ and $f$ is an embedding of $x_{1}$ and $x_{3}$ defined as the composition of the embedding of the inverse of $x_{4}$ and the composition of $f$ and the embedding of $x_{5}$.
Function.Embedding.equivOfSurjectivedefMathlib.Logic.Embedding.Basic, function or constantWording
the equivalence of f and hf (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the equivalence of $f$ and $\mathrm{hf}$ is an equivalence from $x$ to $x_{1}$.
Function.Embedding.inldefMathlib.Logic.Embedding.Basic, function or constantWording
the left injection (from the name)
English
The left injection is an embedding of $x$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{inl}$ and the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{inj}$.
Function.Embedding.inrdefMathlib.Logic.Embedding.Basic, function or constantWording
the right injection (from the name)
English
The right injection is an embedding of $x_{1}$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{inr}$ and the function that maps $x_{2}$ and $x_{3}$ to $\operatorname{inj}$.
Function.Embedding.ofIsEmptydefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding (from the name)
English
The embedding is an embedding of $x$ and $x_{1}$.
Function.Embedding.ofSurjectivedefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding of f and hf (from the name)
English
Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{Surjective}$ holds for $f$. Then the embedding of $f$ and $\mathrm{hf}$ is an embedding of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{surjInv}$ applied to $\mathrm{hf}$ and $\mathrm{Function\_\_injective\_surjInv}$ applied to $\mathrm{hf}$.
Function.Embedding.oneEmbeddingEquivdefMathlib.Logic.Embedding.Basic, function or constantWording
the equivalence (from the docstring)
English
The equivalence is an equivalence from the set of embeddings of $\mathrm{one}$ and $x$ to $x$.
Function.Embedding.optionMapdefMathlib.Logic.Embedding.Basic, function or constantWording
the option map of f (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Then the option map of $f$ is an embedding of $\mathrm{Option}$ applied to $x$ and $\mathrm{Option}$ applied to $x_{1}$.
Function.Embedding.piCongrRightdefMathlib.Logic.Embedding.Basic, function or constantWording
the right product congruence of e (from the name)
English
Let $e$ be a function from elements $a_{2}$ of $x$ to embeddings of $x_{1}$ applied to $a_{2}$ and $x_{2}$ applied to $a_{2}$. Then the right product congruence of $a_{2}$ is an embedding of the set of functions from elements $a$ of $x$ to elements of $x_{1}$ applied to $a$ and the set of functions from elements $a_{1}$ of $x$ to elements of $x_{2}$ applied to $a_{1}$.
Function.Embedding.pprodMapdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $x_{4}$ be an embedding of $x$ and $x_{1}$. Let $x_{5}$ be an embedding of $x_{2}$ and $x_{3}$. Then $\operatorname{pprodMap}$ applied to $x_{4}$ and $x_{5}$ is an embedding of $\mathrm{PProd}$ applied to $x$ and $x_{2}$ and $\mathrm{PProd}$ applied to $x_{1}$ and $x_{3}$.
Function.Embedding.prodMapdefMathlib.Logic.Embedding.Basic, function or constantWording
the product map of x4 and x5 (from the name)
English
Let $x_{4}$ be an embedding of $x$ and $x_{1}$. Let $x_{5}$ be an embedding of $x_{2}$ and $x_{3}$. Then the product map of $x_{4}$ and $x_{5}$ is an embedding of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.
Function.Embedding.punitdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $b$ be an element of $x$. Then $\operatorname{punit}$ applied to $b$ is an embedding of $\mathrm{PUnit}$ and $x$.
Function.Embedding.quotientOutdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{quotientOut}$ applied to $x$ is an embedding of $\mathrm{Quotient}$ applied to $s$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{out}$ and $\mathrm{Quotient\_\_out\_injective}$.
Function.Embedding.refldefMathlib.Logic.Embedding.Basic, function or constantWording
the identity map of x (from the docstring)
English
Let $x$ be a set. Then the identity map of $x$ is an embedding of $x$ and $x$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and $\mathrm{Function\_\_injective\_id}$.
Function.Embedding.sectLdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then $\operatorname{sectL}$ applied to $x$ and $b$ is an embedding of $x$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
Function.Embedding.sectRdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $a$ be an element of $x$. Let $x_{1}$ be a set. Then $\operatorname{sectR}$ applied to $a$ and $x_{1}$ is an embedding of $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
Function.Embedding.setValuedefMathlib.Logic.Embedding.Basic, function or constantWording
the set value of a and b (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the set value of $a$ and $b$ is an embedding of $x$ and $x_{1}$.
Function.Embedding.sigmaMapdefMathlib.Logic.Embedding.Basic, function or constantWording
the sigma map of f and g (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $g$ be a function from elements $a_{1}$ of $x$ to embeddings of $x_{2}$ applied to $a_{1}$ and $x_{3}$ applied to $f$ applied to $a_{1}$. Then the sigma map of $f$ and $a_{1}$ is an embedding of $\Sigma$ applied to the function that maps $a$ to $x_{2}$ applied to $a$ and $\Sigma$ applied to the function that maps $\mathrm{a'}$ to $x_{3}$ applied to $\mathrm{a'}$.
Function.Embedding.sigmaMkdefMathlib.Logic.Embedding.Basic, function or constantWording
the sigma of a (from the name)
English
Let $a$ be an element of $x$. Then the sigma of $a$ is an embedding of $x_{1}$ applied to $a$ and $\Sigma$ applied to the function that maps $x_{2}$ to $x_{1}$ applied to $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $a$ and $\mathrm{sigma\_mk\_injective}$.
Function.Embedding.somedefMathlib.Logic.Embedding.Basic, function or constantEnglish
$\operatorname{some}$ is an embedding of $x$ and $\mathrm{Option}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{some}$ and $\mathrm{Option\_\_some\_injective}$ applied to $x$.
Function.Embedding.subtypedefMathlib.Logic.Embedding.Basic, function or constantWording
the subtype of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the subtype of $p$ is an embedding of $\SubtypeSet {x_{1}}{p (x_{1})}$ and $x$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{ext}$.
Function.Embedding.subtypeMapdefMathlib.Logic.Embedding.Basic, function or constantWording
the subtype map of f and h (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$ such that for all elements $x_{3}$ of $x$, if $p$ holds for $x_{3}$, then $q$ holds for $f$ applied to $x_{3}$. Then the subtype map of $f$ and $h$ is an embedding of $\SubtypeSet {x_{2}}{p (x_{2})}$ and $\SubtypeSet {y}{q (y)}$.
Function.Embedding.sumMapdefMathlib.Logic.Embedding.Basic, function or constantWording
the sum map of x4 and x5 (from the name)
English
Let $x_{4}$ be an embedding of $x$ and $x_{1}$. Let $x_{5}$ be an embedding of $x_{2}$ and $x_{3}$. Then the sum map of $x_{4}$ and $x_{5}$ is an embedding of $\mathrm{Sum}$ applied to $x$ and $x_{2}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{3}$.
Function.Embedding.toFundefMathlib.Logic.Embedding.Basic, function or constantWording
the embedding of self and x2 (from the name)
English
Let $\mathrm{self}$ be an embedding of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then the embedding of $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
Function.Embedding.transdefMathlib.Logic.Embedding.Basic, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $g$ be an embedding of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an embedding of $x$ and $x_{2}$.
Subtype.impEmbeddingdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $p$ and $q$ be functions from elements of $x$ to propositions such that for all elements $x_{3}$ of $x$, if $p$ holds for $x_{3}$, then $q$ holds for $x_{3}$. Then $\operatorname{impEmbedding}$ applied to $p$, $q$ and $h$ is an embedding of $\SubtypeSet {x_{1}}{p (x_{1})}$ and $\SubtypeSet {x_{2}}{q (x_{2})}$.
subtypeOrLeftEmbeddingdefMathlib.Logic.Embedding.Basic, function or constantEnglish
Let $p$ and $q$ be functions from elements of $x$ to propositions. Then $\mathrm{subtypeOrLeftEmbedding}$ applied to $p$ and $q$ is an embedding of $\SubtypeSet {x_{2}}{\mathrm{or} (p (x_{2}), q (x_{2}))}$ and $\mathrm{Sum}$ applied to $\SubtypeSet {x_{3}}{p (x_{3})}$ and $\SubtypeSet {x_{4}}{q (x_{4})}$.
Function.Embedding.codRestrictdefMathlib.Logic.Embedding.Set, function or constantEnglish
Let $p$ be an element of $\wp x_{1}$. Let $f$ be an embedding of $x$ and $x_{1}$ such that for all elements $a$ of $x$, $\MembershipmemMACRoT {p}{f (a)}$. Then $\operatorname{codRestrict}$ applied to $p$, $f$ and $H$ is an embedding of $x$ and the set of elements of $p$.
Function.Embedding.imagedefMathlib.Logic.Embedding.Set, function or constantWording
the image of f (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Then the image of $f$ is an embedding of $\wp x$ and $\wp x_{1}$.
Function.Embedding.optionElimdefMathlib.Logic.Embedding.Set, function or constantWording
the option eliminator of f and x2 (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$ such that $x_{2}$ is not an element of the range of $\operatorname{coe}$ applied to $f$. Then the option eliminator of $f$ and $x_{2}$ is an embedding of $\mathrm{Option}$ applied to $x$ and $x_{1}$.
Function.Embedding.optionEmbeddingEquivdefMathlib.Logic.Embedding.Set, function or constantWording
the option embedding equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the option embedding equivalence of $x$ and $x_{1}$ is an equivalence from the set of embeddings of $\mathrm{Option}$ applied to $x$ and $x_{1}$ to $\Sigma$ applied to the function that maps $f$ to the set of elements of the complement of the range of $\operatorname{coe}$ applied to $f$.
Function.Embedding.sigmaSetdefMathlib.Logic.Embedding.Set, function or constantWording
the sigma set of h (from the name)
English
Assume that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $s$ is pairwise. Then the sigma set of $h$ is an embedding of $\Sigma$ applied to the function that maps $i$ to the set of elements of $s$ applied to $i$ and $x$.
Function.Embedding.sumSetdefMathlib.Logic.Embedding.Set, function or constantWording
the sum set of h (from the name)
English
Assume that $s$ is disjoint to $t$. Then the sum set of $h$ is an embedding of $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of $t$ and $x$.
Set.embeddingOfSubsetdefMathlib.Logic.Embedding.Set, function or constantWording
the embedding of s and t (from the name)
English
Let $s$ and $t$ be elements of $\wp x$ such that $s \leq t$. Then the embedding of $s$ and $t$ is an embedding of the set of elements of $s$ and the set of elements of $t$.
subtypeOrEquivdefMathlib.Logic.Embedding.Set, function or constantEnglish
Let $p$ and $q$ be functions from elements of $x$ to propositions such that $p$ is disjoint to $q$. Then $\mathrm{subtypeOrEquiv}$ applied to $p$, $q$ and $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{\mathrm{or} (p (x_{2}), q (x_{2}))})}{\mathrm{Sum} (\SubtypeSet {x_{3}}{p (x_{3})}, \SubtypeSet {x_{4}}{q (x_{4})})}$.
Directed.sequencedefMathlib.Logic.Encodable.Basic, function or constantWording
the sequence of f and x4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{Directed}$ holds for $r$ and $f$. Let $x_{4}$ be a natural number. Then the sequence of $f$ and $x_{4}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Directed\_\_sequence\_\_\_f}$ applied to $f$ and $\mathrm{hf}$.
EncodableclassMathlib.Logic.Encodable.Basic, predicateWording
x is encodable (from the name)
English
Let $x$ be a set. Then we can say that $x$ is encodable.
Encodable.choosedefMathlib.Logic.Encodable.Basic, function or constantEnglish
Assume that there exists an element $x_{3}$ of $x$, such that $p$ holds for $x_{3}$. Then $\operatorname{choose}$ applied to $h$ is an element of $x$.
Encodable.decodedefMathlib.Logic.Encodable.Basic, function or constantWording
the decode of x1 (from the name)
English
Let $x_{1}$ be a natural number. Then the decode of $x_{1}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.
Encodable.decodeSigmadefMathlib.Logic.Encodable.Basic, function or constantWording
the decode sigma of n (from the name)
English
Let $n$ be a natural number. Then the decode sigma of $n$ is an element of $\mathrm{Option}$ applied to $\Sigma$ applied to $x_{1}$.
Encodable.decodeSubtypedefMathlib.Logic.Encodable.Basic, function or constantWording
the decode subtype of v (from the name)
English
Let $v$ be a natural number. Then the decode subtype of $v$ is an element of $\mathrm{Option}$ applied to $\SubtypeSet {a}{P (a)}$ defined as $\operatorname{bind}$ applied to the decode of $v$ and the function that maps $a$ to $\mathrm{dite}$ applied to $P$ applied to $a$, the function that maps $h$ to $\operatorname{some}$ applied to $a$ and the function that maps $h_{1}$ to $\operatorname{none}$.
Encodable.decodeSumdefMathlib.Logic.Encodable.Basic, function or constantWording
the decode sum of n (from the name)
English
Let $n$ be a natural number. Then the decode sum of $n$ is an element of $\mathrm{Option}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$.
Encodable.decode₂defMathlib.Logic.Encodable.Basic, function or constantWording
the decode of x and n (from the name)
English
Let $x$ be a set. Let $n$ be a natural number. Then the decode of $x$ and $n$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{bind}$ applied to the decode of $n$ and $\operatorname{guard}$ applied to the function that maps $a$ to $\operatorname{decide}$ applied to $\mathrm{Eq} (\operatorname{encode} (a), n)$.
Encodable.encodedefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x_{1}$ be an element of $x$. Then $\operatorname{encode}$ applied to $x_{1}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
Encodable.encode'defMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{encode'}$ applied to $x$ is an embedding of $x$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{encode}$ and $\mathrm{Encodable\_\_encode\_injective}$.
Encodable.encodeSigmadefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x_{4}$ be an element of $\Sigma$ applied to $x_{1}$. Then $\operatorname{encodeSigma}$ applied to $x_{4}$ is a natural number.
Encodable.encodeSubtypedefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x_{1}$ be an element of $\SubtypeSet {a}{P (a)}$. Then $\operatorname{encodeSubtype}$ applied to $x_{1}$ is a natural number.
Encodable.encodeSumdefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x_{4}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then $\operatorname{encodeSum}$ applied to $x_{4}$ is a natural number.
Encodable.equivRangeEncodedefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{equivRangeEncode}$ applied to $x$ is an equivalence from $x$ to the set of elements of the range of $\operatorname{encode}$.
Quotient.repdefMathlib.Logic.Encodable.Basic, function or constantWording
the representation of q (from the name)
English
Let $q$ be an element of $\mathrm{Quotient}$ applied to $s$. Then the representation of $q$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Quotient\_\_exists\_rep}$ applied to $q$.
ULowerdefMathlib.Logic.Encodable.Basic, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{ULower}$ applied to $x$ is an element of the function that maps $x$ to the set of elements of the range of $\operatorname{encode}$.
ULower.downdefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{down}$ applied to $a$ is an element of $\mathrm{ULower}$ applied to $x$ defined as $\operatorname{equiv}$ applied to $x$ and $a$.
ULower.equivdefMathlib.Logic.Encodable.Basic, function or constantWording
the equivalence between the encodable type of x (from the docstring)
English
Let $x$ be a set. Then the equivalence between the encodable type of $x$ is an element of $\EquivMACRoAE {x}{\mathrm{ULower} (x)}$ defined as $\operatorname{equivRangeEncode}$ applied to $x$.
ULower.updefMathlib.Logic.Encodable.Basic, function or constantEnglish
Let $a$ be an element of $\mathrm{ULower}$ applied to $x$. Then $\operatorname{up}$ applied to $a$ is an element of $x$ defined as $\operatorname{symm}$ applied to the equivalence between the encodable type of $x$ and $a$.
Encodable.fintypeArrowdefMathlib.Logic.Encodable.Pi, function or constantWording
the finite type arrow of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the finite type arrow of $x$ and $x_{1}$ is a truncation of the proposition that the set of functions from elements of $x$ to elements of $x_{1}$ is encodable defined as the map of the function that maps $f$ to $\operatorname{ofEquiv}$ applied to the set of functions from elements of $\mathrm{Fin}$ applied to the cardinality of $x$ to elements of $x_{1}$ and the arrow congruence of $f$ and the identity of $x_{1}$ and $\operatorname{truncEquivFin}$ applied to $x$.
Encodable.fintypePidefMathlib.Logic.Encodable.Pi, function or constantWording
the finite type product of x and x1 (from the name)
English
Let $x$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Then the finite type product of $x$ and $x_{1}$ is a truncation of the proposition that the set of functions from elements $a$ of $x$ to elements of $x_{1}$ applied to $a$ is encodable defined as $\operatorname{bind}$ applied to $\operatorname{truncEncodable}$ applied to $x$ and the function that maps $a$ to $\operatorname{bind}$ applied to the finite type arrow of $x$ and $\Sigma$ applied to the function that maps $a_{1}$ to $x_{1}$ applied to $a_{1}$ and the function that maps $f$ to $\operatorname{mk}$ applied to $\operatorname{ofEquiv}$ applied to $\SubtypeSet {a_{2}}{\mathrm{forall} (x , \lambda i . \EqtMACRoH {\operatorname{fst} (a_{2} (i))}{i})}$ and the product equivalence subtype sigma of $x$ and $x_{1}$.
Equiv.arrayEquivListdefMathlib.Logic.Equiv.Array, function or constantWording
the array equivalence list of x (from the name)
English
Let $x$ be a set. Then the array equivalence list of $x$ is an equivalence from $\mathrm{Array}$ applied to $x$ to the set of lists of elements of $x$.
Equiv.Perm.extendDomaindefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $e$ be a permutation of $x$. Let $f$ be an equivalence from $x$ to $\SubtypeSet {x_{3}}{p (x_{3})}$. Then $\operatorname{extendDomain}$ applied to $e$ and $f$ is a permutation of $x_{1}$ defined as the subtype congruence of $\operatorname{permCongr}$ applied to $f$ and $e$ and the identity of $\SubtypeSet {a}{\mathrm{not} (p (a))}$.
Equiv.Perm.subtypeCongrdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype congruence of ep and en (from the name)
English
Let $\mathrm{ep}$ be a permutation of $\SubtypeSet {a_{1}}{p (a_{1})}$. Let $\mathrm{en}$ be a permutation of $\SubtypeSet {a}{\mathrm{not} (p (a))}$. Then the subtype congruence of $\mathrm{ep}$ and $\mathrm{en}$ is a permutation of $x$ defined as $\operatorname{permCongr}$ applied to the sum complement of $p$ and the sum congruence of $\mathrm{ep}$ and $\mathrm{en}$.
Equiv.intEquivNatSumNatdefMathlib.Logic.Equiv.Basic, function or constantWording
the integer equivalence natural sum natural number (from the name)
English
The integer equivalence natural sum natural number is an element of $\EquivMACRoAE {\Integer}{\mathrm{Sum} (\Natural , \Natural)}$.
Equiv.natEquivNatSumPUnitdefMathlib.Logic.Equiv.Basic, function or constantWording
the natural equivalence natural sum unit (from the name)
English
The natural equivalence natural sum unit is an element of $\EquivMACRoAE {\Natural}{\mathrm{Sum} (\Natural , \mathrm{PUnit})}$.
Equiv.natSumPUnitEquivNatdefMathlib.Logic.Equiv.Basic, function or constantWording
the natural sum unit equivalence natural number (from the name)
English
The natural sum unit equivalence natural number is an element of $\EquivMACRoAE {\mathrm{Sum} (\Natural , \mathrm{PUnit})}{\Natural}$ defined as the inverse of the natural equivalence natural sum unit.
Equiv.ofFiberEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the equivalence of e (from the name)
English
Let $e$ be a function from elements $c$ of $x_{2}$ to equivalences from $\SubtypeSet {a}{(\EqtMACRoH {f (a)}{c})}$ to $\SubtypeSet {b}{(\EqtMACRoH {g (b)}{c})}$. Then the equivalence of $c$ is an equivalence from $x$ to $x_{1}$ defined as the function that maps $e$ to the composition of the inverse of the sigma fiber equivalence of $f$ and the composition of the right sigma congruence of $c$ and the sigma fiber equivalence of $g$.
Equiv.piCommdefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $x_{2}$ be a function from elements of $x$ and elements of $x_{1}$ to sets. Then $\operatorname{piComm}$ applied to $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Elem} (x_{1})\rightarrow x_{2} (a , b))}{(\mathrm{Elem} (x_{1})\rightarrow \mathrm{Elem} (x)\rightarrow x_{2} (a_{1} , b_{1}))}$.
Equiv.piCongrdefMathlib.Logic.Equiv.Basic, function or constantWording
the product congruence of x2 and x3 (from the name)
English
Let $x_{2}$ be an equivalence from $x$ to $x_{1}$. Let $x_{3}$ be a function from elements $a_{1}$ of $x$ to elements of $\EquivMACRoAE {W (a_{1})}{Z (x_{2} (a_{1}))}$. Then the product congruence of $x_{2}$ and $a_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow W (a))}{(\mathrm{Elem} (x_{1})\rightarrow Z (b))}$ defined as the function that maps $x_{3}$ to the composition of the right product congruence of $a_{1}$ and the left product congruence of $Z$ and $x_{2}$.
Equiv.piCongr'defMathlib.Logic.Equiv.Basic, function or constantWording
the product congruence of x2 and x3 (from the name)
English
Let $x_{2}$ be an equivalence from $x$ to $x_{1}$. Let $x_{3}$ be a function from elements $b_{1}$ of $x_{1}$ to elements of $\EquivMACRoAE {W (\operatorname{symm} (x_{2} , b_{1}))}{Z (b_{1})}$. Then the product congruence of $x_{2}$ and $b_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow W (a))}{(\mathrm{Elem} (x_{1})\rightarrow Z (b))}$ defined as the function that maps $x_{3}$ to the inverse of the product congruence of the inverse of $x_{2}$ and the function that maps $b$ to the inverse of $b_{1}$ applied to $b$.
Equiv.piCongrFiberwisedefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $e$ be a function from elements $b_{1}$ of $x_{1}$ to elements of $\EquivMACRoAE {(\mathrm{Elem} (\SubtypeSet {a_{1}}{(\EqtMACRoH {f (a_{1})}{b_{1}})})\rightarrow x_{2} (x_{4}))}{x_{3} (b_{1})}$. Then $\operatorname{piCongrFiberwise}$ applied to $b_{1}$ and $e$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{2} (a))}{(\mathrm{Elem} (x_{1})\rightarrow x_{3} (b))}$ defined as the function that maps $e$ to the composition of the composition of the inverse of the product congruence sigma fiber of the function that maps $x_{4}$ to the identity of $x_{2}$ applied to $x_{4}$ and the product curry of the function that maps $b$ and $x_{5}$ to $x_{2}$ applied to $x_{5}$ and the right product congruence of $b_{1}$.
Equiv.piCongrLeftdefMathlib.Logic.Equiv.Basic, function or constantWording
the left product congruence of P and e (from the name)
English
Let $P$ be a function from elements of $x_{1}$ to sets. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $P$ and $e$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow P (e (a)))}{(\mathrm{Elem} (x_{1})\rightarrow P (b))}$ defined as the inverse of the left product congruence of $P$ and the inverse of $e$.
Equiv.piCongrLeft'defMathlib.Logic.Equiv.Basic, function or constantWording
the left product congruence of P and e (from the name)
English
Let $P$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $P$ and $e$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow P (a))}{(\mathrm{Elem} (x_{1})\rightarrow P (\operatorname{symm} (e , b)))}$.
Equiv.piCongrRightdefMathlib.Logic.Equiv.Basic, function or constantWording
the right product congruence of F (from the name)
English
Let $F$ be a function from elements $a_{2}$ of $x$ to elements of $\EquivMACRoAE {x_{1} (a_{2})}{x_{2} (a_{2})}$. Then the right product congruence of $a_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1} (a))}{(\mathrm{Elem} (x)\rightarrow x_{2} (a_{1}))}$.
Equiv.piCongrSetdefMathlib.Logic.Equiv.Basic, function or constantWording
the product congruence set of h (from the name)
English
Assume that $\EqtMACRoH {s}{t}$. Then the product congruence set of $h$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\SubtypeSet {i_{1}}{(\MembershipmemMACRoT {s}{i_{1}})})\rightarrow W (i))}{(\mathrm{Elem} (\SubtypeSet {i_{3}}{(\MembershipmemMACRoT {t}{i_{3}})})\rightarrow W (i_{2}))}$.
Equiv.piCongrSigmaFiberdefMathlib.Logic.Equiv.Basic, function or constantWording
the product congruence sigma fiber of e (from the name)
English
Let $e$ be a function from elements $a_{1}$ of $x$ to elements of $\EquivMACRoAE {x_{2} (a_{1})}{x_{3} (a_{1})}$. Then the product congruence sigma fiber of $a_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\Sigma (\lambda y . \SubtypeSet {x_{5}}{(\EqtMACRoH {f (x_{5})}{y})}))\rightarrow x_{2} (\operatorname{snd} (x_{4})))}{(\mathrm{Elem} (x)\rightarrow x_{3} (a))}$ defined as the function that maps $e$ to the composition of the left product congruence of $x_{2}$ and the sigma fiber equivalence of $f$ and the right product congruence of $a_{1}$.
Equiv.piCurrydefMathlib.Logic.Equiv.Basic, function or constantWording
the product curry of x2 (from the name)
English
Let $x_{2}$ be a function from elements $a_{1}$ of $x$ and elements of $x_{1}$ applied to $a_{1}$ to sets. Then the product curry of $a_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\Sigma (\lambda i . x_{1} (i)))\rightarrow x_{2} (\operatorname{fst} (x_{3}), \operatorname{snd} (x_{3})))}{(\mathrm{Elem} (x)\rightarrow \mathrm{Elem} (x_{1} (a))\rightarrow x_{2} (a , b))}$.
Equiv.piEquivSubtypeSigmadefMathlib.Logic.Equiv.Basic, function or constantWording
the product equivalence subtype sigma of x and x1 (from the name)
English
Let $x$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Then the product equivalence subtype sigma of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1} (i))}{(\SubtypeSet {f}{\mathrm{forall} (x , \lambda i_{1} . \EqtMACRoH {\operatorname{fst} (f (i_{1}))}{i_{1}})})}$.
Equiv.piOptionEquivProddefMathlib.Logic.Equiv.Basic, function or constantWording
the product option equivalence product (from the name)
English
The product option equivalence product is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Option} (x))\rightarrow x_{1} (a))}{\mathrm{Prod} (x_{1} (\operatorname{none}), \mathrm{Elem} (x)\rightarrow x_{1} (\operatorname{some} (a_{1})))}$.
Equiv.punitOfNonemptyOfSubsingletondefMathlib.Logic.Equiv.Basic, function or constantEnglish
$\operatorname{punitOfNonemptyOfSubsingleton}$ is an equivalence from $x$ to $\mathrm{PUnit}$ defined as the equivalence of the function that maps $x_{1}$ to $\operatorname{unit}$ and the function that maps $x_{2}$ to $\operatorname{some}$ applied to $h$.
Equiv.setValuedefMathlib.Logic.Equiv.Basic, function or constantWording
the set value of a and b (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the set value of $a$ and $b$ is an equivalence from $x$ to $x_{1}$ defined as the composition of the swap of $a$ and $\operatorname{symm}$ applied to $f$ and $b$ and $f$.
Equiv.sigmaAssocProddefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma associator product (from the name)
English
The sigma associator product is an element of $\EquivMACRoAE {\Sigma (\lambda \mathrm{ab} . x_{2} (\ProdfstMACRoZ {\mathrm{ab}}, \ProdsndMACRoAA {\mathrm{ab}}))}{\Sigma (\lambda a . \Sigma (\lambda b . x_{2} (a , b)))}$ defined as the composition of the left sigma congruence of the inverse of the sigma equivalence product of $x$ and $x_{1}$ and the sigma associator of $x_{2}$.
Equiv.sigmaNatSuccdefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma natural successor of f (from the name)
English
Let $f$ be a function from natural numbers to sets. Then the sigma natural successor of $f$ is an element of $\EquivMACRoAE {\Sigma (\lambda n . f (n))}{\mathrm{Sum} (f (0), \Sigma (\lambda n_{1} . f (n_{1} + 1)))}$.
Equiv.sigmaOptionEquivOfSomedefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma option equivalence of p and h (from the name)
English
Let $p$ be a function from elements of $\mathrm{Option}$ applied to $x$ to sets such that for all elements $x_{3}$ of $p$ applied to $\operatorname{none}$, we have a contradiction. Then the sigma option equivalence of $p$ and $h$ is an element of $\EquivMACRoAE {\Sigma (\lambda x_{1} . p (x_{1}))}{\Sigma (\lambda x_{2} . p (\operatorname{some} (x_{2})))}$.
Equiv.sigmaSigmaSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma sigma subtype of p and h (from the name)
English
Let $p$ be a function from elements of $\Sigma$ applied to the function that maps $a_{1}$ to $x_{1}$ applied to $a_{1}$ to propositions such that $p$ holds for $\operatorname{mk}$ applied to $a$ and $b$. Then the sigma sigma subtype of $p$ and $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {s}{p (\operatorname{mk} (\operatorname{fst} (s), \operatorname{fst} (\operatorname{snd} (s))))})}{x_{2} (a , b)}$.
Equiv.sigmaSigmaSubtypeEqdefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{sigmaSigmaSubtypeEq}$ applied to $a$ and $b$ is an element of $\EquivMACRoAE {(\SubtypeSet {s}{\mathrm{and} (\EqtMACRoH {\operatorname{fst} (s)}{a}, \EqtMACRoH {\operatorname{fst} (\operatorname{snd} (s))}{b})})}{x_{2} (a , b)}$.
Equiv.sigmaSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma subtype of a (from the name)
English
Let $a$ be an element of $x$. Then the sigma subtype of $a$ is an element of $\EquivMACRoAE {(\SubtypeSet {s}{(\EqtMACRoH {\operatorname{fst} (s)}{a})})}{x_{1} (a)}$.
Equiv.sigmaSubtypeEquivOfSubsetdefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma subtype equivalence of p and q (from the name)
English
Let $p$ be a function from elements of $x$ to sets. Let $q$ be a function from elements of $x$ to propositions such that for all elements $x_{3}$ of $x$, for all elements $x_{4}$ of $p$ applied to $x_{3}$, $q$ holds for $x_{3}$. Then the sigma subtype equivalence of $p$ and $q$ is an element of $\EquivMACRoAE {\Sigma (\lambda x_{1} . p (x_{1}))}{\Sigma (\lambda x_{2} . p (x_{2}))}$.
Equiv.sigmaSubtypeFiberEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma subtype fiber equivalence of f and p (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a function from elements of $x_{1}$ to propositions such that for all elements $x_{3}$ of $x$, $p$ holds for $f$ applied to $x_{3}$. Then the sigma subtype fiber equivalence of $f$ and $p$ is an element of $\EquivMACRoAE {\Sigma (\lambda y . \SubtypeSet {x_{2}}{(\EqtMACRoH {f (x_{2})}{y})})}{x}$.
Equiv.sigmaSubtypeFiberEquivSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the sigma subtype fiber equivalence subtype of f and h (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $x_{4}$ of $x$, $p$ holds for $x_{4}$, if and only if $q$ holds for $f$ applied to $x_{4}$. Then the sigma subtype fiber equivalence subtype of $f$ and $h$ is an element of $\EquivMACRoAE {\Sigma (\lambda y . \SubtypeSet {x_{2}}{(\EqtMACRoH {f (x_{2})}{y})})}{(\SubtypeSet {x_{3}}{p (x_{3})})}$.
Equiv.subtypeCongrdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype congruence of e and f (from the name)
English
Let $e$ be an equivalence from $\SubtypeSet {x_{5}}{p (x_{5})}$ to $\SubtypeSet {x_{6}}{q (x_{6})}$. Let $f$ be an equivalence from $\SubtypeSet {x_{3}}{\mathrm{not} (p (x_{3}))}$ to $\SubtypeSet {x_{4}}{\mathrm{not} (q (x_{4}))}$. Then the subtype congruence of $e$ and $f$ is a permutation of $x$ defined as the composition of the inverse of the sum complement of $p$ and the composition of the sum congruence of $e$ and $f$ and the sum complement of $q$.
Equiv.subtypeEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype equivalence of e and h (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$ such that for all elements $a_{1}$ of $x$, $p$ holds for $a_{1}$, if and only if $q$ holds for $e$ applied to $a_{1}$. Then the subtype equivalence of $e$ and $h$ is an equivalence from $\SubtypeSet {a}{p (a)}$ to $\SubtypeSet {b}{q (b)}$.
Equiv.subtypeEquivCodomaindefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype equivalence codomain of f (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {\mathrm{x'2}}{\mathrm{Neq} (\mathrm{x'2} , x_{1})}$ to elements of $Y$. Then the subtype equivalence codomain of $f$ is an equivalence from $\SubtypeSet {g}{(\EqtMACRoH {\operatorname{comp} (g , \lambda \mathrm{x'1} . \mathrm{Neq} (\mathrm{x'1} , x_{1}))}{f})}$ to $Y$ defined as the composition of the subtype preimage of the function that maps $a$ to $\mathrm{Neq} (a , x_{1})$ and $f$ and $\operatorname{funUnique}$ applied to $\SubtypeSet {\mathrm{x'}}{\mathrm{not} (\mathrm{Neq} (\mathrm{x'} , x_{1}))}$ and $Y$.
Equiv.subtypeEquivOfSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the subtype equivalence of $e$ is an equivalence from $\SubtypeSet {a}{p (e (a))}$ to $\SubtypeSet {b}{p (b)}$.
Equiv.subtypeEquivOfSubtype'defMathlib.Logic.Equiv.Basic, function or constantWording
the subtype equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the subtype equivalence of $e$ is an equivalence from $\SubtypeSet {a}{p (a)}$ to $\SubtypeSet {b}{p (\operatorname{symm} (e , b))}$ defined as the inverse of the subtype equivalence of the inverse of $e$.
Equiv.subtypeEquivPropdefMathlib.Logic.Equiv.Basic, function or constantEnglish
Assume that $\EqtMACRoH {p}{q}$. Then $\operatorname{subtypeEquivProp}$ applied to $h$ is an equivalence from $\SubtypeSet {x_{1}}{p (x_{1})}$ to $\SubtypeSet {x_{2}}{q (x_{2})}$.
Equiv.subtypeEquivRightdefMathlib.Logic.Equiv.Basic, function or constantWording
the right subtype equivalence of e (from the name)
English
Assume that for all elements $x_{3}$ of $x$, $p$ holds for $x_{3}$, if and only if $q$ holds for $x_{3}$. Then the right subtype equivalence of $e$ is an equivalence from $\SubtypeSet {x_{1}}{p (x_{1})}$ to $\SubtypeSet {x_{2}}{q (x_{2})}$ defined as the subtype equivalence of the identity of $x$ and $e$.
Equiv.subtypePiEquivPidefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype product equivalence product (from the name)
English
The subtype product equivalence product is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . p (a , f (a)))})}{(\mathrm{Elem} (x)\rightarrow \SubtypeSet {b}{p (a_{1} , b)})}$.
Equiv.subtypePreimagedefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype preimage of p and x3 (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Let $x_{3}$ be a function from elements of $\SubtypeSet {a_{3}}{p (a_{3})}$ to elements of $x_{1}$. Then the subtype preimage of $p$ and $x_{3}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{4}}{(\EqtMACRoH {\operatorname{comp} (x_{4} , \lambda a_{1} . p (a_{1}))}{x_{3}})})}{(\mathrm{Elem} (\SubtypeSet {a_{2}}{\mathrm{not} (p (a_{2}))})\rightarrow x_{1})}$.
Equiv.subtypeQuotientEquivQuotientSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype quotient equivalence quotient subtype of x1 and x4 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to propositions. Let $x_{4}$ be a function from elements of $\mathrm{Quotient}$ applied to $x_{2}$ to propositions such that for all elements $a$ of $x$, $x_{1}$ holds for $a$, if and only if $x_{4}$ holds for $\operatorname{mk}$ applied to $x_{2}$ and $a$. Assume that for all elements $x_{6}$ of $\SubtypeSet {x_{8}}{x_{1} (x_{8})}$, for all elements $y$ of $\SubtypeSet {x_{7}}{x_{1} (x_{7})}$, $\operatorname{r}$ holds for $x_{6}$ and $y$, if and only if $\operatorname{r}$ holds for $x_{6}$ and $y$. Then the subtype quotient equivalence quotient subtype of $x_{1}$ and $x_{4}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{5}}{x_{4} (x_{5})})}{\mathrm{Quotient} (x_{3})}$.
Equiv.subtypeSigmaEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype sigma equivalence of p and q (from the name)
English
Let $p$ be a function from elements of $x$ to sets. Let $q$ be a function from elements of $x$ to propositions. Then the subtype sigma equivalence of $p$ and $q$ is an element of $\EquivMACRoAE {(\SubtypeSet {y}{q (\operatorname{fst} (y))})}{\Sigma (\lambda x_{1} . p (x_{1}))}$.
Equiv.subtypeSubtypeEquivSubtypedefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype subtype equivalence subtype of h (from the name)
English
Assume that for all elements $x_{3}$ of $x$, if $q$ holds for $x_{3}$, then $p$ holds for $x_{3}$. Then the subtype subtype equivalence subtype of $h$ is an equivalence from $\SubtypeSet {x_{1}}{q (x_{1})}$ to $\SubtypeSet {x_{2}}{q (x_{2})}$.
Equiv.subtypeSubtypeEquivSubtypeExistsdefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $q$ be a function from elements of $\SubtypeSet {x_{3}}{p (x_{3})}$ to propositions. Then $\operatorname{subtypeSubtypeEquivSubtypeExists}$ applied to $p$ and $q$ is an equivalence from $\SubtypeSet {x_{1}}{q (x_{1})}$ to $\SubtypeSet {a}{\mathrm{exists} (p (a), \lambda h . q (a))}$.
Equiv.subtypeSubtypeEquivSubtypeInterdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype subtype equivalence subtype intersection of p and q (from the name)
English
Let $p$ and $q$ be functions from elements of $x$ to propositions. Then the subtype subtype equivalence subtype intersection of $p$ and $q$ is an equivalence from $\SubtypeSet {x_{1}}{q (x_{1})}$ to $\SubtypeSet {x_{2}}{\mathrm{and} (p (x_{2}), q (x_{2}))}$.
Equiv.subtypeUnivEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the subtype universal set equivalence of h (from the name)
English
Assume that for all elements $x_{2}$ of $x$, $p$ holds for $x_{2}$. Then the subtype universal set equivalence of $h$ is an equivalence from $\SubtypeSet {x_{1}}{p (x_{1})}$ to $x$.
Equiv.swapdefMathlib.Logic.Equiv.Basic, function or constantWording
the swap of a and b (from the name)
English
Let $a$ and $b$ be elements of $x$. Then the swap of $a$ and $b$ is a permutation of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{swapCore}$ applied to $b$, $\operatorname{swapCore}$ applied to $b$, the function that maps $r$ to $\mathrm{Equiv\_\_swapCore\_swapCore}$ applied to $r$, $a$ and $b$ and the function that maps $r_{1}$ to $\mathrm{Equiv\_\_swapCore\_swapCore}$ applied to $r_{1}$, $a$ and $b$.
Equiv.swapCoredefMathlib.Logic.Equiv.Basic, function or constantWording
the swap of b and r (from the name)
English
Let $a$, $b$ and $r$ be elements of $x$. Then the swap of $b$ and $r$ is an element of $x$ defined as $\iteMACRoG {(\EqtMACRoH {r}{a})}{b}{(\iteMACRoG {(\EqtMACRoH {r}{b})}{a}{r})}$.
Equiv.uniqueCongrdefMathlib.Logic.Equiv.Basic, function or constantWording
the unique congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the unique congruence of $e$ is an equivalence from the proposition that $x$ is unique to the proposition that $x_{1}$ is unique.
Function.Involutive.toPermdefMathlib.Logic.Equiv.Basic, function or constantWording
the permutation of f and h (from the name)
English
Let $f$ be an involutive function from elements of $x$ to elements of $x$. Then the permutation of $f$ and $h$ is a permutation of $x$ defined as $\operatorname{mk}$ applied to $f$, $f$, $\operatorname{leftInverse}$ applied to $h$ and $\operatorname{rightInverse}$ applied to $h$.
equivOfSubsingletonOfSubsingletondefMathlib.Logic.Equiv.Basic, function or constantWording
the equivalence of f and g (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then the equivalence of $f$ and $g$ is an equivalence from $x$ to $x_{1}$.
uniqueEquivEquivUniquedefMathlib.Logic.Equiv.Basic, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\mathrm{uniqueEquivEquivUnique}$ applied to $x$ and $x_{1}$ is an equivalence from the proposition that $x$ is unique to $\EquivMACRoAE {x}{x_{1}}$ defined as the equivalence of the function that maps $x_{3}$ to the equivalence of $x$ and $x_{1}$ and $\operatorname{unique}$.
uniqueUniqueEquivdefMathlib.Logic.Equiv.Basic, function or constantWording
the unique unique equivalence (from the name)
English
The unique unique equivalence is an equivalence from the proposition that the proposition that $x$ is unique is unique to the proposition that $x$ is unique.
Equiv.boolNotdefMathlib.Logic.Equiv.Bool, function or constantWording
the boolean negation function (from the docstring)
English
The boolean negation function is a permutation of $\mathrm{Bool}$ defined as the permutation of $\operatorname{not}$ and $\mathrm{Bool\_\_involutive\_not}$.
EquivstructureMathlib.Logic.Equiv.Defs, typeWording
equivalence from x to x1 (by hand)
English
Let $x$ and $x_{1}$ be sets. Then $\EquivMACRoAE {x}{x_{1}}$ is a set.
Equiv.PermdefMathlib.Logic.Equiv.Defs, typeWording
permutation of x (from the name)
English
Let $x$ be a set. Then a permutation of $x$ is an element of the function that maps $x$ to $\EquivMACRoAE {x}{x}$.
Equiv.Perm.sigmaCongrRightdefMathlib.Logic.Equiv.Defs, function or constantWording
the right sigma congruence of F (from the name)
English
Let $F$ be a function from elements $a_{1}$ of $x$ to permutations of $x_{1}$ applied to $a_{1}$. Then the right sigma congruence of $a_{1}$ is a permutation of $\Sigma$ applied to the function that maps $a$ to $x_{1}$ applied to $a$ defined as the function that maps $F$ to the right sigma congruence of $a_{1}$.
Equiv.arrowCongrdefMathlib.Logic.Equiv.Defs, function or constantWording
the arrow congruence of x4 and x5 (from the name)
English
Let $x_{4}$ be an equivalence from $x$ to $x_{2}$. Let $x_{5}$ be an equivalence from $x_{1}$ to $x_{3}$. Then the arrow congruence of $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1})}{(\mathrm{Elem} (x_{2})\rightarrow x_{3})}$.
Equiv.arrowCongr'defMathlib.Logic.Equiv.Defs, function or constantWording
the arrow congruence of x4 and x5 (from the name)
English
Let $x_{4}$ be an equivalence from $x$ to $x_{2}$. Let $x_{5}$ be an equivalence from $x_{1}$ to $x_{3}$. Then the arrow congruence of $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1})}{(\mathrm{Elem} (x_{2})\rightarrow x_{3})}$ defined as the arrow congruence of $x_{4}$ and $x_{5}$.
Equiv.arrowPUnitEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantWording
the arrow unit equivalence unit of x (from the name)
English
Let $x$ be a set. Then the arrow unit equivalence unit of $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{PUnit})}{\mathrm{PUnit}}$.
Equiv.arrowPUnitOfIsEmptydefMathlib.Logic.Equiv.Defs, function or constantWording
the arrow unit of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the arrow unit of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1})}{\mathrm{PUnit}}$.
Equiv.bijectiveEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the bijective equivalence (from the name)
English
The bijective equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{Bijective} (f)})}{(\EquivMACRoAE {x}{x_{1}})}$.
Equiv.castdefMathlib.Logic.Equiv.Defs, function or constantWording
the cast of h (from the name)
English
Assume that $\EqtMACRoH {x}{x_{1}}$. Then the cast of $h$ is an equivalence from $x$ to $x_{1}$.
Equiv.conjdefMathlib.Logic.Equiv.Defs, function or constantWording
the conjugate of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the conjugate of $e$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x)}{(\mathrm{Elem} (x_{1})\rightarrow x_{1})}$ defined as the arrow congruence of $e$ and $e$.
Equiv.emptyArrowEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantWording
the empty arrow equivalence unit of x (from the name)
English
Let $x$ be a set. Then the empty arrow equivalence unit of $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Empty})\rightarrow x)}{\mathrm{PUnit}}$ defined as the arrow unit of $\mathrm{Empty}$ and $x$.
Equiv.equivCongrdefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence congruence of ab and cd (from the name)
English
Let $\mathrm{ab}$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{cd}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the equivalence congruence of $\mathrm{ab}$ and $\mathrm{cd}$ is an equivalence from $\EquivMACRoAE {x}{x_{2}}$ to $\EquivMACRoAE {x_{1}}{x_{3}}$.
Equiv.equivEmptydefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x$ be a set. Then $\operatorname{equivEmpty}$ applied to $x$ is an equivalence from $x$ to $\mathrm{Empty}$ defined as the equivalence of $x$ and $\mathrm{Empty}$.
Equiv.equivEmptyEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence empty equivalence of x (from the name)
English
Let $x$ be a set. Then the equivalence empty equivalence of $x$ is an equivalence from $\EquivMACRoAE {x}{\mathrm{Empty}}$ to the proposition that $x$ is empty.
Equiv.equivOfIsEmptydefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalence of $x$ and $x_{1}$ is an equivalence from $x$ to $x_{1}$.
Equiv.equivPEmptydefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x$ be a set. Then $\operatorname{equivPEmpty}$ applied to $x$ is an equivalence from $x$ to $\mathrm{PEmpty}$ defined as the equivalence of $x$ and $\mathrm{PEmpty}$.
Equiv.equivPUnitdefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence unit of x (from the name)
English
Let $x$ be a set. Then the equivalence unit of $x$ is an equivalence from $x$ to $\mathrm{PUnit}$ defined as the equivalence of $x$ and $\mathrm{PUnit}$.
Equiv.falseArrowEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantWording
the false arrow equivalence unit of x (from the name)
English
Let $x$ be a set. Then the false arrow equivalence unit of $x$ is an element of $\EquivMACRoAE {(\mathrm{Proof} (\mathrm{false})\rightarrow x)}{\mathrm{PUnit}}$ defined as the arrow unit of the proposition that we have a contradiction and $x$.
Equiv.funUniquedefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1})}{x_{1}}$ defined as $\operatorname{piUnique}$ applied to the function that maps $x_{3}$ to $x_{1}$.
Equiv.functionSwapdefMathlib.Logic.Equiv.Defs, function or constantWording
the function swap of x2 (from the name)
English
Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be a function from elements of $x$ and elements of $x_{1}$ to sets. Then the function swap of $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Elem} (x_{1})\rightarrow x_{2} (a , b))}{(\mathrm{Elem} (x_{1})\rightarrow \mathrm{Elem} (x)\rightarrow x_{2} (a_{1} , b_{1}))}$.
Equiv.invFundefMathlib.Logic.Equiv.Defs, function or constantWording
the inverse function of self and x2 (from the name)
English
Let $\mathrm{self}$ be an equivalence from $x$ to $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the inverse function of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
Equiv.ofBijectivedefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence of f and hf (from the name)
English
Let $f$ be a bijective function from elements of $x$ to elements of $x_{1}$. Then the equivalence of $f$ and $\mathrm{hf}$ is an equivalence from $x$ to $x_{1}$.
Equiv.ofIffdefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence of h (from the name)
English
Assume that $P$, if and only if $Q$. Then the equivalence of $h$ is an equivalence from $P$ to $Q$.
Equiv.ofUniquedefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalence of $x$ and $x_{1}$ is an equivalence from $x$ to $x_{1}$.
Equiv.pSigmaAssocdefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma associator of x2 (from the name)
English
Let $x_{2}$ be a function from elements $a_{1}$ of $x$ and elements of $x_{1}$ applied to $a_{1}$ to sets. Then the sigma associator of $a_{1}$ is an element of $\EquivMACRoAE {\mathrm{PSigma} (\lambda \mathrm{ab} . x_{2} (\operatorname{fst} (\mathrm{ab}), \operatorname{snd} (\mathrm{ab})))}{\mathrm{PSigma} (\lambda a . \mathrm{PSigma} (\lambda b . x_{2} (a , b)))}$.
Equiv.pemptyArrowEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x$ be a set. Then $\operatorname{pemptyArrowEquivPUnit}$ applied to $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{PEmpty})\rightarrow x)}{\mathrm{PUnit}}$ defined as the arrow unit of $\mathrm{PEmpty}$ and $x$.
Equiv.permCongrdefMathlib.Logic.Equiv.Defs, function or constantWording
the permutation congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the permutation congruence of $e$ is an equivalence from the set of permutations of $x$ to the set of permutations of $x_{1}$ defined as the equivalence congruence of $e$ and $e$.
Equiv.piUniquedefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x_{2}$ be a function from elements of $x$ to sets. Then $\operatorname{piUnique}$ applied to $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{2} (i))}{x_{2} (\operatorname{default})}$.
Equiv.pliftdefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\operatorname{plift}$ is an element of $\EquivMACRoAE {\mathrm{PLift} (x)}{x}$ defined as $\operatorname{mk}$ applied to $\operatorname{down}$, $\operatorname{up}$, $\mathrm{PLift\_\_up\_down}$ and $\mathrm{PLift\_\_down\_up}$.
Equiv.propEquivBooldefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\operatorname{propEquivBool}$ is an equivalence from the set of propositions to $\mathrm{Bool}$.
Equiv.propEquivPEmptydefMathlib.Logic.Equiv.Defs, function or constantEnglish
Assume that it is not the case that $p$. Then $\operatorname{propEquivPEmpty}$ applied to $h$ is an equivalence from $p$ to $\mathrm{PEmpty}$ defined as $\operatorname{equivPEmpty}$ applied to $p$.
Equiv.propEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantEnglish
Assume that $p$. Then $\operatorname{propEquivPUnit}$ applied to $h$ is an equivalence from $p$ to $\mathrm{PUnit}$ defined as the equivalence unit of $p$.
Equiv.psigmaCongrRightdefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $F$ be a function from elements $a_{2}$ of $x$ to elements of $\EquivMACRoAE {x_{1} (a_{2})}{x_{2} (a_{2})}$. Then $\operatorname{psigmaCongrRight}$ applied to $a_{2}$ and $F$ is an element of $\EquivMACRoAE {\mathrm{PSigma} (\lambda a . x_{1} (a))}{\mathrm{PSigma} (\lambda a_{1} . x_{2} (a_{1}))}$.
Equiv.psigmaEquivSigmadefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x_{1}$ be a function from elements of $x$ to sets. Then $\operatorname{psigmaEquivSigma}$ applied to $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{PSigma} (\lambda i . x_{1} (i))}{\Sigma (\lambda i_{1} . x_{1} (i_{1}))}$.
Equiv.psigmaEquivSigmaPLiftdefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x_{1}$ be a function from elements of $x$ to sets. Then $\operatorname{psigmaEquivSigmaPLift}$ applied to $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{PSigma} (\lambda i . x_{1} (i))}{\Sigma (\lambda i_{1} . \mathrm{PLift} (x_{1} (\operatorname{down} (i_{1}))))}$.
Equiv.psigmaEquivSubtypedefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $P$ be a function from elements of $x$ to propositions. Then $\operatorname{psigmaEquivSubtype}$ applied to $P$ is an element of $\EquivMACRoAE {\mathrm{PSigma} (\lambda i . P (i))}{(\SubtypeSet {x_{1}}{P (x_{1})})}$.
Equiv.punitArrowEquivdefMathlib.Logic.Equiv.Defs, function or constantEnglish
Let $x$ be a set. Then $\operatorname{punitArrowEquiv}$ applied to $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{PUnit})\rightarrow x)}{x}$ defined as $\operatorname{funUnique}$ applied to $\mathrm{PUnit}$ and $x$.
Equiv.punitEquivPUnitdefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\operatorname{punitEquivPUnit}$ is an equivalence from $\mathrm{PUnit}$ to $\mathrm{PUnit}$.
Equiv.refldefMathlib.Logic.Equiv.Defs, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an equivalence from $x$ to $x$.
Equiv.sigmaAssocdefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma associator of x2 (from the name)
English
Let $x_{2}$ be a function from elements $a_{1}$ of $x$ and elements of $x_{1}$ applied to $a_{1}$ to sets. Then the sigma associator of $a_{1}$ is an element of $\EquivMACRoAE {\Sigma (\lambda \mathrm{ab} . x_{2} (\operatorname{fst} (\mathrm{ab}), \operatorname{snd} (\mathrm{ab})))}{\Sigma (\lambda a . \Sigma (\lambda b . x_{2} (a , b)))}$.
Equiv.sigmaCongrdefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma congruence of f and F (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Let $F$ be a function from elements $a$ of $x$ to elements of $\EquivMACRoAE {x_{2} (a)}{x_{3} (f (a))}$. Then the sigma congruence of $f$ and $a$ is an element of $\EquivMACRoAE {\Sigma (x_{2})}{\Sigma (x_{3})}$ defined as the function that maps $F$ to the composition of the right sigma congruence of $a$ and the left sigma congruence of $f$.
Equiv.sigmaCongrLeftdefMathlib.Logic.Equiv.Defs, function or constantWording
the left sigma congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left sigma congruence of $e$ is an element of $\EquivMACRoAE {\Sigma (\lambda a . x_{2} (e (a)))}{\Sigma (\lambda a_{1} . x_{2} (a_{1}))}$.
Equiv.sigmaCongrLeft'defMathlib.Logic.Equiv.Defs, function or constantWording
the left sigma congruence of f (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Then the left sigma congruence of $f$ is an element of $\EquivMACRoAE {\Sigma (\lambda a . x_{2} (a))}{\Sigma (\lambda a_{1} . x_{2} (\operatorname{symm} (f , a_{1})))}$ defined as the inverse of the left sigma congruence of the inverse of $f$.
Equiv.sigmaCongrRightdefMathlib.Logic.Equiv.Defs, function or constantWording
the right sigma congruence of F (from the name)
English
Let $F$ be a function from elements $a_{2}$ of $x$ to elements of $\EquivMACRoAE {x_{1} (a_{2})}{x_{2} (a_{2})}$. Then the right sigma congruence of $a_{2}$ is an element of $\EquivMACRoAE {\Sigma (\lambda a . x_{1} (a))}{\Sigma (\lambda a_{1} . x_{2} (a_{1}))}$.
Equiv.sigmaEquivProddefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma equivalence product of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the sigma equivalence product of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\Sigma (\lambda x_{2} . x_{1})}{\mathrm{Prod} (x , x_{1})}$.
Equiv.sigmaEquivProdOfEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma equivalence product of F (from the name)
English
Let $F$ be a function from elements $a$ of $x$ to elements of $\EquivMACRoAE {x_{2} (a)}{x_{1}}$. Then the sigma equivalence product of $a$ is an element of $\EquivMACRoAE {\Sigma (x_{2})}{\mathrm{Prod} (x , x_{1})}$ defined as the function that maps $F$ to the composition of the right sigma congruence of $a$ and the sigma equivalence product of $x$ and $x_{1}$.
Equiv.sigmaPLiftEquivSubtypedefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma lift equivalence subtype of P (from the name)
English
Let $P$ be a function from elements of $x$ to propositions. Then the sigma lift equivalence subtype of $P$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . \mathrm{PLift} (P (i)))}{(\SubtypeSet {x_{1}}{P (x_{1})})}$ defined as the composition of the composition of the inverse of $\operatorname{psigmaEquivSigma}$ applied to the function that maps $x_{1}$ to $\mathrm{PLift}$ applied to $P$ applied to $x_{1}$ and $\operatorname{psigmaCongrRight}$ applied to the function that maps $x_{2}$ to $\operatorname{plift}$ and $\operatorname{psigmaEquivSubtype}$ applied to $P$.
Equiv.sigmaULiftPLiftEquivSubtypedefMathlib.Logic.Equiv.Defs, function or constantWording
the sigma lift lift equivalence subtype of P (from the name)
English
Let $P$ be a function from elements of $x$ to propositions. Then the sigma lift lift equivalence subtype of $P$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . \mathrm{ULift} (\mathrm{PLift} (P (i))))}{(\SubtypeSet {x_{1}}{P (x_{1})})}$ defined as the composition of the right sigma congruence of the function that maps $x_{1}$ to the lift and the sigma lift equivalence subtype of $P$.
Equiv.sumIsLeftdefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\operatorname{sumIsLeft}$ is an equivalence from $\SubtypeSet {x_{2}}{(\EqtMACRoH {\operatorname{isLeft} (x_{2})}{\operatorname{true}})}$ to $x$.
Equiv.sumIsRightdefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\operatorname{sumIsRight}$ is an equivalence from $\SubtypeSet {x_{2}}{(\EqtMACRoH {\operatorname{isRight} (x_{2})}{\operatorname{true}})}$ to $x_{1}$.
Equiv.symmdefMathlib.Logic.Equiv.Defs, function or constantWording
the inverse of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the inverse of $e$ is an equivalence from $x_{1}$ to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{invFun}$ applied to $e$, $\operatorname{toFun}$ applied to $e$, $\mathrm{Equiv\_\_right\_inv}$ applied to $e$ and $\mathrm{Equiv\_\_left\_inv}$ applied to $e$.
Equiv.symmEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the inverse equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the inverse equivalence of $x$ and $x_{1}$ is an equivalence from $\EquivMACRoAE {x}{x_{1}}$ to $\EquivMACRoAE {x_{1}}{x}$.
Equiv.toFundefMathlib.Logic.Equiv.Defs, function or constantWording
the forward map of self and x2 (from the docstring)
English
Let $\mathrm{self}$ be an equivalence from $x$ to $x_{1}$. Let $x_{2}$ be an element of $x$. Then the forward map of $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
Equiv.transdefMathlib.Logic.Equiv.Defs, function or constantWording
the composition of x3 and x4 (from the name)
English
Let $x_{3}$ be an equivalence from $x$ to $x_{1}$. Let $x_{4}$ be an equivalence from $x_{1}$ to $x_{2}$. Then the composition of $x_{3}$ and $x_{4}$ is an equivalence from $x$ to $x_{2}$.
Equiv.trueArrowEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the true arrow equivalence of x (from the name)
English
Let $x$ be a set. Then the true arrow equivalence of $x$ is an element of $\EquivMACRoAE {(\mathrm{Proof} (\mathrm{True})\rightarrow x)}{x}$ defined as $\operatorname{funUnique}$ applied to $\mathrm{True}$ and $x$.
Equiv.uliftdefMathlib.Logic.Equiv.Defs, function or constantWording
the lift (from the name)
English
The lift is an element of $\EquivMACRoAE {\mathrm{ULift} (x)}{x}$ defined as $\operatorname{mk}$ applied to $\operatorname{down}$, $\operatorname{up}$, $\mathrm{ULift\_\_up\_down}$ and $\mathrm{ULift\_\_down\_up}$.
EquivLike.toEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the equivalence of f (from the name)
English
Let $f$ be an element of $F$. Then the equivalence of $f$ is an equivalence from $x$ to $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$, $\operatorname{inv}$ applied to $f$, $\mathrm{EquivLike\_\_left\_inv}$ applied to $f$ and $\mathrm{EquivLike\_\_right\_inv}$ applied to $f$.
Quot.congrdefMathlib.Logic.Equiv.Defs, function or constantWording
the congruence of e and eq (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$ such that for all elements $x_{2}$ and $x_{3}$ of $x$, $\mathrm{ra}$ holds for $x_{2}$ and $x_{3}$, if and only if $\mathrm{rb}$ holds for $e$ applied to $x_{2}$ and $e$ applied to $x_{3}$. Then the congruence of $e$ and $\mathrm{eq}$ is an element of $\EquivMACRoAE {\mathrm{Quot} (\mathrm{ra})}{\mathrm{Quot} (\mathrm{rb})}$.
Quot.congrLeftdefMathlib.Logic.Equiv.Defs, function or constantWording
the left congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{Quot} (r)}{\mathrm{Quot} (\lambda b . \lambda \mathrm{b'} . r (\operatorname{symm} (e , b), \operatorname{symm} (e , \mathrm{b'})))}$.
Quot.congrRightdefMathlib.Logic.Equiv.Defs, function or constantWording
the right congruence of eq (from the name)
English
Assume that for all elements $x_{1}$ and $x_{2}$ of $x$, $r$ holds for $x_{1}$ and $x_{2}$, if and only if $\mathrm{r'}$ holds for $x_{1}$ and $x_{2}$. Then the right congruence of $\mathrm{eq}$ is an element of $\EquivMACRoAE {\mathrm{Quot} (r)}{\mathrm{Quot} (\mathrm{r'})}$ defined as the congruence of the identity of $x$ and $\mathrm{eq}$.
Quotient.congrdefMathlib.Logic.Equiv.Defs, function or constantWording
the congruence of e and eq (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$ such that for all elements $x_{2}$ and $x_{3}$ of $x$, $\operatorname{r}$ holds for $x_{2}$ and $x_{3}$, if and only if $\operatorname{r}$ holds for $e$ applied to $x_{2}$ and $e$ applied to $x_{3}$. Then the congruence of $e$ and $\mathrm{eq}$ is an element of $\EquivMACRoAE {\mathrm{Quotient} (\mathrm{ra})}{\mathrm{Quotient} (\mathrm{rb})}$ defined as the congruence of $e$ and $\mathrm{eq}$.
Quotient.congrRightdefMathlib.Logic.Equiv.Defs, function or constantWording
the right congruence of eq (from the name)
English
Assume that for all elements $x_{1}$ and $x_{2}$ of $x$, $\operatorname{r}$ holds for $x_{1}$ and $x_{2}$, if and only if $\operatorname{r}$ holds for $x_{1}$ and $x_{2}$. Then the right congruence of $\mathrm{eq}$ is an element of $\EquivMACRoAE {\mathrm{Quotient} (r)}{\mathrm{Quotient} (\mathrm{r'})}$ defined as the right congruence of $\mathrm{eq}$.
finOneEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the finite one equivalence (from the name)
English
The finite one equivalence is an element of $\EquivMACRoAE {\mathrm{Fin} (1)}{\mathrm{Unit}}$ defined as the equivalence unit of $\mathrm{Fin}$ applied to $1$.
finTwoEquivdefMathlib.Logic.Equiv.Defs, function or constantEnglish
$\mathrm{finTwoEquiv}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (2)}{\mathrm{Bool}}$.
finZeroEquivdefMathlib.Logic.Equiv.Defs, function or constantWording
the finite zero equivalence (from the name)
English
The finite zero equivalence is an element of $\EquivMACRoAE {\mathrm{Fin} (0)}{\mathrm{Empty}}$ defined as $\operatorname{equivEmpty}$ applied to $\mathrm{Fin}$ applied to $0$.
finZeroEquiv'defMathlib.Logic.Equiv.Defs, function or constantWording
the finite zero equivalence (from the name)
English
The finite zero equivalence is an element of $\EquivMACRoAE {\mathrm{Fin} (0)}{\mathrm{PEmpty}}$ defined as $\operatorname{equivPEmpty}$ applied to $\mathrm{Fin}$ applied to $0$.
Equiv.codRestrictdefMathlib.Logic.Equiv.Embedding, function or constantEnglish
Let $x$ be a set. Let $\mathrm{bs}$ be an element of $\wp x_{1}$. Then $\operatorname{codRestrict}$ applied to $x$ and $\mathrm{bs}$ is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . \MembershipmemMACRoT {\mathrm{bs}}{f (a)})}$ to the set of embeddings of $x$ and the set of elements of $\mathrm{bs}$.
Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricteddefMathlib.Logic.Equiv.Embedding, function or constantEnglish
$\operatorname{prodEmbeddingDisjointEquivSigmaEmbeddingRestricted}$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{Disjoint} (\operatorname{range} (\operatorname{coe} (\ProdfstMACRoZ {f})), \operatorname{range} (\operatorname{coe} (\ProdsndMACRoAA {f})))})}{\Sigma (\lambda f_{1} . \operatorname{Embedding} (x_{1} , \operatorname{Elem} (\operatorname{compl} (\operatorname{range} (\operatorname{coe} (f_{1}))))))}$.
Equiv.sumEmbeddingEquivProdEmbeddingDisjointdefMathlib.Logic.Equiv.Embedding, function or constantEnglish
$\operatorname{sumEmbeddingEquivProdEmbeddingDisjoint}$ is an element of $\EquivMACRoAE {\operatorname{Embedding} (\mathrm{Sum} (x , x_{1}), x_{2})}{(\SubtypeSet {f}{\mathrm{Disjoint} (\operatorname{range} (\operatorname{coe} (\ProdfstMACRoZ {f})), \operatorname{range} (\operatorname{coe} (\ProdsndMACRoAA {f})))})}$.
Equiv.sumEmbeddingEquivSigmaEmbeddingRestricteddefMathlib.Logic.Equiv.Embedding, function or constantEnglish
$\operatorname{sumEmbeddingEquivSigmaEmbeddingRestricted}$ is an equivalence from the set of embeddings of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $x_{2}$ to $\Sigma$ applied to the function that maps $f$ to the set of embeddings of $x_{1}$ and the set of elements of the complement of the range of $\operatorname{coe}$ applied to $f$ defined as the composition of $\operatorname{sumEmbeddingEquivProdEmbeddingDisjoint}$ and $\operatorname{prodEmbeddingDisjointEquivSigmaEmbeddingRestricted}$.
Equiv.uniqueEmbeddingEquivResultdefMathlib.Logic.Equiv.Embedding, function or constantWording
the unique embedding equivalence result (from the name)
English
The unique embedding equivalence result is an equivalence from the set of embeddings of $x$ and $x_{1}$ to $x_{1}$.
Equiv.embeddingFinSuccdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the embedding finite successor of n and x (from the name)
English
Let $n$ be an element of $\Natural$. Let $x$ be a set. Then the embedding finite successor of $n$ and $x$ is an element of $\EquivMACRoAE {\operatorname{Embedding} (\mathrm{Fin} (n + 1), x)}{\Sigma (\lambda e . \SubtypeSet {i}{\mathrm{not} (\MembershipmemMACRoT {\operatorname{range} (\operatorname{coe} (e))}{i})})}$ defined as the composition of the embedding congruence of the finite successor equivalence of $n$ and the identity of $x$ and the option embedding equivalence of $\mathrm{Fin}$ applied to $n$ and $x$.
Fin.appendEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
Let $m$ and $n$ be natural numbers. Then $\operatorname{appendEquiv}$ applied to $m$ and $n$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Elem} (\mathrm{Fin} (m))\rightarrow x , \mathrm{Elem} (\mathrm{Fin} (n))\rightarrow x)}{(\mathrm{Elem} (\mathrm{Fin} (m + n))\rightarrow x)}$.
Fin.castLEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the cast equivalence of h (from the name)
English
Assume that $n \leq m$. Then the cast equivalence of $h$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n)}{(\SubtypeSet {i}{\mathrm{Lt} (\operatorname{val} (i), n)})}$.
Fin.succFunEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the successor function equivalence of x and n (from the name)
English
Let $x$ be a set. Let $n$ be a natural number. Then the successor function equivalence of $x$ and $n$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Fin} (n + 1))\rightarrow x)}{\mathrm{Prod} (\mathrm{Elem} (\mathrm{Fin} (n))\rightarrow x , x)}$ defined as the composition of the inverse of $\operatorname{appendEquiv}$ applied to $n$ and $1$ and the right product congruence of the function that maps $x_{1}$ to $\operatorname{funUnique}$ applied to $\mathrm{Fin}$ applied to $1$ and $x$.
Int.divModEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{divModEquiv}$ applied to $n$ is an element of $\EquivMACRoAE {\Integer}{\mathrm{Prod} (\Integer , \mathrm{Fin} (n))}$.
Nat.divModEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{divModEquiv}$ applied to $n$ is an element of $\EquivMACRoAE {\Natural}{\mathrm{Prod} (\Natural , \mathrm{Fin} (n))}$.
finAddFlipdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite additive flip (from the name)
English
The finite additive flip is an element of $\EquivMACRoAE {\mathrm{Fin} (m + n)}{\mathrm{Fin} (n + m)}$ defined as the composition of the composition of the inverse of the finite sum finite equivalence and $\operatorname{sumComm}$ applied to $\mathrm{Fin}$ applied to $m$ and $\mathrm{Fin}$ applied to $n$ and the finite sum finite equivalence.
finProdFinEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite product finite equivalence (from the name)
English
The finite product finite equivalence is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Fin} (m), \mathrm{Fin} (n))}{\mathrm{Fin} (m \times n)}$.
finSuccAboveEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite successor above equivalence of p (from the name)
English
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the finite successor above equivalence of $p$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n)}{(\SubtypeSet {x}{\mathrm{Neq} (x , p)})}$ defined as $\operatorname{optionSubtype}$ applied to $p$ and the inverse of the finite successor equivalence of $p$.
finSuccEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite successor equivalence of n (from the name)
English
Let $n$ be a natural number. Then the finite successor equivalence of $n$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n + 1)}{\mathrm{Option} (\mathrm{Fin} (n))}$ defined as the finite successor equivalence of $0$.
finSuccEquiv'defMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite successor equivalence of i (from the name)
English
Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the finite successor equivalence of $i$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n + 1)}{\mathrm{Option} (\mathrm{Fin} (n))}$.
finSuccEquivLastdefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
$\mathrm{finSuccEquivLast}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n + 1)}{\mathrm{Option} (\mathrm{Fin} (n))}$ defined as the finite successor equivalence of $\operatorname{last}$ applied to $n$.
finSumFinEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite sum finite equivalence (from the name)
English
The finite sum finite equivalence is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Fin} (m), \mathrm{Fin} (n))}{\mathrm{Fin} (m + n)}$.
finSumNatEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantWording
the finite sum natural equivalence of n (from the name)
English
Let $n$ be a natural number. Then the finite sum natural equivalence of $n$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Fin} (n), \Natural)}{\Natural}$.
finTwoArrowEquivdefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
Let $x$ be a set. Then $\mathrm{finTwoArrowEquiv}$ applied to $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Fin} (2))\rightarrow x)}{\mathrm{Prod} (x , x)}$.
prodEquivPiFinTwodefMathlib.Logic.Equiv.Fin.Basic, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\mathrm{prodEquivPiFinTwo}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{1})}{(\mathrm{Elem} (\mathrm{Fin} (2))\rightarrow \operatorname{vecCons} (x , \operatorname{vecCons} (x_{1} , \operatorname{vecEmpty}), i))}$ defined as the inverse of $\mathrm{piFinTwoEquiv}$ applied to $\operatorname{cons}$ applied to $x$ and $\operatorname{cons}$ applied to $x_{1}$ and $\mathrm{finZeroElim}$.
finCycledefMathlib.Logic.Equiv.Fin.Rotate, function or constantWording
the finite cycle of k (from the name)
English
Let $k$ be an element of $\mathrm{Fin}$ applied to $n$. Then the finite cycle of $k$ is a permutation of $\mathrm{Fin}$ applied to $n$.
finRotatedefMathlib.Logic.Equiv.Fin.Rotate, function or constantEnglish
Let $n$ be a natural number. Then $\mathrm{finRotate}$ applied to $n$ is a permutation of $\mathrm{Fin}$ applied to $n$.
Denumerable.lower'defMathlib.Logic.Equiv.Finset, function or constantEnglish
Let $x$ be a list of natural numbers. Let $x_{1}$ be a natural number. Then $\operatorname{lower'}$ applied to $x$ and $x_{1}$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Denumerable\_\_lower'\_\_\_f}$ and $x_{1}$.
Denumerable.raise'defMathlib.Logic.Equiv.Finset, function or constantEnglish
Let $x$ be a list of natural numbers. Let $x_{1}$ be a natural number. Then $\operatorname{raise'}$ applied to $x$ and $x_{1}$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Denumerable\_\_raise'\_\_\_f}$ and $x_{1}$.
Denumerable.raise'FinsetdefMathlib.Logic.Equiv.Finset, function or constantEnglish
Let $l$ be a list of natural numbers. Let $n$ be a natural number. Then $\operatorname{raise'Finset}$ applied to $l$ and $n$ is a finite set of $\Natural$.
Encodable.fintypeEquivFindefMathlib.Logic.Equiv.Finset, function or constantEnglish
$\operatorname{fintypeEquivFin}$ is an equivalence from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$.
Encodable.sortedUnivdefMathlib.Logic.Equiv.Finset, function or constantEnglish
Let $x$ be a set. Then $\operatorname{sortedUniv}$ applied to $x$ is a list of elements of $x$ defined as the sort of the universal set and $\operatorname{Preimage}$ applied to $\operatorname{coe}$ applied to $\operatorname{encode'}$ applied to $x$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Leq} (x_{3} , x_{4})$.
Equiv.Perm.viaFintypeEmbeddingdefMathlib.Logic.Equiv.Fintype, function or constantEnglish
Let $e$ be a permutation of $x$. Let $f$ be an embedding of $x$ and $x_{1}$. Then $\operatorname{viaFintypeEmbedding}$ applied to $e$ and $f$ is a permutation of $x_{1}$ defined as $\operatorname{extendDomain}$ applied to $e$ and the equivalence range of $f$.
Equiv.extendSubtypedefMathlib.Logic.Equiv.Fintype, function or constantEnglish
Let $e$ be an equivalence from $\SubtypeSet {x_{3}}{p (x_{3})}$ to $\SubtypeSet {x_{4}}{q (x_{4})}$. Then $\operatorname{extendSubtype}$ applied to $e$ is a permutation of $x$ defined as the subtype congruence of $e$ and the complement of $e$.
Equiv.setDiffEquivdefMathlib.Logic.Equiv.Fintype, function or constantWording
the set difference equivalence of h (from the name)
English
Assume that the cardinality of the set of elements of $s$ is equal to the cardinality of the set of elements of $t$. Then the set difference equivalence of $h$ is an equivalence from the set of elements of $\operatorname{sdiff}$ applied to $s$ and $t$ to the set of elements of $\operatorname{sdiff}$ applied to $t$ and $s$.
Equiv.toCompldefMathlib.Logic.Equiv.Fintype, function or constantWording
the complement of e (from the name)
English
Let $e$ be an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to $p$ applied to $x_{3}$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to $q$ applied to $x_{4}$. Then the complement of $e$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that it is not the case that $p$ holds for $x_{1}$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that it is not the case that $q$ holds for $x_{2}$.
Function.Embedding.toEquivRangedefMathlib.Logic.Equiv.Fintype, function or constantWording
the equivalence range of f (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Then the equivalence range of $f$ is an equivalence from $x$ to the set of elements of the range of $\operatorname{coe}$ applied to $f$.
Bifunctor.mapEquivdefMathlib.Logic.Equiv.Functor, function or constantWording
the map equivalence of h1 and #3 (from the name)
English
Let $F$ be a function from sets and sets to sets. Let $h_{1}$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{h'}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the map equivalence of $h_{1}$ and $\mathrm{h'}$ is an element of $\EquivMACRoAE {F (x , x_{2})}{F (x_{1} , x_{3})}$.
Functor.mapEquivdefMathlib.Logic.Equiv.Functor, function or constantWording
the map equivalence of f and h1 (from the name)
English
Let $f$ be a function from sets to sets. Let $h_{1}$ be an equivalence from $x$ to $x_{1}$. Then the map equivalence of $f$ and $h_{1}$ is an element of $\EquivMACRoAE {f (x)}{f (x_{1})}$.
Encodable.decodeListdefMathlib.Logic.Equiv.List, function or constantWording
the decode list of x2 (from the name)
English
Let $x_{2}$ be a natural number. Then the decode list of $x_{2}$ is an element of $\mathrm{Option}$ applied to the set of lists of elements of $x$.
Encodable.encodeListdefMathlib.Logic.Equiv.List, function or constantEnglish
Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{encodeList}$ applied to $x_{2}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Encodable\_\_encodeList\_\_\_f}$.
Equiv.listEquivOfEquivdefMathlib.Logic.Equiv.List, function or constantWording
the list equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the list equivalence of $e$ is an equivalence from the set of lists of elements of $x$ to the set of lists of elements of $x_{1}$.
Equiv.listEquivSelfOfEquivNatdefMathlib.Logic.Equiv.List, function or constantWording
the list equivalence self of e (from the name)
English
Let $e$ be an equivalence from $x$ to $\Natural$. Then the list equivalence self of $e$ is an equivalence from the set of lists of elements of $x$ to $x$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the list equivalence of $e$ and the list natural equivalence natural number and the inverse of $e$.
Equiv.listNatEquivNatdefMathlib.Logic.Equiv.List, function or constantWording
the list natural equivalence natural number (from the name)
English
The list natural equivalence natural number is an equivalence from the set of lists of natural numbers to $\Natural$ defined as $\operatorname{eqv}$ applied to the set of lists of natural numbers.
Equiv.listUniqueEquivdefMathlib.Logic.Equiv.List, function or constantWording
the list unique equivalence of x (from the name)
English
Let $x$ be a set. Then the list unique equivalence of $x$ is an equivalence from the set of lists of elements of $x$ to $\Natural$.
Fintype.truncEncodabledefMathlib.Logic.Equiv.List, function or constantEnglish
Let $x$ be a set. Then $\operatorname{truncEncodable}$ applied to $x$ is a truncation of the proposition that $x$ is encodable defined as $\operatorname{recOnSubsingleton}$ applied to the value of the universal set, the function that maps $l$ and $H$ to $\operatorname{mk}$ applied to $\operatorname{encodableOfList}$ applied to $l$ and $H$ and $\mathrm{Finset\_\_mem\_univ}$.
Denumerable.lowerdefMathlib.Logic.Equiv.Multiset, function or constantEnglish
Let $x$ be a list of natural numbers. Let $x_{1}$ be a natural number. Then $\operatorname{lower}$ applied to $x$ and $x_{1}$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Denumerable\_\_lower\_\_\_f}$ and $x_{1}$.
Denumerable.raisedefMathlib.Logic.Equiv.Multiset, function or constantEnglish
Let $x$ be a list of natural numbers. Let $x_{1}$ be a natural number. Then $\operatorname{raise}$ applied to $x$ and $x_{1}$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Denumerable\_\_raise\_\_\_f}$ and $x_{1}$.
decodeMultisetdefMathlib.Logic.Equiv.Multiset, function or constantWording
the decode multiset of n (from the name)
English
Let $n$ be a natural number. Then the decode multiset of $n$ is an element of $\mathrm{Option}$ applied to the set of multisets of $x$ defined as $\operatorname{map}$ applied to $\operatorname{ofList}$ and the decode of $n$.
encodeMultisetdefMathlib.Logic.Equiv.Multiset, function or constantEnglish
Let $s$ be a multiset of $x$. Then $\mathrm{encodeMultiset}$ applied to $s$ is a natural number.
Equiv.boolProdNatEquivNatdefMathlib.Logic.Equiv.Nat, function or constantWording
the bool product natural equivalence natural number (from the name)
English
The bool product natural equivalence natural number is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Bool} , \Natural)}{\Natural}$.
Equiv.intEquivNatdefMathlib.Logic.Equiv.Nat, function or constantWording
the integer equivalence natural number (from the name)
English
The integer equivalence natural number is an equivalence from $\Integer$ to $\Natural$ defined as the composition of the integer equivalence natural sum natural number and the natural sum natural equivalence natural number.
Equiv.natSumNatEquivNatdefMathlib.Logic.Equiv.Nat, function or constantWording
the natural sum natural equivalence natural number (from the name)
English
The natural sum natural equivalence natural number is an element of $\EquivMACRoAE {\mathrm{Sum} (\Natural , \Natural)}{\Natural}$ defined as the composition of the inverse of the product of $\Natural$ and the bool product natural equivalence natural number.
Equiv.prodEquivOfEquivNatdefMathlib.Logic.Equiv.Nat, function or constantWording
the product equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $\Natural$. Then the product equivalence of $e$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x)}{x}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the product congruence of $e$ and $e$ and the pair equivalence and the inverse of $e$.
Equiv.optionCongrdefMathlib.Logic.Equiv.Option, function or constantWording
the option congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the option congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{Option} (x)}{\mathrm{Option} (x_{1})}$.
Equiv.optionEquivSumPUnitdefMathlib.Logic.Equiv.Option, function or constantWording
the option equivalence sum unit of x (from the name)
English
Let $x$ be a set. Then the option equivalence sum unit of $x$ is an element of $\EquivMACRoAE {\mathrm{Option} (x)}{\mathrm{Sum} (x , \mathrm{PUnit})}$.
Equiv.optionIsSomeEquivdefMathlib.Logic.Equiv.Option, function or constantEnglish
Let $x$ be a set. Then $\operatorname{optionIsSomeEquiv}$ applied to $x$ is an equivalence from $\SubtypeSet {x_{1}}{(\EqtMACRoH {\operatorname{isSome} (x_{1})}{\operatorname{true}})}$ to $x$.
Equiv.optionSubtypedefMathlib.Logic.Equiv.Option, function or constantWording
the option subtype of x3 (from the name)
English
Let $x_{3}$ be an element of $x_{1}$. Then the option subtype of $x_{3}$ is an equivalence from $\SubtypeSet {e}{(\EqtMACRoH {e (\operatorname{none})}{x_{3}})}$ to $\EquivMACRoAE {x}{(\SubtypeSet {y}{\mathrm{Neq} (y , x_{3})})}$.
Equiv.optionSubtypeNedefMathlib.Logic.Equiv.Option, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{optionSubtypeNe}$ applied to $a$ is an element of $\EquivMACRoAE {\mathrm{Option} (\SubtypeSet {b}{\mathrm{Neq} (b , a)})}{x}$ defined as $\operatorname{symm}$ applied to the option subtype of $a$ and the identity of $\SubtypeSet {y_{4}}{\mathrm{Neq} (y_{4} , a)}$.
Equiv.removeNonedefMathlib.Logic.Equiv.Option, function or constantEnglish
Let $e$ be an element of $\EquivMACRoAE {\mathrm{Option} (x)}{\mathrm{Option} (x_{1})}$. Then $\operatorname{removeNone}$ applied to $e$ is an equivalence from $x$ to $x_{1}$.
Equiv.subtypeNeSumPUnitdefMathlib.Logic.Equiv.Option, function or constantEnglish
Let $x_{2}$ be an element of $x$. Then $\operatorname{subtypeNeSumPUnit}$ applied to $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\SubtypeSet {i}{\mathrm{Neq} (i , x_{2})}, \mathrm{PUnit})}{x}$ defined as the composition of the inverse of the option equivalence sum unit of $\SubtypeSet {i}{\mathrm{Neq} (i , x_{2})}$ and $\operatorname{optionSubtypeNe}$ applied to $x_{2}$.
Equiv.toPartialEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the partial equivalence of $e$ is a partial equivalence of $x$ and $x_{1}$.
Equiv.toPartialEquivOfImageEqdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of s and t (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$ such that the image of $\operatorname{coe}$ applied to $e$ and $s$ is equal to $t$. Then the partial equivalence of $s$ and $t$ is a partial equivalence of $x$ and $x_{1}$.
Equiv.transPartialEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the composition partial equivalence of e and #2 (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{f'}$ be a partial equivalence of $x_{1}$ and $x_{2}$. Then the composition partial equivalence of $e$ and $\mathrm{f'}$ is a partial equivalence of $x$ and $x_{2}$.
PartialEquivstructureMathlib.Logic.Equiv.PartialEquiv, typeWording
partial equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the partial equivalences of $x$ and $x_{1}$ are a basic type.
PartialEquiv.EqOnSourcedefMathlib.Logic.Equiv.PartialEquiv, predicateEnglish
Let $e$ and $\mathrm{e'}$ be partial equivalences of $x$ and $x_{1}$. Then $\operatorname{EqOnSource}$ holds for $e$ and $\mathrm{e'}$, if the source of $e$ is equal to the source of $\mathrm{e'}$ and $\operatorname{EqOn}$ holds for $\operatorname{toFun}$ applied to $e$, $\operatorname{toFun}$ applied to $\mathrm{e'}$ and the source of $e$.
PartialEquiv.IsImagedefMathlib.Logic.Equiv.PartialEquiv, predicateEnglish
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{IsImage}$ holds for $e$, $s$ and $t$, if for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of the source of $e$, then the partial equivalence of $e$ and $x_{2}$ is an element of $t$, if and only if $x_{2}$ is an element of $s$.
PartialEquiv.IsImage.restrdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the restriction of h (from the name)
English
Assume that $\operatorname{IsImage}$ holds for $e$, $s$ and $t$. Then the restriction of $h$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.copydefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the copy of s and t (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{toFun}$ applied to $e$ is equal to $f$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{toFun}$ applied to the inverse of $e$ is equal to $g$. Let $s$ be an element of $\wp x$ such that the source of $e$ is equal to $s$. Let $t$ be an element of $\wp x_{1}$ such that the target of $e$ is equal to $t$. Then the copy of $s$ and $t$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.disjointUniondefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the disjoint union of e and hs (from the name)
English
Let $e$ and $\mathrm{e'}$ be partial equivalences of $x$ and $x_{1}$ such that the source of $e$ is disjoint to the source of $\mathrm{e'}$ and the target of $e$ is disjoint to the target of $\mathrm{e'}$. Then the disjoint union of $e$ and $\mathrm{e'}$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.invFundefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the inverse function of self and x2 (from the name)
English
Let $\mathrm{self}$ be a partial equivalence of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the inverse function of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
PartialEquiv.ofSetdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the partial equivalence of $s$ is a partial equivalence of $x$ and $x$.
PartialEquiv.pidefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the product of ei (from the docstring)
English
Let $\mathrm{ei}$ be a function from elements $i_{2}$ of $x$ to partial equivalences of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the product of $i_{2}$ is a partial equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$.
PartialEquiv.piecewisedefMathlib.Logic.Equiv.PartialEquiv, function or constantEnglish
Let $e$ and $\mathrm{e'}$ be partial equivalences of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$ such that $\operatorname{IsImage}$ holds for $e$, $s$ and $t$ and $\operatorname{IsImage}$ holds for $\mathrm{e'}$, $s$ and $t$. Then $\operatorname{piecewise}$ applied to $e$, $\mathrm{e'}$, $s$, $t$, $H$ and $\mathrm{H'}$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.proddefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the product of e and #2 (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $\mathrm{e'}$ be a partial equivalence of $x_{2}$ and $x_{3}$. Then the product of $e$ and $\mathrm{e'}$ is a partial equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.
PartialEquiv.refldefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a partial equivalence of $x$ and $x$ defined as the partial equivalence of the identity of $x$.
PartialEquiv.restrdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the restriction of e and s (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then the restriction of $e$ and $s$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.singledefMathlib.Logic.Equiv.PartialEquiv, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{single}$ applied to $a$ and $b$ is a partial equivalence of $x$ and $x_{1}$.
PartialEquiv.sourcedefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the source of self (from the name)
English
Let $\mathrm{self}$ be a partial equivalence of $x$ and $x_{1}$. Then the source of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
PartialEquiv.symmdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Then the inverse of $e$ is a partial equivalence of $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{invFun}$ applied to $e$, $\operatorname{toFun}$ applied to $e$, the target of $e$, the source of $e$, $\mathrm{PartialEquiv\_\_map\_target'}$ applied to $e$, $\mathrm{PartialEquiv\_\_map\_source'}$ applied to $e$, $\mathrm{PartialEquiv\_\_right\_inv'}$ applied to $e$ and $\mathrm{PartialEquiv\_\_left\_inv'}$ applied to $e$.
PartialEquiv.targetdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the target of self (from the name)
English
Let $\mathrm{self}$ be a partial equivalence of $x$ and $x_{1}$. Then the target of $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
PartialEquiv.toEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the equivalence of e (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Then the equivalence of $e$ is an equivalence from the set of elements of the source of $e$ to the set of elements of the target of $e$.
PartialEquiv.toFundefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of self and x2 (from the name)
English
Let $\mathrm{self}$ be a partial equivalence of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then the partial equivalence of $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
PartialEquiv.transdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $\mathrm{e'}$ be a partial equivalence of $x_{1}$ and $x_{2}$. Then the composition of $e$ and $\mathrm{e'}$ is a partial equivalence of $x$ and $x_{2}$.
PartialEquiv.trans'defMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the composition of e and h (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $\mathrm{e'}$ be a partial equivalence of $x_{1}$ and $x_{2}$ such that the target of $e$ is equal to the source of $\mathrm{e'}$. Then the composition of $e$ and $\mathrm{e'}$ is a partial equivalence of $x$ and $x_{2}$.
PartialEquiv.transEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the composition equivalence of e and #2 (from the name)
English
Let $e$ be a partial equivalence of $x$ and $x_{1}$. Let $\mathrm{f'}$ be an equivalence from $x_{1}$ to $x_{2}$. Then the composition equivalence of $e$ and $\mathrm{f'}$ is a partial equivalence of $x$ and $x_{2}$.
Set.BijOn.toPartialEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of s and t (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$ such that $\operatorname{BijOn}$ holds for $f$, $s$ and $t$. Then the partial equivalence of $s$ and $t$ is a partial equivalence of $x$ and $x_{1}$.
Set.InjOn.toPartialEquivdefMathlib.Logic.Equiv.PartialEquiv, function or constantWording
the partial equivalence of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$ such that $f$ is injective on $s$. Then the partial equivalence of $f$ and $s$ is a partial equivalence of $x$ and $x_{1}$ defined as the partial equivalence of $s$ and the image of $f$ and $s$.
Equiv.Perm.prodExtendRightdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $a$ be an element of $x$. Let $e$ be a permutation of $x_{1}$. Then $\operatorname{prodExtendRight}$ applied to $a$ and $e$ is a permutation of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
Equiv.arrowProdEquivProdArrowdefMathlib.Logic.Equiv.Prod, function or constantWording
the arrow product equivalence product arrow of x1 and x2 (from the name)
English
Let $x$ be a set. Let $x_{1}$ and $x_{2}$ be functions from elements of $x$ to sets. Then the arrow product equivalence product arrow of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Prod} (x_{1} (i), x_{2} (i)))}{\mathrm{Prod} (\mathrm{Elem} (x)\rightarrow x_{1} (i_{1}), \mathrm{Elem} (x)\rightarrow x_{2} (i_{2}))}$.
Equiv.boolArrowEquivProddefMathlib.Logic.Equiv.Prod, function or constantWording
the bool arrow equivalence product of x (from the name)
English
Let $x$ be a set. Then the bool arrow equivalence product of $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Bool})\rightarrow x)}{\mathrm{Prod} (x , x)}$.
Equiv.boolProdEquivSumdefMathlib.Logic.Equiv.Prod, function or constantWording
the product of x (from the docstring)
English
Let $x$ be a set. Then the product of $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Bool} , x)}{\mathrm{Sum} (x , x)}$.
Equiv.currydefMathlib.Logic.Equiv.Prod, function or constantWording
the curry of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the curry of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Prod} (x , x_{1}))\rightarrow x_{2})}{(\mathrm{Elem} (x)\rightarrow \mathrm{Elem} (x_{1})\rightarrow x_{2})}$ defined as $\operatorname{mk}$ applied to $\operatorname{curry}$, $\operatorname{uncurry}$, $\mathrm{Function\_\_uncurry\_curry}$ and $\mathrm{Function\_\_curry\_uncurry}$.
Equiv.emptyProddefMathlib.Logic.Equiv.Prod, function or constantWording
the empty product of x (from the name)
English
Let $x$ be a set. Then the empty product of $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Empty} , x)}{\mathrm{Empty}}$ defined as $\operatorname{equivEmpty}$ applied to $\mathrm{Prod}$ applied to $\mathrm{Empty}$ and $x$.
Equiv.funSplitAtdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $i$ be an element of $x$. Let $x_{2}$ be a set. Then $\operatorname{funSplitAt}$ applied to $i$ and $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{2})}{\mathrm{Prod} (x_{2} , \mathrm{Elem} (\SubtypeSet {j}{\mathrm{Neq} (j , i)})\rightarrow x_{2})}$ defined as $\operatorname{piSplitAt}$ applied to $i$ and the function that maps $x_{3}$ to $x_{2}$.
Equiv.pemptyProddefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ be a set. Then $\operatorname{pemptyProd}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{PEmpty} , x)}{\mathrm{PEmpty}}$ defined as $\operatorname{equivPEmpty}$ applied to $\mathrm{Prod}$ applied to $\mathrm{PEmpty}$ and $x$.
Equiv.piEquivPiSubtypeProddefMathlib.Logic.Equiv.Prod, function or constantWording
the product equivalence product subtype product of p and x1 (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Let $x_{1}$ be a function from elements of $x$ to sets. Then the product equivalence product subtype product of $p$ and $x_{1}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1} (i))}{\mathrm{Prod} (\mathrm{Elem} (\SubtypeSet {x_{3}}{p (x_{3})})\rightarrow x_{1} (i_{1}), \mathrm{Elem} (\SubtypeSet {x_{4}}{\mathrm{not} (p (x_{4}))})\rightarrow x_{1} (i_{2}))}$.
Equiv.piSplitAtdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $i$ be an element of $x$. Let $x_{2}$ be a function from elements of $x$ to sets. Then $\operatorname{piSplitAt}$ applied to $i$ and $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{2} (j))}{\mathrm{Prod} (x_{2} (i), \mathrm{Elem} (\SubtypeSet {j_{2}}{\mathrm{Neq} (j_{2} , i)})\rightarrow x_{2} (j_{1}))}$.
Equiv.pprodCongrdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{5}$ be an equivalence from $x_{2}$ to $x_{3}$. Then $\operatorname{pprodCongr}$ applied to $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {\mathrm{PProd} (x , x_{2})}{\mathrm{PProd} (x_{1} , x_{3})}$.
Equiv.pprodEquivProddefMathlib.Logic.Equiv.Prod, function or constantEnglish
$\operatorname{pprodEquivProd}$ is an element of $\EquivMACRoAE {\mathrm{PProd} (x , x_{1})}{\mathrm{Prod} (x , x_{1})}$.
Equiv.pprodEquivProdPLiftdefMathlib.Logic.Equiv.Prod, function or constantEnglish
$\operatorname{pprodEquivProdPLift}$ is an element of $\EquivMACRoAE {\mathrm{PProd} (x , x_{1})}{\mathrm{Prod} (\mathrm{PLift} (x), \mathrm{PLift} (x_{1}))}$ defined as $\operatorname{pprodProd}$ applied to the inverse of $\operatorname{plift}$ and the inverse of $\operatorname{plift}$.
Equiv.pprodProddefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $\mathrm{ea}$ be an equivalence from $x$ to $x_{2}$. Let $\mathrm{eb}$ be an equivalence from $x_{1}$ to $x_{3}$. Then $\operatorname{pprodProd}$ applied to $\mathrm{ea}$ and $\mathrm{eb}$ is an element of $\EquivMACRoAE {\mathrm{PProd} (x , x_{1})}{\mathrm{Prod} (x_{2} , x_{3})}$ defined as the composition of $\operatorname{pprodCongr}$ applied to $\mathrm{ea}$ and $\mathrm{eb}$ and $\operatorname{pprodEquivProd}$.
Equiv.prodAssocdefMathlib.Logic.Equiv.Prod, function or constantWording
the product associator of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the product associator of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Prod} (x , x_{1}), x_{2})}{\mathrm{Prod} (x , \mathrm{Prod} (x_{1} , x_{2}))}$.
Equiv.prodCommdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{prodComm}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{1})}{\mathrm{Prod} (x_{1} , x)}$.
Equiv.prodCongrdefMathlib.Logic.Equiv.Prod, function or constantWording
the product congruence of x4 and x5 (from the name)
English
Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{5}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the product congruence of $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{2})}{\mathrm{Prod} (x_{1} , x_{3})}$.
Equiv.prodCongrLeftdefMathlib.Logic.Equiv.Prod, function or constantWording
the left product congruence of e (from the name)
English
Let $e$ be a function from elements of $x$ to equivalences from $x_{1}$ to $x_{2}$. Then the left product congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x_{1} , x)}{\mathrm{Prod} (x_{2} , x)}$.
Equiv.prodCongrRightdefMathlib.Logic.Equiv.Prod, function or constantWording
the right product congruence of e (from the name)
English
Let $e$ be a function from elements of $x$ to equivalences from $x_{1}$ to $x_{2}$. Then the right product congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{1})}{\mathrm{Prod} (x , x_{2})}$.
Equiv.prodEmptydefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ be a set. Then $\operatorname{prodEmpty}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , \mathrm{Empty})}{\mathrm{Empty}}$ defined as $\operatorname{equivEmpty}$ applied to $\mathrm{Prod}$ applied to $x$ and $\mathrm{Empty}$.
Equiv.prodPEmptydefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ be a set. Then $\operatorname{prodPEmpty}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , \mathrm{PEmpty})}{\mathrm{PEmpty}}$ defined as $\operatorname{equivPEmpty}$ applied to $\mathrm{Prod}$ applied to $x$ and $\mathrm{PEmpty}$.
Equiv.prodPProddefMathlib.Logic.Equiv.Prod, function or constantWording
the product product of ea and eb (from the name)
English
Let $\mathrm{ea}$ be an equivalence from $x_{2}$ to $x$. Let $\mathrm{eb}$ be an equivalence from $x_{3}$ to $x_{1}$. Then the product product of $\mathrm{ea}$ and $\mathrm{eb}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x_{2} , x_{3})}{\mathrm{PProd} (x , x_{1})}$ defined as the inverse of $\operatorname{pprodProd}$ applied to the inverse of $\mathrm{ea}$ and the inverse of $\mathrm{eb}$.
Equiv.prodPUnitdefMathlib.Logic.Equiv.Prod, function or constantWording
the product unit of x (from the name)
English
Let $x$ be a set. Then the product unit of $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , \mathrm{PUnit})}{x}$.
Equiv.prodPiEquivSumPidefMathlib.Logic.Equiv.Prod, function or constantWording
the product product equivalence sum product of x2 and x3 (from the name)
English
Let $x_{2}$ be a function from elements of $x$ to sets. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Then the product product equivalence sum product of $x_{2}$ and $x_{3}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Elem} (x)\rightarrow x_{2} (i), \mathrm{Elem} (x_{1})\rightarrow x_{3} (\mathrm{i'}))}{(\mathrm{Elem} (\mathrm{Sum} (x , x_{1}))\rightarrow \operatorname{elim} (x_{2} , x_{3} , i_{1}))}$ defined as the inverse of the sum product equivalence product product of $\operatorname{elim}$ applied to $x_{2}$ and $x_{3}$.
Equiv.prodProdProdCommdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $x$, $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Prod} (x , x_{1}), \mathrm{Prod} (x_{2} , x_{3}))}{\mathrm{Prod} (\mathrm{Prod} (x , x_{2}), \mathrm{Prod} (x_{1} , x_{3}))}$.
Equiv.prodSheardefMathlib.Logic.Equiv.Prod, function or constantWording
the product shear of x4 and x5 (from the name)
English
Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{5}$ be a function from elements of $x$ to equivalences from $x_{2}$ to $x_{3}$. Then the product shear of $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{2})}{\mathrm{Prod} (x_{1} , x_{3})}$.
Equiv.prodSubtypeFstEquivSubtypeProddefMathlib.Logic.Equiv.Prod, function or constantWording
the product subtype first component equivalence subtype product (from the name)
English
The product subtype first component equivalence subtype product is an element of $\EquivMACRoAE {(\SubtypeSet {s}{p (\ProdfstMACRoZ {s})})}{\mathrm{Prod} (\SubtypeSet {a}{p (a)}, x_{1})}$.
Equiv.prodUniquedefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{prodUnique}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x_{1})}{x}$ defined as the composition of the product congruence of the identity of $x$ and the equivalence unit of $x_{1}$ and the product unit of $x$.
Equiv.punitProddefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ be a set. Then $\operatorname{punitProd}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{PUnit} , x)}{x}$ defined as $\operatorname{trans}$ applied to $\operatorname{prodComm}$ applied to $\mathrm{PUnit}$ and $x$ and the product unit of $x$.
Equiv.sigmaPUnitdefMathlib.Logic.Equiv.Prod, function or constantWording
the sigma unit of x (from the name)
English
Let $x$ be a set. Then the sigma unit of $x$ is an element of $\EquivMACRoAE {\Sigma (\lambda x_{1} . \mathrm{PUnit})}{x}$.
Equiv.sigmaProdDistribdefMathlib.Logic.Equiv.Prod, function or constantWording
the product of x1 and x2 (from the docstring)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Let $x_{2}$ be a set. Then the product of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\Sigma (\lambda i . x_{1} (i)), x_{2})}{\Sigma (\lambda i_{1} . \mathrm{Prod} (x_{1} (i_{1}), x_{2}))}$.
Equiv.sigmaUniquedefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Then $\operatorname{sigmaUnique}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\Sigma (\lambda a . x_{1} (a))}{x}$ defined as the composition of the right sigma congruence of the function that maps $a$ to the equivalence unit of $x_{1}$ applied to $a$ and the sigma unit of $x$.
Equiv.subtypeProdEquivProddefMathlib.Logic.Equiv.Prod, function or constantWording
the subtype product equivalence product (from the name)
English
The subtype product equivalence product is an element of $\EquivMACRoAE {(\SubtypeSet {c}{\mathrm{and} (p (\ProdfstMACRoZ {c}), q (\ProdsndMACRoAA {c}))})}{\mathrm{Prod} (\SubtypeSet {a}{p (a)}, \SubtypeSet {b}{q (b)})}$.
Equiv.subtypeProdEquivSigmaSubtypedefMathlib.Logic.Equiv.Prod, function or constantWording
the subtype product equivalence sigma subtype of p (from the name)
English
Let $p$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then the subtype product equivalence sigma subtype of $p$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{p (\ProdfstMACRoZ {x_{2}}, \ProdsndMACRoAA {x_{2}})})}{\Sigma (\lambda a . \SubtypeSet {b}{p (a , b)})}$.
Equiv.subtypeSigmaEquivSigmadefMathlib.Logic.Equiv.Prod, function or constantWording
the subtype sigma equivalence sigma (from the name)
English
The subtype sigma equivalence sigma is an element of $\EquivMACRoAE {(\SubtypeSet {c}{\mathrm{and} (p (\operatorname{fst} (c)), q (\operatorname{fst} (c), \operatorname{snd} (c)))})}{\Sigma (\lambda i . \SubtypeSet {b}{q (i , b)})}$.
Equiv.sumArrowEquivProdArrowdefMathlib.Logic.Equiv.Prod, function or constantWording
the sum arrow equivalence product arrow of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the sum arrow equivalence product arrow of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Sum} (x , x_{1}))\rightarrow x_{2})}{\mathrm{Prod} (\mathrm{Elem} (x)\rightarrow x_{2} , \mathrm{Elem} (x_{1})\rightarrow x_{2})}$.
Equiv.sumPiEquivProdPidefMathlib.Logic.Equiv.Prod, function or constantWording
the sum product equivalence product product of x2 (from the name)
English
Let $x_{2}$ be a function from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to sets. Then the sum product equivalence product product of $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Sum} (x , x_{1}))\rightarrow x_{2} (i))}{\mathrm{Prod} (\mathrm{Elem} (x)\rightarrow x_{2} (\operatorname{inl} (i_{1})), \mathrm{Elem} (x_{1})\rightarrow x_{2} (\operatorname{inr} (\mathrm{i'})))}$.
Equiv.sumProdDistribdefMathlib.Logic.Equiv.Prod, function or constantEnglish
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{sumProdDistrib}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Sum} (x , x_{1}), x_{2})}{\mathrm{Sum} (\mathrm{Prod} (x , x_{2}), \mathrm{Prod} (x_{1} , x_{2}))}$.
Equiv.uniqueProddefMathlib.Logic.Equiv.Prod, function or constantWording
the unique product of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the unique product of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x_{1} , x)}{x}$ defined as the composition of the product congruence of the equivalence unit of $x_{1}$ and the identity of $x$ and $\operatorname{punitProd}$ applied to $x$.
Equiv.uniqueSigmadefMathlib.Logic.Equiv.Prod, function or constantWording
the unique sigma of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Then the unique sigma of $x_{1}$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . x_{1} (i))}{x_{1} (\operatorname{default})}$.
optionProdEquivdefMathlib.Logic.Equiv.Prod, function or constantWording
the option product equivalence (from the name)
English
The option product equivalence is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Option} (x), x_{1})}{\mathrm{Sum} (x_{1} , \mathrm{Prod} (x , x_{1}))}$.
subsingletonProdSelfEquivdefMathlib.Logic.Equiv.Prod, function or constantWording
the subsingleton product self equivalence (from the name)
English
The subsingleton product self equivalence is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x)}{x}$.
Equiv.Set.compldefMathlib.Logic.Equiv.Set, function or constantWording
the complement of x4 (from the name)
English
Let $x_{4}$ be an element of $\EquivMACRoAE {\operatorname{Elem} (s)}{\operatorname{Elem} (t)}$. Then the complement of $x_{4}$ is an element of $\EquivMACRoAE {(\SubtypeSet {e}{\mathrm{forall} (\operatorname{Elem} (s), \lambda x_{5} . \EqtMACRoH {e (x_{5})}{x_{4} (x_{5})})})}{(\EquivMACRoAE {\operatorname{Elem} (\operatorname{compl} (s))}{\operatorname{Elem} (\operatorname{compl} (t))})}$.
Equiv.Set.emptydefMathlib.Logic.Equiv.Set, function or constantEnglish
Let $x$ be a set. Then $\operatorname{empty}$ applied to $x$ is an equivalence from the set of elements of $\operatorname{emptyCollection}$ to $\mathrm{Empty}$ defined as $\operatorname{equivEmpty}$ applied to the set of elements of $\operatorname{emptyCollection}$.
Equiv.Set.imagedefMathlib.Logic.Equiv.Set, function or constantWording
the image of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Assume that $f$ is injective. Then the image of $f$ and $s$ is an equivalence from the set of elements of $s$ to the set of elements of the image of $f$ and $s$ defined as the image of $f$ and $s$.
Equiv.Set.imageOfInjOndefMathlib.Logic.Equiv.Set, function or constantWording
the image of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$ such that $f$ is injective on $s$. Then the image of $f$ and $s$ is an equivalence from the set of elements of $s$ to the set of elements of the image of $f$ and $s$.
Equiv.Set.insertdefMathlib.Logic.Equiv.Set, function or constantEnglish
Assume that $a$ is not an element of $s$. Then $\operatorname{insert}$ applied to $H$ is an equivalence from the set of elements of $\operatorname{insert}$ applied to $a$ and $s$ to $\mathrm{Sum}$ applied to the set of elements of $s$ and $\mathrm{PUnit}$.
Equiv.Set.pemptydefMathlib.Logic.Equiv.Set, function or constantEnglish
Let $x$ be a set. Then $\operatorname{pempty}$ applied to $x$ is an equivalence from the set of elements of $\operatorname{emptyCollection}$ to $\mathrm{PEmpty}$ defined as $\operatorname{equivPEmpty}$ applied to the set of elements of $\operatorname{emptyCollection}$.
Equiv.Set.powersetdefMathlib.Logic.Equiv.Set, function or constantWording
the powerset of S (from the name)
English
Let $S$ be an element of $\wp x$. Then the powerset of $S$ is an equivalence from the set of elements of the powerset of $S$ to the power set of the set of elements of $S$.
Equiv.Set.proddefMathlib.Logic.Equiv.Set, function or constantWording
the product of s and t (from the name)
English
Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then the product of $s$ and $t$ is an equivalence from the set of elements of $\operatorname{sprod}$ applied to $s$ and $t$ to $\mathrm{Prod}$ applied to the set of elements of $s$ and the set of elements of $t$ defined as the subtype product equivalence product.
Equiv.Set.rangeInldefMathlib.Logic.Equiv.Set, function or constantWording
the range left injection of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the range left injection of $x$ and $x_{1}$ is an equivalence from the set of elements of the range of $\operatorname{inl}$ to $x$.
Equiv.Set.rangeInrdefMathlib.Logic.Equiv.Set, function or constantWording
the range right injection of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the range right injection of $x$ and $x_{1}$ is an equivalence from the set of elements of the range of $\operatorname{inr}$ to $x_{1}$.
Equiv.Set.rangeSplittingImageEquivdefMathlib.Logic.Equiv.Set, function or constantWording
the range splitting image equivalence of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of the power set of the set of elements of the range of $f$. Then the range splitting image equivalence of $f$ and $s$ is an equivalence from the set of elements of the image of $\operatorname{rangeSplitting}$ applied to $f$ and $s$ to the set of elements of $s$.
Equiv.Set.sepdefMathlib.Logic.Equiv.Set, function or constantEnglish
Let $s$ be an element of $\wp x$. Let $t$ be a function from elements of $x$ to propositions. Then $\operatorname{sep}$ applied to $s$ and $t$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $x_{1}$ is an element of $s$ and $t$ holds for $x_{1}$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $t$ applied to $x_{2}$ defined as the inverse of the subtype subtype equivalence subtype intersection of the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and $t$.
Equiv.Set.singletondefMathlib.Logic.Equiv.Set, function or constantWording
the singleton of a (from the name)
English
Let $a$ be an element of $x$. Then the singleton of $a$ is an equivalence from the set of elements of $\operatorname{singleton}$ applied to $a$ to $\mathrm{PUnit}$.
Equiv.Set.sumCompldefMathlib.Logic.Equiv.Set, function or constantWording
the sum complement of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the sum complement of $s$ is an equivalence from $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of the complement of $s$ to $x$ defined as the sum complement of the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$.
Equiv.Set.sumDiffSubsetdefMathlib.Logic.Equiv.Set, function or constantWording
the sum difference subset of h (from the name)
English
Assume that $s \leq t$. Then the sum difference subset of $h$ is an equivalence from $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of $\operatorname{sdiff}$ applied to $t$ and $s$ to the set of elements of $t$.
Equiv.Set.uniondefMathlib.Logic.Equiv.Set, function or constantWording
the union of H (from the name)
English
Assume that $s$ is disjoint to $t$. Then the union of $H$ is an equivalence from the set of elements of $\UnionunionMACRoAB {s}{t}$ to $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of $t$.
Equiv.Set.union'defMathlib.Logic.Equiv.Set, function or constantWording
the union of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions such that for all elements $x_{3}$ of $x$, if $x_{3}$ is an element of $s$, then $p$ holds for $x_{3}$ and for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of $t$, then it is not the case that $p$ holds for $x_{2}$. Then the union of $p$ is an equivalence from the set of elements of $\UnionunionMACRoAB {s}{t}$ to $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of $t$.
Equiv.Set.unionSumInterdefMathlib.Logic.Equiv.Set, function or constantWording
the union sum intersection of s and t (from the name)
English
Let $s$ and $t$ be elements of $\wp x$. Then the union sum intersection of $s$ and $t$ is an equivalence from $\mathrm{Sum}$ applied to the set of elements of $\UnionunionMACRoAB {s}{t}$ and the set of elements of $\operatorname{inter}$ applied to $s$ and $t$ to $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of $t$.
Equiv.Set.univdefMathlib.Logic.Equiv.Set, function or constantWording
the universal set of x (from the name)
English
Let $x$ be a set. Then the universal set of $x$ is an equivalence from the set of elements of the universal set to $x$.
Equiv.Set.univPidefMathlib.Logic.Equiv.Set, function or constantWording
the set of s (from the docstring)
English
Let $s$ be a function from elements $a_{1}$ of $x$ to elements of $\wp x_{1} (a_{1})$. Then the set of $a_{1}$ is an equivalence from the set of elements of the product of the universal set and $s$ to the set of functions from elements $a$ of $x$ to elements of $s$ applied to $a$.
Equiv.imagedefMathlib.Logic.Equiv.Set, function or constantWording
the image of e and s (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Let $s$ be an element of $\wp x$. Then the image of $e$ and $s$ is an equivalence from the set of elements of $s$ to the set of elements of the image of $\operatorname{coe}$ applied to $e$ and $s$.
Equiv.ofInjectivedefMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of f and hf (from the name)
English
Let $f$ be an injective function from elements of $x$ to elements of $x_{1}$. Then the equivalence of $f$ and $\mathrm{hf}$ is an equivalence from $x$ to the set of elements of the range of $f$ defined as the equivalence of $f$.
Equiv.ofLeftInversedefMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{f\_inv}$ be a function from elements of $\mathrm{Proof}$ applied to $\mathrm{Nonempty}$ applied to $x$ and elements of $x_{1}$ to elements of $x$ such that for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Nonempty}$ applied to $x$, $\operatorname{LeftInverse}$ holds for $\mathrm{f\_inv}$ applied to $h$ and $f$. Then the equivalence of $f$ is an equivalence from $x$ to the set of elements of the range of $f$.
Equiv.ofLeftInverse'defMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of f and f_inv (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{f\_inv}$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{LeftInverse}$ holds for $\mathrm{f\_inv}$ and $f$. Then the equivalence of $f$ and $\mathrm{f\_inv}$ is an equivalence from $x$ to the set of elements of the range of $f$ defined as the equivalence of $f$.
Equiv.ofPreimageEquivdefMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of e (from the name)
English
Let $e$ be a function from elements $c$ of $x_{2}$ to equivalences from the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $c$ to the set of elements of the preimage of $g$ and $\operatorname{singleton}$ applied to $c$. Then the equivalence of $c$ is an equivalence from $x$ to $x_{1}$ defined as the function that maps $e$ to the equivalence of $c$.
Equiv.setCongrdefMathlib.Logic.Equiv.Set, function or constantWording
the set congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the set congruence of $e$ is an equivalence from $\wp x$ to $\wp x_{1}$.
Equiv.setProdEquivSigmadefMathlib.Logic.Equiv.Set, function or constantWording
the set product equivalence sigma of s (from the name)
English
Let $s$ be an element of $\wp \mathrm{Prod} (x , x_{1})$. Then the set product equivalence sigma of $s$ is an equivalence from the set of elements of $s$ to $\Sigma$ applied to the function that maps $x_{2}$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $y$ to $\MembershipmemMACRoT {s}{(\ProdmkMACRoU {x_{2}}{y})}$.
Equiv.sigmaPreimageEquivdefMathlib.Logic.Equiv.Set, function or constantWording
the sigma preimage equivalence of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the sigma preimage equivalence of $f$ is an equivalence from $\Sigma$ applied to the function that maps $b$ to the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $b$ to $x$ defined as the sigma fiber equivalence of $f$.
Set.BijOn.equivdefMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of f and h (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{BijOn}$ holds for $f$, $s$ and $t$. Then the equivalence of $f$ and $h$ is an equivalence from the set of elements of $s$ to the set of elements of $t$ defined as the equivalence of $\operatorname{restrict}$ applied to $f$, $s$, $t$ and $\operatorname{mapsTo}$ applied to $h$ and $\operatorname{bijective}$ applied to $h$.
Set.equivOfEqdefMathlib.Logic.Equiv.Set, function or constantWording
the equivalence of h (from the name)
English
Assume that $\EqtMACRoH {s}{t}$. Then the equivalence of $h$ is an equivalence from the set of elements of $s$ to the set of elements of $t$.
Equiv.Set.sigmadefMathlib.Logic.Equiv.Sigma, function or constantWording
the sigma of s and t (from the name)
English
Let $s$ be an element of $\wp x$. Let $t$ be a function from elements $i_{1}$ of $x$ to elements of $\wp x_{1} (i_{1})$. Then the sigma of $s$ and $i_{1}$ is an equivalence from the set of elements of the sigma of $s$ and $t$ to $\Sigma$ applied to the function that maps $i$ to the set of elements of $t$ applied to $i$ defined as the function that maps $t$ to the subtype sigma equivalence sigma.
Equiv.Perm.sumCongrdefMathlib.Logic.Equiv.Sum, function or constantWording
the sum congruence of ea and eb (from the name)
English
Let $\mathrm{ea}$ be a permutation of $x$. Let $\mathrm{eb}$ be a permutation of $x_{1}$. Then the sum congruence of $\mathrm{ea}$ and $\mathrm{eb}$ is a permutation of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as the sum congruence of $\mathrm{ea}$ and $\mathrm{eb}$.
Equiv.boolEquivPUnitSumPUnitdefMathlib.Logic.Equiv.Sum, function or constantWording
the bool equivalence unit sum unit (from the name)
English
The bool equivalence unit sum unit is an element of $\EquivMACRoAE {\mathrm{Bool}}{\mathrm{Sum} (\mathrm{PUnit} , \mathrm{PUnit})}$.
Equiv.emptySumdefMathlib.Logic.Equiv.Sum, function or constantWording
the empty sum of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the empty sum of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x , x_{1})}{x_{1}}$ defined as the composition of $\operatorname{sumComm}$ applied to $x$ and $x_{1}$ and $\operatorname{sumEmpty}$ applied to $x_{1}$ and $x$.
Equiv.prodSumDistribdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{prodSumDistrib}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x , \mathrm{Sum} (x_{1} , x_{2}))}{\mathrm{Sum} (\mathrm{Prod} (x , x_{1}), \mathrm{Prod} (x , x_{2}))}$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{prodComm}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ and $\operatorname{sumProdDistrib}$ applied to $x_{1}$, $x_{2}$ and $x$ and the sum congruence of $\operatorname{prodComm}$ applied to $x_{1}$ and $x$ and $\operatorname{prodComm}$ applied to $x_{2}$ and $x$.
Equiv.psumCongrdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{5}$ be an equivalence from $x_{2}$ to $x_{3}$. Then $\operatorname{psumCongr}$ applied to $x_{4}$ and $x_{5}$ is an element of $\EquivMACRoAE {\mathrm{PSum} (x , x_{2})}{\mathrm{PSum} (x_{1} , x_{3})}$.
Equiv.psumEquivSumdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{psumEquivSum}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{PSum} (x , x_{1})}{\mathrm{Sum} (x , x_{1})}$.
Equiv.psumSumdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $\mathrm{ea}$ be an equivalence from $x$ to $x_{2}$. Let $\mathrm{eb}$ be an equivalence from $x_{1}$ to $x_{3}$. Then $\operatorname{psumSum}$ applied to $\mathrm{ea}$ and $\mathrm{eb}$ is an element of $\EquivMACRoAE {\mathrm{PSum} (x , x_{1})}{\mathrm{Sum} (x_{2} , x_{3})}$ defined as the composition of $\operatorname{psumCongr}$ applied to $\mathrm{ea}$ and $\mathrm{eb}$ and $\operatorname{psumEquivSum}$ applied to $x_{2}$ and $x_{3}$.
Equiv.sigmaEquivOptionOfInhabiteddefMathlib.Logic.Equiv.Sum, function or constantWording
the sigma equivalence option of x (from the name)
English
Let $x$ be a set. Then the sigma equivalence option of $x$ is an element of $\Sigma$ applied to the function that maps $x_{3}$ to $\EquivMACRoAE {x}{\mathrm{Option} (x_{3})}$.
Equiv.sigmaFiberEquivdefMathlib.Logic.Equiv.Sum, function or constantWording
the sigma fiber equivalence of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the sigma fiber equivalence of $f$ is an element of $\EquivMACRoAE {\Sigma (\lambda y . \SubtypeSet {x_{2}}{(\EqtMACRoH {f (x_{2})}{y})})}{x}$.
Equiv.sigmaSumDistribdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x_{1}$ and $x_{2}$ be functions from elements of $x$ to sets. Then $\operatorname{sigmaSumDistrib}$ applied to $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . \mathrm{Sum} (x_{1} (i), x_{2} (i)))}{\mathrm{Sum} (\Sigma (\lambda i_{1} . x_{1} (i_{1})), \Sigma (\lambda i_{2} . x_{2} (i_{2})))}$.
Equiv.subtypeSumdefMathlib.Logic.Equiv.Sum, function or constantWording
the subtype sum (from the name)
English
The subtype sum is an element of $\EquivMACRoAE {(\SubtypeSet {c}{p (c)})}{\mathrm{Sum} (\SubtypeSet {a}{p (\operatorname{inl} (a))}, \SubtypeSet {b}{p (\operatorname{inr} (b))})}$.
Equiv.sumAssocdefMathlib.Logic.Equiv.Sum, function or constantWording
the sum associator of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the sum associator of $x_{1}$ and $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Sum} (x , x_{1}), x_{2})}{\mathrm{Sum} (x , \mathrm{Sum} (x_{1} , x_{2}))}$.
Equiv.sumCommdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{sumComm}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x , x_{1})}{\mathrm{Sum} (x_{1} , x)}$ defined as $\operatorname{mk}$ applied to $\operatorname{swap}$, $\operatorname{swap}$, $\mathrm{Sum\_\_swap\_swap}$ and $\mathrm{Sum\_\_swap\_swap}$.
Equiv.sumCompldefMathlib.Logic.Equiv.Sum, function or constantWording
the sum complement of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the sum complement of $p$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\SubtypeSet {a}{p (a)}, \SubtypeSet {a_{1}}{\mathrm{not} (p (a_{1}))})}{x}$.
Equiv.sumCongrdefMathlib.Logic.Equiv.Sum, function or constantWording
the sum congruence of ea and eb (from the name)
English
Let $\mathrm{ea}$ be an equivalence from $x$ to $x_{1}$. Let $\mathrm{eb}$ be an equivalence from $x_{2}$ to $x_{3}$. Then the sum congruence of $\mathrm{ea}$ and $\mathrm{eb}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x , x_{2})}{\mathrm{Sum} (x_{1} , x_{3})}$.
Equiv.sumEmptydefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{sumEmpty}$ applied to $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x , x_{1})}{x}$.
Equiv.sumEquivSigmaBooldefMathlib.Logic.Equiv.Sum, function or constantWording
the sum equivalence sigma bool of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the sum equivalence sigma bool of $x$ and $x_{1}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x , x_{1})}{\Sigma (\lambda b . \mathrm{cond} (b , x_{1} , x))}$.
Equiv.sumPSumdefMathlib.Logic.Equiv.Sum, function or constantWording
the sum sum of ea and eb (from the name)
English
Let $\mathrm{ea}$ be an equivalence from $x_{2}$ to $x$. Let $\mathrm{eb}$ be an equivalence from $x_{3}$ to $x_{1}$. Then the sum sum of $\mathrm{ea}$ and $\mathrm{eb}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (x_{2} , x_{3})}{\mathrm{PSum} (x , x_{1})}$ defined as the inverse of $\operatorname{psumSum}$ applied to the inverse of $\mathrm{ea}$ and the inverse of $\mathrm{eb}$.
Equiv.sumSigmaDistribdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $t$ be a function from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to sets. Then $\operatorname{sumSigmaDistrib}$ applied to $t$ is an element of $\EquivMACRoAE {\Sigma (\lambda i . t (i))}{\mathrm{Sum} (\Sigma (\lambda i_{1} . t (\operatorname{inl} (i_{1}))), \Sigma (\lambda i_{2} . t (\operatorname{inr} (i_{2}))))}$.
Equiv.sumSumSumCommdefMathlib.Logic.Equiv.Sum, function or constantEnglish
Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be sets. Then $\operatorname{sumSumSumComm}$ applied to $x$, $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Sum} (x , x_{1}), \mathrm{Sum} (x_{2} , x_{3}))}{\mathrm{Sum} (\mathrm{Sum} (x , x_{2}), \mathrm{Sum} (x_{1} , x_{3}))}$.
Function.FactorsThroughdefMathlib.Logic.Function.Basic, predicateEnglish
Let $g$ be a function from elements of $x$ to elements of $x_{2}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{FactorsThrough}$ holds for $g$ and $f$, if for all elements $a$ and $b$ of $x$, if $\EqtMACRoH {f (a)}{f (b)}$, then $\EqtMACRoH {g (a)}{g (b)}$.
Function.HasUncurryclassMathlib.Logic.Function.Basic, predicateEnglish
Let $x$ be a set. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\operatorname{HasUncurry}$ holds for $x$, $x_{1}$ and $x_{2}$.
Function.HasUncurry.uncurrydefMathlib.Logic.Function.Basic, function or constantEnglish
Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $x_{1}$. Then $\operatorname{uncurry}$ applied to $x_{3}$ and $x_{4}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.
Function.Injective2defMathlib.Logic.Function.Basic, predicateWording
f is injective (from the name)
English
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Then $f$ is injective, if for all elements $x_{3}$ and $x_{4}$ of $x$, for all elements $x_{5}$ and $x_{6}$ of $x_{1}$, if $\EqtMACRoH {f (x_{3} , x_{5})}{f (x_{4} , x_{6})}$, then $\EqtMACRoH {x_{3}}{x_{4}}$ and $\EqtMACRoH {x_{5}}{x_{6}}$.
Function.InvolutivedefMathlib.Logic.Function.Basic, predicateWording
f is involutive (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Then $f$ is involutive, if for all elements $x_{1}$ of $x$, $\EqtMACRoH {f (f (x_{1}))}{x_{1}}$.
Function.IsPartialInvdefMathlib.Logic.Function.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $\mathrm{Option}$ applied to $x$. Then $\operatorname{IsPartialInv}$ holds for $f$ and $g$, if for all elements $x_{2}$ of $x$, for all elements $y$ of $x_{1}$, $\EqtMACRoH {g (y)}{\operatorname{some} (x_{2})}$, if and only if $\EqtMACRoH {f (x_{2})}{y}$.
Function.evaldefMathlib.Logic.Function.Basic, function or constantWording
the evaluation of x2 and f (from the name)
English
Let $x_{2}$ be an element of $x$. Let $f$ be a function from elements $x_{3}$ of $x$ to elements of $x_{1}$ applied to $x_{3}$. Then the evaluation of $x_{2}$ and $x_{3}$ is an element of $x_{1}$ applied to $x_{2}$ defined as the function that maps $f$ to $x_{3}$ applied to $x_{2}$ and $f$.
Function.extenddefMathlib.Logic.Function.Basic, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $x_{2}$. Let $j$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be an element of $x_{1}$. Then $\operatorname{extend}$ applied to $f$, $g$, $j$ and $x_{3}$ is an element of $x_{2}$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $a$ of $x$, such that $\EqtMACRoH {f (a)}{x_{3}}$, the function that maps $h$ to $g$ applied to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $j$ applied to $x_{3}$.
Function.invFundefMathlib.Logic.Function.Basic, function or constantWording
the inverse of f and x2 (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the inverse of $f$ and $x_{2}$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $x_{3}$ of $x$, such that $\EqtMACRoH {f (x_{3})}{x_{2}}$, the function that maps $h_{1}$ to $\operatorname{choose}$ applied to $h_{1}$ and the function that maps $h_{2}$ to $\operatorname{arbitrary}$ applied to $x$.
Function.partialInvdefMathlib.Logic.Function.Basic, function or constantWording
the partial inverse of f and b (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $b$ be an element of $x_{1}$. Then the partial inverse of $f$ and $b$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $a$ of $x$, such that $\EqtMACRoH {f (a)}{b}$, the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $\operatorname{none}$.
Function.sometimesdefMathlib.Logic.Function.Basic, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{sometimes}$ applied to $f$ is an element of $x_{1}$ defined as $\mathrm{dite}$ applied to $\mathrm{Nonempty}$ applied to $x$, the function that maps $h_{1}$ to $f$ applied to $\operatorname{choice}$ applied to $h_{1}$ and the function that maps $h_{2}$ to $\operatorname{choice}$ applied to $h$.
Function.surjInvdefMathlib.Logic.Function.Basic, function or constantWording
the inverse of h and b (from the docstring)
English
Assume that $\operatorname{Surjective}$ holds for $f$. Let $b$ be an element of $x_{1}$. Then the inverse of $h$ and $b$ is an element of $x$ defined as $\operatorname{choose}$ applied to $h$ applied to $b$.
Function.updatedefMathlib.Logic.Function.Basic, function or constantEnglish
Let $f$ be a function from elements $a_{1}$ of $x$ to elements of $x_{1}$ applied to $a_{1}$. Let $\mathrm{a'}$ and $a$ be elements of $x$. Let $v$ be an element of $x_{1}$ applied to $\mathrm{a'}$. Then $\operatorname{update}$ applied to $a_{1}$, $f$, $\mathrm{a'}$, $v$ and $a$ is an element of $x_{1}$ applied to $a$ defined as the function that maps $a$ to $\mathrm{dite}$ applied to $\EqtMACRoH {v}{f}$, the function that maps $h$ to $\operatorname{ndrec}$ applied to $\mathrm{a'}$ and $\operatorname{symm}$ applied to $h$, the function that maps $h_{1}$ to $a_{1}$ applied to $v$ and $a$.
Set.SeparatesPointsdefMathlib.Logic.Function.Basic, predicateEnglish
Let $A$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1})$. Then $\operatorname{SeparatesPoints}$ holds for $A$, if for all elements $x_{2}$ and $y$ of $x$, if $x_{2} \neq y$, then there exists a function $f$ from elements of $x$ to elements of $x_{1}$, such that $f$ is an element of $A$ and $f (x_{2})\neq f (y)$.
Set.piecewisedefMathlib.Logic.Function.Basic, function or constantEnglish
Let $s$ be an element of $\wp x$. Let $f$ be a function from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$. Let $g$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then $\operatorname{piecewise}$ applied to $s$, $i_{2}$, $f$, $i_{1}$, $g$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $g$ and $i$ to $\iteMACRoG {(\MembershipmemMACRoT {s}{i_{1}})}{i_{2} (i_{1})}{f (i_{1})}$.
Function.CoequalizerdefMathlib.Logic.Function.Coequalizer, typeWording
coequalizer of f and g (from the name)
English
Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Then a coequalizer of $f$ and $g$ is an element of the function that maps $f$ and $g$ to $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $f$ and $g$.
Function.Coequalizer.RelinductiveMathlib.Logic.Function.Coequalizer, predicateEnglish
Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ and $x_{3}$ be elements of $x_{1}$. Then we can say that $\operatorname{Rel}$ holds for $f$, $g$, $x_{2}$ and $x_{3}$.
Function.Coequalizer.descdefMathlib.Logic.Function.Coequalizer, function or constantEnglish
Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x_{2}$ such that $\EqtMACRoH {\operatorname{comp} (u , f)}{\operatorname{comp} (u , g)}$. Let $x_{3}$ be a coequalizer of $f$ and $g$. Then $\operatorname{desc}$ applied to $f$, $g$, $u$, $\mathrm{hu}$ and $x_{3}$ is an element of $x_{2}$.
Function.Coequalizer.mkdefMathlib.Logic.Function.Coequalizer, function or constantEnglish
Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{mk}$ applied to $f$, $g$ and $x_{2}$ is a coequalizer of $f$ and $g$ defined as $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $f$ and $g$ and $x_{2}$.
CompTripleclassMathlib.Logic.Function.CompTypeclasses, predicateEnglish
Let $x$ be a function from elements of $M$ to elements of $N$. Let $x_{1}$ be a function from elements of $N$ to elements of $P$. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $M$ to elements of $P$. Then we can say that $\mathrm{CompTriple}$ holds for $x$, $x_{1}$ and $x_{2}$.
CompTriple.IsIdclassMathlib.Logic.Function.CompTypeclasses, predicateWording
x is a identity (from the name)
English
Let $x$ be a function from elements of $M$ to elements of $M$. Then we can say that $x$ is an identity.
Function.CommutedefMathlib.Logic.Function.Conjugate, predicateEnglish
Let $f$ and $g$ be functions from elements of $x$ to elements of $x$. Then $\operatorname{Commute}$ holds for $f$ and $g$, if $\operatorname{Semiconj}$ holds for $f$, $g$ and $g$.
Function.SemiconjdefMathlib.Logic.Function.Conjugate, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{ga}$ be a function from elements of $x$ to elements of $x$. Let $\mathrm{gb}$ be a function from elements of $x_{1}$ to elements of $x_{1}$. Then $\operatorname{Semiconj}$ holds for $f$, $\mathrm{ga}$ and $\mathrm{gb}$, if for all elements $x_{2}$ of $x$, $\EqtMACRoH {f (\mathrm{ga} (x_{2}))}{\mathrm{gb} (f (x_{2}))}$.
Function.Semiconj₂defMathlib.Logic.Function.Conjugate, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{ga}$ be a function from elements of $x$ and elements of $x$ to elements of $x$. Let $\mathrm{gb}$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to elements of $x_{1}$. Then $\mathrm{Function\_\_Semiconj\_u2082\_}$ holds for $f$, $\mathrm{ga}$ and $\mathrm{gb}$, if for all elements $x_{2}$ and $y$ of $x$, $\EqtMACRoH {f (\mathrm{ga} (x_{2} , y))}{\mathrm{gb} (f (x_{2}), f (y))}$.
Function.IsConstdefMathlib.Logic.Function.Const, predicateWording
f is constant (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is constant, if for all elements $x_{2}$ and $y$ of $x$, $\EqtMACRoH {f (x_{2})}{f (y)}$.
Function.BijectivedefMathlib.Logic.Function.Defs, predicateWording
f is bijective (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is bijective, if $f$ is injective and $\operatorname{Surjective}$ holds for $f$.
Function.IsFixedPtdefMathlib.Logic.Function.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{1}$ be an element of $x$. Then $\operatorname{IsFixedPt}$ holds for $f$ and $x_{1}$, if $\EqtMACRoH {f (x_{1})}{x_{1}}$.
Function.bicompldefMathlib.Logic.Function.Defs, function or constantEnglish
Let $f$ be a function from elements of $x_{2}$ and elements of $x_{3}$ to elements of $x_{4}$. Let $g$ be a function from elements of $x$ to elements of $x_{2}$. Let $h$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{bicompl}$ applied to $f$, $g$, $h$, $a$ and $b$ is an element of $x_{4}$ defined as $f$ applied to $g$ applied to $a$ and $h$ applied to $b$.
Function.bicomprdefMathlib.Logic.Function.Defs, function or constantEnglish
Let $f$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Let $g$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{bicompr}$ applied to $f$, $g$, $a$ and $b$ is an element of $x_{3}$ defined as $f$ applied to $g$ applied to $a$ and $b$.
Function.dcompdefMathlib.Logic.Function.Defs, function or constantEnglish
Let $f$ be a function from elements $x_{5}$ of $x$ and elements $y$ of $x_{1}$ applied to $x_{5}$ to elements of $x_{2}$ applied to $x_{5}$ and $y$. Let $g$ be a function from elements $x_{4}$ of $x$ to elements of $x_{1}$ applied to $x_{4}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{dcomp}$ applied to $x_{5}$, $y$, $f$, $x_{4}$, $g$ and $x_{3}$ is an element of $x_{2}$ applied to $x_{3}$ and $g$ applied to $x_{3}$ defined as the function that maps $x_{4}$, $g$ and $x_{3}$ to $x_{5}$ applied to $f$, $y$ applied to $f$, $x_{4}$, $g$ and $x_{3}$.
Function.diagdefMathlib.Logic.Function.Defs, function or constantWording
the diagonal of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the diagonal of $x_{1}$ is an element of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\ProdmkMACRoU {x_{1}}{x_{1}}$.
Function.onFundefMathlib.Logic.Function.Defs, function or constantEnglish
Let $f$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ and $x_{4}$ be elements of $x$. Then $\operatorname{onFun}$ applied to $f$, $g$, $x_{3}$ and $x_{4}$ is an element of $x_{2}$ defined as $f$ applied to $g$ applied to $x_{3}$ and $g$ applied to $x_{4}$.
Function.proddefMathlib.Logic.Function.Defs, function or constantWording
the product of i2 and g (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$. Let $g$ be a function from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then the product of $f$ and $i_{1}$ is an element of $\mathrm{Prod}$ applied to $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$ defined as the function that maps $g$ and $i$ to $\ProdmkMACRoU {i_{2} (i_{1})}{f (i_{1})}$.
Function.swapdefMathlib.Logic.Function.Defs, function or constantWording
the swap of x4 and y1 (from the name)
English
Let $f$ be a function from elements $x_{4}$ of $x$ and elements $y_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $x_{4}$ and $y_{1}$. Let $y$ be an element of $x_{1}$. Let $x_{3}$ be an element of $x$. Then the swap of $y_{1}$ and $f$ is an element of $x_{2}$ applied to $x_{3}$ and $y$ defined as the function that maps $y$ and $x_{3}$ to $x_{4}$ applied to $f$, $y_{1}$, $y$ and $x_{3}$.
Pi.mapdefMathlib.Logic.Function.Defs, function or constantWording
the map of i2 and x3 (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ and elements of $x_{1}$ applied to $i_{2}$ to elements of $x_{2}$ applied to $i_{2}$. Let $x_{3}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then the map of $f$ and $i_{1}$ is an element of $x_{2}$ applied to $i$ defined as the function that maps $x_{3}$ and $i$ to $i_{2}$ applied to $i_{1}$, $f$ applied to $i_{1}$, $x_{3}$ and $i$.
DependsOndefMathlib.Logic.Function.DependsOn, predicateEnglish
Let $f$ be a function from functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ to elements of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{DependsOn}$ holds for $f$ and $s$, if for all functions $x_{3}$ from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$, for all functions $y$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$, if for all elements $i$ of $x$, if $i$ is an element of $s$, then $\EqtMACRoH {x_{3} (i)}{y (i)}$, then $\EqtMACRoH {f (x_{3})}{f (y)}$.