Definitions: Mathlib.Data, part 1 of 6

CFilter.infdefMathlib.Data.Analysis.Filter, function or constant

Wording

the infimum of x3 and x4 (from the name)

English

Let $\mathrm{self}$ be a filter of $x$ and $x_{1}$. Let $x_{3}$ and $x_{4}$ be elements of $x_{1}$. Then the infimum of $x_{3}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

CFilter.ofEquivdefMathlib.Data.Analysis.Filter, function or constant

Wording

the filter of E and x4 (from the name)

English

Let $E$ be an equivalence from $x_{1}$ to $x_{2}$. Let $x_{4}$ be a filter of $x$ and $x_{1}$. Then the filter of $E$ and $x_{4}$ is a filter of $x$ and $x_{2}$.

CFilter.ptdefMathlib.Data.Analysis.Filter, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a filter of $x$ and $x_{1}$. Then $\operatorname{pt}$ applied to $\mathrm{self}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

CFilter.toFilterdefMathlib.Data.Analysis.Filter, function or constant

Wording

the filter of F (from the name)

English

Let $F$ be a filter of $\wp x$ and $x_{1}$. Then the filter of $F$ is a filter of $x$.

CFilter.toRealizerdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer of F (from the name)

English

Let $F$ be a filter of $\wp x$ and $x_{1}$. Then the realizer of $F$ is a realizer of the filter of $F$.

Filter.RealizerstructureMathlib.Data.Analysis.Filter, type

Wording

realizer of f (from the name)

English

Let $f$ be a filter of $x$. Then the realizers of $f$ are a basic type.

