Equiv.Finset.proddefMathlib.Data.Finset.Prod, function or constantWording
the product of s and t (from the docstring)
English
Let $s$ be a finite set of $x$. Let $t$ be a finite set of $x_{1}$. Then the product of $s$ and $t$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{sprod} (s , t)}{x_{2}})})}{\mathrm{Prod} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}, \SubtypeSet {x_{4}}{(\MembershipmemMACRoT {t}{x_{4}})})}$.
Finset.diagdefMathlib.Data.Finset.Prod, function or constantWording
the diagonal of s (from the name)
English
Let $s$ be a finite set of $x$. Then the diagonal of $s$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x$ defined as the map of $\operatorname{mk}$ applied to $\operatorname{diag}$ and $\mathrm{Function\_\_diag\_injective}$ and $s$.
Finset.offDiagdefMathlib.Data.Finset.Prod, function or constantEnglish
Let $s$ be a finite set of $x$. Then $\operatorname{offDiag}$ applied to $s$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x$.
Finset.productdefMathlib.Data.Finset.Prod, function or constantWording
the product of s and t (from the name)
English
Let $s$ be a finite set of $x$. Let $t$ be a finite set of $x_{1}$. Then the product of $s$ and $t$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
Finset.rangedefMathlib.Data.Finset.Range, function or constantWording
the range of n (by hand)
English
Let $n$ be a natural number. Then the range of $n$ is a finite set of $\Natural$ defined as $\operatorname{mk}$ applied to the range of $n$ and $\mathrm{Multiset\_\_nodup\_range}$ applied to $n$.
notMemRangeEquivdefMathlib.Data.Finset.Range, function or constantEnglish
Let $k$ be a natural number. Then $\mathrm{notMemRangeEquiv}$ applied to $k$ is an equivalence from $\SubtypeSet {n}{\mathrm{not} (\MembershipmemMACRoT {\FinsetrangeMACRoN {k}}{n})}$ to $\Natural$.
Finset.SMulAntidiagonaldefMathlib.Data.Finset.SMulAntidiagonal, function or constantEnglish
Let $a$ be an element of $P$ such that $\operatorname{smulAntidiagonal}$ applied to $s$, $t$ and $a$ is finite. Then $\operatorname{SMulAntidiagonal}$ applied to $a$ and $h$ is a finite set of $\mathrm{Prod}$ applied to $G$ and $P$ defined as the finite set of $h$.
Finset.VAddAntidiagonaldefMathlib.Data.Finset.SMulAntidiagonal, function or constantEnglish
Let $a$ be an element of $P$ such that $\operatorname{vaddAntidiagonal}$ applied to $s$, $t$ and $a$ is finite. Then $\operatorname{VAddAntidiagonal}$ applied to $a$ and $h$ is a finite set of $\mathrm{Prod}$ applied to $G$ and $P$ defined as the finite set of $h$.
Finset.sigmadefMathlib.Data.Finset.Sigma, function or constantWording
the sigma of s and t (from the name)
English
Let $s$ be a finite set of $x$. Let $t$ be a function from elements $i_{1}$ of $x$ to finite sets of $x_{1}$ applied to $i_{1}$. Then the sigma of $s$ and $i_{1}$ is a finite set of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$.
Finset.sigmaLiftdefMathlib.Data.Finset.Sigma, function or constantWording
the sigma lift of i and a (from the name)
English
Let $f$ be a function from elements $i$ of $x$ and elements of $x_{1}$ applied to $i$ and elements of $x_{2}$ applied to $i$ to finite sets of $x_{3}$ applied to $i$. Let $a$ be an element of $\Sigma$ applied to $x_{1}$. Let $b$ be an element of $\Sigma$ applied to $x_{2}$. Then the sigma lift of $f$ and $a$ is a finite set of $\Sigma$ applied to $x_{3}$.
Finset.slicedefMathlib.Data.Finset.Slice, function or constantWording
the slice of x1 and r (from the name)
English
Let $x_{1}$ be a finite set of the set of finite sets of $x$. Let $r$ be a natural number. Then the slice of $x_{1}$ and $r$ is a finite set of the set of finite sets of $x$ defined as $\FinsetFilter {A}{\mathrm{Eq} (\FinsetcardMACRoM {A}, r)}{x_{1}}$.
Set.SizeddefMathlib.Data.Finset.Slice, predicateEnglish
Let $r$ be a natural number. Let $A$ be an element of the power set of the set of finite sets of $x$. Then $\operatorname{Sized}$ holds for $r$ and $A$, if for all finite sets $x_{1}$ of $x$, if $x_{1}$ is an element of $A$, then $\FinsetcardMACRoM {x_{1}}= r$.
Finset.orderEmbOfCardLedefMathlib.Data.Finset.Sort, function or constantWording
the order embedding of s and h (from the name)
English
Let $s$ be a finite set of $x$ such that $k \leq \FinsetcardMACRoM {s}$. Then the order embedding of $s$ and $h$ is an order embedding of $\mathrm{Fin}$ applied to $k$ and $x$.
Finset.orderEmbOfFindefMathlib.Data.Finset.Sort, function or constantWording
the order embedding of s and h (from the name)
English
Let $s$ be a finite set of $x$ such that $\FinsetcardMACRoM {s}= k$. Then the order embedding of $s$ and $h$ is an order embedding of $\mathrm{Fin}$ applied to $k$ and $x$ defined as the composition of the order embedding of the order isomorphism of $s$ and $h$ and the subtype of the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$.
Finset.orderIsoOfFindefMathlib.Data.Finset.Sort, function or constantWording
the order isomorphism of s and h (from the name)
English
Let $s$ be a finite set of $x$ such that $\FinsetcardMACRoM {s}= k$. Then the order isomorphism of $s$ and $h$ is an order isomorphism of $\mathrm{Fin}$ applied to $k$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
Finset.sortdefMathlib.Data.Finset.Sort, function or constantWording
the sort of s and r (from the name)
English
Let $s$ be a finite set of $x$. Let $r$ be an element of $\mathrm{autoParam}$ applied to the set of functions from elements of $x$ and elements of $x$ to propositions and $\mathrm{Finset\_\_sort\_\_\_auto\_1}$. Then the sort of $s$ and $r$ is a list of elements of $x$ defined as the sort of the value of $s$ and $r$.
Fintype.orderIsoFinOfCardEqdefMathlib.Data.Finset.Sort, function or constantEnglish
Let $x$ be a set such that the cardinality of $x$ is equal to $k$. Then $\operatorname{orderIsoFinOfCardEq}$ applied to $x$ and $h$ is an order isomorphism of $\mathrm{Fin}$ applied to $k$ and $x$ defined as the composition of the order isomorphism of the universal set and $h$ and the composition of the order isomorphism of the universal set and the universal set and the universal set.
Finset.disjSumdefMathlib.Data.Finset.Sum, function or constantEnglish
Let $s$ be a finite set of $x$. Let $t$ be a finite set of $x_{1}$. Then $\operatorname{disjSum}$ applied to $s$ and $t$ is a finite set of $\mathrm{Sum}$ applied to $x$ and $x_{1}$.
Finset.sumEquivdefMathlib.Data.Finset.Sum, function or constantWording
the sum equivalence (from the name)
English
The sum equivalence is an order isomorphism of the set of finite sets of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to the set of finite sets of $x$ and the set of finite sets of $x_{1}$.
Finset.toLeftdefMathlib.Data.Finset.Sum, function or constantWording
the left of u (from the name)
English
Let $u$ be a finite set of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then the left of $u$ is a finite set of $x$.
Finset.toRightdefMathlib.Data.Finset.Sum, function or constantWording
the right of u (from the name)
English
Let $u$ be a finite set of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Then the right of $u$ is a finite set of $x_{1}$.
Finset.complsdefMathlib.Data.Finset.Sups, function or constantEnglish
Let $x_{2}$ be a finite set of $x$. Then $\operatorname{compls}$ applied to $x_{2}$ is a finite set of $x$ defined as the map of $\operatorname{mk}$ applied to $\operatorname{compl}$ and $\mathrm{compl\_injective}$ and $x_{2}$.
Finset.diffsdefMathlib.Data.Finset.Sups, function or constantEnglish
Let $x_{3}$ and $x_{4}$ be finite sets of $x$. Then $\operatorname{diffs}$ applied to $x_{3}$ and $x_{4}$ is a finite set of $x$ defined as the image of $x_{3}$ and $x_{4}$.
Finset.disjSupsdefMathlib.Data.Finset.Sups, function or constantEnglish
Let $s$ and $t$ be finite sets of $x$. Then $\operatorname{disjSups}$ applied to $s$ and $t$ is a finite set of $x$ defined as the forward image of $\FinsetFilter {\mathrm{ab1}}{\mathrm{Disjoint} (\ProdfstMACRoZ {\mathrm{ab1}}, \ProdsndMACRoAA {\mathrm{ab1}})}{\operatorname{sprod} (s , t)}$ under the function that maps $\mathrm{ab}$ to $\MaxmaxMACRoAF {\ProdfstMACRoZ {\mathrm{ab}}}{\ProdsndMACRoAA {\mathrm{ab}}}$.
Finset.symdefMathlib.Data.Finset.Sym, function or constantWording
the symmetric power of s and n (from the name)
English
Let $s$ be a finite set of $x$. Let $n$ be a natural number. Then the symmetric power of $s$ and $n$ is a finite set of the set of symmetric powers of $x$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{Finset\_\_sym\_\_\_f}$ applied to $s$.
Finset.sym2defMathlib.Data.Finset.Sym, function or constantWording
the symmetric power of s (from the name)
English
Let $s$ be a finite set of $x$. Then the symmetric power of $s$ is a finite set of the set of symmetric squares of $x$.
Finset.symInsertEquivdefMathlib.Data.Finset.Sym, function or constantEnglish
Assume that it is not the case that $\MembershipmemMACRoT {s}{a}$. Then $\operatorname{symInsertEquiv}$ applied to $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{sym} (\operatorname{insert} (a , s), n)}{x_{2}})})}{\Sigma (\lambda i . \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{sym} (s , n - \operatorname{val} (i))}{x_{3}})})}$.
Finset.biUniondefMathlib.Data.Finset.Union, function or constantEnglish
Let $s$ be a finite set of $x$. Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$. Then $\operatorname{biUnion}$ applied to $s$ and $t$ is a finite set of $x_{1}$ defined as the finite set of $\operatorname{bind}$ applied to the value of $s$ and the function that maps $a$ to the value of $t$ applied to $a$.
Finset.disjiUniondefMathlib.Data.Finset.Union, function or constantEnglish
Let $s$ be a finite set of $x$. Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$ such that $s$ is a pairwise disjoint with respect to $t$. Then $\operatorname{disjiUnion}$ applied to $s$, $t$ and $\mathrm{hf}$ is a finite set of $x_{1}$.
Function.updateFinsetdefMathlib.Data.Finset.Update, function or constantEnglish
Let $x_{3}$ be a function from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$. Let $s$ be a finite set of $x$. Let $y$ be a function from elements $i_{1}$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then $\operatorname{updateFinset}$ applied to $i_{2}$, $x_{3}$, $s$, $i_{1}$, $y$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $y$ and $i$ to $\mathrm{dite}$ applied to $\MembershipmemMACRoT {x_{3}}{i_{1}}$, the function that maps $\mathrm{hi}$ to $s$ applied to $i_{1}$, the function that maps $\mathrm{hi1}$ to $i_{2}$ applied to $i_{1}$, $y$ and $i$.
AList.lookupFinsuppdefMathlib.Data.Finsupp.AList, function or constantEnglish
Let $l$ be a list of the function that maps $\mathrm{\_x}$ to $M$. Then $\operatorname{lookupFinsupp}$ applied to $l$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.toAListdefMathlib.Data.Finsupp.AList, function or constantWording
the list of f (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the list of $f$ is a list of the function that maps $\mathrm{\_x}$ to $M$.
Finsupp.antidiagonal'defMathlib.Data.Finsupp.Antidiagonal, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{antidiagonal'}$ applied to $f$ is an element of $\FinsuppMACRoQ {\mathrm{Prod} (\FinsuppMACRoQ {x}{\Natural}, \FinsuppMACRoQ {x}{\Natural})}{\Natural}$ defined as $\operatorname{toFinsupp}$ applied to the map of $\operatorname{map}$ applied to $\operatorname{coe}$ applied to the finitely supported function and $\operatorname{coe}$ applied to the finitely supported function and $\operatorname{antidiagonal}$ applied to $\operatorname{toMultiset}$ applied to $f$.
Finsupp.comapDomaindefMathlib.Data.Finsupp.Basic, function or constantWording
the preimage domain of f and l (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be an element of $\FinsuppMACRoQ {x_{1}}{M}$ such that $f$ is injective on the preimage of $f$ and the support of $l$. Then the preimage domain of $f$ and $l$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.comapDomain.addMonoidHomdefMathlib.Data.Finsupp.Basic, function or constantWording
the additive monoid homomorphism of hf (from the name)
English
Assume that $f$ is injective. Then the additive monoid homomorphism of $\mathrm{hf}$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x_{1}}{M}$ and $\FinsuppMACRoQ {x}{M}$.
Finsupp.currydefMathlib.Data.Finsupp.Basic, function or constantWording
the curry of f (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$. Then the curry of $f$ is an element of $\FinsuppMACRoQ {x}{(\FinsuppMACRoQ {x_{1}}{M})}$.
Finsupp.curryAddEquivdefMathlib.Data.Finsupp.Basic, function or constantWording
the curry additive equivalence (from the name)
English
The curry additive equivalence is an additive equivalence of $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$ and $\FinsuppMACRoQ {x}{(\FinsuppMACRoQ {x_{1}}{M})}$.
Finsupp.curryEquivdefMathlib.Data.Finsupp.Basic, function or constantWording
the curry equivalence (from the name)
English
The curry equivalence is an equivalence from $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$ to $\FinsuppMACRoQ {x}{(\FinsuppMACRoQ {x_{1}}{M})}$ defined as $\operatorname{mk}$ applied to $\operatorname{curry}$, $\operatorname{uncurry}$, $\mathrm{Finsupp\_\_uncurry\_curry}$ and $\mathrm{Finsupp\_\_curry\_uncurry}$.
Finsupp.domCongrdefMathlib.Data.Finsupp.Basic, function or constantWording
the domain congruence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the domain congruence of $e$ is an additive equivalence of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{1}}{M}$.
Finsupp.equivCongrLeftdefMathlib.Data.Finsupp.Basic, function or constantWording
the left equivalence congruence of f (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Then the left equivalence congruence of $f$ is an equivalence from $\FinsuppMACRoQ {x}{M}$ to $\FinsuppMACRoQ {x_{1}}{M}$.
Finsupp.equivMapDomaindefMathlib.Data.Finsupp.Basic, function or constantWording
the equivalence map domain of f and l (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Let $l$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the equivalence map domain of $f$ and $l$ is an element of $\FinsuppMACRoQ {x_{1}}{M}$.
Finsupp.extendDomaindefMathlib.Data.Finsupp.Basic, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {(\SubtypeSet {x_{3}}{P (x_{3})})}{M}$. Then $\operatorname{extendDomain}$ applied to $f$ is an element of $\FinsuppMACRoQ {x}{M}$ defined as $\operatorname{piecewise}$ applied to $f$ and $0$.
Finsupp.filterdefMathlib.Data.Finsupp.Basic, function or constantWording
the filter of p and f (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the filter of $p$ and $f$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.filterAddHomdefMathlib.Data.Finsupp.Basic, function or constantWording
the filter additive homomorphism of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the filter additive homomorphism of $p$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{M}$.
Finsupp.frangedefMathlib.Data.Finsupp.Basic, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then $\operatorname{frange}$ applied to $f$ is a finite set of $M$ defined as the forward image of the support of $f$ under $\operatorname{coe}$ applied to $f$.
Finsupp.graphdefMathlib.Data.Finsupp.Basic, function or constantWording
the graph of f (from the docstring)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the graph of $f$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $M$.
Finsupp.mapDomaindefMathlib.Data.Finsupp.Basic, function or constantWording
the map domain of f and x3 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the map domain of $f$ and $x_{3}$ is an element of $\FinsuppMACRoQ {x_{1}}{M}$ defined as the sum of $x_{3}$ and the function that maps $a$ to $\FinsuppsingleMACRoS {f (a)}$.
Finsupp.mapDomain.addMonoidHomdefMathlib.Data.Finsupp.Basic, function or constantWording
the additive monoid homomorphism of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{1}}{M}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mapDomain}$ applied to $f$ and $\mathrm{Finsupp\_\_mapDomain\_zero}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Finsupp\_\_mapDomain\_add}$.
Finsupp.mapDomainEmbeddingdefMathlib.Data.Finsupp.Basic, function or constantWording
the map domain embedding of f (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Then the map domain embedding of $f$ is an embedding of $\FinsuppMACRoQ {x}{\Natural}$ and $\FinsuppMACRoQ {x_{1}}{\Natural}$.
Finsupp.piecewisedefMathlib.Data.Finsupp.Basic, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {(\SubtypeSet {x_{3}}{P (x_{3})})}{M}$. Let $g$ be an element of $\FinsuppMACRoQ {(\SubtypeSet {a}{\mathrm{not} (P (a))})}{M}$. Then $\operatorname{piecewise}$ applied to $f$ and $g$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.restrictSupportEquivdefMathlib.Data.Finsupp.Basic, function or constantEnglish
Let $s$ be an element of $\wp x$. Let $M$ be a set. Then $\operatorname{restrictSupportEquiv}$ applied to $s$ and $M$ is an equivalence from $\SubtypeSet {f}{\mathrm{Leq} (\FinsuppsupportMACRoR {f}, s)}$ to the set of finitely supported functions from the set of elements of $s$ to $M$.
Finsupp.sigmaFinsuppAddEquivPiFinsuppdefMathlib.Data.Finsupp.Basic, function or constantWording
the sigma finitely supported function additive equivalence product finitely supported function (from the name)
English
The sigma finitely supported function additive equivalence product finitely supported function is an additive equivalence of $\FinsuppMACRoQ {\Sigma (\lambda j . x_{3} (j))}{x_{2}}$ and the set of functions from elements $j_{1}$ of $x$ to elements of $\FinsuppMACRoQ {x_{3} (j_{1})}{x_{2}}$.
Finsupp.sigmaFinsuppEquivPiFinsuppdefMathlib.Data.Finsupp.Basic, function or constantWording
the sigma finitely supported function equivalence product finitely supported function (from the name)
English
The sigma finitely supported function equivalence product finitely supported function is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {\Sigma (\lambda j . x_{3} (j))}{x})}{(\mathrm{Elem} (x_{1})\rightarrow \FinsuppMACRoQ {x_{3} (j_{1})}{x})}$.
Finsupp.splitdefMathlib.Data.Finsupp.Basic, function or constantWording
the split of l and i (from the name)
English
Let $l$ be an element of $\FinsuppMACRoQ {\Sigma (\lambda i_{1} . x_{1} (i_{1}))}{M}$. Let $i$ be an element of $x$. Then the split of $l$ and $i$ is an element of $\FinsuppMACRoQ {x_{1} (i)}{M}$.
Finsupp.splitCompdefMathlib.Data.Finsupp.Basic, function or constantWording
the split composition of l and g (from the name)
English
Let $l$ be an element of $\FinsuppMACRoQ {\Sigma (\lambda i_{2} . x_{1} (i_{2}))}{M}$. Let $g$ be a function from elements $i_{1}$ of $x$ and elements of $\FinsuppMACRoQ {x_{1} (i_{1})}{M}$ to elements of $N$ such that for all elements $i$ of $x$, for all elements $x_{4}$ of $\FinsuppMACRoQ {x_{1} (i)}{M}$, $\EqtMACRoH {x_{4}}{0}$, if and only if $\EqtMACRoH {g (i , x_{4})}{0}$. Then the split composition of $l$ and $i_{1}$ is an element of $\FinsuppMACRoQ {x}{N}$.
Finsupp.splitSupportdefMathlib.Data.Finsupp.Basic, function or constantWording
the split support of l (from the name)
English
Let $l$ be an element of $\FinsuppMACRoQ {\Sigma (\lambda i . x_{1} (i))}{M}$. Then the split support of $l$ is a finite set of $x$ defined as the forward image of the support of $l$ under $\operatorname{fst}$.
Finsupp.subtypeDomaindefMathlib.Data.Finsupp.Basic, function or constantWording
the subtype domain of p and f (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the subtype domain of $p$ and $f$ is an element of $\FinsuppMACRoQ {(\SubtypeSet {x_{2}}{p (x_{2})})}{M}$.
Finsupp.subtypeDomainAddMonoidHomdefMathlib.Data.Finsupp.Basic, function or constantWording
the subtype domain additive monoid homomorphism (from the name)
English
The subtype domain additive monoid homomorphism is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {(\SubtypeSet {x_{2}}{p (x_{2})})}{M}$.
Finsupp.sumElimdefMathlib.Data.Finsupp.Basic, function or constantWording
the sum eliminator of f and g (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{x_{2}}$. Let $g$ be an element of $\FinsuppMACRoQ {x_{1}}{x_{2}}$. Then the sum eliminator of $f$ and $g$ is an element of $\FinsuppMACRoQ {\mathrm{Sum} (x , x_{1})}{x_{2}}$.
Finsupp.sumFinsuppAddEquivProdFinsuppdefMathlib.Data.Finsupp.Basic, function or constantWording
the sum finitely supported function additive equivalence product finitely supported function (from the name)
English
The sum finitely supported function additive equivalence product finitely supported function is an additive equivalence of $\FinsuppMACRoQ {\mathrm{Sum} (x_{1} , x_{2})}{M}$ and $\mathrm{Prod}$ applied to $\FinsuppMACRoQ {x_{1}}{M}$ and $\FinsuppMACRoQ {x_{2}}{M}$.
Finsupp.sumFinsuppEquivProdFinsuppdefMathlib.Data.Finsupp.Basic, function or constantWording
the sum finitely supported function equivalence product finitely supported function (from the name)
English
The sum finitely supported function equivalence product finitely supported function is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {\mathrm{Sum} (x , x_{1})}{x_{2}})}{\mathrm{Prod} (\FinsuppMACRoQ {x}{x_{2}}, \FinsuppMACRoQ {x_{1}}{x_{2}})}$.
Finsupp.uncurrydefMathlib.Data.Finsupp.Basic, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {x}{(\FinsuppMACRoQ {x_{1}}{M})}$. Then $\operatorname{uncurry}$ applied to $f$ is an element of $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$.
FinsuppstructureMathlib.Data.Finsupp.Defs, typeWording
finitely supported function from x to M (by hand)
English
Let $x$ and $M$ be sets. Then $\FinsuppMACRoQ {x}{M}$ is a set.
Finsupp.embDomaindefMathlib.Data.Finsupp.Defs, function or constantWording
the embedding domain of f and v (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $v$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the embedding domain of $f$ and $v$ is an element of $\FinsuppMACRoQ {x_{1}}{M}$.
Finsupp.equivFunOnFinitedefMathlib.Data.Finsupp.Defs, function or constantEnglish
$\operatorname{equivFunOnFinite}$ is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {x}{M})}{(\mathrm{Elem} (x)\rightarrow M)}$.
Finsupp.mapRangedefMathlib.Data.Finsupp.Defs, function or constantWording
the map range of f and g (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$ such that $\EqtMACRoH {f (0)}{0}$. Let $g$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the map range of $f$ and $g$ is an element of $\FinsuppMACRoQ {x}{N}$.
Finsupp.mapRange.equivdefMathlib.Data.Finsupp.Defs, function or constantWording
the equivalence of e and hf (from the name)
English
Let $e$ be an equivalence from $M$ to $N$ such that $\EqtMACRoH {e (0)}{0}$. Then the equivalence of $e$ and $\mathrm{hf}$ is an equivalence from $\FinsuppMACRoQ {x}{M}$ to $\FinsuppMACRoQ {x}{N}$.
Finsupp.ofSupportFinitedefMathlib.Data.Finsupp.Defs, function or constantWording
the finitely supported function of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $M$ such that the support of $f$ is finite. Then the finitely supported function of $f$ and $\mathrm{hf}$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.onFinsetdefMathlib.Data.Finsupp.Defs, function or constantEnglish
Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $M$ such that for all elements $a$ of $x$, if $f (a)\neq 0$, then $a$ is an element of $s$. Then $\operatorname{onFinset}$ applied to $s$, $f$ and $\mathrm{hf}$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.onFinsetSupportdefMathlib.Data.Finsupp.Defs, function or constantEnglish
Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{onFinsetSupport}$ applied to $s$ and $f$ is a finite set of $x$ defined as $\FinsetFilter {a}{\mathrm{Neq} (f (a), 0)}{s}$.
Finsupp.supportdefMathlib.Data.Finsupp.Defs, function or constantWording
the support of self (by hand)
English
Let $\mathrm{self}$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the support of $\mathrm{self}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Finsupp.toFundefMathlib.Data.Finsupp.Defs, function or constantWording
the underlying function of self and x2 (from the docstring)
English
Let $\mathrm{self}$ be an element of $\FinsuppMACRoQ {x}{M}$. Let $x_{2}$ be an element of $x$. Then the underlying function of $\mathrm{self}$ and $x_{2}$ is an element of $M$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
Finsupp.zipWithdefMathlib.Data.Finsupp.Defs, function or constantEnglish
Let $f$ be a function from elements of $M$ and elements of $N$ to elements of $O$ such that $\EqtMACRoH {f (0 , 0)}{0}$. Let $x_{4}$ be an element of $\FinsuppMACRoQ {x}{M}$. Let $x_{5}$ be an element of $\FinsuppMACRoQ {x}{N}$. Then $\operatorname{zipWith}$ applied to $f$, $\mathrm{hf}$, $x_{4}$ and $x_{5}$ is an element of $\FinsuppMACRoQ {x}{O}$.
Finsupp.consdefMathlib.Data.Finsupp.Fin, function or constantEnglish
Let $y$ be an element of $M$. Let $s$ be an element of $\FinsuppMACRoQ {\mathrm{Fin} (n)}{M}$. Then $\operatorname{cons}$ applied to $y$ and $s$ is an element of $\FinsuppMACRoQ {\mathrm{Fin} (n + 1)}{M}$ defined as $\operatorname{symm}$ applied to $\operatorname{equivFunOnFinite}$ and $\operatorname{cons}$ applied to $y$ and $\operatorname{coe}$ applied to $s$.
Finsupp.taildefMathlib.Data.Finsupp.Fin, function or constantWording
the tail of s (from the name)
English
Let $s$ be an element of $\FinsuppMACRoQ {\mathrm{Fin} (n + 1)}{M}$. Then the tail of $s$ is an element of $\FinsuppMACRoQ {\mathrm{Fin} (n)}{M}$ defined as $\operatorname{symm}$ applied to $\operatorname{equivFunOnFinite}$ and $\operatorname{tail}$ applied to $\operatorname{coe}$ applied to $s$.
Finsupp.indicatordefMathlib.Data.Finsupp.Indicator, function or constantWording
the indicator of s and f (from the name)
English
Let $s$ be a finite set of $x$. Let $f$ be a function from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i}$ to elements of $x_{1}$. Then the indicator of $s$ and $i$ is an element of $\FinsuppMACRoQ {x}{x_{1}}$.
Finsupp.rangeIccdefMathlib.Data.Finsupp.Interval, function or constantWording
the range closed interval of f and g (from the name)
English
Let $f$ and $g$ be elements of $\FinsuppMACRoQ {x}{x_{1}}$. Then the range closed interval of $f$ and $g$ is a finitely supported function from $x$ to the set of finite sets of $x_{1}$.
Finsupp.rangeSingletondefMathlib.Data.Finsupp.Interval, function or constantWording
the range singleton of f (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{x_{1}}$. Then the range singleton of $f$ is a finitely supported function from $x$ to the set of finite sets of $x_{1}$.
Finsupp.LexdefMathlib.Data.Finsupp.Lex, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $N$ and elements of $N$ to propositions. Let $x_{2}$ and $y$ be elements of $\FinsuppMACRoQ {x}{N}$. Then $\operatorname{Lex}$ holds for $r$, $s$, $x_{2}$ and $y$, if $\operatorname{Lex}$ holds for $r$, the function that maps $x_{3}$ to $s$, $\operatorname{coe}$ applied to $x_{2}$ and $\operatorname{coe}$ applied to $y$.
MonomialOrderstructureMathlib.Data.Finsupp.MonomialOrder, typeWording
monomial order of x (from the name)
English
Let $x$ be a set. Then the monomial orders of $x$ are a basic type.
MonomialOrder.lexdefMathlib.Data.Finsupp.MonomialOrder, function or constantEnglish
$\operatorname{lex}$ is a monomial order of $x$.
MonomialOrder.syndefMathlib.Data.Finsupp.MonomialOrder, typeEnglish
Let $\mathrm{self}$ be a monomial order of $x$. Then an element of $\operatorname{syn}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
MonomialOrder.toSyndefMathlib.Data.Finsupp.MonomialOrder, function or constantEnglish
Let $\mathrm{self}$ be a monomial order of $x$. Then $\operatorname{toSyn}$ applied to $\mathrm{self}$ is an additive equivalence of $\FinsuppMACRoQ {x}{\Natural}$ and $\operatorname{syn}$ applied to $\mathrm{self}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.
MonomialOrder.toWithBotSyndefMathlib.Data.Finsupp.MonomialOrder, function or constantEnglish
Let $m$ be a monomial order of $x$. Then $\operatorname{toWithBotSyn}$ applied to $m$ is an additive equivalence of $\mathrm{WithBot}$ applied to $\FinsuppMACRoQ {x}{\Natural}$ and $\mathrm{WithBot}$ applied to $\operatorname{syn}$ applied to $m$ defined as $\operatorname{withBotCongr}$ applied to $\operatorname{toSyn}$ applied to $m$.
DegLexdefMathlib.Data.Finsupp.MonomialOrder.DegLex, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{DegLex}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Finsupp.DegLexdefMathlib.Data.Finsupp.MonomialOrder.DegLex, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from natural numbers and natural numbers to propositions. Let $x_{1}$ and $x_{2}$ be elements of $\FinsuppMACRoQ {x}{\Natural}$. Then $\operatorname{DegLex}$ holds for $r$, $s$, $x_{1}$ and $x_{2}$, if $\operatorname{onFun}$ holds for $\operatorname{Lex}$ applied to $s$ and $\operatorname{Lex}$ applied to $r$ and $s$, the function that maps $x_{1}$ to $\ProdmkMACRoU {\operatorname{degree} (x_{1})}{x_{1}}$, $x_{1}$ and $x_{2}$.
MonomialOrder.degLexdefMathlib.Data.Finsupp.MonomialOrder.DegLex, function or constantEnglish
$\operatorname{degLex}$ is a monomial order of $x$.
ofDegLexdefMathlib.Data.Finsupp.MonomialOrder.DegLex, function or constantEnglish
$\mathrm{ofDegLex}$ is an element of $\EquivMACRoAE {\mathrm{DegLex} (x)}{x}$ defined as the identity of $\mathrm{DegLex}$ applied to $x$.
toDegLexdefMathlib.Data.Finsupp.MonomialOrder.DegLex, function or constantEnglish
$\mathrm{toDegLex}$ is an element of $\EquivMACRoAE {x}{\mathrm{DegLex} (x)}$ defined as the identity of $x$.
Finsupp.orderIsoMultisetdefMathlib.Data.Finsupp.Multiset, function or constantWording
the order isomorphism multiset (from the name)
English
The order isomorphism multiset is an order isomorphism of $\FinsuppMACRoQ {x}{\Natural}$ and the set of multisets of $x$.
Finsupp.toMultisetdefMathlib.Data.Finsupp.Multiset, function or constantWording
the multiset (from the name)
English
The multiset is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{\Natural}$ and the set of multisets of $x$.
Multiset.toFinsuppdefMathlib.Data.Finsupp.Multiset, function or constantWording
the finitely supported function (from the name)
English
The finitely supported function is an additive equivalence of the set of multisets of $x$ and $\FinsuppMACRoQ {x}{\Natural}$.
Sym.equivNatSumdefMathlib.Data.Finsupp.Multiset, function or constantWording
the equivalence natural sum of x and n (from the name)
English
Let $x$ be a set. Let $n$ be an element of $\Natural$. Then the equivalence natural sum of $x$ and $n$ is an element of $\EquivMACRoAE {\mathrm{Sym} (x , n)}{(\SubtypeSet {P}{\mathrm{Eq} (\operatorname{sum} (P , \lambda x_{2} . \mathrm{id}), n)})}$.
Sym.equivNatSumOfFintypedefMathlib.Data.Finsupp.Multiset, function or constantWording
the equivalence natural sum of x and n (from the name)
English
Let $x$ be a set. Let $n$ be a natural number. Then the equivalence natural sum of $x$ and $n$ is an equivalence from the set of symmetric powers of $x$ and $n$ to $\SubtypeSet {P}{\mathrm{Eq} (\FinsetSum {\FinsetunivMACRoAC}{i}{P (i)}, n)}$.
Finsupp.neLocusdefMathlib.Data.Finsupp.NeLocus, function or constantEnglish
Let $f$ and $g$ be elements of $\FinsuppMACRoQ {x}{N}$. Then $\operatorname{neLocus}$ applied to $f$ and $g$ is a finite set of $x$ defined as $\FinsetFilter {x_{4}}{\mathrm{Neq} (f (x_{4}), g (x_{4}))}{(\UnionunionMACRoAB {\FinsuppsupportMACRoR {f}}{\FinsuppsupportMACRoR {g}})}$.
Finsupp.Internal.elabSingle₀defMathlib.Data.Finsupp.Notation, function or constantEnglish
generation took over the time limit
Finsupp.Internal.elabUpdate₀defMathlib.Data.Finsupp.Notation, function or constantEnglish
generation took over the time limit
Finsupp.fun₀defMathlib.Data.Finsupp.Notation, function or constantWording
the function (from the name)
English
generation took over the time limit
Finsupp.fun₀.matchAltsdefMathlib.Data.Finsupp.Notation, function or constantEnglish
generation took over the time limit
Finsupp.fun₀.matchAlts.parenthesizerdefMathlib.Data.Finsupp.Notation, function or constantEnglish
generation took over the time limit
Finsupp.fun₀.parenthesizerdefMathlib.Data.Finsupp.Notation, function or constantEnglish
generation took over the time limit
Finsupp.optionElimdefMathlib.Data.Finsupp.Option, function or constantWording
the option eliminator of y and f (from the name)
English
Let $y$ be an element of $M$. Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the option eliminator of $y$ and $f$ is an element of $\FinsuppMACRoQ {\mathrm{Option} (x)}{M}$ defined as the inverse function of the option equivalence and $\ProdmkMACRoU {y}{f}$.
Finsupp.optionEquivdefMathlib.Data.Finsupp.Option, function or constantWording
the option equivalence (from the name)
English
The option equivalence is an element of $\EquivMACRoAE {(\FinsuppMACRoQ {\mathrm{Option} (x)}{M})}{\mathrm{Prod} (M , \FinsuppMACRoQ {x}{M})}$.
Finsupp.somedefMathlib.Data.Finsupp.Option, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {\mathrm{Option} (x)}{M}$. Then $\operatorname{some}$ applied to $f$ is an element of $\FinsuppMACRoQ {x}{M}$.
Quot.liftFinsuppdefMathlib.Data.Finsupp.Quotient, function or constantWording
the lift finitely supported function of f and h (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{x_{1}}$ such that for all elements $a$ and $b$ of $x$, if $r$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then the lift finitely supported function of $f$ and $h$ is an element of $\FinsuppMACRoQ {\mathrm{Quot} (r)}{x_{1}}$.
Quotient.liftFinsuppdefMathlib.Data.Finsupp.Quotient, function or constantWording
the lift finitely supported function of f and h (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{x_{1}}$ such that for all elements $a$ and $b$ of $x$, if $\operatorname{r}$ holds for $a$ and $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then the lift finitely supported function of $f$ and $h$ is an element of $\FinsuppMACRoQ {\mathrm{Quotient} (s)}{x_{1}}$ defined as the lift finitely supported function of $f$ and $h$.
Setoid.liftFinsuppEquivdefMathlib.Data.Finsupp.Quotient, function or constantWording
the lift finitely supported function equivalence of s and hs (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Assume that for all elements $a_{1}$ of $x$, $\operatorname{ofPred}$ applied to the function that maps $b_{1}$ to $\operatorname{r}$ applied to $b_{1}$ and $a_{1}$ is finite. Then the lift finitely supported function equivalence of $s$ and $\mathrm{hs}$ is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . \mathrm{forall} (x , \lambda b . \mathrm{if} (\operatorname{r} (a , b), \EqtMACRoH {f (a)}{f (b)})))}$ to $\FinsuppMACRoQ {\mathrm{Quotient} (s)}{x_{1}}$.
Finsupp.DistribMulActionHom.singledefMathlib.Data.Finsupp.SMul, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{single}$ applied to $a$ is a distributive multiplicative action homomorphism of $M$ and $\FinsuppMACRoQ {x}{M}$.
Finsupp.embSigmadefMathlib.Data.Finsupp.Sigma, function or constantWording
the embedding sigma of f (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x_{1} (k)}{M}$. Then the embedding sigma of $f$ is an element of $\FinsuppMACRoQ {\Sigma (\lambda k_{1} . x_{1} (k_{1}))}{M}$ defined as the embedding domain of the sigma of $k$ and $f$.
Finsupp.erasedefMathlib.Data.Finsupp.Single, function or constantEnglish
Let $a$ be an element of $x$. Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then $\operatorname{erase}$ applied to $a$ and $f$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.singledefMathlib.Data.Finsupp.Single, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $M$. Then $\FinsuppsingleMACRoS {a}{b}$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.uniqueEquivdefMathlib.Data.Finsupp.Single, function or constantWording
the unique equivalence of a (from the name)
English
Let $a$ be an element of $x$. Then the unique equivalence of $a$ is an equivalence from $\FinsuppMACRoQ {x}{M}$ to $M$.
Finsupp.updatedefMathlib.Data.Finsupp.Single, function or constantEnglish
Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Let $a$ be an element of $x$. Let $b$ be an element of $M$. Then $\operatorname{update}$ applied to $f$, $a$ and $b$ is an element of $\FinsuppMACRoQ {x}{M}$.
DFinsupp.toFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the finitely supported function of f (from the name)
English
Let $f$ be a finitely supported function of the function that maps $x_{4}$ to $M$. Then the finitely supported function of $f$ is an element of $\FinsuppMACRoQ {x}{M}$.
Finsupp.toDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the finitely supported function of f (from the name)
English
Let $f$ be an element of $\FinsuppMACRoQ {x}{M}$. Then the finitely supported function of $f$ is a finitely supported function of the function that maps $x_{2}$ to $M$ defined as $\operatorname{mk'}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{mk}$ applied to the value of the support of $f$.
finsuppAddEquivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the finitely supported function additive equivalence finitely supported function (from the name)
English
The finitely supported function additive equivalence finitely supported function is an additive equivalence of $\FinsuppMACRoQ {x}{M}$ and the set of finitely supported functions of the function that maps $x_{4}$ to $M$.
finsuppEquivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the finitely supported function equivalence finitely supported function (from the name)
English
The finitely supported function equivalence finitely supported function is an equivalence from $\FinsuppMACRoQ {x}{M}$ to the set of finitely supported functions of the function that maps $x_{4}$ to $M$ defined as $\operatorname{mk}$ applied to $\operatorname{toDFinsupp}$, $\operatorname{toFinsupp}$, $\mathrm{Finsupp\_\_toDFinsupp\_toFinsupp}$ and $\mathrm{DFinsupp\_\_toFinsupp\_toDFinsupp}$.
finsuppLequivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the finitely supported function linear equivalence finitely supported function of R (from the name)
English
Let $R$ be a set. Then the finitely supported function linear equivalence finitely supported function of $R$ is a linear equivalence of $\FinsuppMACRoQ {x}{M}$ and the set of finitely supported functions of the function that maps $x_{6}$ to $M$.
sigmaFinsuppAddEquivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the sigma finitely supported function additive equivalence finitely supported function (from the name)
English
The sigma finitely supported function additive equivalence finitely supported function is an additive equivalence of $\FinsuppMACRoQ {\Sigma (\lambda i . x_{1} (i))}{N}$ and the set of finitely supported functions of the function that maps $i_{1}$ to $\FinsuppMACRoQ {x_{1} (i_{1})}{N}$.
sigmaFinsuppEquivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the sigma finitely supported function equivalence finitely supported function (from the name)
English
The sigma finitely supported function equivalence finitely supported function is an equivalence from $\FinsuppMACRoQ {\Sigma (\lambda i . x_{1} (i))}{N}$ to the set of finitely supported functions of the function that maps $i_{1}$ to $\FinsuppMACRoQ {x_{1} (i_{1})}{N}$.
sigmaFinsuppLequivDFinsuppdefMathlib.Data.Finsupp.ToDFinsupp, function or constantWording
the sigma finitely supported function linear equivalence finitely supported function of R (from the name)
English
Let $R$ be a set. Then the sigma finitely supported function linear equivalence finitely supported function of $R$ is a linear equivalence of $\FinsuppMACRoQ {\Sigma (\lambda i . x_{1} (i))}{N}$ and the set of finitely supported functions of the function that maps $i_{1}$ to $\FinsuppMACRoQ {x_{1} (i_{1})}{N}$.
Finsupp.NonTorsionWeightclassMathlib.Data.Finsupp.Weight, predicateEnglish
Let $R$ be a set. Let $w$ be a function from elements of $x$ to elements of $M$. Then we can say that $\operatorname{NonTorsionWeight}$ holds for $R$ and $w$.
Finsupp.degreedefMathlib.Data.Finsupp.Weight, function or constantWording
the degree (from the docstring)
English
The degree is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{R}$ and $R$.
Finsupp.weightdefMathlib.Data.Finsupp.Weight, function or constantEnglish
Let $w$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{weight}$ applied to $w$ is an additive monoid homomorphism of $\FinsuppMACRoQ {x}{R}$ and $M$ defined as the additive monoid homomorphism of the linear combination of $R$ and $w$.
truncOfMultisetExistsMemdefMathlib.Data.Fintype.Basic, function or constantWording
the truncation of s and h (from the name)
English
Let $s$ be a multiset of $x$ such that there exists an element $x_{1}$ of $x$, such that $x_{1}$ is an element of $s$. Then the truncation of $s$ and $h$ is a truncation of $x$.
truncOfNonemptyFintypedefMathlib.Data.Fintype.Basic, function or constantWording
the truncation of x (from the name)
English
Let $x$ be a set. Then the truncation of $x$ is a truncation of $x$.
truncSigmaOfExistsdefMathlib.Data.Fintype.Basic, function or constantWording
the truncation sigma of h (from the name)
English
Assume that there exists an element $a_{1}$ of $x$, such that $P$ holds for $a_{1}$. Then the truncation sigma of $h$ is a truncation of $\mathrm{PSigma}$ applied to the function that maps $a$ to $P$ applied to $a$ defined as the truncation of $\mathrm{PSigma}$ applied to the function that maps $a$ to $P$ applied to $a$.
Fintype.carddefMathlib.Data.Fintype.Card, function or constantWording
the cardinality of x (from the name)
English
Let $x$ be a set. Then the cardinality of $x$ is a natural number defined as the cardinality of the universal set.
Fintype.cardEqZeroEquivEquivEmptydefMathlib.Data.Fintype.Card, function or constantEnglish
$\operatorname{cardEqZeroEquivEquivEmpty}$ is an equivalence from the proposition that the cardinality of $x$ is equal to $0$ to $\EquivMACRoAE {x}{\mathrm{Empty}}$ defined as the composition of the equivalence of $\mathrm{Fintype\_\_card\_eq\_zero\_iff}$ and the inverse of the equivalence empty equivalence of $x$.
truncOfCardPosdefMathlib.Data.Fintype.Card, function or constantWording
the truncation of h (from the name)
English
Assume that $0$ is less than the cardinality of $x$. Then the truncation of $h$ is a truncation of $x$ defined as the truncation of $x$.
Finset.univdefMathlib.Data.Fintype.Defs, function or constantWording
the universal set (by hand)
English
The universal set is a finite set of $x$ defined as $\operatorname{elems}$.
FintypeclassMathlib.Data.Fintype.Defs, predicateWording
x is a finite type (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a finite type.
Fintype.elemsdefMathlib.Data.Fintype.Defs, function or constantEnglish
$\operatorname{elems}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Equiv.embeddingEquivOfFinitedefMathlib.Data.Fintype.EquivFin, function or constantWording
the embedding equivalence of x (from the name)
English
Let $x$ be a set. Then the embedding equivalence of $x$ is an equivalence from the set of embeddings of $x$ and $x$ to $\EquivMACRoAE {x}{x}$.
Equiv.ofLeftInverseOfCardLEdefMathlib.Data.Fintype.EquivFin, function or constantWording
the equivalence of f and g (from the name)
English
Assume that the cardinality of $x_{1}$ is less than or equal to the cardinality of $x$. 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$ such that $\operatorname{LeftInverse}$ holds for $g$ and $f$. Then the equivalence of $f$ and $g$ is an equivalence from $x$ to $x_{1}$ defined as $\operatorname{mk}$ applied to $f$, $g$, $h_{1}$ and $\mathrm{Function\_\_LeftInverse\_\_rightInverse\_of\_card\_le}$ applied to $h_{1}$ and $h$.
Equiv.ofRightInverseOfCardLEdefMathlib.Data.Fintype.EquivFin, function or constantWording
the equivalence of f and g (from the name)
English
Assume that the cardinality of $x$ is less than or equal to the cardinality of $x_{1}$. 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$ such that $\operatorname{RightInverse}$ holds for $g$ and $f$. Then the equivalence of $f$ and $g$ is an equivalence from $x$ to $x_{1}$ defined as $\operatorname{mk}$ applied to $f$, $g$, $\mathrm{Function\_\_RightInverse\_\_leftInverse\_of\_card\_le}$ applied to $h_{1}$ and $h$ and $h_{1}$.
Finset.equivFindefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Let $s$ be a finite set of $x$. Then $\operatorname{equivFin}$ applied to $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})})}{\mathrm{Fin} (\FinsetcardMACRoM {s})}$.
Finset.equivFinOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Assume that $\FinsetcardMACRoM {s}= n$. Then $\operatorname{equivFinOfCardEq}$ applied to $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})})}{\mathrm{Fin} (n)}$.
Finset.equivOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantWording
the equivalence of h (from the name)
English
Assume that $\FinsetcardMACRoM {s}= \FinsetcardMACRoM {t}$. Then the equivalence of $h$ is an equivalence from $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})}$.
Fintype.equivFindefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Let $x$ be a set. Then $\operatorname{equivFin}$ applied to $x$ is an equivalence from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$ defined as $\operatorname{out}$ applied to $\operatorname{truncEquivFin}$ applied to $x$.
Fintype.equivFinOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Assume that the cardinality of $x$ is equal to $n$. Then $\operatorname{equivFinOfCardEq}$ applied to $h$ is an element of $\EquivMACRoAE {x}{\mathrm{Fin} (n)}$ defined as $\operatorname{out}$ applied to $\operatorname{truncEquivFinOfCardEq}$ applied to $h$.
Fintype.equivOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantWording
the equivalence of h (from the name)
English
Assume that the cardinality of $x$ is equal to the cardinality of $x_{1}$. Then the equivalence of $h$ is an equivalence from $x$ to $x_{1}$ defined as $\operatorname{out}$ applied to the truncation equivalence of $h$.
Fintype.truncEquivFindefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Let $x$ be a set. Then $\operatorname{truncEquivFin}$ applied to $x$ is a truncation of the set of equivalences from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$.
Fintype.truncEquivFinOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Assume that the cardinality of $x$ is equal to $n$. Then $\operatorname{truncEquivFinOfCardEq}$ applied to $h$ is a truncation of $\EquivMACRoAE {x}{\mathrm{Fin} (n)}$ defined as the map of the function that maps $e$ to the composition of $e$ and the finite congruence of $h$ and $\operatorname{truncEquivFin}$ applied to $x$.
Fintype.truncEquivOfCardEqdefMathlib.Data.Fintype.EquivFin, function or constantWording
the truncation equivalence of h (from the name)
English
Assume that the cardinality of $x$ is equal to the cardinality of $x_{1}$. Then the truncation equivalence of $h$ is a truncation of $\EquivMACRoAE {x}{x_{1}}$ defined as $\operatorname{bind}$ applied to $\operatorname{truncEquivFinOfCardEq}$ applied to $h$ and the function that maps $e$ to the map of the function that maps $\mathrm{e'}$ to the composition of $e$ and the inverse of $\mathrm{e'}$ and $\operatorname{truncEquivFin}$ applied to $x_{1}$.
Fintype.truncFinBijectiondefMathlib.Data.Fintype.EquivFin, function or constantWording
the truncation finite bijection of x (from the name)
English
Let $x$ be a set. Then the truncation finite bijection of $x$ is a truncation of $\SubtypeSet {f}{\operatorname{Bijective} (f)}$.
Function.Embedding.equivOfFiniteSelfEmbeddingdefMathlib.Data.Fintype.EquivFin, function or constantWording
the equivalence of e (from the name)
English
Let $e$ be an embedding of $x$ and $x$. Then the equivalence of $e$ is an equivalence from $x$ to $x$.
Function.Embedding.truncOfCardLEdefMathlib.Data.Fintype.EquivFin, function or constantWording
the truncation of h (from the name)
English
Assume that the cardinality of $x$ is less than or equal to the cardinality of $x_{1}$. Then the truncation of $h$ is a truncation of the set of embeddings of $x$ and $x_{1}$ defined as $\operatorname{bind}$ applied to $\operatorname{truncEquivFin}$ applied to $x$ and the function that maps $\mathrm{ea}$ to the map of the function that maps $\mathrm{eb}$ to the composition of the embedding of $\mathrm{ea}$ and the composition of $\operatorname{castLEEmb}$ applied to $h$ and the embedding of the inverse of $\mathrm{eb}$ and $\operatorname{truncEquivFin}$ applied to $x_{1}$.
Infinite.natEmbeddingdefMathlib.Data.Fintype.EquivFin, function or constantWording
the natural embedding of x (from the name)
English
Let $x$ be a set. Then the natural embedding of $x$ is an embedding of $\Natural$ and $x$.
fintypeOrInfinitedefMathlib.Data.Fintype.EquivFin, function or constantEnglish
Let $x$ be a set. Then $\mathrm{fintypeOrInfinite}$ applied to $x$ is an element of $\mathrm{PSum}$ applied to the proposition that $x$ is a finite type and the proposition that $x$ is infinite defined as $\mathrm{dite}$ applied to the proposition that $x$ is infinite, the function that maps $h$ to $\operatorname{inr}$ applied to $h$ and the function that maps $h_{1}$ to $\operatorname{inl}$ applied to $\mathrm{fintypeOfNotInfinite}$ applied to $h_{1}$.
Fintype.bijInvdefMathlib.Data.Fintype.Inv, function or constantWording
the bijection inverse of f_bij and b (from the name)
English
Assume that $f$ is bijective. Let $b$ be an element of $x_{1}$. Then the bijection inverse of $\mathrm{f\_bij}$ and $b$ is an element of $x$ defined as $\operatorname{choose}$ applied to the function that maps $a$ to $\EqtMACRoH {f (a)}{b}$ and $\operatorname{existsUnique}$ applied to $\mathrm{f\_bij}$ and $b$.
Fintype.choosedefMathlib.Data.Fintype.Inv, function or constantEnglish
Let $p$ be a function from elements of $x$ to propositions such that $\mathrm{ExistsUnique}$ holds for the function that maps $a$ to $p$ applied to $a$. Then $\operatorname{choose}$ applied to $p$ and $\mathrm{hp}$ is an element of $x$ defined as $\operatorname{chooseX}$ applied to $p$ and $\mathrm{hp}$.
Fintype.chooseXdefMathlib.Data.Fintype.Inv, function or constantEnglish
Let $p$ be a function from elements of $x$ to propositions such that $\mathrm{ExistsUnique}$ holds for the function that maps $a_{1}$ to $p$ applied to $a_{1}$. Then $\operatorname{chooseX}$ applied to $p$ and $\mathrm{hp}$ is an element of $\SubtypeSet {a}{p (a)}$.
Function.Embedding.invOfMemRangedefMathlib.Data.Fintype.Inv, function or constantWording
the inverse of f and b (from the docstring)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $b$ be an element of the range of $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $b$ is an element of $x$ defined as the inverse of $\operatorname{injective}$ applied to $f$ and $b$.
Function.Injective.invOfMemRangedefMathlib.Data.Fintype.Inv, function or constantWording
the inverse of hf and x4 (from the docstring)
English
Assume that $f$ is injective. Let $x_{4}$ be an element of the range of $f$. Then the inverse of $\mathrm{hf}$ and $x_{4}$ is an element of $x$.
Multiset.listsdefMathlib.Data.Fintype.List, function or constantWording
the list of x1 (from the name)
English
Let $x_{1}$ be a multiset of $x$. Then the list of $x_{1}$ is a multiset of the set of lists of elements of $x$.
Fintype.truncRecEmptyOptiondefMathlib.Data.Fintype.Option, function or constantEnglish
Let $\mathrm{of\_equiv}$ be a function from sets $x_{7}$ and sets $x_{8}$ and equivalences from $x_{7}$ to $x_{8}$ and elements of $P$ applied to $x_{7}$ to elements of $P$ applied to $x_{8}$. Let $\mathrm{h\_empty}$ be an element of $P$ applied to $\mathrm{PEmpty}$. Let $\mathrm{h\_option}$ be a function from sets $x_{3}$ and elements of $\mathrm{Proof}$ applied to the proposition that $x_{3}$ is a finite type and elements of $\mathrm{Proof}$ applied to $\mathrm{DecidableEq}$ applied to $x_{3}$ and elements of $P$ applied to $x_{3}$ to elements of $P$ applied to $\mathrm{Option}$ applied to $x_{3}$. Let $x$ be a set. Then $\operatorname{truncRecEmptyOption}$ applied to $x_{7}$, $x_{8}$, $\mathrm{of\_equiv}$, $\mathrm{h\_empty}$, $x_{3}$, $\mathrm{h\_option}$ and $x$ is a truncation of $P$ applied to $x$.
permsOfFinsetdefMathlib.Data.Fintype.Perm, function or constantEnglish
Let $s$ be a finite set of $x$. Then $\mathrm{permsOfFinset}$ applied to $s$ is a finite set of the set of permutations of $x$.
permsOfListdefMathlib.Data.Fintype.Perm, function or constantEnglish
Let $x_{2}$ be a list of elements of $x$. Then $\mathrm{permsOfList}$ applied to $x_{2}$ is a list of permutations of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{permsOfList\_\_\_f}$.
Fintype.piFinsetdefMathlib.Data.Fintype.Pi, function or constantWording
the product finite set of t (from the name)
English
Let $t$ be a function from elements $a_{1}$ of $x$ to finite sets of $x_{3}$ applied to $a_{1}$. Then the product finite set of $a_{1}$ is a finite set of the set of functions from elements $a$ of $x$ to elements of $x_{3}$ applied to $a$.
Quotient.finChoicedefMathlib.Data.Fintype.Quotient, function or constantWording
the finite choice of q (from the name)
English
Let $q$ be a function from elements $i$ of $x$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i$. Then the finite choice of $i$ is an element of $\mathrm{Quotient}$ applied to $\mathrm{piSetoid}$.
Quotient.finChoiceEquivdefMathlib.Data.Fintype.Quotient, function or constantWording
the finite choice equivalence (from the name)
English
The finite choice equivalence is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Quotient} (S (i)))}{\mathrm{Quotient} (\mathrm{piSetoid})}$.
Quotient.finHRecOndefMathlib.Data.Fintype.Quotient, function or constantEnglish
Let $q$ be a function from elements $i_{4}$ of $x$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i_{4}$. Let $f$ be a function from functions $a_{1}$ from elements $i_{3}$ of $x$ to elements of $x_{3}$ applied to $i_{3}$ to elements of $C$ applied to the function that maps $x_{4}$ to $\operatorname{mk}$ applied to $S$ applied to $x_{4}$ and $a_{1}$ applied to $x_{4}$ such that for all functions $a$ from elements $i_{2}$ of $x$ to elements of $x_{3}$ applied to $i_{2}$, for all functions $b$ from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$, if for all elements $i$ of $x$, $\operatorname{Equiv}$ holds for $a$ applied to $i$ and $b$ applied to $i$, then $\mathrm{HEq}$ holds for $f$ applied to $a$ and $f$ applied to $b$. Then $\operatorname{finHRecOn}$ applied to $i_{4}$, $q$, $a_{1}$, $f$ and $h$ is an element of $C$ applied to $q$.
Quotient.finLiftOndefMathlib.Data.Fintype.Quotient, function or constantEnglish
Let $q$ be a function from elements $i_{4}$ of $x$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i_{4}$. Let $f$ be a function from functions from elements $i_{3}$ of $x$ to elements of $x_{3}$ applied to $i_{3}$ to elements of $x_{4}$ such that for all functions $a$ from elements $i_{2}$ of $x$ to elements of $x_{3}$ applied to $i_{2}$, for all functions $b$ from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$, if for all elements $i$ of $x$, $\operatorname{Equiv}$ holds for $a$ applied to $i$ and $b$ applied to $i$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{finLiftOn}$ applied to $i_{4}$, $q$, $f$ and $h$ is an element of $x_{4}$ defined as the function that maps $h$ to $\operatorname{liftOn}$ applied to the finite choice of $i_{4}$, $q$, $f$ and $h$.
Quotient.finRecOndefMathlib.Data.Fintype.Quotient, function or constantEnglish
Let $q$ be a function from elements $i_{6}$ of $x$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i_{6}$. Let $f$ be a function from functions $a_{1}$ from elements $i_{5}$ of $x$ to elements of $x_{3}$ applied to $i_{5}$ to elements of $C$ applied to the function that maps $x_{4}$ to $\operatorname{mk}$ applied to $S$ applied to $x_{4}$ and $a_{1}$ applied to $x_{4}$ such that for all functions $a$ from elements $i_{4}$ of $x$ to elements of $x_{3}$ applied to $i_{4}$, for all functions $b$ from elements $i_{3}$ of $x$ to elements of $x_{3}$ applied to $i_{3}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to the proposition that for all elements $i_{2}$ of $x$, $\operatorname{Equiv}$ holds for $a$ applied to $i_{2}$ and $b$ applied to $i_{2}$, $\EqtMACRoH {\operatorname{ndrec} (f (a), \mathrm{funext} (\lambda i_{1} . \operatorname{sound} (h_{1} (i_{1}))))}{f (b)}$. Then $\operatorname{finRecOn}$ applied to $i_{6}$, $q$, $a_{1}$, $f$ and $h$ is an element of $C$ applied to $q$.
Quotient.listChoicedefMathlib.Data.Fintype.Quotient, function or constantWording
the list choice of q (from the name)
English
Let $q$ be a function from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {l}{i}$ to elements of $\mathrm{Quotient}$ applied to $S$ applied to $i$. Then the list choice of $i$ is an element of $\mathrm{Quotient}$ applied to $\mathrm{piSetoid}$ defined as the function that maps $q$ to $\operatorname{brecOn}$ applied to $l$, $\mathrm{Quotient\_\_listChoice\_\_\_f}$, $i$ and $q$.
Trunc.finChoicedefMathlib.Data.Fintype.Quotient, function or constantWording
the finite choice of q (from the name)
English
Let $q$ be a function from elements $i_{1}$ of $x$ to truncations of $x_{3}$ applied to $i_{1}$. Then the finite choice of $i_{1}$ is a truncation of the set of functions from elements $i$ of $x$ to elements of $x_{3}$ applied to $i$ defined as the function that maps $q$ to the map of $\mathrm{id}$ and the finite choice of $i_{1}$.
Trunc.finChoiceEquivdefMathlib.Data.Fintype.Quotient, function or constantWording
the finite choice equivalence (from the name)
English
The finite choice equivalence is an equivalence from the set of functions from elements $i$ of $x$ to truncations of $x_{3}$ applied to $i$ to the set of truncations of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$.
Trunc.finLiftOndefMathlib.Data.Fintype.Quotient, function or constantEnglish
Let $q$ be a function from elements $i_{3}$ of $x$ to truncations of $x_{3}$ applied to $i_{3}$. Let $f$ be a function from functions from elements $i_{2}$ of $x$ to elements of $x_{3}$ applied to $i_{2}$ to elements of $x_{4}$ such that for all functions $a$ from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$, for all functions $b$ from elements $i$ of $x$ to elements of $x_{3}$ applied to $i$, $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{finLiftOn}$ applied to $i_{3}$, $q$, $f$ and $h$ is an element of $x_{4}$ defined as the function that maps $h$ to $\operatorname{finLiftOn}$ applied to $i_{3}$, $q$, the function that maps $x_{5}$, $x_{6}$ and $h_{1}$ to $f$ applied to $x_{5}$ and $x_{6}$ and $h$.
Trunc.finRecOndefMathlib.Data.Fintype.Quotient, function or constantEnglish
Let $q$ be a function from elements $i_{3}$ of $x$ to truncations of $x_{3}$ applied to $i_{3}$. Let $f$ be a function from functions $a_{1}$ from elements $i_{2}$ of $x$ to elements of $x_{3}$ applied to $i_{2}$ to elements of $C$ applied to the function that maps $x_{6}$ to $\operatorname{mk}$ applied to $a_{1}$ applied to $x_{6}$ such that for all functions $a$ from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$, for all functions $b$ from elements $i$ of $x$ to elements of $x_{3}$ applied to $i$, $\EqtMACRoH {\operatorname{ndrec} (f (a), \mathrm{funext} (\lambda x_{5} . \operatorname{eq} (\operatorname{mk} (a (x_{5})), \operatorname{mk} (b (x_{5})))))}{f (b)}$. Then $\operatorname{finRecOn}$ applied to $i_{3}$, $q$, $a_{1}$, $f$ and $h$ is an element of $C$ applied to $q$ defined as the function that maps $f$ and $h$ to $\operatorname{finRecOn}$ applied to $i_{3}$, the function that maps $x_{4}$ to $q$ applied to $x_{4}$, the function that maps $x_{5}$, $x_{6}$ and $h_{1}$ to $a_{1}$ applied to $x_{5}$ and $x_{6}$, $f$ and $h$.
Fintype.finsetEquivSetdefMathlib.Data.Fintype.Sets, function or constantWording
the finite set equivalence set (from the name)
English
The finite set equivalence set is an equivalence from the set of finite sets of $x$ to $\wp x$.
Fintype.finsetOrderIsoSetdefMathlib.Data.Fintype.Sets, function or constantWording
the finite set order isomorphism set (from the name)
English
The finite set order isomorphism set is an order isomorphism of the set of finite sets of $x$ and $\wp x$ defined as $\operatorname{mk}$ applied to the finite set equivalence set and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Finset\_\_coe\_subset}$.
Set.toFinsetdefMathlib.Data.Fintype.Sets, function or constantWording
the finite set of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the finite set of $s$ is a finite set of $x$ defined as the map of the subtype of the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and the universal set.
finsetStxdefMathlib.Data.Fintype.Sets, function or constantEnglish
generation took over the time limit
precheckFinsetStxdefMathlib.Data.Fintype.Sets, function or constantEnglish
generation took over the time limit
finSumEquivOfFinsetdefMathlib.Data.Fintype.Sort, function or constantWording
the finite sum equivalence of hm and hn (from the name)
English
Assume that $\FinsetcardMACRoM {s}= m$. Assume that the cardinality of the complement of $s$ is equal to $n$. Then the finite sum equivalence of $\mathrm{hm}$ and $\mathrm{hn}$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Fin} (m), \mathrm{Fin} (n))}{x}$ defined as $\operatorname{trans}$ applied to the sum congruence of $\operatorname{toEquiv}$ applied to the order isomorphism of $s$ and $\mathrm{hm}$ and the composition of $\operatorname{toEquiv}$ applied to the order isomorphism of the complement of $s$ and $\mathrm{hn}$ and the equivalence of $\mathrm{Finset\_\_coe\_compl}$ applied to $s$ and the sum complement of $s$.
monoEquivOfFindefMathlib.Data.Fintype.Sort, function or constantWording
the monotone equivalence of x and h (from the name)
English
Let $x$ be a set such that the cardinality of $x$ is equal to $k$. Then the monotone equivalence of $x$ and $h$ is an order isomorphism of $\mathrm{Fin}$ applied to $k$ and $x$ defined as the composition of the order isomorphism of the universal set and $h$ and the composition of the order isomorphism of the universal set and the universal set and the universal set.
HolordefMathlib.Data.Holor, typeWording
holor of x and ds (from the name)
English
Let $x$ be a set. Let $\mathrm{ds}$ be a list of natural numbers. Then a holor of $x$ and $\mathrm{ds}$ is an element of the function that maps $x$ and $\mathrm{ds}$ to the set of functions from holor indexes of $\mathrm{ds}$ to elements of $x$.
Holor.CPRankMaxinductiveMathlib.Data.Holor, predicateEnglish
Let $x_{3}$ be a natural number. Let $x_{4}$ be a holor of $x$ and $\mathrm{ds}$. Then we can say that $\operatorname{CPRankMax}$ holds for $x_{3}$ and $x_{4}$.
Holor.CPRankMax.belowinductiveMathlib.Data.Holor, predicateEnglish
Assume that $\operatorname{CPRankMax}$ holds for $x_{3}$ and $x_{4}$. Then we can say that $\operatorname{below}$ holds for $t$.
Holor.CPRankMax1inductiveMathlib.Data.Holor, predicateEnglish
Let $x_{2}$ be a holor of $x$ and $\mathrm{ds}$. Then we can say that $\operatorname{CPRankMax1}$ holds for $x_{2}$.
Holor.CPRankMax1.belowinductiveMathlib.Data.Holor, predicateEnglish
Assume that $\operatorname{CPRankMax1}$ holds for $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
Holor.assocLeftdefMathlib.Data.Holor, function or constantWording
the left associator of x4 (from the name)
English
Let $x_{4}$ be a holor of $x$ and $\operatorname{hAppend}$ applied to $x_{1}$ and $\operatorname{hAppend}$ applied to $x_{2}$ and $x_{3}$. Then the left associator of $x_{4}$ is a holor of $x$ and $\operatorname{hAppend}$ applied to $\operatorname{hAppend}$ applied to $x_{1}$ and $x_{2}$ and $x_{3}$.
Holor.assocRightdefMathlib.Data.Holor, function or constantWording
the right associator of x4 (from the name)
English
Let $x_{4}$ be a holor of $x$ and $\operatorname{hAppend}$ applied to $\operatorname{hAppend}$ applied to $x_{1}$ and $x_{2}$ and $x_{3}$. Then the right associator of $x_{4}$ is a holor of $x$ and $\operatorname{hAppend}$ applied to $x_{1}$ and $\operatorname{hAppend}$ applied to $x_{2}$ and $x_{3}$.
Holor.cprankdefMathlib.Data.Holor, function or constantEnglish
Let $x_{2}$ be a holor of $x$ and $\mathrm{ds}$. Then $\operatorname{cprank}$ applied to $x_{2}$ is a natural number.
Holor.muldefMathlib.Data.Holor, function or constantWording
the product of x4 and y (from the name)
English
Let $x_{4}$ be a holor of $x$ and $x_{1}$. Let $y$ be a holor of $x$ and $x_{2}$. Then the product of $x_{4}$ and $y$ is a holor of $x$ and $\operatorname{hAppend}$ applied to $x_{1}$ and $x_{2}$ defined as the function that maps $t$ to $x_{4} (\operatorname{take} (t))\times y (\operatorname{drop} (t))$.
Holor.slicedefMathlib.Data.Holor, function or constantWording
the slice of x1 and i (from the name)
English
Let $x_{1}$ be a holor of $x$ and $\operatorname{cons}$ applied to $d$ and $\mathrm{ds}$. Let $i$ be a natural number such that $i < d$. Then the slice of $x_{1}$ and $i$ is a holor of $x$ and $\mathrm{ds}$ defined as the function that maps $\mathrm{is}$ to $x_{1}$ applied to $\operatorname{cons}$ applied to $i$ and $\mathrm{is}$.
Holor.unitVecdefMathlib.Data.Holor, function or constantWording
the unit vector of d and j (from the name)
English
Let $d$ and $j$ be natural numbers. Then the unit vector of $d$ and $j$ is a holor of $x$ and $\operatorname{cons}$ applied to $d$ and $\operatorname{nil}$ defined as the function that maps $\mathrm{ti}$ to $\iteMACRoG {(\EqtMACRoH {\mathrm{ti}}{\operatorname{cons} (j , \operatorname{nil})})}{1}{0}$.
HolorIndexdefMathlib.Data.Holor, typeWording
holor index of ds (from the name)
English
Let $\mathrm{ds}$ be a list of natural numbers. Then a holor index of $\mathrm{ds}$ is an element of the function that maps $\mathrm{ds}$ to $\SubtypeSet {\mathrm{is}}{\mathrm{List\_\_Forall\_u2082\_} (\lambda x . \lambda x_{1} . \mathrm{Lt} (x , x_{1}), \mathrm{is} , \mathrm{ds})}$.
HolorIndex.assocLeftdefMathlib.Data.Holor, function or constantWording
the left associator of x3 (from the name)
English
Let $x_{3}$ be a holor index of $\operatorname{hAppend}$ applied to $x$ and $\operatorname{hAppend}$ applied to $x_{1}$ and $x_{2}$. Then the left associator of $x_{3}$ is a holor index of $\operatorname{hAppend}$ applied to $\operatorname{hAppend}$ applied to $x$ and $x_{1}$ and $x_{2}$.
HolorIndex.assocRightdefMathlib.Data.Holor, function or constantWording
the right associator of x3 (from the name)
English
Let $x_{3}$ be a holor index of $\operatorname{hAppend}$ applied to $\operatorname{hAppend}$ applied to $x$ and $x_{1}$ and $x_{2}$. Then the right associator of $x_{3}$ is a holor index of $\operatorname{hAppend}$ applied to $x$ and $\operatorname{hAppend}$ applied to $x_{1}$ and $x_{2}$.
HolorIndex.dropdefMathlib.Data.Holor, function or constantEnglish
Let $x_{2}$ be a holor index of $\operatorname{hAppend}$ applied to $x_{1}$ and $x$. Then $\operatorname{drop}$ applied to $x_{2}$ is a holor index of $x$.
HolorIndex.takedefMathlib.Data.Holor, function or constantEnglish
Let $x_{2}$ be a holor index of $\operatorname{hAppend}$ applied to $x_{1}$ and $x$. Then $\operatorname{take}$ applied to $x_{2}$ is a holor index of $x_{1}$.
Mathlib.IneqinductiveMathlib.Data.Ineq, typeEnglish
The elements of $\operatorname{Ineq}$ are a basic type.
Mathlib.Ineq.cmpdefMathlib.Data.Ineq, function or constantWording
the comparison of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be elements of $\operatorname{Ineq}$. Then the comparison of $x$ and $x_{1}$ is an element of $\mathrm{Ordering}$.
Mathlib.Ineq.ctorElimTypedefMathlib.Data.Ineq, typeEnglish
Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{eq}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{le}$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{lt}$.
Mathlib.Ineq.eqconstructorMathlib.Data.Ineq, function or constantEnglish
$\operatorname{eq}$ is an element of $\operatorname{Ineq}$.
Mathlib.Ineq.leconstructorMathlib.Data.Ineq, function or constantEnglish
$\operatorname{le}$ is an element of $\operatorname{Ineq}$.
Mathlib.Ineq.ltconstructorMathlib.Data.Ineq, function or constantEnglish
$\operatorname{lt}$ is an element of $\operatorname{Ineq}$.
Mathlib.Ineq.maxdefMathlib.Data.Ineq, function or constantWording
the maximum of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be elements of $\operatorname{Ineq}$. Then the maximum of $x$ and $x_{1}$ is an element of $\operatorname{Ineq}$.
Mathlib.Ineq.ofNatdefMathlib.Data.Ineq, function or constantEnglish
Let $x$ be a natural number. Then $\operatorname{ofNat}$ applied to $x$ is an element of $\operatorname{Ineq}$ defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, $\operatorname{eq}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $1$, $\operatorname{le}$ and $\operatorname{lt}$.
Mathlib.Ineq.toStringdefMathlib.Data.Ineq, function or constantWording
the string of x (from the name)
English
Let $x$ be an element of $\operatorname{Ineq}$. Then the string of $x$ is an element of $\mathrm{String}$.
Mathlib.instInhabitedIneq.defaultdefMathlib.Data.Ineq, function or constantWording
the default (from the name)
English
The default is an element of $\operatorname{Ineq}$ defined as $\operatorname{eq}$.
Mathlib.instReprIneq.reprdefMathlib.Data.Ineq, function or constantWording
the representation of x and x1 (from the name)
English
Let $x$ be an element of $\operatorname{Ineq}$. Let $x_{1}$ be a natural number. Then the representation of $x$ and $x_{1}$ is an element of $\operatorname{Format}$.
Int.bitdefMathlib.Data.Int.Bitwise, function or constantWording
the bit of b and x (from the name)
English
Let $b$ be an element of $\mathrm{Bool}$. Let $x$ be an integer. Then the bit of $b$ and $x$ is an integer defined as $\mathrm{cond}$ applied to $b$, the function that maps $x$ to $2 \times x + 1$, the function that maps $x_{1}$ to $2 \times x_{1}$ and $x$.
Int.bitCasesOndefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $n$ be an integer. Let $h$ be a function from elements $b$ of $\mathrm{Bool}$ and integers $n_{1}$ to elements of $C$ applied to the bit of $b$ and $n_{1}$. Then $\operatorname{bitCasesOn}$ applied to $n$, $b$, $n_{1}$ and $h$ is an element of $C$ applied to $n$.
Int.bitwisedefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $f$ be a function from elements of $\mathrm{Bool}$ and elements of $\mathrm{Bool}$ to elements of $\mathrm{Bool}$. Let $x$ and $x_{1}$ be integers. Then $\operatorname{bitwise}$ applied to $f$, $x$ and $x_{1}$ is an integer.
Int.bodddefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $x$ be an integer. Then $\operatorname{bodd}$ applied to $x$ is an element of $\mathrm{Bool}$.
Int.div2defMathlib.Data.Int.Bitwise, function or constantWording
the quotient of x (from the name)
English
Let $x$ be an integer. Then the quotient of $x$ is an integer.
Int.landdefMathlib.Data.Int.Bitwise, function or constantWording
the land of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be integers. Then the land of $x$ and $x_{1}$ is an integer.
Int.ldiffdefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $x$ and $x_{1}$ be integers. Then $\operatorname{ldiff}$ applied to $x$ and $x_{1}$ is an integer.
Int.lnotdefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $x$ be an integer. Then $\operatorname{lnot}$ applied to $x$ is an integer.
Int.lordefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $x$ and $x_{1}$ be integers. Then $\operatorname{lor}$ applied to $x$ and $x_{1}$ is an integer.
Int.natBitwisedefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $f$ be a function from elements of $\mathrm{Bool}$ and elements of $\mathrm{Bool}$ to elements of $\mathrm{Bool}$. Let $m$ and $n$ be natural numbers. Then $\operatorname{natBitwise}$ applied to $f$, $m$ and $n$ is an integer defined as $\mathrm{cond}$ applied to $f$ applied to $\operatorname{false}$ and $\operatorname{false}$, $\operatorname{negSucc}$ applied to $\operatorname{bitwise}$ applied to the function that maps $x$ and $y$ to $\operatorname{not}$ applied to $f$ applied to $x$ and $y$, $m$ and $n$ and $\operatorname{bitwise}$ applied to $f$, $m$ and $n$.
Int.xordefMathlib.Data.Int.Bitwise, function or constantEnglish
Let $x$ and $x_{1}$ be integers. Then $\operatorname{xor}$ applied to $x$ and $x_{1}$ is an integer.
AddCommGroupWithOneclassMathlib.Data.Int.Cast.Defs, predicateWording
R is a additive commutative group with one (from the name)
English
Let $R$ be a set. Then we can say that $R$ is an additive commutative group with one.
AddGroupWithOneclassMathlib.Data.Int.Cast.Defs, predicateWording
R is a additive group with one (from the name)
English
Let $R$ be a set. Then we can say that $R$ is an additive group with one.
Int.castDefdefMathlib.Data.Int.Cast.Defs, function or constantWording
the cast of x2 (from the name)
English
Let $x_{2}$ be an integer. Then the cast of $x_{2}$ is an element of $R$.
Int.castAddHomdefMathlib.Data.Int.Cast.Lemmas, function or constantWording
the cast additive homomorphism of x (from the name)
English
Let $x$ be a set. Then the cast additive homomorphism of $x$ is an additive monoid homomorphism of $\Integer$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toIntCast}$ and $\mathrm{Int\_\_cast\_zero}$ and $\mathrm{Int\_\_cast\_add}$.
Int.castRingHomdefMathlib.Data.Int.Cast.Lemmas, function or constantWording
the cast ring homomorphism of x (from the name)
English
Let $x$ be a set. Then the cast ring homomorphism of $x$ is a ring homomorphism of $\Integer$ and $x$.
Int.ofNatHomdefMathlib.Data.Int.Cast.Lemmas, function or constantWording
the integer (from the name)
English
The integer is a ring homomorphism of $\Natural$ and $\Integer$ defined as the cast ring homomorphism of $\Integer$.
zmultiplesAddHomdefMathlib.Data.Int.Cast.Lemmas, function or constantEnglish
Let $x$ be a set. Then $\mathrm{zmultiplesAddHom}$ applied to $x$ is an additive equivalence of $x$ and the set of additive monoid homomorphisms of $\Integer$ and $x$.
zmultiplesHomdefMathlib.Data.Int.Cast.Lemmas, function or constantEnglish
Let $x$ be a set. Then $\mathrm{zmultiplesHom}$ applied to $x$ is an equivalence from $x$ to the set of additive monoid homomorphisms of $\Integer$ and $x$.
zpowersHomdefMathlib.Data.Int.Cast.Lemmas, function or constantEnglish
Let $x$ be a set. Then $\mathrm{zpowersHom}$ applied to $x$ is an equivalence from $x$ to the set of monoid homomorphisms of the set of multiplicatives of $\Integer$ and $x$ defined as the composition of $\operatorname{ofMul}$ and the composition of $\mathrm{zmultiplesHom}$ applied to $\mathrm{Additive}$ applied to $x$ and the left multiplicative.
zpowersMulHomdefMathlib.Data.Int.Cast.Lemmas, function or constantEnglish
Let $x$ be a set. Then $\mathrm{zpowersMulHom}$ applied to $x$ is a multiplicative equivalence of $x$ and the set of monoid homomorphisms of the set of multiplicatives of $\Integer$ and $x$.
Int.fibdefMathlib.Data.Int.Fib.Basic, function or constantEnglish
Let $n$ be an element of $\Integer$. Then $\operatorname{fib}$ applied to $n$ is an element of $\Integer$ defined as $\iteMACRoG {\mathrm{Leq} (0 , n)}{\operatorname{fib} (\operatorname{toNat} (n))}{(\iteMACRoG {\mathrm{even} (n)}{\operatorname{neg} (\operatorname{fib} (\operatorname{toNat} (\operatorname{neg} (n))))}{\operatorname{fib} (\operatorname{toNat} (\operatorname{neg} (n)))})}$.
Int.gcdAdefMathlib.Data.Int.GCD, function or constantWording
the greatest common divisor of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be integers. Then the greatest common divisor of $x$ and $x_{1}$ is an integer.
Int.gcdBdefMathlib.Data.Int.GCD, function or constantWording
the greatest common divisor of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be integers. Then the greatest common divisor of $x$ and $x_{1}$ is an integer.
Nat.gcdAdefMathlib.Data.Int.GCD, function or constantWording
the greatest common divisor of x and y (from the name)
English
Let $x$ and $y$ be natural numbers. Then the greatest common divisor of $x$ and $y$ is an integer defined as $\ProdfstMACRoZ {\operatorname{xgcd} (x , y)}$.
Nat.gcdBdefMathlib.Data.Int.GCD, function or constantWording
the greatest common divisor of x and y (from the name)
English
Let $x$ and $y$ be natural numbers. Then the greatest common divisor of $x$ and $y$ is an integer defined as $\ProdsndMACRoAA {\operatorname{xgcd} (x , y)}$.
Nat.xgcddefMathlib.Data.Int.GCD, function or constantEnglish
Let $x$ and $y$ be natural numbers. Then $\operatorname{xgcd}$ applied to $x$ and $y$ is an element of $\mathrm{Prod}$ applied to $\Integer$ and $\Integer$ defined as $\ProdsndMACRoAA {\operatorname{xgcdAux} (x , 1 , 0 , y , 0 , 1)}$.
Int.inductionOn'defMathlib.Data.Int.Init, function or constantEnglish
Let $z$ and $b$ be integers. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $b$. Let $\mathrm{succ}$ be a function from integers $k_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (b , k_{1})$ and elements of $\mathrm{motive}$ applied to $k_{1}$ to elements of $\mathrm{motive}$ applied to $k_{1} + 1$. Let $\mathrm{pred}$ be a function from integers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (k , b)$ and elements of $\mathrm{motive}$ applied to $k$ to elements of $\mathrm{motive}$ applied to $k - 1$. Then $\operatorname{inductionOn'}$ applied to $z$, $b$, $\mathrm{zero}$, $k_{1}$, $\mathrm{succ}$, $k$ and $\mathrm{pred}$ is an element of $\mathrm{motive}$ applied to $z$.
Int.inductionOn'.negdefMathlib.Data.Int.Init, function or constantWording
the negative case of b (from the docstring)
English
Let $b$ be an integer. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $b$. Let $\mathrm{pred}$ be a function from integers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (k , b)$ and elements of $\mathrm{motive}$ applied to $k$ to elements of $\mathrm{motive}$ applied to $k - 1$. Let $n$ be a natural number. Then the negative case of $b$ is an element of $\mathrm{motive}$ applied to $b + \operatorname{negSucc} (n)$ defined as the function that maps $n$ to $\operatorname{brecOn}$ applied to $\mathrm{pred}$, $\mathrm{Int\_\_inductionOn'\_\_neg\_\_\_f}$ applied to $b$, $\mathrm{zero}$ and $k$ and $n$.
Int.inductionOn'.posdefMathlib.Data.Int.Init, function or constantWording
the positive case of b (from the docstring)
English
Let $b$ be an integer. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $b$. Let $\mathrm{succ}$ be a function from integers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (b , k)$ and elements of $\mathrm{motive}$ applied to $k$ to elements of $\mathrm{motive}$ applied to $k + 1$. Let $n$ be a natural number. Then the positive case of $b$ is an element of $\mathrm{motive}$ applied to $b + n$ defined as the function that maps $n$ to $\operatorname{brecOn}$ applied to $\mathrm{succ}$, $\mathrm{Int\_\_inductionOn'\_\_pos\_\_\_f}$ applied to $b$, $\mathrm{zero}$ and $k$ and $n$.
Int.leInductiondefMathlib.Data.Int.Init, function or constantEnglish
Let $\mathrm{base}$ be an element of $\mathrm{motive}$ applied to $m$ and $\mathrm{Int\_\_le\_refl}$ applied to $m$. Let $\mathrm{succ}$ be a function from integers $n_{1}$ and elements $\mathrm{hmn1}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n_{1})$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $\mathrm{hmn1}$ to elements of $\mathrm{motive}$ applied to $n_{1} + 1$ and $\mathrm{Int\_\_le\_add\_one}$ applied to $\mathrm{hmn1}$. Let $n$ be an integer such that $m \leq n$. Then $\operatorname{leInduction}$ applied to $\mathrm{base}$, $n_{1}$, $\mathrm{hmn1}$, $\mathrm{succ}$, $n$ and $\mathrm{hmn}$ is an element of $\mathrm{motive}$ applied to $n$ and $\mathrm{hmn}$.
Int.leInductionDowndefMathlib.Data.Int.Init, function or constantEnglish
Let $\mathrm{base}$ be an element of $\mathrm{motive}$ applied to $m$ and $\mathrm{Int\_\_le\_refl}$ applied to $m$. Let $\mathrm{pred}$ be a function from integers $n_{1}$ and elements $\mathrm{hnm1}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (n_{1} , m)$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $\mathrm{hnm1}$ to elements of $\mathrm{motive}$ applied to $n_{1} - 1$ and $\mathrm{Int\_\_leInductionDown\_\_\_proof\_2}$ applied to $n_{1}$ and $\mathrm{hnm1}$. Let $n$ be an integer such that $n \leq m$. Then $\operatorname{leInductionDown}$ applied to $\mathrm{base}$, $n_{1}$, $\mathrm{hnm1}$, $\mathrm{pred}$, $n$ and $\mathrm{hnm}$ is an element of $\mathrm{motive}$ applied to $n$ and $\mathrm{hnm}$.
Int.natModdefMathlib.Data.Int.Init, function or constantWording
the modulus of m and n (from the docstring)
English
Let $m$ and $n$ be integers. Then the modulus of $m$ and $n$ is a natural number defined as $\operatorname{toNat}$ applied to $\HModhModMACRoF {m}{n}$.
Int.negInductiondefMathlib.Data.Int.Init, function or constantWording
the negation induction of n3 and neg (from the name)
English
Let $\mathrm{nat}$ be a function from natural numbers $n_{3}$ to elements of $\mathrm{motive}$ applied to $n_{3}$. Let $\mathrm{neg}$ be a function from functions from natural numbers $n_{2}$ to elements of $\mathrm{motive}$ applied to $n_{2}$ and natural numbers $n_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{neg}$ applied to $n_{1}$. Let $n$ be an integer. Then the negation induction of $\mathrm{nat}$ and $n_{1}$ is an element of $\mathrm{motive}$ applied to $n$.
Int.preddefMathlib.Data.Int.Init, function or constantWording
the predecessor of a (from the name)
English
Let $a$ be an integer. Then the predecessor of $a$ is an integer defined as $a - 1$.
Int.strongRecdefMathlib.Data.Int.Init, function or constantEnglish
Let $\mathrm{lt}$ be a function from integers $n_{2}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (n_{2} , m)$ to elements of $\mathrm{motive}$ applied to $n_{2}$. Let $\mathrm{ge}$ be a function from integers $n_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Geq} (n_{1} , m)$ and functions from integers $k$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (k , n_{1})$ to elements of $\mathrm{motive}$ applied to $k$ to elements of $\mathrm{motive}$ applied to $n_{1}$. Let $n$ be an integer. Then $\operatorname{strongRec}$ applied to $n_{2}$, $\mathrm{lt}$, $n_{1}$, $\mathrm{ge}$ and $n$ is an element of $\mathrm{motive}$ applied to $n$.
Int.succdefMathlib.Data.Int.Init, function or constantWording
the successor of a (from the name)
English
Let $a$ be an integer. Then the successor of $a$ is an integer defined as $a + 1$.
Int.clogdefMathlib.Data.Int.Log, function or constantEnglish
Let $b$ be an element of $\Natural$. Let $r$ be an element of $R$. Then $\operatorname{clog}$ applied to $b$ and $r$ is an element of $\Integer$ defined as $\iteMACRoG {\mathrm{Leq} (1 , r)}{\operatorname{clog} (b , \operatorname{ceil} (r))}{\operatorname{neg} (\operatorname{log} (b , \operatorname{floor} (\operatorname{inv} (r))))}$.
Int.clogZPowGidefMathlib.Data.Int.Log, function or constantEnglish
Let $R$ be a set. Assume that $1 < b$. Then $\operatorname{clogZPowGi}$ applied to $R$ and $\mathrm{hb}$ is a Galois insertion of the function that maps $r$ to $\operatorname{clog}$ applied to $b$ and $r$ and the function that maps $z$ to $b ^ {z}$.
Int.logdefMathlib.Data.Int.Log, function or constantWording
the logarithm of b and r (from the name)
English
Let $b$ be an element of $\Natural$. Let $r$ be an element of $R$. Then the logarithm of $b$ and $r$ is an element of $\Integer$ defined as $\iteMACRoG {\mathrm{Leq} (1 , r)}{\operatorname{log} (b , \operatorname{floor} (r))}{\operatorname{neg} (\operatorname{clog} (b , \operatorname{ceil} (\operatorname{inv} (r))))}$.
Int.zpowLogGidefMathlib.Data.Int.Log, function or constantEnglish
Let $R$ be a set. Assume that $1 < b$. Then $\operatorname{zpowLogGi}$ applied to $R$ and $\mathrm{hb}$ is a Galois coinsertion of the function that maps $z$ to $b ^ {z}$ and the function that maps $r$ to the logarithm of $b$ and $r$.
Int.ModEqdefMathlib.Data.Int.ModEq, predicateEnglish
Let $n$, $a$ and $b$ be integers. Then $\operatorname{ModEq}$ holds for $n$, $a$ and $b$, if $\HModhModMACRoF {a}{n}= \HModhModMACRoF {b}{n}$.
Int.natAbsHomdefMathlib.Data.Int.NatAbs, function or constantWording
the natural absolute value homomorphism (from the name)
English
The natural absolute value homomorphism is a monoid with zero homomorphism of $\Integer$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\IntnatAbsMACRoY$ and $\mathrm{Int\_\_natAbs\_zero}$, $\mathrm{Int\_\_natAbs\_one}$ and $\mathrm{Int\_\_natAbs\_mul}$.
Int.rangedefMathlib.Data.Int.Range, function or constantWording
the range of m and n (from the name)
English
Let $m$ and $n$ be integers. Then the range of $m$ and $n$ is a list of integers defined as $\operatorname{map}$ applied to the function that maps $r$ to $m + r$ and $\operatorname{range}$ applied to $\operatorname{toNat}$ applied to $n - m$.
Int.sqrtdefMathlib.Data.Int.Sqrt, function or constantWording
the square root of z (from the name)
English
Let $z$ be an integer. Then the square root of $z$ is an integer defined as $\NatsqrtMACRoD {\operatorname{toNat} (z)}$.
WithZeroMulInt.toNNRealdefMathlib.Data.Int.WithZero, function or constantEnglish
Assume that $e \neq 0$. Then $\operatorname{toNNReal}$ applied to $\mathrm{he}$ is a monoid with zero homomorphism of $\mathrm{WithZero}$ applied to the set of multiplicatives of $\Integer$ and $\mathrm{NNReal}$.
LawfulXorclassMathlib.Data.LawfulXor.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{LawfulXor}$ holds for $x$.
Equiv.xordefMathlib.Data.LawfulXor.Equiv, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{xor}$ applied to $a$ is a permutation of $x$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $\operatorname{hXor}$ applied to $a$ and $x_{3}$, the function that maps $x_{4}$ to $\operatorname{hXor}$ applied to $a$ and $x_{4}$, $\mathrm{xor\_cancel\_left}$ applied to $a$ and $\mathrm{xor\_cancel\_left}$ applied to $a$.
AListstructureMathlib.Data.List.AList, typeWording
list of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Then the lists of $x_{1}$ are a basic type.
AList.DisjointdefMathlib.Data.List.AList, predicateWording
x2 is disjoint to x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be lists of $x_{1}$. Then $x_{2}$ is disjoint to $x_{3}$, if for all elements $k$ of $x$, if $k$ is an element of the key of $x_{2}$, then $k$ is not an element of the key of $x_{3}$.
AList.entriesdefMathlib.Data.List.AList, function or constantWording
the entry of self (from the name)
English
Let $\mathrm{self}$ be a list of $x_{1}$. Then the entry of $\mathrm{self}$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AList.erasedefMathlib.Data.List.AList, function or constantEnglish
Let $a$ be an element of $x$. Let $s$ be a list of $x_{1}$. Then $\operatorname{erase}$ applied to $a$ and $s$ is a list of $x_{1}$.
AList.foldldefMathlib.Data.List.AList, function or constantEnglish
Let $f$ be a function from elements of $x_{2}$ and elements $a$ of $x$ and elements of $x_{1}$ applied to $a$ to elements of $x_{2}$. Let $d$ be an element of $x_{2}$. Let $m$ be a list of $x_{1}$. Then $\operatorname{foldl}$ applied to $a$, $f$, $d$ and $m$ is an element of $x_{2}$ defined as the function that maps $m$ to $\operatorname{foldl}$ applied to the function that maps $r$ and $a$ to $a$ applied to $r$, $\operatorname{fst}$ applied to $a$ and $\operatorname{snd}$ applied to $a$, $f$, the entry of $d$ and $m$.
AList.insertdefMathlib.Data.List.AList, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $s$ be a list of $x_{1}$. Then $\operatorname{insert}$ applied to $a$, $b$ and $s$ is a list of $x_{1}$.
AList.insertRecdefMathlib.Data.List.AList, function or constantEnglish
Let $H_{0}$ be an element of $C$ applied to $\operatorname{emptyCollection}$. Let $\mathrm{IH}$ be a function from elements $a$ of $x$ and elements $b$ of $x_{1}$ applied to $a$ and lists $l_{1}$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is not an element of $l_{1}$ and elements of $C$ applied to $l_{1}$ to elements of $C$ applied to $\operatorname{insert}$ applied to $a$, $b$ and $l_{1}$. Let $l$ be a list of $x_{1}$. Then $\operatorname{insertRec}$ applied to $H_{0}$, $a$, $b$, $l_{1}$, $\mathrm{IH}$ and $l$ is an element of $C$ applied to $l$.
AList.keysdefMathlib.Data.List.AList, function or constantWording
the key of s (from the name)
English
Let $s$ be a list of $x_{1}$. Then the key of $s$ is a list of elements of $x$ defined as the key of the entry of $s$.
AList.lookupdefMathlib.Data.List.AList, function or constantEnglish
Let $a$ be an element of $x$. Let $s$ be a list of $x_{1}$. Then $\operatorname{lookup}$ applied to $a$ and $s$ is an element of $\mathrm{Option}$ applied to $x_{1}$ applied to $a$ defined as $\operatorname{dlookup}$ applied to $a$ and the entry of $s$.
AList.replacedefMathlib.Data.List.AList, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $s$ be a list of $x_{1}$. Then $\operatorname{replace}$ applied to $a$, $b$ and $s$ is a list of $x_{1}$.
AList.singletondefMathlib.Data.List.AList, function or constantWording
the singleton association list of a and b (from the docstring)
English
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Then the singleton association list of $a$ and $b$ is a list of $x_{1}$.
AList.uniondefMathlib.Data.List.AList, function or constantWording
the union of x3 and x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be lists of $x_{1}$. Then the union of $x_{3}$ and $x_{4}$ is a list of $x_{1}$.
List.toAListdefMathlib.Data.List.AList, function or constantWording
the list of l (from the name)
English
Let $l$ be a list of elements of $\Sigma$ applied to $x_{2}$. Then the list of $l$ is a list of $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{dedupKeys}$ applied to $l$ and $\mathrm{List\_\_nodupKeys\_dedupKeys}$ applied to $l$.
List.chainsdefMathlib.Data.List.Chain, typeWording
chain of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then a chain of $r$ is an element of the function that maps $r$ to $\SubtypeSet {l}{\operatorname{IsChain} (\mathrm{flip} (r), l)}$.
List.lex_chainsdefMathlib.Data.List.Chain, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $l$ and $m$ be chains of $r$. Then $\mathrm{List\_\_lex\_chains}$ holds for $r$, $l$ and $m$, if $\operatorname{Lex}$ holds for $r$, $l$ and $m$.
CycledefMathlib.Data.List.Cycle, typeWording
cycle of x (from the name)
English
Let $x$ be a set. Then a cycle of $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $x$.
Cycle.ChaindefMathlib.Data.List.Cycle, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $c$ be a cycle of $x$. Then we can say that $\operatorname{Chain}$ holds for $r$ and $c$.
Cycle.MemdefMathlib.Data.List.Cycle, predicateEnglish
Let $s$ be a cycle of $x$. Let $a$ be an element of $x$. Then we can say that $\operatorname{Mem}$ holds for $s$ and $a$.
Cycle.NodupdefMathlib.Data.List.Cycle, predicateEnglish
Let $s$ be a cycle of $x$. Then we can say that $\operatorname{Nodup}$ holds for $s$.
Cycle.NontrivialdefMathlib.Data.List.Cycle, predicateWording
s is nontrivial (from the name)
English
Let $s$ be a cycle of $x$. Then $s$ is nontrivial, if there exist elements $x_{1}$ and $y$ of $x$, such that $x_{1} \neq y$, $x_{1}$ is an element of $s$ and $y$ is an element of $s$.
Cycle.SubsingletondefMathlib.Data.List.Cycle, predicateWording
s is a subsingleton (from the name)
English
Let $s$ be a cycle of $x$. Then $s$ is a subsingleton, if the length of $s$ is less than or equal to $1$.
Cycle.lengthdefMathlib.Data.List.Cycle, function or constantWording
the length of s (from the name)
English
Let $s$ be a cycle of $x$. Then the length of $s$ is a natural number.
Cycle.listsdefMathlib.Data.List.Cycle, function or constantWording
the list of s (from the name)
English
Let $s$ be a cycle of $x$. Then the list of $s$ is a multiset of the set of lists of elements of $x$.
Cycle.mapdefMathlib.Data.List.Cycle, function or constantWording
the map of f and x2 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a cycle of $x$. Then the map of $f$ and $x_{2}$ is a cycle of $x_{1}$ defined as the map of $\operatorname{map}$ applied to $f$ and $x_{2}$.
Cycle.nextdefMathlib.Data.List.Cycle, function or constantEnglish
Let $s$ be a cycle of $x$ such that $\operatorname{Nodup}$ holds for $s$. Let $x_{2}$ be an element of $x$ such that $x_{2}$ is an element of $s$. Then $\operatorname{next}$ applied to $s$, $\mathrm{\_hs}$, $x_{2}$ and $\mathrm{\_hx}$ is an element of $x$.
Cycle.nildefMathlib.Data.List.Cycle, function or constantEnglish
$\operatorname{nil}$ is a cycle of $x$ defined as the cycle of $\operatorname{nil}$.
Cycle.ofListdefMathlib.Data.List.Cycle, function or constantWording
the cycle of x1 (from the name)
English
Let $x_{1}$ be a list of elements of $x$. Then the cycle of $x_{1}$ is a cycle of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{r}$ and $x_{1}$.
Cycle.prevdefMathlib.Data.List.Cycle, function or constantEnglish
Let $s$ be a cycle of $x$ such that $\operatorname{Nodup}$ holds for $s$. Let $x_{2}$ be an element of $x$ such that $x_{2}$ is an element of $s$. Then $\operatorname{prev}$ applied to $s$, $\mathrm{\_hs}$, $x_{2}$ and $\mathrm{\_hx}$ is an element of $x$.
Cycle.reversedefMathlib.Data.List.Cycle, function or constantWording
the reverse of s (from the name)
English
Let $s$ be a cycle of $x$. Then the reverse of $s$ is a cycle of $x$ defined as the map of $\operatorname{reverse}$ and $s$.
Cycle.toFinsetdefMathlib.Data.List.Cycle, function or constantWording
the finite set of s (from the name)
English
Let $s$ be a cycle of $x$. Then the finite set of $s$ is a finite set of $x$ defined as the finite set of the multiset of $s$.
Cycle.toMultisetdefMathlib.Data.List.Cycle, function or constantWording
the multiset of s (from the name)
English
Let $s$ be a cycle of $x$. Then the multiset of $s$ is a multiset of $x$.
List.nextdefMathlib.Data.List.Cycle, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $x_{2}$ be an element of $x$ such that $x_{2}$ is an element of $l$. Then $\operatorname{next}$ applied to $l$, $x_{2}$ and $h$ is an element of $x$ defined as $\operatorname{nextOr}$ applied to $l$, $x_{2}$ and $\operatorname{get}$ applied to $l$ and $\operatorname{mk}$ applied to $0$ and $\mathrm{List\_\_length\_pos\_of\_mem}$ applied to $h$.
List.nextOrdefMathlib.Data.List.Cycle, function or constantEnglish
Let $x_{2}$ be a list of elements of $x$. Let $x_{3}$ and $x_{4}$ be elements of $x$. Then $\operatorname{nextOr}$ applied to $x_{2}$, $x_{3}$ and $x_{4}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{List\_\_nextOr\_\_\_f}$, $x_{3}$ and $x_{4}$.
List.prevdefMathlib.Data.List.Cycle, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $x_{2}$ be an element of $x$ such that $x_{2}$ is an element of $l$. Then $\operatorname{prev}$ applied to $l$, $x_{2}$ and $h$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{List\_\_prev\_\_\_f}$, $x_{2}$ and $h$.
List.ForalldefMathlib.Data.List.Defs, predicateEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $x_{1}$ be a list of elements of $x$. Then $\operatorname{Forall}$ holds for $p$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $x_{1}$ and $\mathrm{List\_\_Forall\_\_\_f}$ applied to $p$.
List.andMdefMathlib.Data.List.Defs, function or constantEnglish
Let $x_{1}$ be a list of elements of $m$ applied to $\mathrm{Bool}$. Then $\operatorname{andM}$ applied to $x_{1}$ is an element of $m$ applied to $\mathrm{Bool}$ defined as $\operatorname{allM}$ applied to $\mathrm{id}$ and $x_{1}$.
List.choosedefMathlib.Data.List.Defs, function or constantEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a list of elements of $x$ such that there exists an element $a$ of $x$, such that $a$ is an element of $l$ and $p$ holds for $a$. Then $\operatorname{choose}$ applied to $p$, $l$ and $\mathrm{hp}$ is an element of $x$ defined as $\operatorname{chooseX}$ applied to $p$, $l$ and $\mathrm{hp}$.
List.chooseXdefMathlib.Data.List.Defs, function or constantEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a list of elements of $x$ such that there exists an element $a_{1}$ of $x$, such that $a_{1}$ is an element of $l$ and $p$ holds for $a_{1}$. Then $\operatorname{chooseX}$ applied to $p$, $l$ and $h$ is an element of $\SubtypeSet {a}{\mathrm{and} (\MembershipmemMACRoT {l}{a}, p (a))}$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{List\_\_chooseX\_\_\_f}$ applied to $p$ and $h$.
List.consecutivePairsdefMathlib.Data.List.Defs, function or constantWording
the consecutive pair of l (from the name)
English
Let $l$ be a list of elements of $x$. Then the consecutive pair of $l$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\operatorname{zip}$ applied to $l$ and $\operatorname{tail}$ applied to $l$.
List.dedupdefMathlib.Data.List.Defs, function or constantEnglish
Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{dedup}$ applied to $x_{2}$ is a list of elements of $x$ defined as $\operatorname{pwFilter}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Neq} (x_{2} , x_{3})$ and $x_{2}$.
List.destutterdefMathlib.Data.List.Defs, function or constantEnglish
Let $R$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{destutter}$ applied to $R$ and $x_{2}$ is a list of elements of $x$.
List.destutter'defMathlib.Data.List.Defs, function or constantEnglish
Let $R$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{2}$ be an element of $x$. Let $x_{3}$ be a list of elements of $x$. Then $\operatorname{destutter'}$ applied to $R$, $x_{2}$ and $x_{3}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{List\_\_destutter'\_\_\_f}$ applied to $R$ and $x_{2}$.
List.findMdefMathlib.Data.List.Defs, function or constantEnglish
Let $\mathrm{tac}$ be a function from elements of $x$ to elements of $m$ applied to $\mathrm{PUnit}$. Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{findM}$ applied to $\mathrm{tac}$ and $x_{2}$ is an element of $m$ applied to $x$ defined as $\operatorname{firstM}$ applied to the function that maps $a$ to $\operatorname{mapConstRev}$ applied to $\mathrm{tac}$ applied to $a$ and $a$ and $x_{2}$.
List.findM?'defMathlib.Data.List.Defs, function or constantEnglish
Let $p$ be a function from elements of $x_{1}$ to elements of $m$ applied to $\mathrm{ULift}$ applied to $\mathrm{Bool}$. Let $x_{2}$ be a list of elements of $x_{1}$. Then $\mathrm{List\_\_findM?'}$ applied to $p$ and $x_{2}$ is an element of $m$ applied to $\mathrm{Option}$ applied to $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{List\_\_findM?'\_\_\_f}$ applied to $p$.
List.foldlIdxMdefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from natural numbers and elements of $x_{2}$ and elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $b$ be an element of $x_{2}$. Let $\mathrm{as}$ be a list of elements of $x_{1}$. Then $\operatorname{foldlIdxM}$ applied to $f$, $b$ and $\mathrm{as}$ is an element of $m$ applied to $x_{2}$ defined as $\operatorname{foldlIdx}$ applied to the function that maps $i$, $\mathrm{ma}$ and $b_{1}$ to $\operatorname{bind}$ applied to $\mathrm{ma}$ and the function that maps $a$ to $f$ applied to $i$, $a$ and $b_{1}$, $\operatorname{pure}$ applied to $b$, $\mathrm{as}$ and $0$.
List.foldrIdxMdefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from natural numbers and elements of $x_{1}$ and elements of $x_{2}$ to elements of $m$ applied to $x_{2}$. Let $b$ be an element of $x_{2}$. Let $\mathrm{as}$ be a list of elements of $x_{1}$. Then $\operatorname{foldrIdxM}$ applied to $f$, $b$ and $\mathrm{as}$ is an element of $m$ applied to $x_{2}$ defined as $\operatorname{foldrIdx}$ applied to the function that maps $i$, $a$ and $\mathrm{mb}$ to $\operatorname{bind}$ applied to $\mathrm{mb}$ and the function that maps $b_{1}$ to $f$ applied to $i$, $a$ and $b_{1}$, $\operatorname{pure}$ applied to $b$, $\mathrm{as}$ and $0$.
List.getIdefMathlib.Data.List.Defs, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $n$ be a natural number. Then $\operatorname{getI}$ applied to $l$ and $n$ is an element of $x$ defined as $\operatorname{getD}$ applied to $l$, $n$ and $\operatorname{default}$.
List.getLastIdefMathlib.Data.List.Defs, function or constantWording
the last element of x2 (from the docstring)
English
Let $x_{2}$ be a list of elements of $x$. Then the last element of $x_{2}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{List\_\_getLastI\_\_\_f}$.
List.headIdefMathlib.Data.List.Defs, function or constantWording
the head of x2 (from the docstring)
English
Let $x_{2}$ be a list of elements of $x$. Then the head of $x_{2}$ is an element of $x$.
List.iteratedefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $a$ be an element of $x$. Let $n$ be a natural number. Then $\operatorname{iterate}$ applied to $f$, $a$ and $n$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{List\_\_iterate\_\_\_f}$ applied to $f$ and $a$.
List.iterateTRdefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Let $a$ be an element of $x$. Let $n$ be a natural number. Then $\operatorname{iterateTR}$ applied to $f$, $a$ and $n$ is a list of elements of $x$ defined as $\operatorname{loop}$ applied to $f$, $a$, $n$ and $\operatorname{nil}$.
List.mapAccumrdefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$. Let $x_{3}$ be a list of elements of $x$. Let $x_{4}$ be an element of $x_{2}$. Then $\operatorname{mapAccumr}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Prod}$ applied to $x_{2}$ and the set of lists of elements of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{List\_\_mapAccumr\_\_\_f}$ applied to $f$ and $x_{4}$.
List.mapAccumr₂defMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ and elements of $x_{2}$ to elements of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$. Let $x_{4}$ be a list of elements of $x$. Let $x_{5}$ be a list of elements of $x_{1}$. Let $x_{6}$ be an element of $x_{2}$. Then $\mathrm{List\_\_mapAccumr\_u2082\_}$ applied to $f$, $x_{4}$, $x_{5}$ and $x_{6}$ is an element of $\mathrm{Prod}$ applied to $x_{2}$ and the set of lists of elements of $x_{3}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$, $\mathrm{List\_\_mapAccumr\_u2082\_\_\_\_f}$ applied to $f$, $x_{5}$ and $x_{6}$.
List.mapAsyncChunkeddefMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{xs}$ be a list of elements of $x$. Let $\mathrm{chunk\_size}$ be an element of $\mathrm{optParam}$ applied to $\Natural$ and $1024$. Then $\operatorname{mapAsyncChunked}$ applied to $f$, $\mathrm{xs}$ and $\mathrm{chunk\_size}$ is a list of elements of $x_{1}$ defined as $\operatorname{flatMap}$ applied to $\operatorname{get}$ and $\operatorname{map}$ applied to the function that maps $\mathrm{xs1}$ to $\operatorname{spawn}$ applied to the function that maps $x_{2}$ to $\operatorname{map}$ applied to $f$ and $\mathrm{xs1}$ and $\operatorname{default}$ and $\operatorname{toChunks}$ applied to $\mathrm{chunk\_size}$ and $\mathrm{xs}$.
List.mapDiagM'defMathlib.Data.List.Defs, function or constantWording
the map diagonal of f and x2 (from the name)
English
Let $f$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to elements of $m$ applied to $\mathrm{Unit}$. Let $x_{2}$ be a list of elements of $x_{1}$. Then the map diagonal of $f$ and $x_{2}$ is an element of $m$ applied to $\mathrm{Unit}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{List\_\_mapDiagM'\_\_\_f}$ applied to $f$.
List.mapIdxM'defMathlib.Data.List.Defs, function or constantWording
the map index of f and as (from the name)
English
Let $f$ be a function from natural numbers and elements of $x_{1}$ to elements of $m$ applied to $\mathrm{PUnit}$. Let $\mathrm{as}$ be a list of elements of $x_{1}$. Then the map index of $f$ and $\mathrm{as}$ is an element of $m$ applied to $\mathrm{PUnit}$ defined as $\operatorname{mapIdxMAux'}$ applied to $f$, $0$ and $\mathrm{as}$.
List.map₂LeftdefMathlib.Data.List.Defs, function or constantWording
the left map of x3 and x4 (from the name)
English
Let $f$ be a function from elements of $x$ and elements of $\mathrm{Option}$ applied to $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a list of elements of $x$. Let $x_{4}$ be a list of elements of $x_{1}$. Then the left map of $x_{3}$ and $x_{4}$ is a list of elements of $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{List\_\_map\_u2082\_Left\_\_\_f}$ applied to $f$ and $x_{4}$.
List.map₂Left'defMathlib.Data.List.Defs, function or constantWording
the left map of x3 and x4 (from the name)
English
Let $f$ be a function from elements of $x$ and elements of $\mathrm{Option}$ applied to $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a list of elements of $x$. Let $x_{4}$ be a list of elements of $x_{1}$. Then the left map of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Prod}$ applied to the set of lists of elements of $x_{2}$ and the set of lists of elements of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{List\_\_map\_u2082\_Left'\_\_\_f}$ applied to $f$ and $x_{4}$.
List.map₂RightdefMathlib.Data.List.Defs, function or constantWording
the right map of as and bs (from the name)
English
Let $f$ be a function from elements of $\mathrm{Option}$ applied to $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $\mathrm{as}$ be a list of elements of $x$. Let $\mathrm{bs}$ be a list of elements of $x_{1}$. Then the right map of $\mathrm{as}$ and $\mathrm{bs}$ is a list of elements of $x_{2}$ defined as the left map of $\mathrm{bs}$ and $\mathrm{as}$.
List.map₂Right'defMathlib.Data.List.Defs, function or constantWording
the right map of as and bs (from the name)
English
Let $f$ be a function from elements of $\mathrm{Option}$ applied to $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $\mathrm{as}$ be a list of elements of $x$. Let $\mathrm{bs}$ be a list of elements of $x_{1}$. Then the right map of $\mathrm{as}$ and $\mathrm{bs}$ is an element of $\mathrm{Prod}$ applied to the set of lists of elements of $x_{2}$ and the set of lists of elements of $x$ defined as the left map of $\mathrm{bs}$ and $\mathrm{as}$.
List.orMdefMathlib.Data.List.Defs, function or constantEnglish
Let $x_{1}$ be a list of elements of $m$ applied to $\mathrm{Bool}$. Then $\operatorname{orM}$ applied to $x_{1}$ is an element of $m$ applied to $\mathrm{Bool}$ defined as $\operatorname{anyM}$ applied to $\mathrm{id}$ and $x_{1}$.
List.permutationsdefMathlib.Data.List.Defs, function or constantWording
the permutation of l (from the name)
English
Let $l$ be a list of elements of $x$. Then the permutation of $l$ is a list of lists of elements of $x$ defined as $\operatorname{cons}$ applied to $l$ and $\operatorname{permutationsAux}$ applied to $l$ and $\operatorname{nil}$.
List.permutations'defMathlib.Data.List.Defs, function or constantWording
the permutation of x1 (from the name)
English
Let $x_{1}$ be a list of elements of $x$. Then the permutation of $x_{1}$ is a list of lists of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{List\_\_permutations'\_\_\_f}$.
List.replaceIfdefMathlib.Data.List.Defs, function or constantEnglish
Let $x_{1}$ and $x_{3}$ be lists of elements of $x$. Let $x_{2}$ be a list of elements of $\mathrm{Bool}$. Then $\operatorname{replaceIf}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{List\_\_replaceIf\_\_\_f}$, $x_{2}$ and $x_{3}$.
List.takeIdefMathlib.Data.List.Defs, function or constantEnglish
Let $n$ be a natural number. Let $l$ be a list of elements of $x$. Then $\operatorname{takeI}$ applied to $n$ and $l$ is a list of elements of $x$ defined as $\operatorname{takeD}$ applied to $n$, $l$ and $\operatorname{default}$.
List.zipWith3defMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ and elements of $x_{2}$ to elements of $x_{3}$. Let $x_{4}$ be a list of elements of $x$. Let $x_{5}$ be a list of elements of $x_{1}$. Let $x_{6}$ be a list of elements of $x_{2}$. Then $\operatorname{zipWith3}$ applied to $f$, $x_{4}$, $x_{5}$ and $x_{6}$ is a list of elements of $x_{3}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$, $\mathrm{List\_\_zipWith3\_\_\_f}$ applied to $f$, $x_{5}$ and $x_{6}$.
List.zipWith4defMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ and elements of $x_{2}$ and elements of $x_{3}$ to elements of $x_{4}$. Let $x_{5}$ be a list of elements of $x$. Let $x_{6}$ be a list of elements of $x_{1}$. Let $x_{7}$ be a list of elements of $x_{2}$. Let $x_{8}$ be a list of elements of $x_{3}$. Then $\operatorname{zipWith4}$ applied to $f$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ is a list of elements of $x_{4}$ defined as $\operatorname{brecOn}$ applied to $x_{5}$, $\mathrm{List\_\_zipWith4\_\_\_f}$ applied to $f$, $x_{6}$, $x_{7}$ and $x_{8}$.
List.zipWith5defMathlib.Data.List.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ and elements of $x_{2}$ and elements of $x_{3}$ and elements of $x_{4}$ to elements of $x_{5}$. Let $x_{6}$ be a list of elements of $x$. Let $x_{7}$ be a list of elements of $x_{1}$. Let $x_{8}$ be a list of elements of $x_{2}$. Let $x_{9}$ be a list of elements of $x_{3}$. Let $x_{10}$ be a list of elements of $x_{4}$. Then $\operatorname{zipWith5}$ applied to $f$, $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ is a list of elements of $x_{5}$ defined as $\operatorname{brecOn}$ applied to $x_{6}$, $\mathrm{List\_\_zipWith5\_\_\_f}$ applied to $f$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$.
List.rdropdefMathlib.Data.List.DropRight, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $n$ be a natural number. Then $\operatorname{rdrop}$ applied to $l$ and $n$ is a list of elements of $x$ defined as $\operatorname{take}$ applied to $\operatorname{length} (l)- n$ and $l$.
List.rdropWhiledefMathlib.Data.List.DropRight, function or constantEnglish
Let $p$ be a function from elements of $x$ to elements of $\mathrm{Bool}$. Let $l$ be a list of elements of $x$. Then $\operatorname{rdropWhile}$ applied to $p$ and $l$ is a list of elements of $x$ defined as $\operatorname{reverse}$ applied to $\operatorname{dropWhile}$ applied to $p$ and $\operatorname{reverse}$ applied to $l$.
List.rtakedefMathlib.Data.List.DropRight, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $n$ be a natural number. Then $\operatorname{rtake}$ applied to $l$ and $n$ is a list of elements of $x$ defined as $\operatorname{drop}$ applied to $\operatorname{length} (l)- n$ and $l$.
List.rtakeWhiledefMathlib.Data.List.DropRight, function or constantEnglish
Let $p$ be a function from elements of $x$ to elements of $\mathrm{Bool}$. Let $l$ be a list of elements of $x$. Then $\operatorname{rtakeWhile}$ applied to $p$ and $l$ is a list of elements of $x$ defined as $\operatorname{reverse}$ applied to $\operatorname{takeWhile}$ applied to $p$ and $\operatorname{reverse}$ applied to $l$.
List.DuplicateinductiveMathlib.Data.List.Duplicate, predicateEnglish
Let $x_{1}$ be an element of $x$. Let $x_{2}$ be a list of elements of $x$. Then we can say that $\operatorname{Duplicate}$ holds for $x_{1}$ and $x_{2}$.
List.Duplicate.belowinductiveMathlib.Data.List.Duplicate, predicateEnglish
Assume that $\operatorname{Duplicate}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
List.SublistForall₂inductiveMathlib.Data.List.Forall2, predicateEnglish
Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $x_{2}$ be a list of elements of $x$. Let $x_{3}$ be a list of elements of $x_{1}$. Then we can say that $\mathrm{List\_\_SublistForall\_u2082\_}$ holds for $R$, $x_{2}$ and $x_{3}$.
List.SublistForall₂.belowinductiveMathlib.Data.List.Forall2, predicateEnglish
Assume that $\mathrm{List\_\_SublistForall\_u2082\_}$ holds for $R$, $x_{2}$ and $x_{3}$. Then we can say that $\mathrm{List\_\_SublistForall\_u2082\_\_\_below}$ holds for $t$.
List.bidirectionalRecdefMathlib.Data.List.Induction, function or constantEnglish
Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{singleton}$ be a function from elements $a_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $a_{1}$ and $\operatorname{nil}$. Let $\mathrm{cons\_append}$ be a function from elements $a$ of $x$ and lists $l_{1}$ of elements of $x$ and elements $b$ of $x$ and elements of $\mathrm{motive}$ applied to $l_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $a$ and $\operatorname{hAppend}$ applied to $l_{1}$ and $\operatorname{cons}$ applied to $b$ and $\operatorname{nil}$. Let $l$ be a list of elements of $x$. Then $\operatorname{bidirectionalRec}$ applied to $\mathrm{nil}$, $a_{1}$, $\mathrm{singleton}$, $a$, $l_{1}$, $b$, $\mathrm{cons\_append}$ and $l$ is an element of $\mathrm{motive}$ applied to $l$.
List.bidirectionalRecOndefMathlib.Data.List.Induction, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $H_{0}$ be an element of $C$ applied to $\operatorname{nil}$. Let $H_{1}$ be a function from elements $a_{1}$ of $x$ to elements of $C$ applied to $\operatorname{cons}$ applied to $a_{1}$ and $\operatorname{nil}$. Let $\mathrm{Hn}$ be a function from elements $a$ of $x$ and lists $l_{1}$ of elements of $x$ and elements $b$ of $x$ and elements of $C$ applied to $l_{1}$ to elements of $C$ applied to $\operatorname{cons}$ applied to $a$ and $\operatorname{hAppend}$ applied to $l_{1}$ and $\operatorname{cons}$ applied to $b$ and $\operatorname{nil}$. Then $\operatorname{bidirectionalRecOn}$ applied to $l$, $H_{0}$, $a_{1}$, $H_{1}$, $a$, $l_{1}$, $b$ and $\mathrm{Hn}$ is an element of $C$ applied to $l$ defined as the function that maps $a$, $l_{1}$, $b$ and $\mathrm{Hn}$ to $\operatorname{bidirectionalRec}$ applied to $H_{0}$, $a_{1}$, $H_{1}$, $l$, $a$, $l_{1}$, $b$ and $\mathrm{Hn}$.
List.recNeNildefMathlib.Data.List.Induction, function or constantEnglish
Let $\mathrm{singleton}$ be a function from elements $x_{3}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{3}$ and $\operatorname{nil}$ and $\mathrm{List\_\_cons\_ne\_nil}$ applied to $x_{3}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from elements $x_{1}$ of $x$ and lists $\mathrm{xs}$ of elements of $x$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (\mathrm{xs} , \operatorname{nil})$ and elements of $\mathrm{motive}$ applied to $\mathrm{xs}$ and $h_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $\mathrm{xs}$ and $\mathrm{List\_\_cons\_ne\_nil}$ applied to $x_{1}$ and $\mathrm{xs}$. Let $l$ be a list of elements of $x$ such that $l \neq \operatorname{nil}$. Then $\operatorname{recNeNil}$ applied to $x_{3}$, $\mathrm{singleton}$, $x_{1}$, $\mathrm{xs}$, $h_{1}$, $\mathrm{cons}$, $l$ and $h$ is an element of $\mathrm{motive}$ applied to $l$ and $h$ defined as the function that maps $h_{1}$, $\mathrm{cons}$, $l$ and $h$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{List\_\_recNeNil\_\_\_f}$ applied to $x_{3}$ and $\mathrm{singleton}$, $\mathrm{xs}$, $h_{1}$, $\mathrm{cons}$, $l$ and $h$.
List.recOnNeNildefMathlib.Data.List.Induction, function or constantEnglish
Let $l$ be a list of elements of $x$ such that $l \neq \operatorname{nil}$. Let $\mathrm{singleton}$ be a function from elements $x_{3}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{3}$ and $\operatorname{nil}$ and $\mathrm{List\_\_cons\_ne\_nil}$ applied to $x_{3}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from elements $x_{1}$ of $x$ and lists $\mathrm{xs}$ of elements of $x$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (\mathrm{xs} , \operatorname{nil})$ and elements of $\mathrm{motive}$ applied to $\mathrm{xs}$ and $h_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $\mathrm{xs}$ and $\mathrm{List\_\_cons\_ne\_nil}$ applied to $x_{1}$ and $\mathrm{xs}$. Then $\operatorname{recOnNeNil}$ applied to $l$, $h$, $x_{3}$, $\mathrm{singleton}$, $x_{1}$, $\mathrm{xs}$, $h_{1}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $l$ and $h$ defined as the function that maps $x_{1}$, $\mathrm{xs}$, $h_{1}$ and $\mathrm{cons}$ to $\operatorname{recNeNil}$ applied to $x_{3}$, $\mathrm{singleton}$, $l$, $h$, $x_{1}$, $\mathrm{xs}$, $h_{1}$ and $\mathrm{cons}$.
List.reverseRecdefMathlib.Data.List.Induction, function or constantEnglish
Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{append\_singleton}$ be a function from lists $l_{1}$ of elements of $x$ and elements $a$ of $x$ and elements of $\mathrm{motive}$ applied to $l_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{hAppend}$ applied to $l_{1}$ and $\operatorname{cons}$ applied to $a$ and $\operatorname{nil}$. Let $l$ be a list of elements of $x$. Then $\operatorname{reverseRec}$ applied to $\mathrm{nil}$, $l_{1}$, $a$, $\mathrm{append\_singleton}$ and $l$ is an element of $\mathrm{motive}$ applied to $l$.
List.reverseRecOndefMathlib.Data.List.Induction, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{append\_singleton}$ be a function from lists $l_{1}$ of elements of $x$ and elements $a$ of $x$ and elements of $\mathrm{motive}$ applied to $l_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{hAppend}$ applied to $l_{1}$ and $\operatorname{cons}$ applied to $a$ and $\operatorname{nil}$. Then $\operatorname{reverseRecOn}$ applied to $l$, $\mathrm{nil}$, $l_{1}$, $a$ and $\mathrm{append\_singleton}$ is an element of $\mathrm{motive}$ applied to $l$ defined as the function that maps $a$ and $\mathrm{append\_singleton}$ to $\operatorname{reverseRec}$ applied to $\mathrm{nil}$, $l_{1}$, $l$, $a$ and $\mathrm{append\_singleton}$.
List.twoStepInductiondefMathlib.Data.List.Induction, function or constantEnglish
Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{singleton}$ be a function from elements $x_{4}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{4}$ and $\operatorname{nil}$. Let $\mathrm{cons\_cons}$ be a function from elements $x_{1}$ of $x$ and elements $y$ of $x$ and lists $\mathrm{xs}$ of elements of $x$ and elements of $\mathrm{motive}$ applied to $\mathrm{xs}$ and functions from elements $y_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $y_{1}$ and $\mathrm{xs}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $\operatorname{cons}$ applied to $y$ and $\mathrm{xs}$. Let $l$ be a list of elements of $x$. Then $\operatorname{twoStepInduction}$ applied to $\mathrm{nil}$, $x_{4}$, $\mathrm{singleton}$, $x_{1}$, $y$, $\mathrm{xs}$, $\mathrm{cons\_cons}$ and $l$ is an element of $\mathrm{motive}$ applied to $l$.
List.InterleavesinductiveMathlib.Data.List.Interleave, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be lists of elements of $x$. Then we can say that $\operatorname{Interleaves}$ holds for $r$, $x_{1}$ and $x_{2}$.
List.Interleaves.belowinductiveMathlib.Data.List.Interleave, predicateEnglish
Assume that $\operatorname{Interleaves}$ holds for $r$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
List.IcodefMathlib.Data.List.Intervals, function or constantEnglish
Let $n$ and $m$ be natural numbers. Then $\operatorname{Ico}$ applied to $n$ and $m$ is a list of natural numbers defined as $\operatorname{range'}$ applied to $n$, $m - n$ and $1$.
List.argmaxdefMathlib.Data.List.MinMax, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a list of elements of $x$. Then $\operatorname{argmax}$ applied to $f$ and $l$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{foldl}$ applied to $\operatorname{argAux}$ applied to the function that maps $b$ and $c$ to $\mathrm{Lt} (f (c), f (b))$, $\operatorname{none}$ and $l$.
List.argmindefMathlib.Data.List.MinMax, function or constantWording
the argmin of f and l (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a list of elements of $x$. Then the argmin of $f$ and $l$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{foldl}$ applied to $\operatorname{argAux}$ applied to the function that maps $b$ and $c$ to $\mathrm{Lt} (f (b), f (c))$, $\operatorname{none}$ and $l$.
List.maximumdefMathlib.Data.List.MinMax, function or constantWording
the maximum of l (from the name)
English
Let $l$ be a list of elements of $x$. Then the maximum of $l$ is an element of $\mathrm{WithBot}$ applied to $x$ defined as $\operatorname{argmax}$ applied to $\mathrm{id}$ and $l$.
List.maximum_of_length_posdefMathlib.Data.List.MinMax, function or constantWording
the maximum value of h (from the docstring)
English
Assume that $0 < \operatorname{length} (l)$. Then the maximum value of $h$ is an element of $x$ defined as $\operatorname{unbot}$ applied to the maximum of $l$ and $\mathrm{List\_\_maximum\_ne\_bot\_of\_length\_pos}$ applied to $h$.
List.minimumdefMathlib.Data.List.MinMax, function or constantWording
the minimum of l (from the name)
English
Let $l$ be a list of elements of $x$. Then the minimum of $l$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as the argmin of $\mathrm{id}$ and $l$.
List.minimum_of_length_posdefMathlib.Data.List.MinMax, function or constantWording
the minimum value of h (from the docstring)
English
Assume that $0 < \operatorname{length} (l)$. Then the minimum value of $h$ is an element of $x$ defined as $\operatorname{untop}$ applied to the minimum of $l$ and $\mathrm{List\_\_minimum\_ne\_top\_of\_length\_pos}$ applied to $h$.
List.Nat.antidiagonaldefMathlib.Data.List.NatAntidiagonal, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{antidiagonal}$ applied to $n$ is a list of elements of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\operatorname{map}$ applied to the function that maps $i$ to $\ProdmkMACRoU {i}{(n - i)}$ and $\operatorname{range}$ applied to $n + 1$.
List.Nodup.getBijectionOfForallMemListdefMathlib.Data.List.NodupEquivFin, function or constantEnglish
Let $l$ be a list of elements of $x$ such that $\operatorname{Nodup}$ holds for $l$ and for all elements $x_{1}$ of $x$, $\MembershipmemMACRoT {l}{x_{1}}$. Then $\operatorname{getBijectionOfForallMemList}$ applied to $l$, $\mathrm{nd}$ and $h$ is an element of $\SubtypeSet {f}{\operatorname{Bijective} (f)}$ defined as the function that maps $i$ to $\operatorname{get}$ applied to $l$ and $i$.
List.Nodup.getEquivdefMathlib.Data.List.NodupEquivFin, function or constantEnglish
Let $l$ be a list of elements of $x$ such that $\operatorname{Nodup}$ holds for $l$. Then $\operatorname{getEquiv}$ applied to $l$ and $H$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\operatorname{length} (l))}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {l}{x_{2}})})}$.
List.Nodup.getEquivOfForallMemListdefMathlib.Data.List.NodupEquivFin, function or constantEnglish
Let $l$ be a list of elements of $x$ such that $\operatorname{Nodup}$ holds for $l$ and for all elements $x_{2}$ of $x$, $x_{2}$ is an element of $l$. Then $\operatorname{getEquivOfForallMemList}$ applied to $l$, $\mathrm{nd}$ and $h$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\operatorname{length} (l))}{x}$.
List.SortedLT.getIsodefMathlib.Data.List.NodupEquivFin, function or constantEnglish
Let $l$ be a list of elements of $x$ such that $\operatorname{SortedLT}$ holds for $l$. Then $\operatorname{getIso}$ applied to $l$ and $H$ is an order isomorphism of $\mathrm{Fin}$ applied to $\operatorname{length}$ applied to $l$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {l}{x_{3}})}$.
List.getEquivOfForallCountEqOnedefMathlib.Data.List.NodupEquivFin, function or constantEnglish
Let $l$ be a list of elements of $x$ such that for all elements $x_{2}$ of $x$, the multiplicity of $x_{2}$ in $l$ is equal to $1$. Then $\operatorname{getEquivOfForallCountEqOne}$ applied to $l$ and $h$ is an element of $\EquivMACRoAE {\mathrm{Fin} (\operatorname{length} (l))}{x}$.
List.equivSigmaTupledefMathlib.Data.List.OfFn, function or constantWording
the equivalence sigma tuple (from the name)
English
The equivalence sigma tuple is an equivalence from the set of lists of elements of $x$ to $\Sigma$ applied to the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$.
List.ofFnRecdefMathlib.Data.List.OfFn, function or constantWording
the list of h and n (from the name)
English
Let $h$ be a function from natural numbers $n$ and functions $f$ from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$ to elements of $C$ applied to $\operatorname{ofFn}$ applied to $f$. Let $l$ be a list of elements of $x$. Then the list of $n$ and $f$ is an element of $C$ applied to $l$.
List.offDiagdefMathlib.Data.List.OffDiag, function or constantEnglish
Let $l$ be a list of elements of $x$. Then $\operatorname{offDiag}$ applied to $l$ is a list of elements of $\mathrm{Prod}$ applied to $x$ and $x$.
List.PalindromeinductiveMathlib.Data.List.Palindrome, predicateWording
x1 is a palindrome (from the name)
English
Let $x_{1}$ be a list of elements of $x$. Then we can say that $x_{1}$ is a palindrome.
List.Palindrome.belowinductiveMathlib.Data.List.Palindrome, predicateEnglish
Assume that $x_{1}$ is a palindrome. Then we can say that $\operatorname{below}$ holds for $t$.
List.HasPerioddefMathlib.Data.List.PeriodicityLemma, predicateEnglish
Let $w$ be a list of elements of $x$. Let $p$ be a natural number. Then $\operatorname{HasPeriod}$ holds for $w$ and $p$, if $\operatorname{IsPrefix}$ holds for $w$ and $\operatorname{hAppend}$ applied to $\operatorname{take}$ applied to $p$ and $w$ and $w$.
List.Pi.consdefMathlib.Data.List.Pi, function or constantEnglish
Let $i$ and $j$ be elements of $x$. Let $l$ be a list of elements of $x$. Let $a$ be an element of $x_{2}$ applied to $i$. Let $f$ be a function from elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {l}{j_{1}}$ to elements of $x_{2}$ applied to $j_{1}$. Assume that $\MembershipmemMACRoT {\operatorname{cons} (i , l)}{j}$. Then $\operatorname{cons}$ applied to $i$, $l$, $a$, $j_{1}$, $f$, $j$ and $h$ is an element of $x_{2}$ applied to $j$ defined as the function that maps $h$ to $\operatorname{cons}$ applied to the multiset of $l$, $i$, $a$, $j_{1}$, $f$, $j$ and $h$.
List.Pi.headdefMathlib.Data.List.Pi, function or constantWording
the head of f (from the name)
English
Let $f$ be a function from elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{cons} (i , l)}{j}$ to elements of $x_{1}$ applied to $j$. Then the head of $j$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $f$ to $j$ applied to $i$, $\mathrm{List\_\_mem\_cons\_self}$ and $f$.
List.Pi.nildefMathlib.Data.List.Pi, function or constantEnglish
Let $x_{1}$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$ such that $i$ is an element of $\operatorname{nil}$. Then $\operatorname{nil}$ applied to $x_{1}$, $i$ and $h$ is an element of $x_{1}$ applied to $i$.
List.Pi.taildefMathlib.Data.List.Pi, function or constantWording
the tail of f and j1 (from the name)
English
Let $f$ be a function from elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{cons} (i , l)}{j_{1}}$ to elements of $x_{1}$ applied to $j_{1}$. Let $j$ be an element of $x$ such that $j$ is an element of $l$. Then the tail of $j_{1}$ and $f$ is an element of $x_{1}$ applied to $j$ defined as the function that maps $h$ to $j_{1}$ applied to $f$, $\mathrm{List\_\_mem\_cons\_of\_mem}$ applied to $i$ and $j$ and $h$.
List.pidefMathlib.Data.List.Pi, function or constantWording
the product of l and x3 (from the name)
English
Let $l$ be a list of elements of $x$. Let $x_{3}$ be a function from elements $i_{1}$ of $x$ to lists of elements of $x_{2}$ applied to $i_{1}$. Then the product of $l$ and $i_{1}$ is a list of functions from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {l}{i}$ to elements of $x_{2}$ applied to $i$ defined as the function that maps $x_{3}$ to $\operatorname{brecOn}$ applied to $l$, $\mathrm{List\_\_pi\_\_\_f}$, $i_{1}$ and $x_{3}$.
List.rangesdefMathlib.Data.List.Range, function or constantWording
the range of x (from the name)
English
Let $x$ be a list of natural numbers. Then the range of $x$ is a list of lists of natural numbers defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{List\_\_ranges\_\_\_f}$.
List.IsRotateddefMathlib.Data.List.Rotate, predicateEnglish
Let $l$ and $\mathrm{l'}$ be lists of elements of $x$. Then $\operatorname{IsRotated}$ holds for $l$ and $\mathrm{l'}$, if there exists a natural number $n$, such that $\EqtMACRoH {\operatorname{rotate} (l , n)}{\mathrm{l'}}$.
List.cyclicPermutationsdefMathlib.Data.List.Rotate, function or constantWording
the cyclic permutation of x1 (from the name)
English
Let $x_{1}$ be a list of elements of $x$. Then the cyclic permutation of $x_{1}$ is a list of lists of elements of $x$.
List.ShortlexdefMathlib.Data.List.Shortlex, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be lists of elements of $x$. Then $\operatorname{Shortlex}$ holds for $r$, $x_{1}$ and $x_{2}$, if $\mathrm{InvImage}$ holds for $\operatorname{Lex}$ applied to the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$ and $\operatorname{Lex}$ applied to $r$, the function that maps $a$ to $\ProdmkMACRoU {\operatorname{length} (a)}{a}$, $x_{1}$ and $x_{2}$.
List.NodupKeysdefMathlib.Data.List.Sigma, predicateEnglish
Let $l$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{NodupKeys}$ holds for $l$, if $\operatorname{Nodup}$ holds for the key of $l$.
List.dedupKeysdefMathlib.Data.List.Sigma, function or constantEnglish
Let $x_{3}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{dedupKeys}$ applied to $x_{3}$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{foldr}$ applied to the function that maps $x_{3}$ to $\operatorname{kinsert}$ applied to $\operatorname{fst}$ applied to $x_{3}$ and $\operatorname{snd}$ applied to $x_{3}$, $\operatorname{nil}$ and $x_{3}$.
List.dlookupdefMathlib.Data.List.Sigma, function or constantEnglish
Let $a$ be an element of $x$. Let $x_{3}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{dlookup}$ applied to $a$ and $x_{3}$ is an element of $\mathrm{Option}$ applied to $x_{1}$ applied to $a$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{List\_\_dlookup\_\_\_f}$ applied to $a$.
List.kerasedefMathlib.Data.List.Sigma, function or constantEnglish
Let $a$ be an element of $x$. Let $x_{3}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{kerase}$ applied to $a$ and $x_{3}$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{eraseP}$ applied to the function that maps $s$ to $\operatorname{decide}$ applied to $\EqtMACRoH {a}{\operatorname{fst} (s)}$ and $x_{3}$.
List.keysdefMathlib.Data.List.Sigma, function or constantWording
the key of x2 (from the name)
English
Let $x_{2}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then the key of $x_{2}$ is a list of elements of $x$ defined as $\operatorname{map}$ applied to $\operatorname{fst}$ and $x_{2}$.
List.kinsertdefMathlib.Data.List.Sigma, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $l$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{kinsert}$ applied to $a$, $b$ and $l$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{cons}$ applied to $\operatorname{mk}$ applied to $a$ and $b$ and $\operatorname{kerase}$ applied to $a$ and $l$.
List.kreplacedefMathlib.Data.List.Sigma, function or constantEnglish
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $x_{3}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{kreplace}$ applied to $a$, $b$ and $x_{3}$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{lookmap}$ applied to the function that maps $s$ to $\iteMACRoG {(\EqtMACRoH {a}{\operatorname{fst} (s)})}{\operatorname{some} (\operatorname{mk} (a , b))}{\operatorname{none}}$ and $x_{3}$.
List.kuniondefMathlib.Data.List.Sigma, function or constantEnglish
Let $x_{3}$ and $x_{4}$ be lists of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{kunion}$ applied to $x_{3}$ and $x_{4}$ is a list of elements of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{List\_\_kunion\_\_\_f}$ and $x_{4}$.
List.lookupAlldefMathlib.Data.List.Sigma, function or constantEnglish
Let $a$ be an element of $x$. Let $x_{3}$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{lookupAll}$ applied to $a$ and $x_{3}$ is a list of elements of $x_{1}$ applied to $a$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{List\_\_lookupAll\_\_\_f}$ applied to $a$.
List.signVariationsdefMathlib.Data.List.SignVariations, function or constantWording
the sign variation of l (from the name)
English
Let $l$ be a list of elements of $x$. Then the sign variation of $l$ is a natural number defined as the difference between $\operatorname{length}$ applied to $\operatorname{destutter}$ applied to the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Neq} (x_{3} , x_{4})$ and $\operatorname{filter}$ applied to the function that maps $x_{5}$ to $\operatorname{decide}$ applied to $\mathrm{Neq} (x_{5} , 0)$ and $\operatorname{map}$ applied to $\operatorname{coe}$ applied to the sign and $l$ and $1$.
List.SortedGEdefMathlib.Data.List.Sort, predicateEnglish
Let $l$ be a list of elements of $x$. Then $\operatorname{SortedGE}$ holds for $l$, if $\operatorname{get}$ applied to $l$ is an antitone.
List.SortedGTdefMathlib.Data.List.Sort, predicateEnglish
Let $l$ be a list of elements of $x$. Then $\operatorname{SortedGT}$ holds for $l$, if $\operatorname{get}$ applied to $l$ is a strict antitone.
List.SortedLEdefMathlib.Data.List.Sort, predicateEnglish
Let $l$ be a list of elements of $x$. Then $\operatorname{SortedLE}$ holds for $l$, if $\operatorname{get}$ applied to $l$ is monotone.
List.SortedLTdefMathlib.Data.List.Sort, predicateEnglish
Let $l$ be a list of elements of $x$. Then $\operatorname{SortedLT}$ holds for $l$, if $\mathrm{StrictMono}$ holds for $\operatorname{get}$ applied to $l$.
List.insertionSortdefMathlib.Data.List.Sort, function or constantWording
the insertion sort of r and x2 (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{2}$ be a list of elements of $x$. Then the insertion sort of $r$ and $x_{2}$ is a list of elements of $x$ defined as $\operatorname{foldr}$ applied to $\operatorname{orderedInsert}$ applied to $r$, $\operatorname{nil}$ and $x_{2}$.
List.orderedInsertdefMathlib.Data.List.Sort, function or constantEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ be an element of $x$. Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{orderedInsert}$ applied to $r$, $a$ and $x_{2}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{List\_\_orderedInsert\_\_\_f}$ applied to $r$ and $a$.
List.splitLengthsdefMathlib.Data.List.SplitLengths, function or constantWording
the split length of x1 and x2 (from the name)
English
Let $x_{1}$ be a list of natural numbers. Let $x_{2}$ be a list of elements of $x$. Then the split length of $x_{1}$ and $x_{2}$ is a list of lists of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{List\_\_splitLengths\_\_\_f}$ and $x_{2}$.
List.sublistsLendefMathlib.Data.List.Sublists, function or constantWording
the list of all sublists of n and l (from the docstring)
English
Let $n$ be a natural number. Let $l$ be a list of elements of $x$. Then the list of all sublists of $n$ and $l$ is a list of lists of elements of $x$ defined as $\operatorname{sublistsLenAux}$ applied to $n$, $l$, $\mathrm{id}$ and $\operatorname{nil}$.
List.symdefMathlib.Data.List.Sym, function or constantWording
the symmetric power of n and x1 (from the name)
English
Let $n$ be a natural number. Let $x_{1}$ be a list of elements of $x$. Then the symmetric power of $n$ and $x_{1}$ is a list of symmetric powers of $x$ and $n$ defined as $\mathrm{List\_\_sym\_\_\_unary}$ applied to $\operatorname{mk}$ applied to $n$ and $x_{1}$.
List.sym2defMathlib.Data.List.Sym, function or constantWording
the symmetric power of x1 (from the name)
English
Let $x_{1}$ be a list of elements of $x$. Then the symmetric power of $x_{1}$ is a list of symmetric squares of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{List\_\_sym2\_\_\_f}$.
List.TFAEdefMathlib.Data.List.TFAE, predicateEnglish
Let $l$ be a list of propositions. Then $\operatorname{TFAE}$ holds for $l$, if for all propositions $x$, if $x$ is an element of $l$, then for all propositions $y$, if $y$ is an element of $l$, then $x$, if and only if $y$.
List.toFinsuppdefMathlib.Data.List.ToFinsupp, function or constantWording
the finitely supported function of l (from the name)
English
Let $l$ be a list of elements of $M$. Then the finitely supported function of $l$ is an element of $\FinsuppMACRoQ {\Natural}{M}$.
List.TriplewiseinductiveMathlib.Data.List.Triplewise, predicateEnglish
Let $p$ be a function from elements of $x$ and elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ be a list of elements of $x$. Then we can say that $\operatorname{Triplewise}$ holds for $p$ and $x_{1}$.
List.Triplewise.belowinductiveMathlib.Data.List.Triplewise, predicateEnglish
Assume that $\operatorname{Triplewise}$ holds for $p$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.