Filter.Realizer.FdefMathlib.Data.Analysis.Filter, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a realizer of $f$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a filter of $\wp x$ and $\mathrm{Filter\_\_Realizer\_\_\_u3c3\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Filter.Realizer.binddefMathlib.Data.Analysis.Filter, function or constant

Wording

no wording

English

Let $F$ be a realizer of $f$. Let $G$ be a function from elements $i$ of $x$ to realizers of $m$ applied to $i$. Then $\operatorname{bind}$ applied to $F$, $i$ and $G$ is a realizer of $\operatorname{bind}$ applied to $f$ and $m$.

Filter.Realizer.botdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer for the bottom filter (from the docstring)

English

The realizer for the bottom filter is a realizer of the bottom defined as the realizer of $\mathrm{Filter\_\_principal\_empty}$ and the realizer for the principal filter of $\operatorname{emptyCollection}$.

Filter.Realizer.cofinitedefMathlib.Data.Analysis.Filter, function or constant

Wording

the cofinite (from the name)

English

The cofinite is a realizer of the cofinite filter.

Filter.Realizer.comapdefMathlib.Data.Analysis.Filter, function or constant

Wording

the preimage of m and F (from the name)

English

Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $F$ be a realizer of $f$. Then the preimage of $m$ and $F$ is a realizer of the preimage of $m$ and $f$.

Filter.Realizer.iSupdefMathlib.Data.Analysis.Filter, function or constant

Wording

the supremum of F (from the name)

English

Let $F$ be a function from elements $i_{1}$ of $x$ to realizers of $f$ applied to $i_{1}$. Then the supremum of $i_{1}$ is a realizer of the supremum of the function that maps $i$ to $f$ applied to $i$.

Filter.Realizer.infdefMathlib.Data.Analysis.Filter, function or constant

Wording

the infimum of F and G (from the name)

English

Let $F$ be a realizer of $f$. Let $G$ be a realizer of $g$. Then the infimum of $F$ and $G$ is a realizer of $\MinminMACRoAG {f}{g}$.

Filter.Realizer.mapdefMathlib.Data.Analysis.Filter, function or constant

Wording

the map of m and F (from the name)

English

Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $F$ be a realizer of $f$. Then the map of $m$ and $F$ is a realizer of the forward map of $m$ and $f$.

Filter.Realizer.ofEqdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer of e and F (from the name)

English

Assume that $\EqtMACRoH {f}{g}$. Let $F$ be a realizer of $f$. Then the realizer of $e$ and $F$ is a realizer of $g$.

Filter.Realizer.ofEquivdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer of F and E (from the name)

English

Let $F$ be a realizer of $f$. Let $E$ be an element of $\EquivMACRoAE {\mathrm{Filter\_\_Realizer\_\_\_u3c3\_} (F)}{x_{1}}$. Then the realizer of $F$ and $E$ is a realizer of $f$.

Filter.Realizer.ofFilterdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer of f (from the name)

English

Let $f$ be a filter of $x$. Then the realizer of $f$ is a realizer of $f$.

Filter.Realizer.principaldefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer for the principal filter of s (from the docstring)

English

Let $s$ be an element of $\wp x$. Then the realizer for the principal filter of $s$ is a realizer of the principal filter of $s$.

Filter.Realizer.proddefMathlib.Data.Analysis.Filter, function or constant

Wording

the product of F and G (from the name)

English

Let $F$ be a realizer of $f$. Let $G$ be a realizer of $g$. Then the product of $F$ and $G$ is a realizer of $\operatorname{sprod}$ applied to $f$ and $g$ defined as the infimum of the preimage of $\ProdfstMACRoZ$ and $F$ and the preimage of $\ProdsndMACRoAA$ and $G$.

Filter.Realizer.supdefMathlib.Data.Analysis.Filter, function or constant

Wording

the supremum of F and G (from the name)

English

Let $F$ be a realizer of $f$. Let $G$ be a realizer of $g$. Then the supremum of $F$ and $G$ is a realizer of $\MaxmaxMACRoAF {f}{g}$.

Filter.Realizer.topdefMathlib.Data.Analysis.Filter, function or constant

Wording

the realizer for the top filter (from the docstring)

English

The realizer for the top filter is a realizer of the top defined as the realizer of $\mathrm{Filter\_\_principal\_univ}$ and the realizer for the principal filter of the universal set.

Filter.Realizer.σdefMathlib.Data.Analysis.Filter, type

Wording

no wording

English

Let $\mathrm{self}$ be a realizer of $f$. Then an element of $\mathrm{Filter\_\_Realizer\_\_\_u3c3\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Data.Analysis.Topology

Compact.RealizerdefMathlib.Data.Analysis.Topology, type

Wording

realizer of s (from the name)

English

Let $s$ be an element of $\wp x$. Then a realizer of $s$ is an element of the function that maps $s$ to the set of functions from filters $f$ of $x$ and realizers $F$ of $f$ and elements $x_{2}$ of $\mathrm{Filter\_\_Realizer\_\_\_u3c3\_}$ applied to $F$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (f , \operatorname{bot})$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\operatorname{f} (\operatorname{F} (F), x_{2}), s)$ to elements of $\SubtypeSet {a}{\mathrm{and} (\MembershipmemMACRoT {s}{a}, \mathrm{Neq} (\MinminMACRoAG {\mathrm{nhds} (a)}{f}, \operatorname{bot}))}$.

CtopstructureMathlib.Data.Analysis.Topology, type

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$ are a basic type.

Ctop.RealizerstructureMathlib.Data.Analysis.Topology, type

Wording

realizer of x (from the name)

English

Let $x$ be a set. Then the realizers of $x$ are a basic type.

Ctop.Realizer.FdefMathlib.Data.Analysis.Topology, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a realizer of $x$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is an element of $\mathrm{Ctop}$ applied to $x$ and $\mathrm{Ctop\_\_Realizer\_\_\_u3c3\_}$ applied to $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Ctop.Realizer.iddefMathlib.Data.Analysis.Topology, function or constant

Wording

the identity (from the name)

English

The identity is a realizer of $x$.

Ctop.Realizer.nhdsdefMathlib.Data.Analysis.Topology, function or constant

Wording

the neighbourhood filter of F and a (from the name)

English

Let $F$ be a realizer of $x$. Let $a$ be an element of $x$. Then the neighbourhood filter of $F$ and $a$ is a realizer of the neighbourhood filter of $a$.

Ctop.Realizer.ofEquivdefMathlib.Data.Analysis.Topology, function or constant

Wording

the realizer of F and E (from the name)

English

Let $F$ be a realizer of $x$. Let $E$ be an element of $\EquivMACRoAE {\mathrm{Ctop\_\_Realizer\_\_\_u3c3\_} (F)}{x_{1}}$. Then the realizer of $F$ and $E$ is a realizer of $x$.

Ctop.Realizer.σdefMathlib.Data.Analysis.Topology, type

Wording

no wording

English

Let $\mathrm{self}$ be a realizer of $x$. Then an element of $\mathrm{Ctop\_\_Realizer\_\_\_u3c3\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Ctop.fdefMathlib.Data.Analysis.Topology, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Ctop.interdefMathlib.Data.Analysis.Topology, function or constant

Wording

the intersection of b and x2 (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$. Let $a$ and $b$ be elements of $x_{1}$. Let $x_{2}$ be an element of $x$ such that $\MembershipmemMACRoT {\operatorname{inter} (\operatorname{f} (\mathrm{self} , a), \operatorname{f} (\mathrm{self} , b))}{x_{2}}$. Then the intersection of $b$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $a$, $b$, $x_{2}$ and $h$.

Ctop.ofEquivdefMathlib.Data.Analysis.Topology, function or constant

Wording

no wording

English

Let $E$ be an equivalence from $x_{1}$ to $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$. Then $\operatorname{ofEquiv}$ applied to $E$ and $x_{3}$ is an element of $\mathrm{Ctop}$ applied to $x$ and $x_{2}$.

Ctop.toRealizerdefMathlib.Data.Analysis.Topology, function or constant

Wording

the realizer of F (from the name)

English

Let $F$ be an element of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$. Then the realizer of $F$ is a realizer of $x$.

Ctop.topdefMathlib.Data.Analysis.Topology, function or constant

Wording

the top of self and x2 (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{Ctop}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then the top of $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

LocallyFinite.RealizerstructureMathlib.Data.Analysis.Topology, type

Wording

realizer of F and f (from the name)

English

Let $F$ be a realizer of $x$. Let $f$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then the realizers of $F$ and $f$ are a basic type.

LocallyFinite.Realizer.basdefMathlib.Data.Analysis.Topology, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a realizer of $F$ and $f$. Let $a$ be an element of $x$. Then $\operatorname{bas}$ applied to $\mathrm{self}$ and $a$ is an element of $\SubtypeSet {s}{(\MembershipmemMACRoT {\operatorname{f} (\operatorname{F} (F), s)}{a})}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $a$.

Mathlib.Data.BitVec

BitVec.equivFindefMathlib.Data.BitVec, function or constant

Wording

no wording

English

$\operatorname{equivFin}$ is a ring isomorphism of $\mathrm{BitVec}$ applied to $m$ and $\mathrm{Fin}$ applied to $2 ^ {m}$.

Mathlib.Data.Bool.Basic

Bool.carrydefMathlib.Data.Bool.Basic, function or constant

Wording

no wording

English

Let $x$, $y$ and $c$ be elements of $\mathrm{Bool}$. Then $\operatorname{carry}$ applied to $x$, $y$ and $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{or}$ applied to $\operatorname{or}$ applied to $\operatorname{and}$ applied to $x$ and $y$ and $\operatorname{and}$ applied to $x$ and $c$ and $\operatorname{and}$ applied to $y$ and $c$.

Bool.ofNatdefMathlib.Data.Bool.Basic, function or constant

Wording

the bool of n (from the name)

English

Let $n$ be a natural number. Then the bool of $n$ is an element of $\mathrm{Bool}$ defined as $\operatorname{decide}$ applied to $\mathrm{Neq} (n , 0)$.

Bool.xor3defMathlib.Data.Bool.Basic, function or constant

Wording

no wording

English

Let $x$, $y$ and $c$ be elements of $\mathrm{Bool}$. Then $\operatorname{xor3}$ applied to $x$, $y$ and $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{xor}$ applied to $\operatorname{xor}$ applied to $x$ and $y$ and $c$.

Mathlib.Data.Bundle

Bundle.PullbackdefMathlib.Data.Bundle, type

Wording

pullback of E and x (from the name)

English

Let $f$ be a function from elements of $\mathrm{B'}$ to elements of $B$. Let $E$ be a function from elements of $B$ to sets. Let $x$ be an element of $\mathrm{B'}$. Then a pullback of $E$ and $x$ is an element of the function that maps $f$, $E$ and $x$ to $E$ applied to $f$ applied to $x$.

Bundle.Pullback.liftdefMathlib.Data.Bundle, function or constant

Wording

the lift of f and x (from the name)

English

Let $f$ be a function from elements of $\mathrm{B'}$ to elements of $B$. Let $x$ be a total space of $F$ and the set of elements of $\operatorname{Pullback}$ applied to $E$. Then the lift of $f$ and $x$ is a total space of $F$ and $E$ defined as $\operatorname{mk}$ applied to $f$ applied to the projection of $x$ and the second component of $x$.

Bundle.TotalSpacestructureMathlib.Data.Bundle, type

Wording

total space of F and E (from the name)

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Then the total spaces of $F$ and $E$ are a basic type.

Bundle.TotalSpace.mk'defMathlib.Data.Bundle, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x$ be an element of $B$. Let $y$ be an element of $E$ applied to $x$. Then $\operatorname{mk'}$ applied to $F$, $x$ and $y$ is a total space of $F$ and $E$ defined as $\operatorname{mk}$ applied to $x$ and $y$.

Bundle.TotalSpace.projdefMathlib.Data.Bundle, function or constant

Wording

the projection of self (from the name)

English

Let $\mathrm{self}$ be a total space of $F$ and $E$. Then the projection of $\mathrm{self}$ is an element of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Bundle.TotalSpace.snddefMathlib.Data.Bundle, function or constant

Wording

the second component of self (from the name)

English

Let $\mathrm{self}$ be a total space of $F$ and $E$. Then the second component of $\mathrm{self}$ is an element of $E$ applied to the projection of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Bundle.TotalSpace.toProddefMathlib.Data.Bundle, function or constant

Wording

the product of B and F (from the name)

English

Let $B$ and $F$ be sets. Then the product of $B$ and $F$ is an equivalence from the set of total spaces of $F$ and the function that maps $x$ to $F$ to $\mathrm{Prod}$ applied to $B$ and $F$.

Bundle.TotalSpace.trivialSnddefMathlib.Data.Bundle, function or constant

Wording

the trivial second component of x (from the name)

English

Let $B$ and $F$ be sets. Let $x$ be a total space of $F$ and $\operatorname{Trivial}$ applied to $B$ and $F$. Then the trivial second component of $x$ is an element of $F$ defined as the second component of $x$.

Bundle.TrivialdefMathlib.Data.Bundle, type

Wording

no wording

English

Let $B$ and $F$ be sets. Let $x$ be an element of $B$. Then an element of $\operatorname{Trivial}$ applied to $B$, $F$ and $x$ is an element of the function that maps $B$, $F$ and $x$ to $F$.

Bundle.pullbackTotalSpaceEmbeddingdefMathlib.Data.Bundle, function or constant

Wording

the pullback total space embedding of f and x (from the name)

English

Let $f$ be a function from elements of $\mathrm{B'}$ to elements of $B$. Let $x$ be a total space of $F$ and the set of elements of $\operatorname{Pullback}$ applied to $E$. Then the pullback total space embedding of $f$ and $x$ is an element of $\mathrm{Prod}$ applied to $\mathrm{B'}$ and the set of total spaces of $F$ and $E$ defined as $\ProdmkMACRoU {\operatorname{proj} (x)}{\operatorname{mk} (f (\operatorname{proj} (x)), \operatorname{snd} (x))}$.

Mathlib.Data.DFinsupp.BigOperators

DFinsupp.evalAddMonoidHomdefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the evaluation additive monoid homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the evaluation additive monoid homomorphism of $i$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ and $x_{1}$ applied to $i$ defined as the composition of the evaluation additive monoid homomorphism of $x_{1}$ and $i$ and the coercion function additive monoid homomorphism.

DFinsupp.liftAddHomdefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the lift additive homomorphism (from the name)

English

The lift additive homomorphism is an additive equivalence of the set of functions from elements $i$ of $x$ to additive monoid homomorphisms of $x_{2}$ applied to $i$ and $x_{1}$ and the set of additive monoid homomorphisms of the set of finitely supported functions of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$ and $x_{1}$.

DFinsupp.proddefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$. Let $g$ be a function from elements $i$ of $x$ and elements of $x_{2}$ applied to $i$ to elements of $x_{1}$. Then the product of $f$ and $i$ is an element of $x_{1}$ defined as the function that maps $g$ to $\FinsetProd {\operatorname{support} (f)}{i}{i (i , f (i))}{g}$.

DFinsupp.sumdefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the sum of f and g (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$. Let $g$ be a function from elements $i$ of $x$ and elements of $x_{2}$ applied to $i$ to elements of $x_{1}$. Then the sum of $f$ and $i$ is an element of $x_{1}$ defined as the function that maps $g$ to $\FinsetSum {\operatorname{support} (f)}{i}{i (i , f (i))}{g}$.

DFinsupp.sumAddHomdefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the sum additive homomorphism of x6 (from the name)

English

Let $x_{6}$ be a function from elements $i_{1}$ of $x$ to additive monoid homomorphisms of $x_{2}$ applied to $i_{1}$ and $x_{1}$. Then the sum additive homomorphism of $i_{1}$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and $x_{1}$.

DFinsupp.sumZeroHomdefMathlib.Data.DFinsupp.BigOperators, function or constant

Wording

the sum zero homomorphism of x6 (from the name)

English

Let $x_{6}$ be a function from elements $i_{1}$ of $x$ to zero homomorphisms of $x_{2}$ applied to $i_{1}$ and $x_{1}$. Then the sum zero homomorphism of $i_{1}$ is a zero homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and $x_{1}$.

Mathlib.Data.DFinsupp.Defs

DFinsuppstructureMathlib.Data.DFinsupp.Defs, type

Wording

finitely supported function of x1 (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Then the finitely supported functions of $x_{1}$ are a basic type.

DFinsupp.coeFnAddMonoidHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$.

DFinsupp.comapDomaindefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the preimage domain of h and f (from the name)

English

Let $h$ be an injective function from elements of $x_{2}$ to elements of $x$. Let $f$ be a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$. Then the preimage domain of $h$ and $f$ is a finitely supported function of the function that maps $k$ to $x_{1}$ applied to $h$ applied to $k$.

DFinsupp.comapDomain'defMathlib.Data.DFinsupp.Defs, function or constant

Wording

the preimage domain of h and #3 (from the name)

English

Let $h$ be a function from elements of $x_{2}$ to elements of $x$ such that $\operatorname{LeftInverse}$ holds for $\mathrm{h'}$ and $h$. Let $f$ be a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$. Then the preimage domain of $h$ and $f$ is a finitely supported function of the function that maps $k$ to $x_{1}$ applied to $h$ applied to $k$ defined as $\operatorname{mk'}$ applied to the function that maps $x_{4}$ to $f$ applied to $h$ applied to $x_{4}$ and the map of the function that maps $s$ to the map of $\mathrm{h'}$ and $s$ and the support of $f$.

DFinsupp.equivCongrLeftdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the left equivalence congruence of h (from the name)

English

Let $h$ be an equivalence from $x$ to $x_{2}$. Then the left equivalence congruence of $h$ is an equivalence from the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ to the set of finitely supported functions of the function that maps $k$ to $x_{1}$ applied to $\operatorname{symm}$ applied to $h$ and $k$.

DFinsupp.equivFunOnFintypedefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the equivalence function on finite type (from the name)

English

The equivalence function on finite type is an equivalence from the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ to the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$.

DFinsupp.equivProdDFinsuppdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the equivalence product finitely supported function (from the name)

English

The equivalence product finitely supported function is an equivalence from the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ to $\mathrm{Prod}$ applied to $x_{1}$ applied to $\operatorname{none}$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $\operatorname{some}$ applied to $i_{1}$.

DFinsupp.erasedefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $x_{4}$ be a finitely supported function of the function that maps $i_{2}$ to $x_{1}$ applied to $i_{2}$. Then $\operatorname{erase}$ applied to $i$ and $x_{4}$ is a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as $\operatorname{mk'}$ applied to the function that maps $j$ to $\iteMACRoG {(\EqtMACRoH {j}{i})}{0}{\operatorname{toFun} (x_{4} , j)}$ and the map of the function that maps $\mathrm{xs}$ to $\mathrm{xs}$ and the support of $x_{4}$.

DFinsupp.eraseAddHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then $\operatorname{eraseAddHom}$ applied to $x_{1}$ and $i$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ and the set of finitely supported functions of the function that maps $i_{2}$ to $x_{1}$ applied to $i_{2}$.

DFinsupp.extendWithdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x_{1}$ applied to $\operatorname{none}$. Let $f$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $\operatorname{some}$ applied to $i_{1}$. Then $\operatorname{extendWith}$ applied to $a$ and $f$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$.

DFinsupp.filterdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the filter of p and x4 (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $x_{4}$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Then the filter of $p$ and $x_{4}$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$ defined as $\operatorname{mk'}$ applied to the function that maps $i$ to $\iteMACRoG {p (i)}{x_{4} (i)}{0}$ and the map of the function that maps $\mathrm{xs}$ to $\mathrm{xs}$ and the support of $x_{4}$.

DFinsupp.filterAddMonoidHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the filter additive monoid homomorphism of x1 and p (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $p$ be a function from elements of $x$ to propositions. Then the filter additive monoid homomorphism of $x_{1}$ and $p$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$.

DFinsupp.mapRangedefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the map range of f and hf (from the name)

English

Let $f$ be a function from elements $i_{3}$ of $x$ and elements of $x_{1}$ applied to $i_{3}$ to elements of $x_{2}$ applied to $i_{3}$ such that for all elements $i_{2}$ of $x$, $\EqtMACRoH {f (i_{2} , 0)}{0}$. Let $x_{5}$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Then the map range of $i_{3}$ and $\mathrm{hf}$ is a finitely supported function of the function that maps $i$ to $x_{2}$ applied to $i$ defined as the function that maps $x_{5}$ to $\operatorname{mk'}$ applied to the function that maps $i$ to $i_{3}$ applied to $i$ and $\mathrm{hf}$ applied to $i$, the map of the function that maps $s$ to $s$ and the support of $\mathrm{hf}$ and $x_{5}$.

DFinsupp.mapRange.addEquivdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the additive equivalence of e (from the name)

English

Let $e$ be a function from elements $i_{2}$ of $x$ to additive equivalences of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the additive equivalence of $i_{2}$ is an additive equivalence of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$.

DFinsupp.mapRange.addMonoidHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be a function from elements $i_{2}$ of $x$ to additive monoid homomorphisms of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the additive monoid homomorphism of $i_{2}$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$.

DFinsupp.mkdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $x_{4}$ be a function from elements $i_{1}$ of $s$ to elements of $x_{1}$ applied to $i_{1}$. Then $\operatorname{mk}$ applied to $s$, $i_{1}$ and $x_{4}$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$ defined as the function that maps $x_{4}$ to $\operatorname{mk'}$ applied to the function that maps $i$ to $\mathrm{dite}$ applied to $\MembershipmemMACRoT {s}{i}$, the function that maps $H$ to $i_{1}$ applied to $i$ and the function that maps $H_{1}$ to $0$, $\operatorname{mk}$ applied to the value of $s$ and $x_{4}$.

DFinsupp.mkAddGroupHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the additive group homomorphism of s (from the name)

English

Let $s$ be a finite set of $x$. Then the additive group homomorphism of $s$ is an additive monoid homomorphism of the set of functions from elements $i$ of $s$ to elements of $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$.

DFinsupp.piecewisedefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $x_{3}$ be a finitely supported function of the function that maps $i_{2}$ to $x_{1}$ applied to $i_{2}$. Let $y$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{piecewise}$ applied to $x_{3}$, $y$ and $s$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$.

DFinsupp.sigmaFinsetFunEquivdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the sigma finite set function equivalence (from the name)

English

The sigma finite set function equivalence is an equivalence from the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ to $\Sigma$ applied to the function that maps $s$ to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ to elements of $\SubtypeSet {x_{5}}{\mathrm{Neq} (x_{5} , 0)}$ defined as the composition of the inverse of the sigma fiber equivalence of $\operatorname{support}$ and the right sigma congruence of $\operatorname{subtypeSupportEqEquiv}$.

DFinsupp.singledefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $i$. Then $\operatorname{single}$ applied to $i$ and $b$ is a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as $\operatorname{mk'}$ applied to $\operatorname{single}$ applied to $i$ and $b$ and $\operatorname{mk}$ applied to $\operatorname{singleton}$ applied to $i$.

DFinsupp.singleAddHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the single additive homomorphism of x1 and i (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then the single additive homomorphism of $x_{1}$ and $i$ is an additive monoid homomorphism of $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$.

DFinsupp.subtypeDomaindefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the subtype domain of p and x4 (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $x_{4}$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Then the subtype domain of $p$ and $x_{4}$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$ defined as $\operatorname{mk'}$ applied to the function that maps $i$ to $x_{4}$ applied to $i$ and the map of the function that maps $\mathrm{xs}$ to the map of the function that maps $j$ to $j$ and $\operatorname{attach}$ applied to the filter of $p$ and $\mathrm{xs}$ and the support of $x_{4}$.

DFinsupp.subtypeDomainAddMonoidHomdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the subtype domain additive monoid homomorphism of x1 and p (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $p$ be a function from elements of $x$ to propositions. Then the subtype domain additive monoid homomorphism of $x_{1}$ and $p$ is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$.

DFinsupp.subtypeSupportEqEquivdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{subtypeSupportEqEquiv}$ applied to $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{(\EqtMACRoH {\operatorname{support} (f)}{s})})}{(\mathrm{Elem} (\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})})\rightarrow \SubtypeSet {x_{5}}{\mathrm{Neq} (x_{5} , 0)})}$.

DFinsupp.supportdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the support of f (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$. Then the support of $f$ is a finite set of $x$.

DFinsupp.support'defMathlib.Data.DFinsupp.Defs, function or constant

Wording

the support of self (from the docstring)

English

Let $\mathrm{self}$ be a finitely supported function of $x_{1}$. Then the support of $\mathrm{self}$ is a truncation of $\SubtypeSet {s}{\mathrm{forall} (x , \lambda i . \mathrm{or} (\MembershipmemMACRoT {s}{i}, \EqtMACRoH {\operatorname{toFun} (\mathrm{self} , i)}{0}))}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

DFinsupp.toFundefMathlib.Data.DFinsupp.Defs, function or constant

Wording

the underlying function of self and i (from the docstring)

English

Let $\mathrm{self}$ be a finitely supported function of $x_{1}$. Let $i$ be an element of $x$. Then the underlying function of $\mathrm{self}$ and $i$ is an element of $x_{1}$ applied to $i$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

DFinsupp.updatedefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $f$ be a finitely supported function of the function that maps $i_{2}$ to $x_{1}$ applied to $i_{2}$. Let $i$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $i$. Then $\operatorname{update}$ applied to $f$, $i$ and $b$ is a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ defined as $\operatorname{mk'}$ applied to $\operatorname{update}$ applied to $\operatorname{coe}$ applied to $f$, $i$ and $b$ and the map of the function that maps $s$ to $\operatorname{cons}$ applied to $i$ and $s$ and the support of $f$.

DFinsupp.zipWithdefMathlib.Data.DFinsupp.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements $i_{4}$ of $x$ and elements of $x_{2}$ applied to $i_{4}$ and elements of $x_{3}$ applied to $i_{4}$ to elements of $x_{1}$ applied to $i_{4}$ such that for all elements $i_{3}$ of $x$, $\EqtMACRoH {f (i_{3} , 0 , 0)}{0}$. Let $x_{7}$ be a finitely supported function of the function that maps $i_{2}$ to $x_{2}$ applied to $i_{2}$. Let $y$ be a finitely supported function of the function that maps $i_{1}$ to $x_{3}$ applied to $i_{1}$. Then $\operatorname{zipWith}$ applied to $i_{4}$, $f$, $\mathrm{hf}$, $x_{7}$ and $y$ is a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$ defined as the function that maps $y$ to $\operatorname{mk'}$ applied to the function that maps $i$ to $i_{4}$ applied to $i$, $\mathrm{hf}$ applied to $i$ and $x_{7}$ applied to $i$, $\operatorname{bind}$ applied to the support of $\mathrm{hf}$ and the function that maps $\mathrm{xs}$ to the map of the function that maps $\mathrm{ys}$ to $\mathrm{xs} + \mathrm{ys}$ and the support of $x_{7}$ and $y$.

Mathlib.Data.DFinsupp.Interval

DFinsupp.pidefMathlib.Data.DFinsupp.Interval, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to the set of finite sets of $x_{1}$ applied to $i_{1}$. Then the product of $f$ is a finite set of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ defined as $\operatorname{dfinsupp}$ applied to the support of $f$ and $\operatorname{coe}$ applied to $f$.

DFinsupp.rangeIccdefMathlib.Data.DFinsupp.Interval, function or constant

Wording

the range closed interval of f and g (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{2}$ to $x_{1}$ applied to $i_{2}$. Let $g$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Then the range closed interval of $f$ and $g$ is a finitely supported function of the function that maps $i$ to the set of finite sets of $x_{1}$ applied to $i$ defined as $\operatorname{mk'}$ applied to the function that maps $i$ to $\FinsetIccMACRoAH {f (i)}{g (i)}$ and $\operatorname{bind}$ applied to the support of $f$ and the function that maps $\mathrm{fs}$ to the map of the function that maps $\mathrm{gs}$ to $\mathrm{fs} + \mathrm{gs}$ and the support of $g$.

DFinsupp.singletondefMathlib.Data.DFinsupp.Interval, function or constant

Wording

the singleton of f (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Then the singleton of $f$ is a finitely supported function of the function that maps $i$ to the set of finite sets of $x_{1}$ applied to $i$ defined as $\operatorname{mk'}$ applied to the function that maps $i$ to $\operatorname{singleton}$ applied to $f$ applied to $i$ and the map of the function that maps $s$ to $s$ and the support of $f$.

Finset.dfinsuppdefMathlib.Data.DFinsupp.Interval, function or constant

Wording

no wording

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 $\operatorname{dfinsupp}$ applied to $s$, $i_{1}$ and $t$ is a finite set of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$.

Mathlib.Data.DFinsupp.Lex

DFinsupp.LexdefMathlib.Data.DFinsupp.Lex, predicate

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements $i_{2}$ of $x$ and elements of $x_{1}$ applied to $i_{2}$ and elements of $x_{1}$ applied to $i_{2}$ to propositions. Let $x_{3}$ be a finitely supported function of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Let $y$ be a finitely supported function of the function that maps $i$ to $x_{1}$ applied to $i$. Then $\operatorname{Lex}$ holds for $r$, $i_{2}$, $s$, $x_{3}$ and $y$, if $\operatorname{Lex}$ holds for $r$, the function that maps $x_{4}$ to $i_{2}$ applied to $x_{4}$, $\operatorname{coe}$ applied to $s$, $\operatorname{coe}$ applied to $x_{3}$ and $y$.

Mathlib.Data.DFinsupp.Module

DFinsupp.coeFnLinearMapdefMathlib.Data.DFinsupp.Module, function or constant

Wording

the coercion function linear map of x1 (from the name)

English

Let $x_{1}$ be a set. Then the coercion function linear map of $x_{1}$ is a linear map of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$.

DFinsupp.filterLinearMapdefMathlib.Data.DFinsupp.Module, function or constant

Wording

the filter linear map of x2 and p (from the name)

English

Let $x_{1}$ be a set. Let $x_{2}$ be a function from elements of $x$ to sets. Let $p$ be a function from elements of $x$ to propositions. Then the filter linear map of $x_{2}$ and $p$ is a linear map of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$.

DFinsupp.subtypeDomainLinearMapdefMathlib.Data.DFinsupp.Module, function or constant

Wording

the subtype domain linear map of x2 and p (from the name)

English

Let $x_{1}$ be a set. Let $x_{2}$ be a function from elements of $x$ to sets. Let $p$ be a function from elements of $x$ to propositions. Then the subtype domain linear map of $x_{2}$ and $p$ is a linear map of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{2}$ applied to $i_{1}$.

Mathlib.Data.DFinsupp.Multiset

DFinsupp.toMultisetdefMathlib.Data.DFinsupp.Multiset, function or constant

Wording

the multiset (from the name)

English

The multiset is an additive monoid homomorphism of the set of finitely supported functions of the function that maps $x_{2}$ to $\Natural$ and the set of multisets of $x$ defined as the sum additive homomorphism of the function that maps $a$ to $\operatorname{replicateAddMonoidHom}$ applied to $a$.

Multiset.equivDFinsuppdefMathlib.Data.DFinsupp.Multiset, function or constant

Wording

the equivalence finitely supported function (from the name)

English

The equivalence finitely supported function is an additive equivalence of the set of multisets of $x$ and the set of finitely supported functions of the function that maps $x_{2}$ to $\Natural$.

Multiset.toDFinsuppdefMathlib.Data.DFinsupp.Multiset, function or constant

Wording

the finitely supported function (from the name)

English

The finitely supported function is an additive monoid homomorphism of the set of multisets of $x$ and the set of finitely supported functions of the function that maps $x_{2}$ to $\Natural$.

Mathlib.Data.DFinsupp.NeLocus

DFinsupp.neLocusdefMathlib.Data.DFinsupp.NeLocus, function or constant

Wording

no wording

English

Let $f$ be a finitely supported function of the function that maps $a_{1}$ to $N$ applied to $a_{1}$. Let $g$ be a finitely supported function of the function that maps $a$ to $N$ applied to $a$. 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 {\operatorname{support} (f)}{\operatorname{support} (g)})}$.

Mathlib.Data.DFinsupp.Notation

DFinsupp.Internal.elabSingle₀defMathlib.Data.DFinsupp.Notation, function or constant

Wording

no wording

English

$\operatorname{TermElab}$.

DFinsupp.Internal.elabUpdate₀defMathlib.Data.DFinsupp.Notation, function or constant

Wording

no wording

English

$\operatorname{TermElab}$.

Mathlib.Data.DFinsupp.Order

DFinsupp.orderEmbeddingToFundefMathlib.Data.DFinsupp.Order, function or constant

Wording

the order embedding to function (from the name)

English

The order embedding to function is an order embedding of the set of finitely supported functions of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$.

Mathlib.Data.DFinsupp.Sigma

DFinsupp.sigmaCurrydefMathlib.Data.DFinsupp.Sigma, function or constant

Wording

the sigma curry of f (from the name)

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to $x_{2}$ applied to $\operatorname{fst}$ applied to $i_{1}$ and $\operatorname{snd}$ applied to $i_{1}$. Then the sigma curry of $f$ is a finitely supported function of the function that maps $i$ to the set of finitely supported functions of the function that maps $j$ to $x_{2}$ applied to $i$ and $j$.

DFinsupp.sigmaCurryEquivdefMathlib.Data.DFinsupp.Sigma, function or constant

Wording

the sigma curry equivalence (from the name)

English

The sigma curry equivalence is an equivalence from the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ to the set of finitely supported functions of the function that maps $i_{1}$ to the set of finitely supported functions of the function that maps $j$ to $x_{2}$ applied to $i_{1}$ and $j$.

DFinsupp.sigmaUncurrydefMathlib.Data.DFinsupp.Sigma, function or constant

Wording

no wording

English

Let $f$ be a finitely supported function of the function that maps $i_{1}$ to the set of finitely supported functions of the function that maps $j$ to $x_{2}$ applied to $i_{1}$ and $j$. Then $\operatorname{sigmaUncurry}$ applied to $f$ is a finitely supported function of the function that maps $i$ to $x_{2}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ defined as $\operatorname{mk'}$ applied to the function that maps $i$ to $\operatorname{coe}$ applied to $f$, $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and $\operatorname{bind}$ applied to the support of $f$ and the function that maps $s$ to the map of the function that maps $\mathrm{fs}$ to $\operatorname{bind}$ applied to the value of $\operatorname{attach}$ applied to the finite set of $s$ and the function that maps $i_{2}$ to the map of $\operatorname{mk}$ applied to $i_{2}$ and $\mathrm{fs}$ applied to $i_{2}$ and the finite choice of the function that maps $i_{3}$ to the support of $f$ applied to $i_{3}$.

Mathlib.Data.DList.Instances

Batteries.DList.listEquivDListdefMathlib.Data.DList.Instances, function or constant

Wording

the list equivalence list of x (from the name)

English

Let $x$ be a set. Then the list equivalence list of $x$ is an equivalence from the set of lists of elements of $x$ to $\operatorname{DList}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ofList}$, $\operatorname{toList}$, the function that maps $x_{1}$ to $\mathrm{Batteries\_\_DList\_\_toList\_ofList}$ applied to $x_{1}$ and the function that maps $x_{2}$ to $\mathrm{Batteries\_\_DList\_\_ofList\_toList}$ applied to $x_{2}$.

Mathlib.Data.Dyadic

Dyadic.stepdefMathlib.Data.Dyadic, function or constant

Wording

the step of prec (from the name)

English

Let $\mathrm{prec}$ be an integer. Then the step of $\mathrm{prec}$ is an element of $\mathrm{Dyadic}$.

Dyadic.toRealdefMathlib.Data.Dyadic, function or constant

Wording

no wording

English

Let $d$ be an element of $\mathrm{Dyadic}$. Then $\operatorname{toReal}$ applied to $d$ is a real number defined as $\operatorname{cast}$ applied to $\operatorname{toRat}$ applied to $d$.

Dyadic.toRealAddMonoidHomdefMathlib.Data.Dyadic, function or constant

Wording

the real additive monoid homomorphism (from the name)

English

The real additive monoid homomorphism is an additive monoid homomorphism of $\mathrm{Dyadic}$ and $\Real$.

Dyadic.toRealOrderEmbeddingdefMathlib.Data.Dyadic, function or constant

Wording

the real order embedding (from the name)

English

The real order embedding is an order embedding of $\mathrm{Dyadic}$ and $\Real$.

Mathlib.Data.ENat.Basic

AddHom.ENatMapdefMathlib.Data.ENat.Basic, function or constant

Wording

the natural map of f (from the name)

English

Let $f$ be an additive homomorphism of $\Natural$ and $N$. Then the natural map of $f$ is an additive homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $N$.

ENat.liftdefMathlib.Data.ENat.Basic, function or constant

Wording

the lift of x and h (from the name)

English

Let $x$ be a natural number such that $x$ is less than the top. Then the lift of $x$ and $h$ is a natural number.

ENat.mapdefMathlib.Data.ENat.Basic, function or constant

Wording

the map of f and k (from the name)

English

Let $f$ be a function from natural numbers to elements of $x$. Let $k$ be a natural number. Then the map of $f$ and $k$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as the map of $f$ and $k$.

ENat.toNatdefMathlib.Data.ENat.Basic, function or constant

Wording

the natural number of x (from the name)

English

Let $x$ be a natural number. Then the natural number of $x$ is a natural number defined as $\operatorname{untopD}$ applied to $0$ and $x$.

OneHom.ENatMapdefMathlib.Data.ENat.Basic, function or constant

Wording

the natural map of f (from the name)

English

Let $f$ be an one homomorphism of $\Natural$ and $N$. Then the natural map of $f$ is an one homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $N$.

ZeroHom.ENatMapdefMathlib.Data.ENat.Basic, function or constant

Wording

the natural map of f (from the name)

English

Let $f$ be a zero homomorphism of $\Natural$ and $N$. Then the natural map of $f$ is a zero homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $N$.

Mathlib.Data.ENat.Defs

ENatdefMathlib.Data.ENat.Defs, type

Wording

natural number (from the name)

English

A natural number is an element of $\mathrm{WithTop}$ applied to $\Natural$.

ENat.recTopCoedefMathlib.Data.ENat.Defs, function or constant

Wording

no wording

English

Let $\mathrm{top}$ be an element of $C$ applied to the top. Let $\mathrm{coe}$ be a function from natural numbers $a$ to elements of $C$ applied to $a$. Let $n$ be a natural number. Then $\operatorname{recTopCoe}$ applied to $\mathrm{top}$, $a$, $\mathrm{coe}$ and $n$ is an element of $C$ applied to $n$.

Mathlib.Data.ENat.Monoid

AddMonoidHom.ENatMapdefMathlib.Data.ENat.Monoid, function or constant

Wording

the natural map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $\Natural$ and $N$. Then the natural map of $f$ is an additive monoid homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $N$.

ENat.toNatHomdefMathlib.Data.ENat.Monoid, function or constant

Wording

the natural homomorphism (from the name)

English

The natural homomorphism is a monoid with zero homomorphism of the set of natural numbers and $\Natural$.

MonoidWithZeroHom.ENatMapdefMathlib.Data.ENat.Monoid, function or constant

Wording

the natural map of f and hf (from the name)

English

Let $f$ be a monoid with zero homomorphism of $\Natural$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the natural map of $f$ and $\mathrm{hf}$ is a monoid with zero homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $S$.

RingHom.ENatMapdefMathlib.Data.ENat.Monoid, function or constant

Wording

the natural map of f and hf (from the name)

English

Let $f$ be a ring homomorphism of $\Natural$ and $S$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the natural map of $f$ and $\mathrm{hf}$ is a ring homomorphism of the set of natural numbers and $\mathrm{WithTop}$ applied to $S$.

Mathlib.Data.EReal.Basic

ENNReal.toERealdefMathlib.Data.EReal.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{toEReal}$ applied to $x$ is an element of $\mathrm{EReal}$.

ERealdefMathlib.Data.EReal.Basic, type

Wording

no wording

English

An element of $\mathrm{EReal}$ is an element of $\mathrm{WithBot}$ applied to $\mathrm{WithTop}$ applied to $\Real$.

EReal.muldefMathlib.Data.EReal.Basic, function or constant

Wording

the product of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be elements of $\mathrm{EReal}$. Then the product of $x$ and $x_{1}$ is an element of $\mathrm{EReal}$.

EReal.neTopBotEquivRealdefMathlib.Data.EReal.Basic, function or constant

Wording

no wording

English

$\operatorname{neTopBotEquivReal}$ is an equivalence from the set of elements of the complement of $\operatorname{insert}$ applied to the bottom and $\operatorname{singleton}$ applied to the top to $\Real$.

EReal.orderEmbeddingdefMathlib.Data.EReal.Basic, function or constant

Wording

the order embedding (from the name)

English

The order embedding is an order embedding of $\Real$ and $\mathrm{EReal}$.

EReal.toENNRealdefMathlib.Data.EReal.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{EReal}$. Then $\operatorname{toENNReal}$ applied to $x$ is an element of $\mathrm{ENNReal}$ defined as $\iteMACRoG {(\EqtMACRoH {x}{\operatorname{top}})}{\operatorname{top}}{\operatorname{ofReal} (\operatorname{toReal} (x))}$.

EReal.toRealdefMathlib.Data.EReal.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{EReal}$. Then $\operatorname{toReal}$ applied to $x$ is a real number.

Real.toERealdefMathlib.Data.EReal.Basic, function or constant

Wording

no wording

English

Let $x$ be a real number. Then $\operatorname{toEReal}$ applied to $x$ is an element of $\mathrm{EReal}$ defined as $\operatorname{comp}$ applied to $\operatorname{some}$, $\operatorname{some}$ and $x$.

Real.toERealAddHomdefMathlib.Data.EReal.Basic, function or constant

Wording

the real additive homomorphism (from the name)

English

The real additive homomorphism is an additive monoid homomorphism of $\Real$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toEReal}$ and $\mathrm{EReal\_\_coe\_zero}$ and $\mathrm{EReal\_\_coe\_add}$.

Mathlib.Data.EReal.Inv

EReal.absdefMathlib.Data.EReal.Inv, function or constant

Wording

the absolute value of x (from the name)

English

Let $x$ be an element of $\mathrm{EReal}$. Then the absolute value of $x$ is an element of $\mathrm{ENNReal}$.

EReal.invdefMathlib.Data.EReal.Inv, function or constant

Wording

the inverse of x (from the name)

English

Let $x$ be an element of $\mathrm{EReal}$. Then the inverse of $x$ is an element of $\mathrm{EReal}$.

Mathlib.Data.EReal.Operations

EReal.negdefMathlib.Data.EReal.Operations, function or constant

Wording

the negation of x (from the name)

English

Let $x$ be an element of $\mathrm{EReal}$. Then the negation of $x$ is an element of $\mathrm{EReal}$.

EReal.negOrderIsodefMathlib.Data.EReal.Operations, function or constant

Wording

the negation order isomorphism (from the name)

English

The negation order isomorphism is an order isomorphism of $\mathrm{EReal}$ and the set of order duals of $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x$ to $\operatorname{toDual}$ applied to $\operatorname{neg}$ applied to $x$, the function that maps $x_{1}$ to $\operatorname{neg}$ applied to $\operatorname{ofDual}$ applied to $x_{1}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the negation of $\mathrm{EReal}$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the negation of $\mathrm{EReal}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{EReal\_\_neg\_le\_neg\_iff}$.

EReal.recENNRealdefMathlib.Data.EReal.Operations, function or constant

Wording

no wording

English

Let $\mathrm{coe}$ be a function from elements $x_{2}$ of $\mathrm{ENNReal}$ to elements of $\mathrm{motive}$ applied to $\operatorname{toEReal}$ applied to $x_{2}$. Let $\mathrm{neg\_coe}$ be a function from elements $x_{1}$ of $\mathrm{ENNReal}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (0 , x_{1})$ to elements of $\mathrm{motive}$ applied to $\operatorname{neg}$ applied to $\operatorname{toEReal}$ applied to $x_{1}$. Let $x$ be an element of $\mathrm{EReal}$. Then $\operatorname{recENNReal}$ applied to $x_{2}$, $\mathrm{coe}$, $x_{1}$, $\mathrm{neg\_coe}$ and $x$ is an element of $\mathrm{motive}$ applied to $x$.

Mathlib.Data.Erased

Erased.OutTypedefMathlib.Data.Erased, type

Wording

no wording

English

Let $a$ be an element of $\mathrm{Erased}$ applied to the set of sets. Then an element of $\operatorname{OutType}$ applied to $a$ is an element of the function that maps $a$ to $\operatorname{out}$ applied to $a$.

Erased.binddefMathlib.Data.Erased, function or constant

Wording

no wording

English

Let $a$ be an element of $\mathrm{Erased}$ applied to $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{Erased}$ applied to $x_{1}$. Then $\operatorname{bind}$ applied to $a$ and $f$ is an element of $\mathrm{Erased}$ applied to $x_{1}$ defined as the function that maps $b$ to $b$.

Erased.choicedefMathlib.Data.Erased, function or constant

Wording

the choice of h (from the name)

English

Assume that $\mathrm{Nonempty}$ holds for $x$. Then the choice of $h$ is an element of $\mathrm{Erased}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{choice}$ applied to $h$.

Erased.equivdefMathlib.Data.Erased, function or constant

Wording

the equivalence of x (from the name)

English

Let $x$ be a set. Then the equivalence of $x$ is an element of $\EquivMACRoAE {\mathrm{Erased} (x)}{x}$ defined as $\operatorname{mk}$ applied to $\operatorname{out}$, $\operatorname{mk}$, $\mathrm{Erased\_\_mk\_out}$ and $\mathrm{Erased\_\_out\_mk}$.

Erased.joindefMathlib.Data.Erased, function or constant

Wording

the join of a (from the name)

English

Let $a$ be an element of $\mathrm{Erased}$ applied to $\mathrm{Erased}$ applied to $x$. Then the join of $a$ is an element of $\mathrm{Erased}$ applied to $x$ defined as $\operatorname{bind}$ applied to $a$ and $\mathrm{id}$.

Erased.mapdefMathlib.Data.Erased, function or constant

Wording

the map of f and a (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $\mathrm{Erased}$ applied to $x$. Then the map of $f$ and $a$ is an element of $\mathrm{Erased}$ applied to $x_{1}$ defined as $\operatorname{bind}$ applied to $a$ and $\operatorname{comp}$ applied to $\operatorname{mk}$ and $f$.

Mathlib.Data.FP.Basic

FP.FloatinductiveMathlib.Data.FP.Basic, type

Wording

no wording

English

The elements of $\operatorname{Float}$ are a basic type.

FP.Float.adddefMathlib.Data.FP.Basic, function or constant

Wording

the sum of x and x1 (from the name)

English

Let $\mathrm{mode}$ be a mode. Let $x$ and $x_{1}$ be elements of $\operatorname{Float}$. Then the sum of $x$ and $x_{1}$ is an element of $\operatorname{Float}$.

FP.Float.ctorElimTypedefMathlib.Data.FP.Basic, type

Wording

no wording

English

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 the set of functions from elements $x$ of $\mathrm{Bool}$ to elements of $\mathrm{motive}$ applied to the infimum of $x$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{nan}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\mathrm{Bool}$ and integers $e$ and natural numbers $m$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{ValidFinite}$ applied to $e$ and $m$ to elements of $\mathrm{motive}$ applied to $\operatorname{finite}$ applied to $x_{1}$, $e$, $m$ and $h$.

FP.Float.divdefMathlib.Data.FP.Basic, function or constant

Wording

the quotient of x and x1 (from the name)

English

Let $\mathrm{mode}$ be a mode. Let $x$ and $x_{1}$ be elements of $\operatorname{Float}$. Then the quotient of $x$ and $x_{1}$ is an element of $\operatorname{Float}$.

FP.Float.finiteconstructorMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{Bool}$. Let $e$ be an integer. Let $m$ be a natural number such that $\operatorname{ValidFinite}$ holds for $e$ and $m$. Then $\operatorname{finite}$ applied to $x$, $e$, $m$ and $h$ is an element of $\operatorname{Float}$.

FP.Float.infconstructorMathlib.Data.FP.Basic, function or constant

Wording

the infimum of x (from the name)

English

Let $x$ be an element of $\mathrm{Bool}$. Then the infimum of $x$ is an element of $\operatorname{Float}$.

FP.Float.isFinitedefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\operatorname{Float}$. Then $\operatorname{isFinite}$ applied to $x$ is an element of $\mathrm{Bool}$.

FP.Float.isZerodefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\operatorname{Float}$. Then $\operatorname{isZero}$ applied to $x$ is an element of $\mathrm{Bool}$.

FP.Float.muldefMathlib.Data.FP.Basic, function or constant

Wording

the product of x and x1 (from the name)

English

Let $\mathrm{mode}$ be a mode. Let $x$ and $x_{1}$ be elements of $\operatorname{Float}$. Then the product of $x$ and $x_{1}$ is an element of $\operatorname{Float}$.

FP.Float.nanconstructorMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{nan}$ is an element of $\operatorname{Float}$.

FP.Float.negdefMathlib.Data.FP.Basic, function or constant

Wording

the negation of x (from the name)

English

Let $x$ be an element of $\operatorname{Float}$. Then the negation of $x$ is an element of $\operatorname{Float}$.

FP.Float.signdefMathlib.Data.FP.Basic, function or constant

Wording

the sign of x (from the name)

English

Let $x$ be an element of $\operatorname{Float}$. Then the sign of $x$ is an element of $\mathrm{Bool}$.

FP.Float.sign'defMathlib.Data.FP.Basic, function or constant

Wording

the sign of x (from the name)

English

Let $x$ be an element of $\operatorname{Float}$. Then the sign of $x$ is an element of $\mathrm{Semiquot}$ applied to $\mathrm{Bool}$.

FP.Float.subdefMathlib.Data.FP.Basic, function or constant

Wording

the difference of f1 and f2 (from the name)

English

Let $\mathrm{mode}$ be a mode. Let $f_{1}$ and $f_{2}$ be elements of $\operatorname{Float}$. Then the difference of $f_{1}$ and $f_{2}$ is an element of $\operatorname{Float}$ defined as the sum of $f_{1}$ and $\operatorname{neg}$ applied to $f_{2}$.

FP.Float.zerodefMathlib.Data.FP.Basic, function or constant

Wording

the zero of s (from the name)

English

Let $s$ be an element of $\mathrm{Bool}$. Then the zero of $s$ is an element of $\operatorname{Float}$ defined as $\operatorname{finite}$ applied to $s$, $\operatorname{emin}$, $0$ and $\operatorname{valid}$.

FP.FloatCfgclassMathlib.Data.FP.Basic, predicate

Wording

no wording

English

We can say that $\operatorname{FloatCfg}$.

FP.FloatCfg.emaxdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{emax}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

FP.FloatCfg.precdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{prec}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

FP.RModeinductiveMathlib.Data.FP.Basic, type

Wording

mode (from the name)

English

The modes are a basic type.

FP.RMode.NEconstructorMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{NE}$ is a mode.

FP.ValidFinitedefMathlib.Data.FP.Basic, predicate

Wording

no wording

English

Let $e$ be an integer. Let $m$ be a natural number. Then $\operatorname{ValidFinite}$ holds for $e$ and $m$, if $\operatorname{emin} \leq e + \operatorname{prec} - 1 \leq \operatorname{emax}$ and $e = \MaxmaxMACRoAF {(e + \operatorname{size} (m)- \operatorname{prec})}{\operatorname{emin}}$.

FP.divNatLtTwoPowdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $n$ and $d$ be natural numbers. Let $x$ be an integer. Then $\operatorname{divNatLtTwoPow}$ applied to $n$, $d$ and $x$ is an element of $\mathrm{Bool}$.

FP.emaxdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{emax}$ is a natural number defined as $\operatorname{emax}$.

FP.emindefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{emin}$ is an integer defined as $1 - \operatorname{emax}$.

FP.instInhabitedRMode.defaultdefMathlib.Data.FP.Basic, function or constant

Wording

the default (from the name)

English

The default is a mode defined as $\operatorname{NE}$.

FP.nextDndefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\operatorname{Float}$. Then $\operatorname{nextDn}$ applied to $x$ is an element of $\operatorname{Float}$.

FP.nextDnPosdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $e$ be an integer. Let $m$ be a natural number such that $\operatorname{ValidFinite}$ holds for $e$ and $m$. Then $\operatorname{nextDnPos}$ applied to $e$, $m$ and $v$ is an element of $\operatorname{Float}$.

FP.nextUpdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $\operatorname{Float}$. Then $\operatorname{nextUp}$ applied to $x$ is an element of $\operatorname{Float}$.

FP.nextUpPosdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $e$ be an integer. Let $m$ be a natural number such that $\operatorname{ValidFinite}$ holds for $e$ and $m$. Then $\operatorname{nextUpPos}$ applied to $e$, $m$ and $v$ is an element of $\operatorname{Float}$.

FP.ofPosRatDndefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $n$ and $d$ be positive natural numbers. Then $\operatorname{ofPosRatDn}$ applied to $n$ and $d$ is an element of $\mathrm{Prod}$ applied to $\operatorname{Float}$ and $\mathrm{Bool}$.

FP.ofRatdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be a mode. Let $x_{1}$ be a rational number. Then $\operatorname{ofRat}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Float}$.

FP.ofRatDndefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $r$ be a rational number. Then $\operatorname{ofRatDn}$ applied to $r$ is an element of $\operatorname{Float}$ defined as the negation of $\operatorname{ofRatUp}$ applied to $\operatorname{neg}$ applied to $r$.

FP.ofRatUpdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

Let $x$ be a rational number. Then $\operatorname{ofRatUp}$ applied to $x$ is an element of $\operatorname{Float}$.

FP.precdefMathlib.Data.FP.Basic, function or constant

Wording

no wording

English

$\operatorname{prec}$ is a natural number defined as $\operatorname{prec}$.

FP.toRatdefMathlib.Data.FP.Basic, function or constant

Wording

the rational number of f and h (from the name)

English

Let $f$ be an element of $\operatorname{Float}$ such that $\EqtMACRoH {\operatorname{isFinite} (f)}{\operatorname{true}}$. Then the rational number of $f$ and $h$ is a rational number.

Int.shift2defMathlib.Data.FP.Basic, function or constant

Wording

the shift of b and x (from the name)

English

Let $a$ and $b$ be natural numbers. Let $x$ be an integer. Then the shift of $b$ and $x$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$.

Mathlib.Data.Fin.Basic

Fin.equivSubtypedefMathlib.Data.Fin.Basic, function or constant

Wording

the equivalence subtype (from the name)

English

The equivalence subtype is an element of $\EquivMACRoAE {\mathrm{Fin} (n)}{(\SubtypeSet {i}{\mathrm{Lt} (i , n)})}$.

Fin.rec0defMathlib.Data.Fin.Basic, function or constant

Wording

no wording

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $0$. Then $\operatorname{rec0}$ applied to $i$ is an element of $x$ applied to $i$.

Fin.tacticFin_omegadefMathlib.Data.Fin.Basic, function or constant

Wording

no wording

English

generation took over the time limit

finZeroElimdefMathlib.Data.Fin.Basic, function or constant

Wording

the finite zero eliminator of x1 (from the name)

English

Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $0$. Then the finite zero eliminator of $x_{1}$ is an element of $x$ applied to $x_{1}$ defined as $\operatorname{elim0}$ applied to $x_{1}$.

Mathlib.Data.Fin.Embedding

Fin.addNatEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the additive natural embedding of m (from the name)

English

Let $m$ be a natural number. Then the additive natural embedding of $m$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + m$.

Fin.castAddEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the cast additive embedding of m (from the name)

English

Let $m$ be a natural number. Then the cast additive embedding of $m$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + m$ defined as $\operatorname{castLEEmb}$ applied to $\mathrm{Nat\_\_le\_add\_right}$ applied to $n$ and $m$.

Fin.castLEEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

no wording

English

Assume that $n \leq m$. Then $\operatorname{castLEEmb}$ applied to $h$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $m$ defined as $\operatorname{mk}$ applied to $\operatorname{castLE}$ applied to $h$ and $\mathrm{Fin\_\_castLE\_injective}$ applied to $h$.

Fin.castSuccEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the cast successor embedding (from the name)

English

The cast successor embedding is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the cast additive embedding of $1$.

Fin.natAddEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the natural additive embedding of n (from the name)

English

Let $n$ be a natural number. Then the natural additive embedding of $n$ is an embedding of $\mathrm{Fin}$ applied to $m$ and $\mathrm{Fin}$ applied to $n + m$.

Fin.natAdd_castLEEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

no wording

English

Assume that $n \leq m$. Then $\mathrm{Fin\_\_natAdd\_castLEEmb}$ applied to $\mathrm{hmn}$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $m$.

Fin.succAboveEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the successor above embedding of p (from the name)

English

Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the successor above embedding of $p$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as $\operatorname{mk}$ applied to $\operatorname{succAbove}$ applied to $p$ and $\mathrm{Fin\_\_succAbove\_right\_injective}$.

Fin.succEmbdefMathlib.Data.Fin.Embedding, function or constant

Wording

the successor embedding of n (from the name)

English

Let $n$ be a natural number. Then the successor embedding of $n$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as $\operatorname{mk}$ applied to $\operatorname{succ}$ and $\mathrm{Fin\_\_succ\_injective}$ applied to $n$.

Fin.valEmbeddingdefMathlib.Data.Fin.Embedding, function or constant

Wording

the value embedding (from the name)

English

The value embedding is an embedding of $\mathrm{Fin}$ applied to $n$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{Fin\_\_val\_injective}$.

Mathlib.Data.Fin.Fin2

Fin2inductiveMathlib.Data.Fin.Fin2, type

Wording

no wording

English

Let $x$ be a natural number. Then the elements of $\mathrm{Fin2}$ applied to $x$ are a basic type.

Fin2.IsLTclassMathlib.Data.Fin.Fin2, predicate

Wording

no wording

English

Let $m$ and $n$ be natural numbers. Then we can say that $\operatorname{IsLT}$ holds for $m$ and $n$.

Fin2.adddefMathlib.Data.Fin.Fin2, function or constant

Wording

the sum of i and k (from the name)

English

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $k$ be a natural number. Then the sum of $i$ and $k$ is an element of $\mathrm{Fin2}$ applied to $n + k$ defined as $\operatorname{brecOn}$ applied to $k$ and $\mathrm{Fin2\_\_add\_\_\_f}$ applied to $i$.

Fin2.cases'defMathlib.Data.Fin.Fin2, function or constant

Wording

the case of H2 and n1 (from the name)

English

Let $H_{1}$ be an element of $C$ applied to $\operatorname{fz}$. Let $H_{2}$ be a function from elements $n_{1}$ of $\mathrm{Fin2}$ applied to $n$ to elements of $C$ applied to $\operatorname{fs}$ applied to $n_{1}$. Let $i$ be an element of $\mathrm{Fin2}$ applied to the successor of $n$. Then the case of $n_{1}$ and $H_{2}$ is an element of $C$ applied to $i$.

Fin2.castSuccdefMathlib.Data.Fin.Fin2, function or constant

Wording

the cast successor of x (from the name)

English

Let $x$ be an element of $\mathrm{Fin2}$ applied to $n$. Then the cast successor of $x$ is an element of $\mathrm{Fin2}$ applied to $n + 1$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Fin2\_\_castSucc\_\_\_f}$.

Fin2.ctorElimTypedefMathlib.Data.Fin.Fin2, type

Wording

no wording

English

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 the set of functions from natural numbers $n$ to elements of $\mathrm{motive}$ applied to $n + 1$ and $\operatorname{fz}$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $n_{1}$ and elements $x$ of $\mathrm{Fin2}$ applied to $n_{1}$ to elements of $\mathrm{motive}$ applied to $n_{1} + 1$ and $\operatorname{fs}$ applied to $x$.

Fin2.elim0defMathlib.Data.Fin.Fin2, function or constant

Wording

the eliminator of i (from the name)

English

Let $i$ be an element of $\mathrm{Fin2}$ applied to $0$. Then the eliminator of $i$ is an element of $C$ applied to $i$.

Fin2.equivFindefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{equivFin}$ applied to $n$ is an element of $\EquivMACRoAE {\mathrm{Fin2} (n)}{\mathrm{Fin} (n)}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFin}$, $\operatorname{ofFin}$, $\mathrm{Fin2\_\_ofFin\_toFin}$ and $\mathrm{Fin2\_\_toFin\_ofFin}$.

Fin2.fsconstructorMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{Fin2}$ applied to $n$. Then $\operatorname{fs}$ applied to $x$ is an element of $\mathrm{Fin2}$ applied to $n + 1$.

Fin2.fzconstructorMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

$\operatorname{fz}$ is an element of $\mathrm{Fin2}$ applied to $n + 1$.

Fin2.insertPermdefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be elements of $\mathrm{Fin2}$ applied to $n$. Then $\operatorname{insertPerm}$ applied to $x$ and $x_{1}$ is an element of $\mathrm{Fin2}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{Fin2\_\_insertPerm\_\_\_f}$ and $x_{1}$.

Fin2.lastdefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

$\operatorname{last}$ is an element of $\mathrm{Fin2}$ applied to $n + 1$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{Fin2\_\_last\_\_\_f}$.

Fin2.leftdefMathlib.Data.Fin.Fin2, function or constant

Wording

the left of k and x (from the name)

English

Let $k$ be a natural number. Let $x$ be an element of $\mathrm{Fin2}$ applied to $n$. Then the left of $k$ and $x$ is an element of $\mathrm{Fin2}$ applied to $k + n$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Fin2\_\_left\_\_\_f}$ applied to $k$.

Fin2.ofFindefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{ofFin}$ applied to $i$ is an element of $\mathrm{Fin2}$ applied to $n$ defined as $\operatorname{succRec}$ applied to the function that maps $x$ to $\operatorname{fz}$, the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{fs}$ and $i$.

Fin2.ofNat'defMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $m$ be a natural number. Then $\operatorname{ofNat'}$ applied to $m$ is an element of $\mathrm{Fin2}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Fin2\_\_ofNat'\_\_\_f}$, $m$ and $h$.

Fin2.optOfNatdefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $x$ be a natural number. Then $\operatorname{optOfNat}$ applied to $x$ is an element of $\mathrm{Option}$ applied to $\mathrm{Fin2}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Fin2\_\_optOfNat\_\_\_f}$ and $x$.

Fin2.remapLeftdefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\mathrm{Fin2}$ applied to $m$ to elements of $\mathrm{Fin2}$ applied to $n$. Let $k$ be a natural number. Let $x$ be an element of $\mathrm{Fin2}$ applied to $m + k$. Then $\operatorname{remapLeft}$ applied to $f$, $k$ and $x$ is an element of $\mathrm{Fin2}$ applied to $n + k$ defined as $\operatorname{brecOn}$ applied to $k$, $\mathrm{Fin2\_\_remapLeft\_\_\_f}$ applied to $f$ and $x$.

Fin2.revdefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $x$ be an element of $\mathrm{Fin2}$ applied to $n$. Then $\operatorname{rev}$ applied to $x$ is an element of $\mathrm{Fin2}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Fin2\_\_rev\_\_\_f}$.

Fin2.toFindefMathlib.Data.Fin.Fin2, function or constant

Wording

no wording

English

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Then $\operatorname{toFin}$ applied to $i$ is an element of $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{brecOn}$ applied to $i$ and $\mathrm{Fin2\_\_toFin\_\_\_f}$.

Fin2.toNatdefMathlib.Data.Fin.Fin2, function or constant

Wording

the natural number of x (from the name)

English

Let $x$ be an element of $\mathrm{Fin2}$ applied to $n$. Then the natural number of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{Fin2\_\_toNat\_\_\_f}$.

Mathlib.Data.Fin.FlagRange

Flag.rangeFindefMathlib.Data.Fin.FlagRange, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ such that $f$ applied to $0$ is equal to the bottom, $f$ applied to $\operatorname{last}$ applied to $n$ is equal to the top and for all elements $k$ of $\mathrm{Fin}$ applied to $n$, $\mathrm{WCovBy}$ holds for $f$ applied to $\operatorname{castSucc}$ applied to $k$ and $f$ applied to $\operatorname{succ}$ applied to $k$. Then $\operatorname{rangeFin}$ applied to $f$, $h_{0}$, $\mathrm{hlast}$ and $\mathrm{hcovBy}$ is a flag of $x$.

Mathlib.Data.Fin.Rev

Fin.revPermdefMathlib.Data.Fin.Rev, function or constant

Wording

no wording

English

$\operatorname{revPerm}$ is a permutation of $\mathrm{Fin}$ applied to $n$ defined as the permutation of $\operatorname{rev}$ and $\mathrm{Fin\_\_rev\_involutive}$.

Mathlib.Data.Fin.SuccPred

Fin.castPreddefMathlib.Data.Fin.SuccPred, function or constant

Wording

the cast predecessor of i and h (from the name)

English

Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$ such that $i \neq \operatorname{last} (n)$. Then the cast predecessor of $i$ and $h$ is an element of $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{castLT}$ applied to $i$ and $\mathrm{Fin\_\_val\_lt\_last}$ applied to $h$.

Fin.predAbovedefMathlib.Data.Fin.SuccPred, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{Fin}$ applied to $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{predAbove}$ applied to $p$ and $i$ is an element of $\mathrm{Fin}$ applied to $n$.

Fin.succAbovedefMathlib.Data.Fin.SuccPred, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{succAbove}$ applied to $p$ and $i$ is an element of $\mathrm{Fin}$ applied to $n + 1$ defined as $\iteMACRoG {\mathrm{Lt} (\operatorname{castSucc} (i), p)}{\operatorname{castSucc} (i)}{\operatorname{succ} (i)}$.

finCongrdefMathlib.Data.Fin.SuccPred, function or constant

Wording

the finite congruence of eq (from the name)

English

Assume that $n = m$. Then the finite congruence of $\mathrm{eq}$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n)}{\mathrm{Fin} (m)}$ defined as $\operatorname{mk}$ applied to $\operatorname{cast}$ applied to $\mathrm{eq}$, $\operatorname{cast}$ applied to $\operatorname{symm}$ applied to $\mathrm{eq}$, $\mathrm{Fin\_\_leftInverse\_cast}$ applied to $\mathrm{eq}$ and $\mathrm{Fin\_\_rightInverse\_cast}$ applied to $\mathrm{eq}$.

Mathlib.Data.Fin.Tuple.Basic

Fin.appenddefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $b$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $m + n$. Then $\operatorname{append}$ applied to $a$, $b$ and $x_{1}$ is an element of $x$ defined as $\operatorname{addCases}$ applied to $a$, $b$ and $x_{1}$.

Fin.consdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $x$ applied to $0$. Let $p$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succ}$ applied to $i_{1}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{cons}$ applied to $x_{1}$, $i_{1}$, $p$ and $i$ is an element of $x$ applied to $i$ defined as the function that maps $i$ to $\operatorname{cases}$ applied to $x_{1}$, $i_{1}$, $p$ and $i$.

Fin.consCasesdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $\mathrm{cons}$ be a function from elements $x_{2}$ of $x$ applied to $0$ and functions $x_{3}$ from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succ}$ applied to $i_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{2}$ and $x_{3}$. Let $x_{1}$ be a function from elements $i$ of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x$ applied to $i$. Then $\operatorname{consCases}$ applied to $x_{2}$, $x_{3}$, $\mathrm{cons}$, $i$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $x_{1}$.

Fin.consEquivdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Then $\operatorname{consEquiv}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x (0), \mathrm{Elem} (\mathrm{Fin} (n))\rightarrow x (\operatorname{succ} (i)))}{(\mathrm{Elem} (\mathrm{Fin} (n + 1))\rightarrow x (i_{1}))}$.

Fin.consInductiondefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $\mathrm{elim0}$ be an element of $\mathrm{motive}$ applied to $0$ and $\operatorname{elim0}$. Let $\mathrm{cons}$ be a function from natural numbers $n_{1}$ and elements $x_{3}$ of $x$ and functions $x_{4}$ from elements of $\mathrm{Fin}$ applied to $n_{1}$ to elements of $x$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $x_{4}$ to elements of $\mathrm{motive}$ applied to $n_{1} + 1$ and $\operatorname{cons}$ applied to $x_{3}$ and $x_{4}$. Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then $\operatorname{consInduction}$ applied to $\mathrm{elim0}$, $n_{1}$, $x_{3}$, $x_{4}$, $\mathrm{cons}$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $n$ and $x_{1}$ defined as the function that maps $x_{4}$, $\mathrm{cons}$ and $x_{1}$ to $\operatorname{brecOn}$ applied to $n$, $\mathrm{Fin\_\_consInduction\_\_\_f}$ applied to $\mathrm{elim0}$ and $n_{1}$, $x_{3}$, $x_{4}$, $\mathrm{cons}$ and $x_{1}$.

Fin.contractNthdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $j$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $\mathrm{op}$ be a function from elements of $x$ and elements of $x$ to elements of $x$. Let $g$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$. Let $k$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{contractNth}$ applied to $j$, $\mathrm{op}$, $g$ and $k$ is an element of $x$ defined as $\iteMACRoG {\mathrm{Lt} (\operatorname{val} (k), \operatorname{val} (j))}{g (\operatorname{castSucc} (k))}{(\iteMACRoG {\mathrm{Eq} (\operatorname{val} (k), \operatorname{val} (j))}{\mathrm{op} (g (\operatorname{castSucc} (k)), g (\operatorname{succ} (k)))}{g (\operatorname{succ} (k))})}$.

Fin.finddefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to propositions such that there exists an element $k$ of $\mathrm{Fin}$ applied to $n$, such that $p$ holds for $k$. Then $\operatorname{find}$ applied to $p$ and $h$ is an element of $\mathrm{Fin}$ applied to $n$.

Fin.initdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $q$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{init}$ applied to $i_{1}$, $q$ and $i$ is an element of $x$ applied to $\operatorname{castSucc}$ applied to $i$ defined as the function that maps $i$ to $i_{1}$ applied to $\operatorname{castSucc}$ applied to $q$ and $i$.

Fin.insertNthdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 1$. Let $x_{1}$ be an element of $x$ applied to $i$. Let $p$ be a function from elements $j_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succAbove}$ applied to $i$ and $j_{1}$. Then $\operatorname{insertNth}$ applied to $i$, $x_{1}$, $j_{1}$, $p$ and $j$ is an element of $x$ applied to $j$ defined as the function that maps $j$ to the successor above case of $j_{1}$ and $p$.

Fin.insertNthEquivdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{insertNthEquiv}$ applied to $x$ and $p$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x (p), \mathrm{Elem} (\mathrm{Fin} (n))\rightarrow x (\operatorname{succAbove} (p , i)))}{(\mathrm{Elem} (\mathrm{Fin} (n + 1))\rightarrow x (i_{1}))}$.

Fin.removeNthdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{removeNth}$ applied to $p$, $i_{1}$, $f$ and $i$ is an element of $x$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ defined as the function that maps $i$ to $i_{1}$ applied to $\operatorname{succAbove}$ applied to $p$ and $f$ and $i$.

Fin.repeatdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $m$ be a natural number. Let $a$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $m \times n$. Then $\operatorname{repeat}$ applied to $m$, $a$ and $x_{1}$ is an element of $x$ defined as $a$ applied to $\operatorname{modNat}$ applied to $x_{1}$.

Fin.snocdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{castSucc}$ applied to $i_{1}$. Let $x_{1}$ be an element of $x$ applied to $\operatorname{last}$ applied to $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{snoc}$ applied to $i_{1}$, $p$, $x_{1}$ and $i$ is an element of $x$ applied to $i$.

Fin.snocCasesdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $\mathrm{snoc}$ be a function from functions $\mathrm{xs}$ from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{castSucc}$ applied to $i_{1}$ and elements $x_{2}$ of $x$ applied to $\operatorname{last}$ applied to $n$ to elements of $\mathrm{motive}$ applied to $\operatorname{snoc}$ applied to $\mathrm{xs}$ and $x_{2}$. Let $x_{1}$ be a function from elements $i$ of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x$ applied to $i$. Then $\operatorname{snocCases}$ applied to $\mathrm{xs}$, $x_{2}$, $\mathrm{snoc}$, $i$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $x_{1}$.

Fin.snocEquivdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Then $\operatorname{snocEquiv}$ applied to $x$ is an element of $\EquivMACRoAE {\mathrm{Prod} (x (\operatorname{last} (n)), \mathrm{Elem} (\mathrm{Fin} (n))\rightarrow x (\operatorname{castSucc} (i)))}{(\mathrm{Elem} (\mathrm{Fin} (n + 1))\rightarrow x (i_{1}))}$.

Fin.snocInductiondefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $\mathrm{elim0}$ be an element of $\mathrm{motive}$ applied to $0$ and $\operatorname{elim0}$. Let $\mathrm{snoc}$ be a function from natural numbers $n_{1}$ and functions $x_{3}$ from elements of $\mathrm{Fin}$ applied to $n_{1}$ to elements of $x$ and elements $x_{4}$ of $x$ and elements of $\mathrm{motive}$ applied to $n_{1}$ and $x_{3}$ to elements of $\mathrm{motive}$ applied to $n_{1} + 1$ and $\operatorname{snoc}$ applied to $x_{3}$ and $x_{4}$. Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then $\operatorname{snocInduction}$ applied to $\mathrm{elim0}$, $n_{1}$, $x_{3}$, $x_{4}$, $\mathrm{snoc}$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $n$ and $x_{1}$ defined as the function that maps $x_{4}$, $\mathrm{snoc}$ and $x_{1}$ to $\operatorname{brecOn}$ applied to $n$, $\mathrm{Fin\_\_snocInduction\_\_\_f}$ applied to $\mathrm{elim0}$ and $n_{1}$, $x_{3}$, $x_{4}$, $\mathrm{snoc}$ and $x_{1}$.

Fin.succAboveCasesdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

the successor above case of p and j1 (from the name)

English

Let $i$ and $j$ be elements of $\mathrm{Fin}$ applied to $n + 1$. Let $x_{1}$ be an element of $x$ applied to $i$. Let $p$ be a function from elements $j_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succAbove}$ applied to $i$ and $j_{1}$. Then the successor above case of $j_{1}$ and $p$ is an element of $x$ applied to $j$.

Fin.taildefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

the tail of q and i1 (from the docstring)

English

Let $q$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the tail of $i_{1}$ and $q$ is an element of $x$ applied to $\operatorname{succ}$ applied to $i$ defined as the function that maps $i$ to $i_{1}$ applied to $\operatorname{succ}$ applied to $q$ and $i$.

piFinTwoEquivdefMathlib.Data.Fin.Tuple.Basic, function or constant

Wording

no wording

English

Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\mathrm{piFinTwoEquiv}$ applied to $x$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (\mathrm{Fin} (2))\rightarrow x (i))}{\mathrm{Prod} (x (0), x (1))}$.

Mathlib.Data.Fin.Tuple.Curry

Function.FromTypes.currydefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

the curry of x1 (from the name)

English

Let $x_{1}$ be a function from functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $p$ applied to $i$ to elements of $x$. Then the curry of $x_{1}$ is an element of $\operatorname{FromTypes}$ applied to $p$ and $x$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Function\_\_FromTypes\_\_curry\_\_\_f}$, $p$, $x$ and $x_{1}$.

Function.FromTypes.curryEquivdefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

the curry equivalence of p (from the name)

English

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to sets. Then the curry equivalence of $p$ is an element of $\EquivMACRoAE {((\mathrm{Elem} (\mathrm{Fin} (n))\rightarrow p (i))\rightarrow x)}{\operatorname{FromTypes} (p , x)}$ defined as $\operatorname{mk}$ applied to $\operatorname{curry}$, $\operatorname{uncurry}$, $\mathrm{Function\_\_FromTypes\_\_uncurry\_curry}$ and $\mathrm{Function\_\_FromTypes\_\_curry\_uncurry}$.

Function.FromTypes.uncurrydefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

no wording

English

Let $f$ be an element of $\operatorname{FromTypes}$ applied to $p$ and $x$. Let $x_{1}$ be a function from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $p$ applied to $i$. Then $\operatorname{uncurry}$ applied to $f$, $i$ and $x_{1}$ is an element of $x$ defined as the function that maps $x_{1}$ to $\operatorname{brecOn}$ applied to $n$, $\mathrm{Function\_\_FromTypes\_\_uncurry\_\_\_f}$, $p$, $x$, $f$, $i$ and $x_{1}$.

Function.OfArity.currydefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

the curry of f (from the name)

English

Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$ to elements of $x_{1}$. Then the curry of $f$ is an arity of $x_{1}$ and $n$ defined as the curry of $f$.

Function.OfArity.curryEquivdefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

the curry equivalence of n (from the name)

English

Let $n$ be a natural number. Then the curry equivalence of $n$ is an equivalence from the set of functions from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$ to elements of $x_{1}$ to the set of arities of $x_{1}$ and $n$ defined as the curry equivalence of the function that maps $x_{2}$ to $x$.

Function.OfArity.uncurrydefMathlib.Data.Fin.Tuple.Curry, function or constant

Wording

no wording

English

Let $f$ be an arity of $x_{1}$ and $n$. Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then $\operatorname{uncurry}$ applied to $f$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{uncurry}$ applied to $f$ and $x_{2}$.

Mathlib.Data.Fin.Tuple.Embedding

Fin.Embedding.appenddefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

Assume that the range of $\operatorname{coe}$ applied to $x_{1}$ is disjoint to the range of $\operatorname{coe}$ applied to $y$. Then $\operatorname{append}$ applied to $h$ is an embedding of $\mathrm{Fin}$ applied to $m + n$ and $x$.

Fin.Embedding.consdefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

Let $x_{1}$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $x$ such that $a$ is not an element of the range of $\operatorname{coe}$ applied to $x_{1}$. Then $\operatorname{cons}$ applied to $x_{1}$ and $\mathrm{ha}$ is an embedding of $\mathrm{Fin}$ applied to $n + 1$ and $x$.

Fin.Embedding.initdefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

Let $x_{1}$ be an embedding of $\mathrm{Fin}$ applied to $n + 1$ and $x$. Then $\operatorname{init}$ applied to $x_{1}$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $x$.

Fin.Embedding.snocdefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

Let $x_{1}$ be an embedding of $\mathrm{Fin}$ applied to $n$ and $x$ such that $a$ is not an element of the range of $\operatorname{coe}$ applied to $x_{1}$. Then $\operatorname{snoc}$ applied to $x_{1}$ and $\mathrm{ha}$ is an embedding of $\mathrm{Fin}$ applied to $n + 1$ and $x$.

Fin.Embedding.taildefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

the tail of x1 (from the name)

English

Let $x_{1}$ be an embedding of $\mathrm{Fin}$ applied to $n + 1$ and $x$. Then the tail of $x_{1}$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $x$.

Function.Embedding.embFinTwodefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

Assume that $a \neq b$. Then $\operatorname{embFinTwo}$ applied to $h$ is an embedding of $\mathrm{Fin}$ applied to $2$ and $x$ defined as the inverse function of $\operatorname{twoEmbeddingEquiv}$ and $\ProdmkMACRoU {a}{b}$.

Function.Embedding.twoEmbeddingEquivdefMathlib.Data.Fin.Tuple.Embedding, function or constant

Wording

no wording

English

$\operatorname{twoEmbeddingEquiv}$ is an equivalence from the set of embeddings of $\mathrm{Fin}$ applied to $2$ and $x$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\mathrm{Function\_\_Embedding\_\_twoEmbeddingEquiv\_\_match\_1}$ applied to the function that maps $x_{2}$ to the set of propositions, $x_{1}$ and the function that maps $a$ and $b$ to $\mathrm{Neq} (a , b)$.

Mathlib.Data.Fin.Tuple.NatAntidiagonal

Finset.Nat.antidiagonalTupledefMathlib.Data.Fin.Tuple.NatAntidiagonal, function or constant

Wording

the antidiagonal tuple of k and n (from the name)

English

Let $k$ and $n$ be natural numbers. Then the antidiagonal tuple of $k$ and $n$ is a finite set of the set of functions from elements of $\mathrm{Fin}$ applied to $k$ to natural numbers defined as $\operatorname{mk}$ applied to the antidiagonal tuple of $k$ and $n$ and $\mathrm{Multiset\_\_Nat\_\_nodup\_antidiagonalTuple}$ applied to $k$ and $n$.

Finset.Nat.sigmaAntidiagonalTupleEquivTupledefMathlib.Data.Fin.Tuple.NatAntidiagonal, function or constant

Wording

the sigma antidiagonal tuple equivalence tuple of k (from the name)

English

Let $k$ be an element of $\Natural$. Then the sigma antidiagonal tuple equivalence tuple of $k$ is an element of $\EquivMACRoAE {\Sigma (\lambda n . \SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{antidiagonalTuple} (k , n)}{x})})}{(\mathrm{Elem} (\mathrm{Fin} (k))\rightarrow \Natural)}$.

List.Nat.antidiagonalTupledefMathlib.Data.Fin.Tuple.NatAntidiagonal, function or constant

Wording

the antidiagonal tuple of k and x (from the name)

English

Let $k$ and $x$ be natural numbers. Then the antidiagonal tuple of $k$ and $x$ is a list of functions from elements of $\mathrm{Fin}$ applied to $k$ to natural numbers defined as $\operatorname{brecOn}$ applied to $k$, $\mathrm{List\_\_Nat\_\_antidiagonalTuple\_\_\_f}$ and $x$.

Multiset.Nat.antidiagonalTupledefMathlib.Data.Fin.Tuple.NatAntidiagonal, function or constant

Wording

the antidiagonal tuple of k and n (from the name)

English

Let $k$ and $n$ be natural numbers. Then the antidiagonal tuple of $k$ and $n$ is a multiset of the set of functions from elements of $\mathrm{Fin}$ applied to $k$ to natural numbers defined as the multiset of the antidiagonal tuple of $k$ and $n$.

Mathlib.Data.Fin.Tuple.Reflection

Fin.prod_univ_ofNatdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the product universal set (from the name)

English

The product universal set is an element of $\operatorname{Simproc}$.

Fin.sum_univ_ofNatdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the sum universal set (from the name)

English

The sum universal set is an element of $\operatorname{Simproc}$.

FinVec.ExistsdefMathlib.Data.Fin.Tuple.Reflection, predicate

Wording

no wording

English

Let $x_{1}$ be a function from functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$ to propositions. Then $\operatorname{Exists}$ holds for $x_{1}$, if $\operatorname{brecOn}$ holds for $m$, $\mathrm{FinVec\_\_Exists\_\_\_f}$ and $x_{1}$.

FinVec.ForalldefMathlib.Data.Fin.Tuple.Reflection, predicate

Wording

no wording

English

Let $x_{1}$ be a function from functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$ to propositions. Then $\operatorname{Forall}$ holds for $x_{1}$, if $\operatorname{brecOn}$ holds for $m$, $\mathrm{FinVec\_\_Forall\_\_\_f}$ and $x_{1}$.

FinVec.etaExpanddefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

no wording

English

Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $m$. Then $\operatorname{etaExpand}$ applied to $v$ and $x_{1}$ is an element of $x$ defined as the map of $v$ and $x_{1}$.

FinVec.mapdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the map of x2 and x3 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $x_{3}$ be an element of $\mathrm{Fin}$ applied to $m$. Then the map of $x_{2}$ and $x_{3}$ is an element of $x_{1}$ defined as the sequence of $x_{2}$ and $x_{3}$.

FinVec.mkProdEqQdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

no wording

English

generation took over the time limit

FinVec.mkSumEqQdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

no wording

English

generation took over the time limit

FinVec.proddefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the product of x3 (from the name)

English

Let $x_{3}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Then the product of $x_{3}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $m$, $\mathrm{FinVec\_\_prod\_\_\_f}$ and $x_{3}$.

FinVec.seqdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the sequence of x3 and x4 (from the name)

English

Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ and elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $m$. Then the sequence of $x_{3}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $m$, $\mathrm{FinVec\_\_seq\_\_\_f}$, $x_{2}$, $x_{3}$ and $x_{4}$.

FinVec.sumdefMathlib.Data.Fin.Tuple.Reflection, function or constant

Wording

the sum of x3 (from the name)

English

Let $x_{3}$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Then the sum of $x_{3}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $m$, $\mathrm{FinVec\_\_sum\_\_\_f}$ and $x_{3}$.

Mathlib.Data.Fin.Tuple.Sort

Tuple.graphdefMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

the graph of f (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then the graph of $f$ is a finite set of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $\mathrm{Fin}$ applied to $n$ defined as the forward image of the universal set under the function that maps $i$ to $\ProdmkMACRoU {f (i)}{i}$.

Tuple.graph.projdefMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

the projection of x2 (from the name)

English

Let $x_{2}$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{graph} (f)}{x_{3}})}$. Then the projection of $x_{2}$ is an element of $x$ defined as $\ProdfstMACRoZ {x_{2}}$.

Tuple.graphEquiv₁defMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

the graph equivalence of f (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then the graph equivalence of $f$ is an element of $\EquivMACRoAE {\mathrm{Fin} (n)}{(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{graph} (f)}{x_{2}})})}$.

Tuple.graphEquiv₂defMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

the graph equivalence of f (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then the graph equivalence of $f$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{graph} (f)}{x_{2}})}$.

Tuple.sortdefMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

the sort of f (from the name)

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then the sort of $f$ is a permutation of $\mathrm{Fin}$ applied to $n$ defined as the composition of $\operatorname{toEquiv}$ applied to the graph equivalence of $f$ and the inverse of the graph equivalence of $f$.

Tuple.sortDescdefMathlib.Data.Fin.Tuple.Sort, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then $\operatorname{sortDesc}$ applied to $f$ is a permutation of $\mathrm{Fin}$ applied to $n$ defined as the sort of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $f$.

Mathlib.Data.Fin.Tuple.Take

Fin.takedefMathlib.Data.Fin.Tuple.Take, function or constant

Wording

no wording

English

Let $m$ be a natural number such that $m \leq n$. Let $v$ be a function from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $i_{1}$. Let $i$ be an element of $\mathrm{Fin}$ applied to $m$. Then $\operatorname{take}$ applied to $m$, $h$, $i_{1}$, $v$ and $i$ is an element of $x$ applied to $\operatorname{castLE}$ applied to $h$ and $i$ defined as the function that maps $i$ to $i_{1}$ applied to $\operatorname{castLE}$ applied to $h$ and $v$ and $i$.

Mathlib.Data.Fin.VecNotation

Matrix.cons_valdefMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

$\operatorname{DSimproc}$.

Matrix.matchVecConsPrefixopaqueMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

generation took over the time limit

Matrix.vecAlt0defMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

Assume that $m = n + n$. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $k$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{vecAlt0}$ applied to $\mathrm{hm}$, $v$ and $k$ is an element of $x$.

Matrix.vecAlt1defMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

Assume that $m = n + n$. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $k$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{vecAlt1}$ applied to $\mathrm{hm}$, $v$ and $k$ is an element of $x$.

Matrix.vecAppenddefMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

Assume that $o = m + n$. Let $u$ be a function from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$. Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $o$. Then $\operatorname{vecAppend}$ applied to $\mathrm{ho}$, $u$, $v$ and $x_{1}$ is an element of $x$ defined as $\operatorname{comp}$ applied to $\operatorname{append}$ applied to $u$ and $v$, $\operatorname{cast}$ applied to $\mathrm{ho}$ and $x_{1}$.

Matrix.vecConsdefMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

Let $h$ be an element of $x$. Let $t$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to the successor of $n$. Then $\operatorname{vecCons}$ applied to $h$, $t$ and $x_{1}$ is an element of $x$ defined as $\operatorname{cons}$ applied to $h$, $t$ and $x_{1}$.

Matrix.vecEmptydefMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $0$. Then $\operatorname{vecEmpty}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{elim0}$ applied to $x_{1}$.

Matrix.vecHeaddefMathlib.Data.Fin.VecNotation, function or constant

Wording

the vector head of v (from the name)

English

Let $v$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x$. Then the vector head of $v$ is an element of $x$ defined as $v$ applied to $0$.

Matrix.vecNotationdefMathlib.Data.Fin.VecNotation, function or constant

Wording

the vector notation (from the name)

English

generation took over the time limit

Matrix.vecTaildefMathlib.Data.Fin.VecNotation, function or constant

Wording

the vector tail of v and x1 (from the name)

English

Let $v$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $n$. Then the vector tail of $v$ and $x_{1}$ is an element of $x$ defined as $\operatorname{comp}$ applied to $v$, $\operatorname{succ}$ and $x_{1}$.

PiFin.mkLiteralQdefMathlib.Data.Fin.VecNotation, function or constant

Wording

no wording

English

generation took over the time limit

Mathlib.Data.FinEnum

FinEnumclassMathlib.Data.FinEnum, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{FinEnum}$ holds for $x$.

FinEnum.Finset.enumdefMathlib.Data.FinEnum, function or constant

Wording

no wording

English

Let $x_{2}$ be a list of elements of $x$. Then $\operatorname{enum}$ applied to $x_{2}$ is a list of finite sets of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{FinEnum\_\_Finset\_\_enum\_\_\_f}$.

FinEnum.carddefMathlib.Data.FinEnum, function or constant

Wording

the cardinality of x (from the name)

English

Let $x$ be a set. Then the cardinality of $x$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

FinEnum.equivdefMathlib.Data.FinEnum, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

FinEnum.toListdefMathlib.Data.FinEnum, function or constant

Wording

the list of x (from the name)

English

Let $x$ be a set. Then the list of $x$ is a list of elements of $x$ defined as $\operatorname{map}$ applied to $\operatorname{coe}$ applied to the inverse of the equivalence and $\operatorname{finRange}$ applied to the cardinality of $x$.

List.Pi.enumdefMathlib.Data.FinEnum, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements of $x$ to sets. Then $\operatorname{enum}$ applied to $x_{2}$ is a list of functions from elements $a$ of $x$ to elements of $x_{2}$ applied to $a$ defined as $\operatorname{map}$ applied to the function that maps $f$ and $x_{4}$ to $f$ applied to $x_{4}$ and $\mathrm{FinEnum\_\_mem\_toList}$ applied to $x_{4}$ and the product of the list of $x$ and the function that maps $x_{5}$ to the list of $x_{2}$ applied to $x_{5}$.

Mathlib.Data.FinEnum.Option

FinEnum.recEmptyOptiondefMathlib.Data.FinEnum.Option, function or constant

Wording

no wording

English

Let $\mathrm{finChoice}$ be a function from natural numbers $n$ to elements of $\mathrm{Fin}$ applied to $n + 1$. Let $\mathrm{congr}$ be a function from sets $x_{5}$ and sets $x_{6}$ and elements $x_{7}$ of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{5}$ and elements $x_{8}$ of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{6}$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{6}$ is equal to the cardinality of $x_{5}$ and elements of $P$ applied to $x_{5}$ to elements of $P$ applied to $x_{6}$. Let $\mathrm{empty}$ be an element of $P$ applied to $\mathrm{PEmpty}$. Let $\mathrm{option}$ be a function from sets $x_{2}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{2}$ and elements of $P$ applied to $x_{2}$ to elements of $P$ applied to $\mathrm{Option}$ applied to $x_{2}$. Let $x$ be a set. Then $\operatorname{recEmptyOption}$ applied to $n$, $\mathrm{finChoice}$, $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{2}$, $\mathrm{option}$ and $x$ is an element of $P$ applied to $x$ defined as the function that maps $x_{8}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{2}$, $\mathrm{option}$ and $x$ to $\mathrm{FinEnum\_\_recEmptyOption\_\_\_unary}$ applied to $n$, $\mathrm{finChoice}$, $x_{5}$, $x_{6}$, $\operatorname{mk}$ applied to $x_{7}$ and $x_{1}$, $x_{8}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{2}$, $\mathrm{option}$ and $x$.

FinEnum.recOnEmptyOptiondefMathlib.Data.FinEnum.Option, function or constant

Wording

no wording

English

Assume that $\mathrm{FinEnum}$ holds for $x$. Let $\mathrm{finChoice}$ be a function from natural numbers $n$ to elements of $\mathrm{Fin}$ applied to $n + 1$. Let $\mathrm{congr}$ be a function from sets $x_{4}$ and sets $x_{5}$ and elements $x_{6}$ of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{4}$ and elements $x_{7}$ of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{5}$ and elements of $\mathrm{Proof}$ applied to the proposition that the cardinality of $x_{5}$ is equal to the cardinality of $x_{4}$ and elements of $P$ applied to $x_{4}$ to elements of $P$ applied to $x_{5}$. Let $\mathrm{empty}$ be an element of $P$ applied to $\mathrm{PEmpty}$. Let $\mathrm{option}$ be a function from sets $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{FinEnum}$ applied to $x_{1}$ and elements of $P$ applied to $x_{1}$ to elements of $P$ applied to $\mathrm{Option}$ applied to $x_{1}$. Then $\operatorname{recOnEmptyOption}$ applied to $\mathrm{aenum}$, $n$, $\mathrm{finChoice}$, $x_{4}$, $x_{5}$, $x_{6}$, $x_{7}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{1}$ and $\mathrm{option}$ is an element of $P$ applied to $x$ defined as the function that maps $x_{6}$, $x_{7}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{1}$ and $\mathrm{option}$ to $\operatorname{recEmptyOption}$ applied to $n$, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{finChoice}$ applied to $x_{1}$ and $x_{2}$, $x_{4}$, the function that maps $x_{3}$ to $x_{5}$ applied to $x_{3}$, $x$, $x_{6}$, $x_{7}$, $\mathrm{congr}$, $\mathrm{empty}$, $x_{1}$ and $\mathrm{option}$.

Mathlib.Data.Finmap

AList.toFinmapdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $s$ be a list of $x_{1}$. Then $\operatorname{toFinmap}$ applied to $s$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to the multiset of the entry of $s$ and $\operatorname{nodupKeys}$ applied to $s$.

FinmapstructureMathlib.Data.Finmap, type

Wording

no wording

English

Let $x_{1}$ be a function from elements of $x$ to sets. Then the elements of $\mathrm{Finmap}$ applied to $x_{1}$ are a basic type.

Finmap.DisjointdefMathlib.Data.Finmap, predicate

Wording

x2 is disjoint to x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Finmap}$ applied to $x_{1}$. Then $x_{2}$ is disjoint to $x_{3}$, if for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $x_{2}$, then $x_{4}$ is not an element of $x_{3}$.

Finmap.alldefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{2}$ of $x$ and elements of $x_{1}$ applied to $x_{2}$ to elements of $\mathrm{Bool}$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{all}$ applied to $x_{2}$, $f$ and $s$ is an element of $\mathrm{Bool}$.

Finmap.anydefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $f$ be a function from elements $x_{2}$ of $x$ and elements of $x_{1}$ applied to $x_{2}$ to elements of $\mathrm{Bool}$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{any}$ applied to $x_{2}$, $f$ and $s$ is an element of $\mathrm{Bool}$.

Finmap.entriesdefMathlib.Data.Finmap, function or constant

Wording

the entry of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then the entry of $\mathrm{self}$ is a multiset of $\Sigma$ applied to $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Finmap.erasedefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{erase}$ applied to $a$ and $s$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$.

Finmap.extractdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{extract}$ applied to $a$ and $s$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x_{1}$ applied to $a$ and $\mathrm{Finmap}$ applied to $x_{1}$.

Finmap.foldldefMathlib.Data.Finmap, function or constant

Wording

no wording

English

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}$ such that for all elements $d_{1}$ of $x_{2}$, for all elements $x_{3}$ of $x$, for all elements $x_{4}$ of $x_{1}$ applied to $x_{3}$, for all elements $x_{5}$ of $x$, for all elements $x_{6}$ of $x_{1}$ applied to $x_{5}$, $\EqtMACRoH {f (f (d_{1} , x_{3} , x_{4}), x_{5} , x_{6})}{f (f (d_{1} , x_{5} , x_{6}), x_{3} , x_{4})}$. Let $d$ be an element of $x_{2}$. Let $m$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{foldl}$ applied to $a$, $f$, $H$, $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 $d_{1}$ and $s$ to $a$ applied to $d_{1}$, $\operatorname{fst}$ applied to $s$ and $\operatorname{snd}$ applied to $s$, $H$, the entry of $d$ and $m$.

Finmap.insertdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{insert}$ applied to $a$, $b$ and $s$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$.

Finmap.keysdefMathlib.Data.Finmap, function or constant

Wording

the key of s (from the name)

English

Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then the key of $s$ is a finite set of $x$.

Finmap.keysLookupEquivdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

$\operatorname{keysLookupEquiv}$ is an element of $\EquivMACRoAE {\mathrm{Finmap} (x_{1})}{(\SubtypeSet {f}{\mathrm{forall} (x , \lambda i . \mathrm{iff} (\EqtMACRoH {\operatorname{isSome} (\ProdsndMACRoAA {f})}{\operatorname{true}}, \MembershipmemMACRoT {\ProdfstMACRoZ {f}}{i}))})}$.

Finmap.liftOndefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Let $f$ be a function from lists of $x_{1}$ to elements of $x_{2}$ such that for all lists $a$ and $b$ of $x_{1}$, if $\operatorname{Perm}$ holds for the entry of $a$ and the entry of $b$, then $\EqtMACRoH {f (a)}{f (b)}$. Then $\operatorname{liftOn}$ applied to $s$, $f$ and $H$ is an element of $x_{2}$.

Finmap.liftOn₂defMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Finmap}$ applied to $x_{1}$. Let $f$ be a function from lists of $x_{1}$ and lists of $x_{1}$ to elements of $x_{2}$ such that for all lists $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ of $x_{1}$, if $\operatorname{Perm}$ holds for the entry of $x_{5}$ and the entry of $x_{7}$, then if $\operatorname{Perm}$ holds for the entry of $x_{6}$ and the entry of $x_{8}$, then $\EqtMACRoH {f (x_{5} , x_{6})}{f (x_{7} , x_{8})}$. Then $\mathrm{Finmap\_\_liftOn\_u2082\_}$ applied to $x_{3}$, $x_{4}$, $f$ and $H$ is an element of $x_{2}$.

Finmap.lookupdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $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{liftOn}$ applied to $s$, $\operatorname{lookup}$ applied to $a$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{AList\_\_perm\_lookup}$.

Finmap.replacedefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $s$ be an element of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{replace}$ applied to $a$, $b$ and $s$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$.

Finmap.sdiffdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $s$ and $\mathrm{s'}$ be elements of $\mathrm{Finmap}$ applied to $x_{1}$. Then $\operatorname{sdiff}$ applied to $s$ and $\mathrm{s'}$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$ defined as $\operatorname{foldl}$ applied to the function that maps $s_{1}$, $x_{3}$ and $x_{4}$ to $\operatorname{erase}$ applied to $x_{3}$ and $s_{1}$, the function that maps $x_{5}$, $x_{6}$, $x_{7}$, $x_{8}$ and $x_{9}$ to $\mathrm{Finmap\_\_erase\_erase}$, $s$ and $\mathrm{s'}$.

Finmap.singletondefMathlib.Data.Finmap, function or constant

Wording

the singleton map 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 map of $a$ and $b$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$ defined as $\operatorname{toFinmap}$ applied to the singleton association list of $a$ and $b$.

Finmap.uniondefMathlib.Data.Finmap, function or constant

Wording

the union of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Finmap}$ applied to $x_{1}$. Then the union of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$.

List.toFinmapdefMathlib.Data.Finmap, function or constant

Wording

no wording

English

Let $s$ be a list of elements of $\Sigma$ applied to $x_{1}$. Then $\operatorname{toFinmap}$ applied to $s$ is an element of $\mathrm{Finmap}$ applied to $x_{1}$ defined as $\operatorname{toFinmap}$ applied to the list of $s$.

Multiset.NodupKeysdefMathlib.Data.Finmap, predicate

Wording

no wording

English

Let $s$ be a multiset of $\Sigma$ applied to $x_{1}$. Then we can say that $\operatorname{NodupKeys}$ holds for $s$.

Multiset.keysdefMathlib.Data.Finmap, function or constant

Wording

the key of s (from the name)

English

Let $s$ be a multiset of $\Sigma$ applied to $x_{1}$. Then the key of $s$ is a multiset of $x$ defined as the map of $\operatorname{fst}$ and $s$.

Mathlib.Data.Finset.Attach

Finset.attachdefMathlib.Data.Finset.Attach, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{attach}$ applied to $s$ is a finite set of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$.

Mathlib.Data.Finset.Basic

Equiv.Finset.disjUnionEquivdefMathlib.Data.Finset.Basic, function or constant

Wording

no wording

English

Let $s$ and $t$ be finite sets of $x$ such that $s$ is disjoint to $t$. Then $\operatorname{disjUnionEquiv}$ applied to $s$, $t$ and $h$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}, \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})})}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{disjUnion} (s , t , h)}{x_{4}})})}$.

Equiv.Finset.uniondefMathlib.Data.Finset.Basic, function or constant

Wording

the union of s and t (from the name)

English

Let $s$ and $t$ be finite sets of $x$ such that $s$ is disjoint to $t$. Then the union of $s$ and $t$ is an element of $\EquivMACRoAE {\mathrm{Sum} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}, \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})})}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {(\UnionunionMACRoAB {s}{t})}{x_{4}})})}$.

Equiv.piFinsetUniondefMathlib.Data.Finset.Basic, function or constant

Wording

the product finite set union of x2 and h (from the name)

English

Let $x_{2}$ be a function from elements of $x$ to sets. Assume that $s$ is disjoint to $t$. Then the product finite set union of $x_{2}$ and $h$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Elem} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})})\rightarrow x_{2} (i), \mathrm{Elem} (\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {t}{x_{4}})})\rightarrow x_{2} (i_{1}))}{(\mathrm{Elem} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(\UnionunionMACRoAB {s}{t})}{x_{5}})})\rightarrow x_{2} (i_{2}))}$ defined as the composition of the inverse of the sum product equivalence product product of the function that maps $b$ to $x_{2}$ applied to $\operatorname{union}$ applied to $s$, $t$, $h$ and $b$ and the left product congruence of the function that maps $i$ to $x_{2}$ applied to $i$ and the union of $s$ and $t$.

Finset.choosedefMathlib.Data.Finset.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a finite set of $x$ such that $\mathrm{ExistsUnique}$ holds for the function that maps $a$ to the proposition 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}$.

Finset.chooseXdefMathlib.Data.Finset.Basic, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Let $l$ be a finite set of $x$ such that $\mathrm{ExistsUnique}$ holds for the function that maps $a_{1}$ to the proposition that $a_{1}$ is an element of $l$ and $p$ holds for $a_{1}$. Then $\operatorname{chooseX}$ applied to $p$, $l$ and $\mathrm{hp}$ is an element of $\SubtypeSet {a}{\mathrm{and} (\MembershipmemMACRoT {l}{a}, p (a))}$ defined as $\operatorname{chooseX}$ applied to $p$, the value of $l$ and $\mathrm{hp}$.

Finset.equivToSetdefMathlib.Data.Finset.Basic, function or constant

Wording

the equivalence to set of s (from the name)

English

Let $s$ be a finite set of $x$. Then the equivalence to set of $s$ is an equivalence from $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ to the set of elements of $s$.

Mathlib.Data.Finset.Card

Finset.carddefMathlib.Data.Finset.Card, function or constant

Wording

the cardinality of s (by hand)

English

Let $s$ be a finite set of $x$. Then the cardinality of $s$ is a natural number defined as the cardinality of the value of $s$.

Finset.strongDownwardInductiondefMathlib.Data.Finset.Card, function or constant

Wording

the strong downward induction of H and x1 (from the name)

English

Let $H$ be a function from finite sets $x_{1}$ of $x$ and functions from finite sets $x_{3}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\FinsetcardMACRoM {x_{3}}, n)$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{1} , x_{3})$ to elements of $p$ applied to $x_{3}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\FinsetcardMACRoM {x_{1}}, n)$ to elements of $p$ applied to $x_{1}$. Let $s$ be a finite set of $x$ such that $\FinsetcardMACRoM {s}\leq n$. Then the strong downward induction of $x_{1}$ and $H$ is an element of $p$ applied to $s$.

Finset.strongDownwardInductionOndefMathlib.Data.Finset.Card, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $H$ be a function from finite sets $x_{1}$ of $x$ and functions from finite sets $x_{3}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\FinsetcardMACRoM {x_{3}}, n)$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{1} , x_{3})$ to elements of $p$ applied to $x_{3}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\FinsetcardMACRoM {x_{1}}, n)$ to elements of $p$ applied to $x_{1}$. Assume that $\FinsetcardMACRoM {s}\leq n$. Then $\operatorname{strongDownwardInductionOn}$ applied to $s$, $x_{1}$, $H$ and $h$ is an element of $p$ applied to $s$ defined as the function that maps $h$ to the strong downward induction of $x_{1}$ and $s$.

Finset.strongInductiondefMathlib.Data.Finset.Card, function or constant

Wording

the strong induction of H and s1 (from the name)

English

Let $H$ be a function from finite sets $s_{1}$ of $x$ and functions from finite sets $t$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (t , s_{1})$ to elements of $p$ applied to $t$ to elements of $p$ applied to $s_{1}$. Let $s$ be a finite set of $x$. Then the strong induction of $s_{1}$ and $H$ is an element of $p$ applied to $s$.

Finset.strongInductionOndefMathlib.Data.Finset.Card, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $x_{1}$ be a function from finite sets $s_{1}$ of $x$ and functions from finite sets $t$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (t , s_{1})$ to elements of $p$ applied to $t$ to elements of $p$ applied to $s_{1}$. Then $\operatorname{strongInductionOn}$ applied to $s$, $s_{1}$ and $x_{1}$ is an element of $p$ applied to $s$ defined as the function that maps $x_{1}$ to the strong induction of $s_{1}$ and $s$.

Mathlib.Data.Finset.Dedup

Finset.toListdefMathlib.Data.Finset.Dedup, function or constant

Wording

the list of s (from the name)

English

Let $s$ be a finite set of $x$. Then the list of $s$ is a list of elements of $x$ defined as the list of the value of $s$.

List.toFinsetdefMathlib.Data.Finset.Dedup, function or constant

Wording

the finite set of l (from the name)

English

Let $l$ be a list of elements of $x$. Then the finite set of $l$ is a finite set of $x$ defined as the finite set of the multiset of $l$.

Multiset.toFinsetdefMathlib.Data.Finset.Dedup, function or constant

Wording

the finite set of s (from the name)

English

Let $s$ be a multiset of $x$. Then the finite set of $s$ is a finite set of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{dedup}$ applied to $s$ and $\mathrm{Multiset\_\_nodup\_dedup}$ applied to $s$.

Mathlib.Data.Finset.Defs

FinsetstructureMathlib.Data.Finset.Defs, type

Wording

finite set of x (by hand)

English

Let $x$ be a set. Then the finite sets of $x$ are a basic type.

Finset.coeEmbdefMathlib.Data.Finset.Defs, function or constant

Wording

the coercion embedding (from the name)

English

The coercion embedding is an order embedding of the set of finite sets of $x$ and $\wp x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{instSetLike}$ and $\mathrm{Finset\_\_coe\_injective}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Finset\_\_coe\_subset}$.

Finset.valdefMathlib.Data.Finset.Defs, function or constant

Wording

the value of self (from the name)

English

Let $\mathrm{self}$ be a finite set of $x$. Then the value of $\mathrm{self}$ is a multiset of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Data.Finset.Density

Finset.densdefMathlib.Data.Finset.Density, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{dens}$ applied to $s$ is a nonnegative rational number defined as the quotient of the cardinality of $s$ and the cardinality of $x$.

Mathlib.Data.Finset.Disjoint

Finset.disjUniondefMathlib.Data.Finset.Disjoint, function or constant

Wording

no wording

English

Let $s$ and $t$ be finite sets of $x$ such that $s$ is disjoint to $t$. Then $\operatorname{disjUnion}$ applied to $s$, $t$ and $h$ is a finite set of $x$.

Mathlib.Data.Finset.Empty

Finset.NonemptydefMathlib.Data.Finset.Empty, predicate

Wording

s is nonempty (from the name)

English

Let $s$ be a finite set of $x$. Then $s$ is nonempty, if there exists an element $x_{1}$ of $x$, such that $x_{1}$ is an element of $s$.

Finset.emptydefMathlib.Data.Finset.Empty, function or constant

Wording

no wording

English

$\operatorname{empty}$ is a finite set of $x$ defined as $\operatorname{mk}$ applied to $0$ and $\mathrm{Multiset\_\_nodup\_zero}$.

Mathlib.Data.Finset.Erase

Finset.erasedefMathlib.Data.Finset.Erase, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $a$ be an element of $x$. Then $\operatorname{erase}$ applied to $s$ and $a$ is a finite set of $x$.

Mathlib.Data.Finset.Filter

Finset.filterdefMathlib.Data.Finset.Filter, function or constant

Wording

the filter of p and s (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a finite set of $x$. Then $\FinsetFilter {p}{s}$ is a finite set of $x$.

Mathlib.Data.Finset.Fin

Finset.attachFindefMathlib.Data.Finset.Fin, function or constant

Wording

no wording

English

Let $s$ be a finite set of $\Natural$ such that for all natural numbers $m$, if $m$ is an element of $s$, then $m < n$. Then $\operatorname{attachFin}$ applied to $s$ and $h$ is a finite set of $\mathrm{Fin}$ applied to $n$.

Mathlib.Data.Finset.Finsupp

Finset.finsuppdefMathlib.Data.Finset.Finsupp, function or constant

Wording

the finitely supported function of s and t (from the name)

English

Let $s$ be a finite set of $x$. Let $t$ be a function from elements of $x$ to finite sets of $x_{1}$. Then the finitely supported function of $s$ and $t$ is a finite set of $\FinsuppMACRoQ {x}{x_{1}}$ defined as the map of $\operatorname{mk}$ applied to $\operatorname{indicator}$ applied to $s$ and $\mathrm{Finsupp\_\_indicator\_injective}$ applied to $s$ and the product of $s$ and $t$.

Finsupp.pidefMathlib.Data.Finset.Finsupp, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a finitely supported function from $x$ to the set of finite sets of $x_{1}$. Then the product of $f$ is a finite set of $\FinsuppMACRoQ {x}{x_{1}}$ defined as the finitely supported function of the support of $f$ and $\operatorname{coe}$ applied to $f$.

Mathlib.Data.Finset.Fold

Finset.folddefMathlib.Data.Finset.Fold, function or constant

Wording

the fold of f and s (from the name)

English

Let $\mathrm{op}$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to elements of $x_{1}$. Let $b$ be an element of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a finite set of $x$. Then the fold of $f$ and $s$ is an element of $x_{1}$ defined as the fold of $b$ and the map of $f$ and the value of $s$.

Mathlib.Data.Finset.Functor

Finset.traversedefMathlib.Data.Finset.Functor, function or constant

Wording

the traverse of f and s (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $F$ applied to $x_{1}$. Let $s$ be a finite set of $x$. Then the traverse of $f$ and $s$ is an element of $F$ applied to the set of finite sets of $x_{1}$ defined as $\operatorname{map}$ applied to $\operatorname{toFinset}$ and the traverse of $f$ and the value of $s$.

Mathlib.Data.Finset.Image

Equiv.finsetCongrdefMathlib.Data.Finset.Image, function or constant

Wording

the finite set congruence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the finite set congruence of $e$ is an equivalence from the set of finite sets of $x$ to the set of finite sets of $x_{1}$.

Equiv.finsetSubtypeCommdefMathlib.Data.Finset.Image, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $x$ to propositions. Then $\operatorname{finsetSubtypeComm}$ applied to $p$ is an equivalence from the set of finite sets of $\SubtypeSet {a}{p (a)}$ to $\SubtypeSet {s}{\mathrm{forall} (x , \lambda a_{1} . \mathrm{if} (\MembershipmemMACRoT {s}{a_{1}}, p (a_{1})))}$.

Equiv.imageFinsetdefMathlib.Data.Finset.Image, function or constant

Wording

the image finite set of e and s (from the name)

English

Let $e$ be an element of $\EquivMACRoAE {x}{x_{1}}$. Let $s$ be a finite set of $x$. Then the image finite set of $e$ and $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})})}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{image} (s , \operatorname{coe} (e))}{x_{4}})})}$.

Finset.equivMapdefMathlib.Data.Finset.Image, function or constant

Wording

the equivalence map of f and s (from the name)

English

Let $f$ be an embedding of $x$ and $x_{1}$. Let $s$ be a finite set of $x$. Then the equivalence map of $f$ and $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{map} (f , s)}{x_{3}})})}$.

Finset.equivOfEqdefMathlib.Data.Finset.Image, function or constant

Wording

the equivalence of h (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the equivalence of $h$ is an equivalence from $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {t}{x_{2}})}$.

Finset.filterMapdefMathlib.Data.Finset.Image, function or constant

Wording

the filter map of f and s (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x_{1}$. Let $s$ be a finite set of $x$. Assume that for all elements $a$ and $\mathrm{a'}$ of $x$, for all elements $b$ of $x_{1}$, if $\MembershipmemMACRoT {f (a)}{b}$, then if $\MembershipmemMACRoT {f (\mathrm{a'})}{b}$, then $\EqtMACRoH {a}{\mathrm{a'}}$. Then the filter map of $f$ and $s$ is a finite set of $x_{1}$.

Finset.imagedefMathlib.Data.Finset.Image, function or constant

Wording

the forward image of s under f (by hand)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a finite set of $x$. Then the forward image of $s$ under $f$ is a finite set of $x_{1}$ defined as the finite set of the map of $f$ and the value of $s$.

Finset.mapdefMathlib.Data.Finset.Image, function or constant

Wording

the map of f and s (from the name)

English

Let $f$ be an embedding of $x$ and $x_{1}$. Let $s$ be a finite set of $x$. Then the map of $f$ and $s$ is a finite set of $x_{1}$.

Finset.mapEmbeddingdefMathlib.Data.Finset.Image, function or constant

Wording

the map embedding of f (from the name)

English

Let $f$ be an embedding of $x$ and $x_{1}$. Then the map embedding of $f$ is an order embedding of the set of finite sets of $x$ and the set of finite sets of $x_{1}$ defined as the order embedding of $\operatorname{map}$ applied to $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Finset\_\_map\_subset\_map}$.

Finset.subtypedefMathlib.Data.Finset.Image, function or constant

Wording

the subtype of p and s (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a finite set of $x$. Then the subtype of $p$ and $s$ is a finite set of $\SubtypeSet {x_{2}}{p (x_{2})}$.

Mathlib.Data.Finset.Insert

Finset.NontrivialdefMathlib.Data.Finset.Insert, predicate

Wording

s is nontrivial (by hand)

English

Let $s$ be a finite set of $x$. Then $s$ is nontrivial, if $s$ is nontrivial.

Finset.consdefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Let $s$ be a finite set of $x$ such that $a$ is not an element of $s$. Then $\operatorname{cons}$ applied to $a$, $s$ and $h$ is a finite set of $x$.

Finset.consPiProddefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Assume that $a$ is not an element of $s$. Let $x_{1}$ be a function from elements $i_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{cons} (a , s , \mathrm{has})}{i_{1}}$ to elements of $f$ applied to $i_{1}$. Then $\operatorname{consPiProd}$ applied to $f$, $\mathrm{has}$, $i_{1}$ and $x_{1}$ is an element of $\mathrm{Prod}$ applied to $f$ applied to $a$ and the set of functions from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i}$ to elements of $f$ applied to $i$ defined as the function that maps $x_{1}$ to $\ProdmkMACRoU {i_{1} (a , \mathrm{Finset\_\_mem\_cons\_self} (a , s))}{i}{\mathrm{hi}}{i_{1} (i , \mathrm{Finset\_\_mem\_cons\_of\_mem} (\mathrm{hi}))}$.

Finset.consPiProdEquivdefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Assume that $a$ is not an element of $s$. Then $\operatorname{consPiProdEquiv}$ applied to $f$ and $\mathrm{has}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Proof} (\MembershipmemMACRoT {\operatorname{cons} (a , s , \mathrm{has})}{i})\rightarrow f (i))}{\mathrm{Prod} (f (a), \mathrm{Elem} (x)\rightarrow \mathrm{Proof} (\MembershipmemMACRoT {s}{i_{1}})\rightarrow f (i_{1}))}$.

Finset.insertPiProddefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Let $x_{2}$ be a function from elements $i_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{insert} (a , s)}{i_{1}}$ to elements of $f$ applied to $i_{1}$. Then $\operatorname{insertPiProd}$ applied to $f$, $i_{1}$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $f$ applied to $a$ and the set of functions from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i}$ to elements of $f$ applied to $i$ defined as the function that maps $x_{2}$ to $\ProdmkMACRoU {i_{1} (a , \mathrm{Finset\_\_mem\_insert\_self} (a , s))}{i}{\mathrm{hi}}{i_{1} (i , \mathrm{Finset\_\_mem\_insert\_of\_mem} (\mathrm{hi}))}$.

Finset.insertPiProdEquivdefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Assume that $a$ is not an element of $s$. Then $\operatorname{insertPiProdEquiv}$ applied to $f$ and $\mathrm{has}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Proof} (\MembershipmemMACRoT {\operatorname{insert} (a , s)}{i})\rightarrow f (i))}{\mathrm{Prod} (f (a), \mathrm{Elem} (x)\rightarrow \mathrm{Proof} (\MembershipmemMACRoT {s}{i_{1}})\rightarrow f (i_{1}))}$.

Finset.prodPiConsdefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Assume that $a$ is not an element of $s$. Let $x_{2}$ be an element of $\mathrm{Prod}$ applied to $f$ applied to $a$ and the set of functions from elements $i_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i_{1}}$ to elements of $f$ applied to $i_{1}$. Let $i$ be an element of $x$ such that $\MembershipmemMACRoT {\operatorname{cons} (a , s , \mathrm{has})}{i}$. Then $\operatorname{prodPiCons}$ applied to $f$, $\mathrm{has}$, $x_{2}$, $i$ and $h$ is an element of $f$ applied to $i$.

Finset.prodPiInsertdefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to sets. Let $x_{2}$ be an element of $\mathrm{Prod}$ applied to $f$ applied to $a$ and the set of functions from elements $i_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i_{1}}$ to elements of $f$ applied to $i_{1}$. Let $i$ be an element of $x$ such that $\MembershipmemMACRoT {\operatorname{insert} (a , s)}{i}$. Then $\operatorname{prodPiInsert}$ applied to $f$, $x_{2}$, $i$ and $h$ is an element of $f$ applied to $i$.

Finset.subtypeInsertEquivOptiondefMathlib.Data.Finset.Insert, function or constant

Wording

no wording

English

Assume that $x_{2}$ is not an element of $t$. Then $\operatorname{subtypeInsertEquivOption}$ applied to $h$ is an element of $\EquivMACRoAE {(\SubtypeSet {i}{(\MembershipmemMACRoT {\operatorname{insert} (x_{2} , t)}{i})})}{\mathrm{Option} (\SubtypeSet {i_{1}}{(\MembershipmemMACRoT {t}{i_{1}})})}$.

Mathlib.Data.Finset.Lattice.Fold

Finset.infdefMathlib.Data.Finset.Lattice.Fold, function or constant

Wording

the infimum of s and f (from the name)

English

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the infimum of $s$ and $f$ is an element of $x$ defined as the fold of $f$ and $s$.

Finset.inf'defMathlib.Data.Finset.Lattice.Fold, function or constant

Wording

the infimum of s and f (from the name)

English

Let $s$ be a nonempty finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the infimum of $s$ and $f$ is an element of $x$.

Finset.supdefMathlib.Data.Finset.Lattice.Fold, function or constant

Wording

the supremum of s and f (from the name)

English

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the supremum of $s$ and $f$ is an element of $x$ defined as the fold of $f$ and $s$.

Finset.sup'defMathlib.Data.Finset.Lattice.Fold, function or constant

Wording

the supremum of s and f (from the name)

English

Let $s$ be a nonempty finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then the supremum of $s$ and $f$ is an element of $x$.

Mathlib.Data.Finset.Max

Finset.maxdefMathlib.Data.Finset.Max, function or constant

Wording

the maximum of s (from the name)

English

Let $s$ be a finite set of $x$. Then the maximum of $s$ is an element of $\mathrm{WithBot}$ applied to $x$ defined as the supremum of $s$ and $\operatorname{some}$.

Finset.max'defMathlib.Data.Finset.Max, function or constant

Wording

the maximum of s and H (from the name)

English

Let $s$ be a nonempty finite set of $x$. Then the maximum of $s$ and $H$ is an element of $x$ defined as the supremum of $s$ and $\mathrm{id}$.

Finset.mindefMathlib.Data.Finset.Max, function or constant

Wording

the minimum of s (from the name)

English

Let $s$ be a finite set of $x$. Then the minimum of $s$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as the infimum of $s$ and $\operatorname{some}$.

Finset.min'defMathlib.Data.Finset.Max, function or constant

Wording

the minimum of s and H (from the name)

English

Let $s$ be a nonempty finite set of $x$. Then the minimum of $s$ and $H$ is an element of $x$ defined as the infimum of $s$ and $\mathrm{id}$.

Mathlib.Data.Finset.MulAntidiagonal

Finset.antidiagonaldefMathlib.Data.Finset.MulAntidiagonal, function or constant

Wording

no wording

English

Assume that $\operatorname{IsPWO}$ holds for $s$. Assume that $\operatorname{IsPWO}$ holds for $t$. Let $a$ be an element of $x$. Then $\operatorname{antidiagonal}$ applied to $\mathrm{hs}$, $\mathrm{ht}$ and $a$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x$.

Finset.mulAntidiagonaldefMathlib.Data.Finset.MulAntidiagonal, function or constant

Wording

no wording

English

Assume that $\operatorname{IsPWO}$ holds for $s$. Assume that $\operatorname{IsPWO}$ holds for $t$. Let $a$ be an element of $x$. Then $\operatorname{mulAntidiagonal}$ applied to $\mathrm{hs}$, $\mathrm{ht}$ and $a$ is a finite set of $\mathrm{Prod}$ applied to $x$ and $x$.

Mathlib.Data.Finset.NAry

Finset.image₂defMathlib.Data.Finset.NAry, function or constant

Wording

the image of s and t (from the name)

English

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $s$ be a finite set of $x$. Let $t$ be a finite set of $x_{1}$. Then the image of $s$ and $t$ is a finite set of $x_{2}$ defined as the forward image of $\operatorname{sprod}$ applied to $s$ and $t$ under $\operatorname{uncurry}$ applied to $f$.

Mathlib.Data.Finset.NatAntidiagonal

Finset.Nat.antidiagonalEquivFindefMathlib.Data.Finset.NatAntidiagonal, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{antidiagonalEquivFin}$ applied to $n$ is an element of $\EquivMACRoAE {(\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{antidiagonal} (n)}{x})})}{\mathrm{Fin} (n + 1)}$.

Mathlib.Data.Finset.NatDivisors

Nat.divisorsHomdefMathlib.Data.Finset.NatDivisors, function or constant

Wording

the divisor homomorphism (from the name)

English

The divisor homomorphism is a monoid homomorphism of $\Natural$ and the set of finite sets of $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{divisors}$ and $\mathrm{Nat\_\_divisors\_one}$ and $\mathrm{Nat\_\_divisors\_mul}$.

Mathlib.Data.Finset.NoncommProd

Finset.noncommProddefMathlib.Data.Finset.NoncommProd, function or constant

Wording

the noncommutative product of s and f (from the name)

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{Pairwise}$ holds for $s$ and $\operatorname{onFun}$ applied to $\mathrm{Commute}$ and $f$. Then the noncommutative product of $s$ and $f$ is an element of $x_{1}$ defined as the noncommutative product of the map of $f$ and the value of $s$ and $\mathrm{Finset\_\_noncommProd\_lemma}$ applied to $s$, $f$ and $\mathrm{comm}$.

Finset.noncommSumdefMathlib.Data.Finset.NoncommProd, function or constant

Wording

the noncommutative sum of s and f (from the name)

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{Pairwise}$ holds for $s$ and $\operatorname{onFun}$ applied to $\mathrm{AddCommute}$ and $f$. Then the noncommutative sum of $s$ and $f$ is an element of $x_{1}$ defined as the noncommutative sum of the map of $f$ and the value of $s$ and $\mathrm{Finset\_\_noncommSum\_lemma}$ applied to $s$, $f$ and $\mathrm{comm}$.

Multiset.noncommFolddefMathlib.Data.Finset.NoncommProd, function or constant

Wording

the noncommutative fold of s and x1 (from the name)

English

Let $\mathrm{op}$ be a function from elements of $x$ and elements of $x$ to elements of $x$. Let $s$ be a multiset of $x$ such that $\operatorname{Pairwise}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and the function that maps $x_{3}$ and $y$ to $\EqtMACRoH {\mathrm{op} (x_{3} , y)}{\mathrm{op} (y , x_{3})}$. Let $x_{1}$ be an element of $x$. Then the noncommutative fold of $s$ and $x_{1}$ is an element of $x$.

Multiset.noncommFoldrdefMathlib.Data.Finset.NoncommProd, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $s$ be a multiset of $x$ such that $\operatorname{Pairwise}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and the function that maps $x_{3}$ and $y$ to the proposition that for all elements $b_{1}$ of $x_{1}$, $\EqtMACRoH {f (x_{3} , f (y , b_{1}))}{f (y , f (x_{3} , b_{1}))}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{noncommFoldr}$ applied to $f$, $s$, $\mathrm{comm}$ and $b$ is an element of $x_{1}$ defined as $\operatorname{foldr}$ applied to $\operatorname{comp}$ applied to $f$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$, $b$ and $\operatorname{attach}$ applied to $s$.

Multiset.noncommProddefMathlib.Data.Finset.NoncommProd, function or constant

Wording

the noncommutative product of s and comm (from the name)

English

Let $s$ be a multiset of $x$ such that $\operatorname{Pairwise}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\mathrm{Commute}$. Then the noncommutative product of $s$ and $\mathrm{comm}$ is an element of $x$ defined as the noncommutative fold of $s$ and $1$.

Multiset.noncommSumdefMathlib.Data.Finset.NoncommProd, function or constant

Wording

the noncommutative sum of s and comm (from the name)

English

Let $s$ be a multiset of $x$ such that $\operatorname{Pairwise}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\mathrm{AddCommute}$. Then the noncommutative sum of $s$ and $\mathrm{comm}$ is an element of $x$ defined as the noncommutative fold of $s$ and $0$.

Mathlib.Data.Finset.Option

Finset.eraseNonedefMathlib.Data.Finset.Option, function or constant

Wording

no wording

English

$\operatorname{eraseNone}$ is an order homomorphism of the set of finite sets of $\mathrm{Option}$ applied to $x$ and the set of finite sets of $x$.

Finset.insertNonedefMathlib.Data.Finset.Option, function or constant

Wording

no wording

English

$\operatorname{insertNone}$ is an order embedding of the set of finite sets of $x$ and the set of finite sets of $\mathrm{Option}$ applied to $x$.

Option.toFinsetdefMathlib.Data.Finset.Option, function or constant

Wording

the finite set of o (from the name)

English

Let $o$ be an element of $\mathrm{Option}$ applied to $x$. Then the finite set of $o$ is a finite set of $x$ defined as $\operatorname{elim}$ applied to $o$, $\operatorname{emptyCollection}$ and $\operatorname{singleton}$.

Mathlib.Data.Finset.PImage

Finset.pimagedefMathlib.Data.Finset.PImage, function or constant

Wording

no wording

English

Let $f$ be a function of $x$ and $x_{1}$. Let $s$ be a finite set of $x$. Then $\operatorname{pimage}$ applied to $f$ and $s$ is a finite set of $x_{1}$ defined as $\operatorname{biUnion}$ applied to $s$ and the function that maps $x_{4}$ to the finite set of $f$ applied to $x_{4}$.

Part.toFinsetdefMathlib.Data.Finset.PImage, function or constant

Wording

the finite set of o (from the name)

English

Let $o$ be a part of $x$. Then the finite set of $o$ is a finite set of $x$ defined as the finite set of the option of $o$.

Mathlib.Data.Finset.Pi

Finset.Pi.consdefMathlib.Data.Finset.Pi, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $a$ and $\mathrm{a'}$ be elements of $x$. Let $b$ be an element of $x_{1}$ applied to $a$. Let $f$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{a_{1}}$ to elements of $x_{1}$ applied to $a_{1}$. Assume that $\MembershipmemMACRoT {\operatorname{insert} (a , s)}{\mathrm{a'}}$. Then $\operatorname{cons}$ applied to $s$, $a$, $b$, $a_{1}$, $f$, $\mathrm{a'}$ and $h$ is an element of $x_{1}$ applied to $\mathrm{a'}$.

Finset.Pi.emptydefMathlib.Data.Finset.Pi, function or constant

Wording

no wording

English

Let $x_{1}$ be a function from elements of $x$ to sets. Let $a$ be an element of $x$ such that $a$ is an element of $\operatorname{emptyCollection}$. Then $\operatorname{empty}$ applied to $x_{1}$, $a$ and $h$ is an element of $x_{1}$ applied to $a$ defined as $\operatorname{empty}$ applied to $x_{1}$, $a$ and $h$.

Finset.pidefMathlib.Data.Finset.Pi, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be a finite set of $x$. Let $t$ be a function from elements $a_{1}$ of $x$ to finite sets of $x_{1}$ applied to $a_{1}$. Then the product of $s$ and $a_{1}$ is a finite set of the set of functions from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{a}$ to elements of $x_{1}$ applied to $a$.

Finset.piDiagdefMathlib.Data.Finset.Pi, function or constant

Wording

the diagonal of s and x1 (from the docstring)

English

Let $s$ be a finite set of $x$. Let $x_{1}$ be a set. Then the diagonal of $s$ and $x_{1}$ is a finite set of the set of functions from elements of $x_{1}$ to elements of $x$ defined as the forward image of $s$ under $\operatorname{const}$ applied to $x_{1}$.

Finset.restrictdefMathlib.Data.Finset.Pi, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$. Then $\operatorname{restrict}$ applied to $s$, $i_{1}$, $f$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $i$ to $i_{1}$ applied to $f$ and $i$.

Finset.restrict₂defMathlib.Data.Finset.Pi, function or constant

Wording

no wording

English

Assume that $s \leq t$. Let $f$ be a function from elements $i_{1}$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})}$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$. Then $\mathrm{Finset\_\_restrict\_u2082\_}$ applied to $\mathrm{hst}$, $i_{1}$, $f$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $i$ to $i_{1}$ applied to $f$ and $i$.

Mathlib.Data.Finset.Piecewise

Finset.piecewisedefMathlib.Data.Finset.Piecewise, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Let $f$ be a function from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$. Let $g$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then $\operatorname{piecewise}$ applied to $s$, $i_{2}$, $f$, $i_{1}$, $g$ and $i$ is an element of $x_{1}$ applied to $i$ defined as the function that maps $g$ and $i$ to $\iteMACRoG {(\MembershipmemMACRoT {s}{i_{1}})}{i_{2} (i_{1})}{f (i_{1})}$.

Mathlib.Data.Finset.Powerset

Finset.powersetdefMathlib.Data.Finset.Powerset, function or constant

Wording

the powerset of s (from the name)

English

Let $s$ be a finite set of $x$. Then the powerset of $s$ is a finite set of the set of finite sets of $x$.

Finset.powersetCarddefMathlib.Data.Finset.Powerset, function or constant

Wording

the powerset cardinality of n and s (from the name)

English

Let $n$ be a natural number. Let $s$ be a finite set of $x$. Then the powerset cardinality of $n$ and $s$ is a finite set of the set of finite sets of $x$.

Finset.ssubsetsdefMathlib.Data.Finset.Powerset, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{ssubsets}$ applied to $s$ is a finite set of the set of finite sets of $x$ defined as $\operatorname{erase}$ applied to the powerset of $s$ and $s$.

Mathlib.Data.Finset.Preimage

Equiv.restrictPreimageFinsetdefMathlib.Data.Finset.Preimage, function or constant

Wording

no wording

English

Let $e$ be an element of $\EquivMACRoAE {x}{x_{1}}$. Let $s$ be a finite set of $x_{1}$. Then $\operatorname{restrictPreimageFinset}$ applied to $e$ and $s$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{preimage} (s , \operatorname{coe} (e))}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})})}$.

Finset.preimagedefMathlib.Data.Finset.Preimage, function or constant

Wording

the preimage of s and f (from the name)

English

Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is injective on the preimage of $f$ and $s$. Then the preimage of $s$ and $f$ is a finite set of $x$.