Definitions: Mathlib.Analysis, part 1 of 5

AbsoluteValue.IsEquivdefMathlib.Analysis.AbsoluteValue.Equivalence, predicate

Wording

no wording

English

Let $v$ and $w$ be absolute values of $R$ and $S$. Then $\operatorname{IsEquiv}$ holds for $v$ and $w$, if for all elements $x_{3}$ and $y$ of $R$, $v (x_{3})\leq v (y)$, if and only if $w (x_{3})\leq w (y)$.

Mathlib.Analysis.Analytic.Basic

AnalyticAtdefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{6}$ be an element of $E$. Then $\mathrm{AnalyticAt}$ holds for $x$, $f$ and $x_{6}$, if there exists a formal multilinear series $p$ of $E$ and $F$, such that $\mathrm{HasFPowerSeriesAt}$ holds for $f$, $p$ and $x_{6}$.

AnalyticOndefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Then $\mathrm{AnalyticOn}$ holds for $x$, $f$ and $s$, if for all elements $x_{6}$ of $E$, if $x_{6}$ is an element of $s$, then $\mathrm{AnalyticWithinAt}$ holds for $x$, $f$, $s$ and $x_{6}$.

AnalyticOnNhddefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Then $\mathrm{AnalyticOnNhd}$ holds for $x$, $f$ and $s$, if for all elements $x_{6}$ of $E$, if $x_{6}$ is an element of $s$, then $\mathrm{AnalyticAt}$ holds for $x$, $f$ and $x_{6}$.

AnalyticWithinAtdefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Let $x_{6}$ be an element of $E$. Then $\mathrm{AnalyticWithinAt}$ holds for $x$, $f$, $s$ and $x_{6}$, if there exists a formal multilinear series $p$ of $E$ and $F$, such that $\mathrm{HasFPowerSeriesWithinAt}$ holds for $f$, $p$, $s$ and $x_{6}$.

HasFPowerSeriesAtdefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{6}$ be an element of $E$. Then $\mathrm{HasFPowerSeriesAt}$ holds for $f$, $p$ and $x_{6}$, if there exists an element $r$ of $\mathrm{ENNReal}$, such that $\mathrm{HasFPowerSeriesOnBall}$ holds for $f$, $p$, $x_{6}$ and $r$.

HasFPowerSeriesOnBallstructureMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{6}$ be an element of $E$. Let $r$ be an element of $\mathrm{ENNReal}$. Then we can say that $\mathrm{HasFPowerSeriesOnBall}$ holds for $f$, $p$, $x_{6}$ and $r$.

HasFPowerSeriesWithinAtdefMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $s$ be an element of $\wp E$. Let $x_{6}$ be an element of $E$. Then $\mathrm{HasFPowerSeriesWithinAt}$ holds for $f$, $p$, $s$ and $x_{6}$, if there exists an element $r$ of $\mathrm{ENNReal}$, such that $\mathrm{HasFPowerSeriesWithinOnBall}$ holds for $f$, $p$, $s$, $x_{6}$ and $r$.

HasFPowerSeriesWithinOnBallstructureMathlib.Analysis.Analytic.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $s$ be an element of $\wp E$. Let $x_{6}$ be an element of $E$. Let $r$ be an element of $\mathrm{ENNReal}$. Then we can say that $\mathrm{HasFPowerSeriesWithinOnBall}$ holds for $f$, $p$, $s$, $x_{6}$ and $r$.

Mathlib.Analysis.Analytic.Binomial

binomialSeriesdefMathlib.Analysis.Analytic.Binomial, function or constant

Wording

the binomial series of x2 and a (from the name)

English

Let $x_{2}$ be a set. Let $a$ be an element of $x$. Then the binomial series of $x_{2}$ and $a$ is a formal multilinear series of $x_{2}$ and $x_{2}$ defined as the formal multilinear series of $x_{2}$ and the function that maps $x_{6}$ to $\operatorname{choose}$ applied to $a$ and $x_{6}$.

Mathlib.Analysis.Analytic.CPolynomial

ContinuousLinearMap.toFormalMultilinearSeriesOfMultilineardefMathlib.Analysis.Analytic.CPolynomial, function or constant

Wording

the formal multilinear series of f (from the name)

English

Let $f$ be a continuous linear map of $G$ and the set of continuous multilinear maps of $\mathrm{Em}$ and $F$. Then the formal multilinear series of $f$ is a formal multilinear series of $\mathrm{Prod}$ applied to $G$ and the set of functions from elements $i$ of $x_{6}$ to elements of $\mathrm{Em}$ applied to $i$ and $F$ defined as the function that maps $n$ to $\mathrm{dite}$ applied to the proposition that the cardinality of $\mathrm{Option}$ applied to $x_{6}$ is equal to $n$, the function that maps $h$ to the domain domain congruence of $\operatorname{equivFinOfCardEq}$ applied to $h$ and the continuous multilinear map option of $f$ and the function that maps $h_{1}$ to $0$.

Mathlib.Analysis.Analytic.CPolynomialDef

CPolynomialAtdefMathlib.Analysis.Analytic.CPolynomialDef, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{6}$ be an element of $E$. Then $\mathrm{CPolynomialAt}$ holds for $x$, $f$ and $x_{6}$, if there exists a formal multilinear series $p$ of $E$ and $F$, such that there exists a natural number $n$, such that $\mathrm{HasFiniteFPowerSeriesAt}$ holds for $f$, $p$, $x_{6}$ and $n$.

CPolynomialOndefMathlib.Analysis.Analytic.CPolynomialDef, predicate

Wording

no wording

English

Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Then $\mathrm{CPolynomialOn}$ holds for $x$, $f$ and $s$, if for all elements $x_{6}$ of $E$, if $x_{6}$ is an element of $s$, then $\mathrm{CPolynomialAt}$ holds for $x$, $f$ and $x_{6}$.

HasFiniteFPowerSeriesAtdefMathlib.Analysis.Analytic.CPolynomialDef, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{6}$ be an element of $E$. Let $n$ be a natural number. Then $\mathrm{HasFiniteFPowerSeriesAt}$ holds for $f$, $p$, $x_{6}$ and $n$, if there exists an element $r$ of $\mathrm{ENNReal}$, such that $\mathrm{HasFiniteFPowerSeriesOnBall}$ holds for $f$, $p$, $x_{6}$, $n$ and $r$.

HasFiniteFPowerSeriesOnBallstructureMathlib.Analysis.Analytic.CPolynomialDef, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $F$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{6}$ be an element of $E$. Let $n$ be a natural number. Let $r$ be an element of $\mathrm{ENNReal}$. Then we can say that $\mathrm{HasFiniteFPowerSeriesOnBall}$ holds for $f$, $p$, $x_{6}$, $n$ and $r$.

Mathlib.Analysis.Analytic.ChangeOrigin

FormalMultilinearSeries.changeOrigindefMathlib.Analysis.Analytic.ChangeOrigin, function or constant

Wording

the change origin of p and x6 (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{6}$ be an element of $E$. Then the change origin of $p$ and $x_{6}$ is a formal multilinear series of $E$ and $F$ defined as the function that maps $k$ to the sum of the change origin series of $p$ and $k$ and $x_{6}$.

FormalMultilinearSeries.changeOriginSeriesdefMathlib.Analysis.Analytic.ChangeOrigin, function or constant

Wording

the change origin series of p and k (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $k$ be a natural number. Then the change origin series of $p$ and $k$ is a formal multilinear series of $E$ and the set of continuous multilinear maps of the function that maps $x_{6}$ to $E$ and $F$.

FormalMultilinearSeries.changeOriginSeriesTermdefMathlib.Analysis.Analytic.ChangeOrigin, function or constant

Wording

the change origin series term of l and s (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $k$ and $l$ be natural numbers. Let $s$ be a finite set of $\mathrm{Fin}$ applied to $k + l$ such that $\FinsetcardMACRoM {s}= l$. Then the change origin series term of $l$ and $s$ is a continuous multilinear map of the function that maps $x_{6}$ to $E$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $E$ and $F$.

FormalMultilinearSeries.derivSeriesdefMathlib.Analysis.Analytic.ChangeOrigin, function or constant

Wording

the derivative series of p (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Then the derivative series of $p$ is a formal multilinear series of $E$ and the set of continuous linear maps of $E$ and $F$ defined as the composition formal multilinear series of the continuous linear map of the continuous linear equivalence of $\mathrm{continuousMultilinearCurryFin1}$ applied to $x$, $E$ and $F$ and the change origin series of $p$ and $1$.

Mathlib.Analysis.Analytic.Composition

Composition.gatherdefMathlib.Analysis.Analytic.Composition, function or constant

Wording

no wording

English

Let $a$ be a composition of $n$. Let $b$ be a composition of the length of $a$. Then $\operatorname{gather}$ applied to $a$ and $b$ is a composition of $n$.

Composition.sigmaEquivSigmaPidefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the sigma equivalence sigma product of n (from the name)

English

Let $n$ be a natural number. Then the sigma equivalence sigma product of $n$ is an equivalence from $\Sigma$ applied to the function that maps $a$ to the set of compositions of the length of $a$ to $\Sigma$ applied to the function that maps $c$ to the set of functions from elements $i$ of $\mathrm{Fin}$ applied to the length of $c$ to compositions of the block function of $c$ and $i$.

ContinuousMultilinearMap.compAlongCompositiondefMathlib.Analysis.Analytic.Composition, function or constant

Wording

no wording

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $c$ be a composition of $n$. Let $f$ be a continuous multilinear map of the function that maps $x_{12}$ to $F$ and $G$. Then $\operatorname{compAlongComposition}$ applied to $p$, $c$ and $f$ is a continuous multilinear map of the function that maps $x_{11}$ to $E$ and $G$.

FormalMultilinearSeries.applyCompositiondefMathlib.Analysis.Analytic.Composition, function or constant

Wording

no wording

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $c$ be a composition of $n$. Let $x_{8}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $E$. Let $x_{9}$ be an element of $\mathrm{Fin}$ applied to the length of $c$. Then $\operatorname{applyComposition}$ applied to $p$, $c$, $x_{8}$ and $x_{9}$ is an element of $F$ defined as $p$ applied to the block function of $c$ and $x_{9}$ and $\operatorname{comp}$ applied to $x_{8}$ and $\operatorname{coe}$ applied to the embedding of $c$ and $x_{9}$.

FormalMultilinearSeries.compdefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the composition of q and p (from the name)

English

Let $q$ be a formal multilinear series of $F$ and $G$. Let $p$ be a formal multilinear series of $E$ and $F$. Then the composition of $q$ and $p$ is a formal multilinear series of $E$ and $G$ defined as the function that maps $n$ to $\FinsetSum {\FinsetunivMACRoAC}{c}{\operatorname{compAlongComposition} (q , p , c)}$.

FormalMultilinearSeries.compAlongCompositiondefMathlib.Analysis.Analytic.Composition, function or constant

Wording

no wording

English

Let $q$ be a formal multilinear series of $F$ and $G$. Let $p$ be a formal multilinear series of $E$ and $F$. Let $c$ be a composition of $n$. Then $\operatorname{compAlongComposition}$ applied to $q$, $p$ and $c$ is a continuous multilinear map of the function that maps $x_{11}$ to $E$ and $G$ defined as $\operatorname{compAlongComposition}$ applied to $p$, $c$ and $q$ applied to the length of $c$.

FormalMultilinearSeries.compChangeOfVariablesdefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the composition change of N and i (from the name)

English

Let $m$, $M$ and $N$ be natural numbers. Let $i$ be an element of $\Sigma$ applied to the function that maps $n_{1}$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n_{1}$ to natural numbers such that $i$ is an element of the composition partial sum source of $M$ and $N$. Then the composition change of $N$ and $i$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of compositions of $n$.

FormalMultilinearSeries.compPartialSumSourcedefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the composition partial sum source of M and N (from the name)

English

Let $m$, $M$ and $N$ be natural numbers. Then the composition partial sum source of $M$ and $N$ is a finite set of $\Sigma$ applied to the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to natural numbers defined as the sigma of $\FinsetIcoMACRoO {m}{M}$ and the function that maps $n$ to the product finite set of the function that maps $\mathrm{\_i}$ to $\FinsetIcoMACRoO {1}{N}$.

FormalMultilinearSeries.compPartialSumTargetdefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the composition partial sum target of M and N (from the name)

English

Let $m$, $M$ and $N$ be natural numbers. Then the composition partial sum target of $M$ and $N$ is a finite set of $\Sigma$ applied to the function that maps $n$ to the set of compositions of $n$.

FormalMultilinearSeries.compPartialSumTargetSetdefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the composition partial sum target set of M and N (from the name)

English

Let $m$, $M$ and $N$ be natural numbers. Then the composition partial sum target set of $M$ and $N$ is an element of the power set of $\Sigma$ applied to the function that maps $n$ to the set of compositions of $n$ defined as $\operatorname{ofPred}$ applied to the function that maps $i$ to the proposition that $m$ is less than or equal to the length of $\operatorname{snd}$ applied to $i$, the length of $\operatorname{snd}$ applied to $i$ is less than $M$ and for all elements $j$ of $\mathrm{Fin}$ applied to the length of $\operatorname{snd}$ applied to $i$, the block function of $\operatorname{snd}$ applied to $i$ and $j$ is less than $N$.

FormalMultilinearSeries.iddefMathlib.Analysis.Analytic.Composition, function or constant

Wording

the identity of x4 (from the name)

English

Let $x$ and $E$ be sets. Let $x_{4}$ be an element of $E$. Then the identity of $x_{4}$ is a formal multilinear series of $E$ and $E$.

Mathlib.Analysis.Analytic.Constructions

alternatingGeometricSeriesdefMathlib.Analysis.Analytic.Constructions, function or constant

Wording

the alternating geometric series of x and A (from the docstring)

English

Let $x$ and $A$ be sets. Then the alternating geometric series of $x$ and $A$ is a formal multilinear series of $A$ and $A$ defined as the formal multilinear series of $A$ and the function that maps $n$ to $\operatorname{neg} (1)^ {n}$.

formalMultilinearSeries_geometricdefMathlib.Analysis.Analytic.Constructions, function or constant

Wording

the geometric series of x and A (from the docstring)

English

Let $x$ and $A$ be sets. Then the geometric series of $x$ and $A$ is a formal multilinear series of $A$ and $A$ defined as the function that maps $n$ to $\operatorname{mkPiAlgebraFin}$ applied to $x$, $n$ and $A$.

Mathlib.Analysis.Analytic.ConvergenceRadius

FormalMultilinearSeries.partialSumdefMathlib.Analysis.Analytic.ConvergenceRadius, function or constant

Wording

the partial sum of n and x8 (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $n$ be a natural number. Let $x_{8}$ be an element of $E$. Then the partial sum of $n$ and $x_{8}$ is an element of $F$ defined as $\FinsetSum {\FinsetrangeMACRoN {n}}{k}{p (k , \lambda x_{9} . x_{8})}$.

FormalMultilinearSeries.radiusdefMathlib.Analysis.Analytic.ConvergenceRadius, function or constant

Wording

the radius of p (from the docstring)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Then the radius of $p$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $r$ to the supremum of the function that maps $C$ to the supremum of the function that maps $h$ to $\operatorname{ofNNReal}$ applied to $r$.

FormalMultilinearSeries.sumdefMathlib.Analysis.Analytic.ConvergenceRadius, function or constant

Wording

the sum of p and x8 (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $x_{8}$ be an element of $E$. Then the sum of $p$ and $x_{8}$ is an element of $F$ defined as the sum of the function that maps $n$ to $p$ applied to $n$ and the function that maps $x_{9}$ to $x_{8}$ and $\operatorname{unconditional}$ applied to $\Natural$.

Mathlib.Analysis.Analytic.Inverse

FormalMultilinearSeries.leftInvdefMathlib.Analysis.Analytic.Inverse, function or constant

Wording

the left inverse of i and x6 (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $i$ be a continuous linear equivalence of $E$ and $F$. Let $x_{6}$ be an element of $E$. Then the left inverse of $i$ and $x_{6}$ is a formal multilinear series of $F$ and $E$.

FormalMultilinearSeries.rightInvdefMathlib.Analysis.Analytic.Inverse, function or constant

Wording

the right inverse of i and x6 (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $i$ be a continuous linear equivalence of $E$ and $F$. Let $x_{6}$ be an element of $E$. Then the right inverse of $i$ and $x_{6}$ is a formal multilinear series of $F$ and $E$.

Mathlib.Analysis.Analytic.IteratedFDeriv

FormalMultilinearSeries.iteratedFDerivSeriesdefMathlib.Analysis.Analytic.IteratedFDeriv, function or constant

Wording

the iterated derivative series of p and k (from the name)

English

Let $p$ be a formal multilinear series of $E$ and $F$. Let $k$ be a natural number. Then the iterated derivative series of $p$ and $k$ is a formal multilinear series of $E$ and the set of continuous multilinear maps of the function that maps $x_{6}$ to $E$ and $F$ defined as $\operatorname{brecOn}$ applied to $k$ and $\mathrm{FormalMultilinearSeries\_\_iteratedFDerivSeries\_\_\_f}$ applied to $p$.

Mathlib.Analysis.Analytic.Linear

ContinuousLinearMap.fpowerSeriesBilineardefMathlib.Analysis.Analytic.Linear, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Let $x_{8}$ be an element of $\mathrm{Prod}$ applied to $E$ and $F$. Then there is a formal multilinear series of $\mathrm{Prod}$ applied to $E$ and $F$ and $G$.

ContinuousLinearMap.uncurryBilineardefMathlib.Analysis.Analytic.Linear, function or constant

Wording

the uncurrying bilinear of f (from the name)

English

Let $f$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the uncurrying bilinear of $f$ is a continuous multilinear map of the function that maps $x_{8}$ to $\mathrm{Prod}$ applied to $E$ and $F$ and $G$ defined as $\operatorname{uncurryLeft}$ applied to the composition of the continuous linear map of the continuous linear equivalence of the inverse of $\mathrm{continuousMultilinearCurryFin1}$ applied to $x$, $\mathrm{Prod}$ applied to $E$ and $F$ and $G$ and the bilinear composition of the first component of $E$ and $F$ and the second component of $E$ and $F$.

Mathlib.Analysis.Analytic.OfScalars

FormalMultilinearSeries.ofScalarsdefMathlib.Analysis.Analytic.OfScalars, function or constant

Wording

the formal multilinear series of E and c (from the name)

English

Let $E$ be a set. Let $c$ be a function from natural numbers to elements of $x$. Then the formal multilinear series of $E$ and $c$ is a formal multilinear series of $E$ and $E$ defined as the function that maps $n$ to $\HSMulhSMulMACRoAL {c (n)}{\operatorname{mkPiAlgebraFin} (x , n , E)}$.

FormalMultilinearSeries.ofScalarsSubmoduledefMathlib.Analysis.Analytic.OfScalars, function or constant

Wording

the formal multilinear series of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the formal multilinear series of $x$ and $E$ is a submodule of $x$ and the set of formal multilinear series of $E$ and $E$.

FormalMultilinearSeries.ofScalarsSumdefMathlib.Analysis.Analytic.OfScalars, function or constant

Wording

the sum of the formal power series of c and x5 (from the docstring)

English

Let $c$ be a function from natural numbers to elements of $x$. Let $x_{5}$ be an element of $E$. Then the sum of the formal power series of $c$ and $x_{5}$ is an element of $E$ defined as the sum of the formal multilinear series of $E$ and $c$ and $x_{5}$.

Mathlib.Analysis.Analytic.Order

analyticOrderAtdefMathlib.Analysis.Analytic.Order, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then $\mathrm{analyticOrderAt}$ applied to $f$ and $x_{4}$ is a natural number.

analyticOrderNatAtdefMathlib.Analysis.Analytic.Order, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then $\mathrm{analyticOrderNatAt}$ applied to $f$ and $x_{4}$ is a natural number defined as the natural number of $\mathrm{analyticOrderAt}$ applied to $f$ and $x_{4}$.

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Delone.DeloneSetstructureMathlib.Analysis.AperiodicOrder.Delone.Basic, type

Wording

no wording

English

Let $X$ be a set. Then the elements of $\operatorname{DeloneSet}$ applied to $X$ are a basic type.

Delone.DeloneSet.carrierdefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

the carrier of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Then the carrier of $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Delone.DeloneSet.copydefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

the copy of packingRadius and coveringRadius (from the name)

English

Let $D$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Let $\mathrm{carrier}$ be an element of $\wp X$. Let $\mathrm{packingRadius}$ and $\mathrm{coveringRadius}$ be elements of $\mathrm{NNReal}$. Assume that $\mathrm{carrier}$ is equal to the carrier of $D$. Assume that $\EqtMACRoH {\mathrm{packingRadius}}{\operatorname{packingRadius} (D)}$. Assume that $\mathrm{coveringRadius}$ is equal to the covering radius of $D$. Then the copy of $\mathrm{packingRadius}$ and $\mathrm{coveringRadius}$ is an element of $\operatorname{DeloneSet}$ applied to $X$.

Delone.DeloneSet.coveringRadiusdefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

the covering radius of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Then the covering radius of $\mathrm{self}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Delone.DeloneSet.mapBilipschitzdefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

no wording

English

Let $f$ be an equivalence from $X$ to $Y$. Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{NNReal}$ such that $0 < x_{2}$, $0 < x_{3}$, $\mathrm{AntilipschitzWith}$ holds for $x_{2}$ and $\operatorname{coe}$ applied to $f$ and $\mathrm{LipschitzWith}$ holds for $x_{3}$ and $\operatorname{coe}$ applied to $f$. Let $D$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Then $\operatorname{mapBilipschitz}$ applied to $f$, $x_{2}$, $x_{3}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$ and $D$ is an element of $\operatorname{DeloneSet}$ applied to $Y$.

Delone.DeloneSet.mapIsometrydefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

the map isometry of f (from the name)

English

Let $f$ be an isometry equivalence of $X$ and $Y$. Then the map isometry of $f$ is an element of $\EquivMACRoAE {\operatorname{DeloneSet} (X)}{\operatorname{DeloneSet} (Y)}$.

Delone.DeloneSet.packingRadiusdefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Then $\operatorname{packingRadius}$ applied to $\mathrm{self}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Delone.DeloneSet.toSetdefMathlib.Analysis.AperiodicOrder.Delone.Basic, function or constant

Wording

the set of D (from the name)

English

Let $D$ be an element of $\operatorname{DeloneSet}$ applied to $X$. Then the set of $D$ is an element of $\wp X$ defined as the carrier of $D$.

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Asymptotics.IsEquivalentdefMathlib.Analysis.Asymptotics.AsymptoticEquivalent, predicate

Wording

u is equivalent to v (from the name)

English

Let $l$ be a filter of $x$. Let $u$ and $v$ be functions from elements of $x$ to elements of $x_{1}$. Then $u$ is equivalent to $v$, if $\operatorname{IsLittleO}$ holds for $l$, $u - v$ and $v$.

Mathlib.Analysis.Asymptotics.Defs

Asymptotics.IsBigOdefMathlib.Analysis.Asymptotics.Defs, predicate

Wording

no wording

English

Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $g$ be a function from elements of $x$ to elements of $F$. Then $\operatorname{IsBigO}$ holds for $l$, $f$ and $g$, if $\operatorname{proj0}$ holds for $\mathrm{Asymptotics\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Asymptotics\_\_Defs\_\_2970832229\_\_\_hygCtx\_\_\_hyg\_\_2}$, $l$, $f$ and $g$.

Asymptotics.IsBigOWithdefMathlib.Analysis.Asymptotics.Defs, predicate

Wording

no wording

English

Let $c$ be a real number. Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $g$ be a function from elements of $x$ to elements of $F$. Then $\operatorname{IsBigOWith}$ holds for $c$, $l$, $f$ and $g$, if $\operatorname{proj0}$ holds for $\mathrm{Asymptotics\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Asymptotics\_\_Defs\_\_126441222\_\_\_hygCtx\_\_\_hyg\_\_2}$, $c$, $l$, $f$ and $g$.

Asymptotics.IsLittleOdefMathlib.Analysis.Asymptotics.Defs, predicate

Wording

no wording

English

Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $g$ be a function from elements of $x$ to elements of $F$. Then $\operatorname{IsLittleO}$ holds for $l$, $f$ and $g$, if $\operatorname{proj0}$ holds for $\mathrm{Asymptotics\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Asymptotics\_\_Defs\_\_1401907169\_\_\_hygCtx\_\_\_hyg\_\_2}$, $l$, $f$ and $g$.

Asymptotics.IsThetadefMathlib.Analysis.Asymptotics.Defs, predicate

Wording

no wording

English

Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $g$ be a function from elements of $x$ to elements of $F$. Then $\operatorname{IsTheta}$ holds for $l$, $f$ and $g$, if $\operatorname{IsBigO}$ holds for $l$, $f$ and $g$ and $\operatorname{IsBigO}$ holds for $l$, $g$ and $f$.

Mathlib.Analysis.Asymptotics.ExpGrowth

ExpGrowth.expGrowthInfdefMathlib.Analysis.Asymptotics.ExpGrowth, function or constant

Wording

the exponential growth infimum of u (from the name)

English

Let $u$ be a function from natural numbers to elements of $\mathrm{ENNReal}$. Then the exponential growth infimum of $u$ is an element of $\mathrm{EReal}$ defined as $\operatorname{liminf}$ applied to the function that maps $n$ to the quotient of the logarithm of $u$ applied to $n$ and $n$ and $\operatorname{atTop}$.

ExpGrowth.expGrowthInfTopHomdefMathlib.Analysis.Asymptotics.ExpGrowth, function or constant

Wording

the exponential growth infimum top homomorphism (from the name)

English

The exponential growth infimum top homomorphism is an infimum top homomorphism of the set of functions from natural numbers to elements of $\mathrm{ENNReal}$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{expGrowthInf}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{ExpGrowth\_\_expGrowthInf\_inf}$ and $\mathrm{ExpGrowth\_\_expGrowthInf\_top}$.

ExpGrowth.expGrowthSupdefMathlib.Analysis.Asymptotics.ExpGrowth, function or constant

Wording

the exponential growth supremum of u (from the name)

English

Let $u$ be a function from natural numbers to elements of $\mathrm{ENNReal}$. Then the exponential growth supremum of $u$ is an element of $\mathrm{EReal}$ defined as the limsup of the function that maps $n$ to the quotient of the logarithm of $u$ applied to $n$ and $n$ and $\operatorname{atTop}$.

ExpGrowth.expGrowthSupBotHomdefMathlib.Analysis.Asymptotics.ExpGrowth, function or constant

Wording

the exponential growth supremum bottom homomorphism (from the name)

English

The exponential growth supremum bottom homomorphism is a supremum bottom homomorphism of the set of functions from natural numbers to elements of $\mathrm{ENNReal}$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{expGrowthSup}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{ExpGrowth\_\_expGrowthSup\_sup}$ and $\mathrm{ExpGrowth\_\_expGrowthSup\_zero}$.

Mathlib.Analysis.Asymptotics.LinearGrowth

LinearGrowth.linearGrowthInfdefMathlib.Analysis.Asymptotics.LinearGrowth, function or constant

Wording

the linear growth infimum of u (from the name)

English

Let $u$ be a function from natural numbers to elements of $R$. Then the linear growth infimum of $u$ is an element of $R$ defined as $\operatorname{liminf}$ applied to the function that maps $n$ to $\frac{ u (n)}{n}$ and $\operatorname{atTop}$.

LinearGrowth.linearGrowthInfTopHomdefMathlib.Analysis.Asymptotics.LinearGrowth, function or constant

Wording

the linear growth infimum top homomorphism (from the name)

English

The linear growth infimum top homomorphism is an infimum top homomorphism of the set of functions from natural numbers to elements of $\mathrm{EReal}$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{linearGrowthInf}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{LinearGrowth\_\_linearGrowthInf\_inf}$ and $\mathrm{LinearGrowth\_\_linearGrowthInf\_top}$.

LinearGrowth.linearGrowthSupdefMathlib.Analysis.Asymptotics.LinearGrowth, function or constant

Wording

the linear growth supremum of u (from the name)

English

Let $u$ be a function from natural numbers to elements of $R$. Then the linear growth supremum of $u$ is an element of $R$ defined as the limsup of the function that maps $n$ to $\frac{ u (n)}{n}$ and $\operatorname{atTop}$.

LinearGrowth.linearGrowthSupBotHomdefMathlib.Analysis.Asymptotics.LinearGrowth, function or constant

Wording

the linear growth supremum bottom homomorphism (from the name)

English

The linear growth supremum bottom homomorphism is a supremum bottom homomorphism of the set of functions from natural numbers to elements of $\mathrm{EReal}$ and $\mathrm{EReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{linearGrowthSup}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{LinearGrowth\_\_linearGrowthSup\_sup}$ and $\mathrm{LinearGrowth\_\_linearGrowthSup\_bot}$.

Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Asymptotics.SuperpolynomialDecaydefMathlib.Analysis.Asymptotics.SuperpolynomialDecay, predicate

Wording

no wording

English

Let $l$ be a filter of $x$. Let $k$ and $f$ be functions from elements of $x$ to elements of $x_{1}$. Then $\operatorname{SuperpolynomialDecay}$ holds for $l$, $k$ and $f$, if for all natural numbers $n$, $\operatorname{Tendsto}$ holds for the function that maps $a$ to $k (a)^ {n}\times f (a)$, $l$ and the neighbourhood filter of $0$.

Mathlib.Analysis.Asymptotics.TVS

Asymptotics.IsBigOTVSstructureMathlib.Analysis.Asymptotics.TVS, predicate

Wording

no wording

English

Let $x$ be a set. Let $l$ be a filter of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $E$. Let $g$ be a function from elements of $x_{1}$ to elements of $F$. Then we can say that $\operatorname{IsBigOTVS}$ holds for $x$, $l$, $f$ and $g$.

Asymptotics.IsLittleOTVSstructureMathlib.Analysis.Asymptotics.TVS, predicate

Wording

no wording

English

Asymptotics.IsThetaTVSdefMathlib.Analysis.Asymptotics.TVS, predicate

Wording

no wording

English

Let $x$ be a set. Let $l$ be a filter of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $E$. Let $g$ be a function from elements of $x_{1}$ to elements of $F$. Then $\operatorname{IsThetaTVS}$ holds for $x$, $l$, $f$ and $g$, if $\operatorname{IsBigOTVS}$ holds for $x$, $l$, $f$ and $g$ and $\operatorname{IsBigOTVS}$ holds for $x$, $l$, $g$ and $f$.

Mathlib.Analysis.BoxIntegral.Basic

BoxIntegral.HasIntegraldefMathlib.Analysis.BoxIntegral.Basic, predicate

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $f$ be a function from functions from elements of $x$ to real numbers to elements of $E$. Let $\mathrm{vol}$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $F$ and the top. Let $y$ be an element of $F$. Then $\operatorname{HasIntegral}$ holds for $I$, $l$, $f$, $\mathrm{vol}$ and $y$, if $\operatorname{Tendsto}$ holds for the integral sum of $f$, $\operatorname{toFilteriUnion}$ applied to $I$ and the top and the neighbourhood filter of $y$.

BoxIntegral.IntegrabledefMathlib.Analysis.BoxIntegral.Basic, predicate

Wording

I is integrable (from the docstring)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $f$ be a function from functions from elements of $x$ to real numbers to elements of $E$. Let $\mathrm{vol}$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $F$ and the top. Then $I$ is integrable, if there exists an element $y$ of $F$, such that $\operatorname{HasIntegral}$ holds for $I$, $l$, $f$, $\mathrm{vol}$ and $y$.

BoxIntegral.Integrable.convergenceRdefMathlib.Analysis.BoxIntegral.Basic, function or constant

Wording

the convergence of x7 and x8 (from the name)

English

Assume that $I$ is integrable. Let $x_{6}$ be a real number. Let $x_{7}$ be an element of $\mathrm{NNReal}$. Let $x_{8}$ be a function from elements of $x$ to real numbers. Then the convergence of $x_{7}$ and $x_{8}$ is an element of $\operatorname{Ioi}$ applied to $0$.

BoxIntegral.Integrable.toBoxAdditivedefMathlib.Analysis.BoxIntegral.Basic, function or constant

Wording

no wording

English

Assume that $I$ is integrable. Then $\operatorname{toBoxAdditive}$ applied to $h_{1}$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $F$ and $\operatorname{some}$ applied to $I$.

BoxIntegral.integraldefMathlib.Analysis.BoxIntegral.Basic, function or constant

Wording

the integral of f and vol (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $f$ be a function from functions from elements of $x$ to real numbers to elements of $E$. Let $\mathrm{vol}$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $F$ and the top. Then the integral of $f$ and $\mathrm{vol}$ is an element of $F$ defined as $\mathrm{dite}$ applied to the proposition that $I$ is integrable, the function that maps $h$ to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $0$.

BoxIntegral.integralSumdefMathlib.Analysis.BoxIntegral.Basic, function or constant

Wording

the integral sum of f (from the docstring)

English

Let $f$ be a function from functions from elements of $x$ to elements of $\Real$ to elements of $E$. Let $\mathrm{vol}$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $F$ and the top. Let $x_{5}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then the integral sum of $f$ is an element of $F$ defined as $\FinsetSum {\operatorname{boxes} (\operatorname{toPrepartition} (x_{5}))}{J}{\operatorname{coe} (\mathrm{vol} , J , f (\operatorname{tag} (J)))}$.

Mathlib.Analysis.BoxIntegral.Box.Basic

BoxIntegral.BoxstructureMathlib.Analysis.BoxIntegral.Box.Basic, type

Wording

no wording

English

Let $x$ be a set. Then the elements of $\operatorname{Box}$ applied to $x$ are a basic type.

BoxIntegral.Box.IccdefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

the closed interval (from the name)

English

The closed interval is an order embedding of $\operatorname{Box}$ applied to $x$ and $\wp (\mathrm{Elem} (x)\rightarrow \Real)$.

BoxIntegral.Box.IoodefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

the interior (from the docstring)

English

The interior is an order homomorphism of $\operatorname{Box}$ applied to $x$ and $\wp (\mathrm{Elem} (x)\rightarrow \Real)$.

BoxIntegral.Box.distortiondefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

the distortion of I (from the docstring)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the distortion of $I$ is an element of $\mathrm{NNReal}$ defined as the supremum of the universal set and the function that maps $i$ to the quotient of the distance of $\operatorname{lower}$ applied to $I$ and $\operatorname{upper}$ applied to $I$ and the distance of $\operatorname{lower}$ applied to $I$ and $i$ and $\operatorname{upper}$ applied to $I$ and $i$.

BoxIntegral.Box.facedefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

the face of I and i (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the face of $I$ and $i$ is an element of $\operatorname{Box}$ applied to $\mathrm{Fin}$ applied to $n$.

BoxIntegral.Box.lowerdefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{Box}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then $\operatorname{lower}$ applied to $\mathrm{self}$ and $x_{1}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

BoxIntegral.Box.mk'defMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

no wording

English

Let $l$ and $u$ be functions from elements of $x$ to real numbers. Then $\operatorname{mk'}$ applied to $l$ and $u$ is an element of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$ defined as $\mathrm{dite}$ applied to the proposition that for all elements $i$ of $x$, $l (i)< u (i)$, the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{mk}$ applied to $l$, $u$ and $h$ and the function that maps $h_{1}$ to the bottom.

BoxIntegral.Box.toSetdefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

the set of I (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the set of $I$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow \Real)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\MembershipmemMACRoT {I}{x_{1}}$.

BoxIntegral.Box.upperdefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

no wording

English

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

BoxIntegral.Box.withBotToSetdefMathlib.Analysis.BoxIntegral.Box.Basic, function or constant

Wording

no wording

English

Let $o$ be an element of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$. Then $\operatorname{withBotToSet}$ applied to $o$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow \Real)$ defined as $\operatorname{elim}$ applied to $o$, $\operatorname{emptyCollection}$ and $\operatorname{toSet}$.

Mathlib.Analysis.BoxIntegral.Box.SubboxInduction

BoxIntegral.Box.splitCenterBoxdefMathlib.Analysis.BoxIntegral.Box.SubboxInduction, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{splitCenterBox}$ applied to $I$ and $s$ is an element of $\operatorname{Box}$ applied to $x$.

BoxIntegral.Box.splitCenterBoxEmbdefMathlib.Analysis.BoxIntegral.Box.SubboxInduction, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then $\operatorname{splitCenterBoxEmb}$ applied to $I$ is an embedding of $\wp x$ and $\operatorname{Box}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{splitCenterBox}$ applied to $I$ and $\mathrm{BoxIntegral\_\_Box\_\_injective\_splitCenterBox}$ applied to $I$.

Mathlib.Analysis.BoxIntegral.Partition.Additive

BoxIntegral.BoxAdditiveMapstructureMathlib.Analysis.BoxIntegral.Partition.Additive, type

Wording

no wording

English

Let $x$ and $M$ be sets. Let $I$ be an element of $\mathrm{WithTop}$ applied to $\operatorname{Box}$ applied to $x$. Then the elements of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $I$ are a basic type.

BoxIntegral.BoxAdditiveMap.mapdefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

the map of f and g (from the name)

English

Let $f$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $x_{3}$. Let $g$ be an additive monoid homomorphism of $M$ and $N$. Then the map of $f$ and $g$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $N$ and $x_{3}$.

BoxIntegral.BoxAdditiveMap.ofMapSplitAdddefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\operatorname{Box}$ applied to $x$ to elements of $M$. Let $x_{2}$ be an element of $\mathrm{WithTop}$ applied to $\operatorname{Box}$ applied to $x$ such that for all elements $I$ of $\operatorname{Box}$ applied to $x$, if $\operatorname{some} (I)\leq x_{2}$, then for all elements $i$ of $x$, for all real numbers $x_{3}$, if $x_{3}$ is an element of the open interval of $\operatorname{lower}$ applied to $I$ and $i$ and $\operatorname{upper}$ applied to $I$ and $i$, then the sum of the eliminator of $f$ and $\operatorname{splitLower}$ applied to $I$, $i$ and $x_{3}$ and the eliminator of $f$ and $\operatorname{splitUpper}$ applied to $I$, $i$ and $x_{3}$ is equal to $f$ applied to $I$. Then $\operatorname{ofMapSplitAdd}$ applied to $f$, $x_{2}$ and $\mathrm{hf}$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $x_{2}$.

BoxIntegral.BoxAdditiveMap.restrictdefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

no wording

English

Let $f$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $x_{2}$. Let $I$ be an element of $\mathrm{WithTop}$ applied to $\operatorname{Box}$ applied to $x$ such that $I \leq x_{2}$. Then $\operatorname{restrict}$ applied to $f$, $I$ and $\mathrm{hI}$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $I$.

BoxIntegral.BoxAdditiveMap.toFundefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $M$ and $I$. Let $x_{2}$ be an element of $\operatorname{Box}$ applied to $x$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

BoxIntegral.BoxAdditiveMap.toSMuldefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

the product of f (from the name)

English

Let $f$ be an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $\Real$ and $x_{1}$. Then the product of $f$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $E$ and $x_{1}$ defined as the map of $f$ and the additive monoid homomorphism of $\operatorname{toLinearMap}$ applied to $\operatorname{lsmul}$ applied to $\Real$ and $\Real$.

BoxIntegral.BoxAdditiveMap.upperSubLowerdefMathlib.Analysis.BoxIntegral.Partition.Additive, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $\operatorname{Box}$ applied to $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a function from real numbers and elements of $\operatorname{Box}$ applied to $\mathrm{Fin}$ applied to $n$ to elements of $G$. Let $\mathrm{fb}$ be a function from elements of $\SetIccMACRoP {\operatorname{lower} (x_{1} , i)}{\operatorname{upper} (x_{1} , i)}$ to elements of $\operatorname{BoxAdditiveMap}$ applied to $\mathrm{Fin}$ applied to $n$, $G$ and $\operatorname{some}$ applied to the face of $x_{1}$ and $i$ such that for all real numbers $x_{2}$, for all elements $\mathrm{hx}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {(\SetIccMACRoP {\operatorname{lower} (x_{1} , i)}{\operatorname{upper} (x_{1} , i)})}{x_{2}}$, for all elements $J$ of $\operatorname{Box}$ applied to $\mathrm{Fin}$ applied to $n$, $\EqtMACRoH {f (x_{2} , J)}{\mathrm{fb} (x_{2} , J)}$. Then $\operatorname{upperSubLower}$ applied to $x_{1}$, $i$, $f$, $\mathrm{fb}$ and $\mathrm{hf}$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $\mathrm{Fin}$ applied to $n + 1$, $G$ and $\operatorname{some}$ applied to $x_{1}$.

Mathlib.Analysis.BoxIntegral.Partition.Basic

BoxIntegral.PrepartitionstructureMathlib.Analysis.BoxIntegral.Partition.Basic, type

Wording

prepartition of I (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the prepartitions of $I$ are a basic type.

BoxIntegral.Prepartition.IsPartitiondefMathlib.Analysis.BoxIntegral.Partition.Basic, predicate

Wording

x1 is a partition (from the name)

English

Let $x_{1}$ be a prepartition of $I$. Then $x_{1}$ is a partition, if for all functions $x_{2}$ from elements of $x$ to real numbers, if $x_{2}$ is an element of $I$, then there exists an element $J$ of $\operatorname{Box}$ applied to $x$, such that $J$ is an element of $x_{1}$ and $x_{2}$ is an element of $J$.

BoxIntegral.Prepartition.biUniondefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a prepartition of $I$. Let $x_{2}$ be a function from elements $J$ of $\operatorname{Box}$ applied to $x$ to prepartitions of $J$. Then $\operatorname{biUnion}$ applied to $x_{1}$, $J$ and $x_{2}$ is a prepartition of $I$.

BoxIntegral.Prepartition.biUnionIndexdefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a prepartition of $I$. Let $x_{2}$ be a function from elements $J_{1}$ of $\operatorname{Box}$ applied to $x$ to prepartitions of $J_{1}$. Let $J$ be an element of $\operatorname{Box}$ applied to $x$. Then $\operatorname{biUnionIndex}$ applied to $x_{1}$, $J_{1}$, $x_{2}$ and $J$ is an element of $\operatorname{Box}$ applied to $x$.

BoxIntegral.Prepartition.boxesdefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a prepartition of $I$. Then $\operatorname{boxes}$ applied to $\mathrm{self}$ is a finite set of $\operatorname{Box}$ applied to $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BoxIntegral.Prepartition.disjUniondefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be prepartitions of $I$ such that the union of $x_{1}$ is disjoint to the union of $x_{2}$. Then $\operatorname{disjUnion}$ applied to $x_{1}$, $x_{2}$ and $h$ is a prepartition of $I$.

BoxIntegral.Prepartition.distortiondefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

the distortion of x1 (from the docstring)

English

Let $x_{1}$ be a prepartition of $I$. Then the distortion of $x_{1}$ is an element of $\mathrm{NNReal}$ defined as the supremum of $\operatorname{boxes}$ applied to $x_{1}$ and $\operatorname{distortion}$.

BoxIntegral.Prepartition.filterdefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

the filter of x1 and p (from the name)

English

Let $x_{1}$ be a prepartition of $I$. Let $p$ be a function from elements of $\operatorname{Box}$ applied to $x$ to propositions. Then the filter of $x_{1}$ and $p$ is a prepartition of $I$.

BoxIntegral.Prepartition.iUniondefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

the union of x1 (from the name)

English

Let $x_{1}$ be a prepartition of $I$. Then the union of $x_{1}$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow \Real)$ defined as the union of the function that maps $J$ to the union of the function that maps $h$ to the set of $J$.

BoxIntegral.Prepartition.ofWithBotdefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

the prepartition of boxes (from the name)

English

Let $\mathrm{boxes}$ be a finite set of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$ such that for all elements $J$ of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$, if $J$ is an element of $\mathrm{boxes}$, then $J \leq \operatorname{some} (I)$ and $\operatorname{Pairwise}$ holds for $\mathrm{boxes}$ and the proposition that $\mathrm{Disjoint}$. Then the prepartition of $\mathrm{boxes}$ is a prepartition of $I$.

BoxIntegral.Prepartition.restrictdefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $x_{1}$ be a prepartition of $I$. Let $J$ be an element of $\operatorname{Box}$ applied to $x$. Then $\operatorname{restrict}$ applied to $x_{1}$ and $J$ is a prepartition of $J$.

BoxIntegral.Prepartition.singledefMathlib.Analysis.BoxIntegral.Partition.Basic, function or constant

Wording

no wording

English

Let $I$ and $J$ be elements of $\operatorname{Box}$ applied to $x$ such that $J \leq I$. Then $\operatorname{single}$ applied to $I$, $J$ and $h$ is a prepartition of $I$.

Mathlib.Analysis.BoxIntegral.Partition.Filter

BoxIntegral.IntegrationParamsstructureMathlib.Analysis.BoxIntegral.Partition.Filter, type

Wording

no wording

English

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

BoxIntegral.IntegrationParams.GPdefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

$\operatorname{GP}$ is an element of $\operatorname{IntegrationParams}$ defined as the bottom.

BoxIntegral.IntegrationParams.HenstockdefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

$\operatorname{Henstock}$ is an element of $\operatorname{IntegrationParams}$ defined as $\operatorname{mk}$ applied to $\operatorname{false}$, $\operatorname{true}$ and $\operatorname{false}$.

BoxIntegral.IntegrationParams.McShanedefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

$\operatorname{McShane}$ is an element of $\operatorname{IntegrationParams}$ defined as $\operatorname{mk}$ applied to $\operatorname{false}$, $\operatorname{false}$ and $\operatorname{false}$.

BoxIntegral.IntegrationParams.MemBaseSetstructureMathlib.Analysis.BoxIntegral.Partition.Filter, predicate

Wording

no wording

English

Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $c$ be an element of $\mathrm{NNReal}$. Let $r$ be a function from functions from elements of $x$ to real numbers to elements of $\operatorname{Ioi}$ applied to $0$. Let $x_{2}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then we can say that $\operatorname{MemBaseSet}$ holds for $l$, $I$, $c$, $r$ and $x_{2}$.

BoxIntegral.IntegrationParams.RConddefMathlib.Analysis.BoxIntegral.Partition.Filter, predicate

Wording

no wording

English

Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $r$ be a function from functions from elements of $x$ to real numbers to elements of $\operatorname{Ioi}$ applied to $0$. Then $\operatorname{RCond}$ holds for $l$ and $r$, if if $\EqtMACRoH {\operatorname{bRiemann} (l)}{\operatorname{true}}$, then for all functions $x_{1}$ from elements of $x$ to real numbers, $\EqtMACRoH {r (x_{1})}{r (0)}$.

BoxIntegral.IntegrationParams.RiemanndefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

$\operatorname{Riemann}$ is an element of $\operatorname{IntegrationParams}$ defined as $\operatorname{mk}$ applied to $\operatorname{true}$, $\operatorname{true}$ and $\operatorname{false}$.

BoxIntegral.IntegrationParams.bDistortiondefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

the distortion of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{IntegrationParams}$. Then the distortion of $\mathrm{self}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

BoxIntegral.IntegrationParams.bHenstockdefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{IntegrationParams}$. Then $\operatorname{bHenstock}$ applied to $\mathrm{self}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

BoxIntegral.IntegrationParams.bRiemanndefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{IntegrationParams}$. Then $\operatorname{bRiemann}$ applied to $\mathrm{self}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

BoxIntegral.IntegrationParams.toFilterdefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

the filter of l and I (from the name)

English

Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the filter of $l$ and $I$ is a filter of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as the supremum of the function that maps $c$ to the filter distortion of $I$ and $c$.

BoxIntegral.IntegrationParams.toFilterDistortiondefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

the filter distortion of I and c (from the name)

English

Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $c$ be an element of $\mathrm{NNReal}$. Then the filter distortion of $I$ and $c$ is a filter of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as the infimum of the function that maps $r$ to the infimum of the function that maps $h$ to the principal filter of $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\operatorname{MemBaseSet}$ applied to $l$, $I$, $c$, $r$ and $x_{2}$.

BoxIntegral.IntegrationParams.toFilterDistortioniUniondefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

Let $l$ be an element of $\operatorname{IntegrationParams}$. Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $c$ be an element of $\mathrm{NNReal}$. Let $x_{2}$ be a prepartition of $I$. Then $\operatorname{toFilterDistortioniUnion}$ applied to $l$, $I$, $c$ and $x_{2}$ is a filter of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as the minimum of the filter distortion of $I$ and $c$ and the principal filter of $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that the union of $x_{3}$ is equal to the union of $x_{2}$.

BoxIntegral.IntegrationParams.toFilteriUniondefMathlib.Analysis.BoxIntegral.Partition.Filter, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $x_{2}$ be a prepartition of $I$. Then $\operatorname{toFilteriUnion}$ applied to $I$ and $x_{2}$ is a filter of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as the supremum of the function that maps $c$ to $\operatorname{toFilterDistortioniUnion}$ applied to $l$, $I$, $c$ and $x_{2}$.

Mathlib.Analysis.BoxIntegral.Partition.Measure

BoxIntegral.BoxAdditiveMap.volumedefMathlib.Analysis.BoxIntegral.Partition.Measure, function or constant

Wording

the volume (from the name)

English

The volume is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, the set of continuous linear maps of $E$ and $E$ and the top defined as the product of $\operatorname{toBoxAdditive}$ applied to the volume.

MeasureTheory.Measure.toBoxAdditivedefMathlib.Analysis.BoxIntegral.Partition.Measure, function or constant

Wording

no wording

English

Let $x_{1}$ be a measure of the set of functions from elements of $x$ to real numbers. Then $\operatorname{toBoxAdditive}$ applied to $x_{1}$ is an element of $\operatorname{BoxAdditiveMap}$ applied to $x$, $\Real$ and the top.

Mathlib.Analysis.BoxIntegral.Partition.Split

BoxIntegral.Box.splitLowerdefMathlib.Analysis.BoxIntegral.Partition.Split, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $i$ be an element of $x$. Let $x_{1}$ be a real number. Then $\operatorname{splitLower}$ applied to $I$, $i$ and $x_{1}$ is an element of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$ defined as $\operatorname{mk'}$ applied to $\operatorname{lower}$ applied to $I$ and $\operatorname{update}$ applied to $\operatorname{upper}$ applied to $I$, $i$ and $\MinminMACRoAG {x_{1}}{\operatorname{upper} (I , i)}$.

BoxIntegral.Box.splitUpperdefMathlib.Analysis.BoxIntegral.Partition.Split, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $i$ be an element of $x$. Let $x_{1}$ be a real number. Then $\operatorname{splitUpper}$ applied to $I$, $i$ and $x_{1}$ is an element of $\mathrm{WithBot}$ applied to $\operatorname{Box}$ applied to $x$ defined as $\operatorname{mk'}$ applied to $\operatorname{update}$ applied to $\operatorname{lower}$ applied to $I$, $i$ and $\MaxmaxMACRoAF {x_{1}}{\operatorname{lower} (I , i)}$ and $\operatorname{upper}$ applied to $I$.

BoxIntegral.Prepartition.compldefMathlib.Analysis.BoxIntegral.Partition.Split, function or constant

Wording

the complement of x1 (from the name)

English

Let $x_{1}$ be a prepartition of $I$. Then the complement of $x_{1}$ is a prepartition of $I$ defined as $\operatorname{choose}$ applied to $\mathrm{BoxIntegral\_\_Prepartition\_\_exists\_iUnion\_eq\_sdiff}$ applied to $x_{1}$.

BoxIntegral.Prepartition.splitdefMathlib.Analysis.BoxIntegral.Partition.Split, function or constant

Wording

the split of i and x1 (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $i$ be an element of $x$. Let $x_{1}$ be a real number. Then the split of $i$ and $x_{1}$ is a prepartition of $I$.

BoxIntegral.Prepartition.splitManydefMathlib.Analysis.BoxIntegral.Partition.Split, function or constant

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Let $s$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $\Real$. Then $\operatorname{splitMany}$ applied to $I$ and $s$ is a prepartition of $I$ defined as the infimum of $s$ and the function that maps $p$ to the split of $\ProdfstMACRoZ {p}$ and $\ProdsndMACRoAA {p}$.

Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

BoxIntegral.Prepartition.splitCenterdefMathlib.Analysis.BoxIntegral.Partition.SubboxInduction, function or constant

Wording

the split center of I (from the name)

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the split center of $I$ is a prepartition of $I$.

BoxIntegral.Prepartition.toSubordinatedefMathlib.Analysis.BoxIntegral.Partition.SubboxInduction, function or constant

Wording

no wording

English

Let $x_{2}$ be a prepartition of $I$. Let $r$ be a function from functions from elements of $x$ to real numbers to elements of $\operatorname{Ioi}$ applied to $0$. Then $\operatorname{toSubordinate}$ applied to $x_{2}$ and $r$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as $\operatorname{choose}$ applied to $\mathrm{BoxIntegral\_\_Prepartition\_\_exists\_tagged\_le\_isHenstock\_isSubordinate\_iUnion\_eq}$ applied to $r$ and $x_{2}$.

BoxIntegral.TaggedPrepartition.unionComplToSubordinatedefMathlib.Analysis.BoxIntegral.Partition.SubboxInduction, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $x_{3}$ be a prepartition of $I$ such that the union of $x_{3}$ is equal to $\operatorname{sdiff}$ applied to the set of $I$ and the union of $x_{2}$. Let $r$ be a function from functions from elements of $x$ to real numbers to elements of $\operatorname{Ioi}$ applied to $0$. Then $\operatorname{unionComplToSubordinate}$ applied to $x_{2}$, $x_{3}$, $\mathrm{hU}$ and $r$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$.

Mathlib.Analysis.BoxIntegral.Partition.Tagged

BoxIntegral.Prepartition.biUnionTaggeddefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

no wording

English

Let $x_{1}$ be a prepartition of $I$. Let $x_{2}$ be a function from elements $J$ of $\operatorname{Box}$ applied to $x$ to elements of $\operatorname{TaggedPrepartition}$ applied to $J$. Then $\operatorname{biUnionTagged}$ applied to $x_{1}$, $J$ and $x_{2}$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$.

BoxIntegral.TaggedPrepartitionstructureMathlib.Analysis.BoxIntegral.Partition.Tagged, type

Wording

no wording

English

Let $I$ be an element of $\operatorname{Box}$ applied to $x$. Then the elements of $\operatorname{TaggedPrepartition}$ applied to $I$ are a basic type.

BoxIntegral.TaggedPrepartition.IsHenstockdefMathlib.Analysis.BoxIntegral.Partition.Tagged, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then $\operatorname{IsHenstock}$ holds for $x_{1}$, if for all elements $J$ of $\operatorname{Box}$ applied to $x$, if $J$ is an element of $x_{1}$, then $\operatorname{tag}$ applied to $J$ is an element of $\operatorname{Icc}$ applied to $J$.

BoxIntegral.TaggedPrepartition.IsPartitiondefMathlib.Analysis.BoxIntegral.Partition.Tagged, predicate

Wording

x1 is a partition (from the docstring)

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then $x_{1}$ is a partition, if $\operatorname{toPrepartition}$ applied to $x_{1}$ is a partition.

BoxIntegral.TaggedPrepartition.IsSubordinatedefMathlib.Analysis.BoxIntegral.Partition.Tagged, predicate

Wording

x2 is subordinate to r (from the name)

English

Let $x_{2}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $r$ be a function from functions from elements of $x$ to real numbers to elements of $\operatorname{Ioi}$ applied to $0$. Then $x_{2}$ is subordinate to $r$, if for all elements $J$ of $\operatorname{Box}$ applied to $x$, if $J$ is an element of $x_{2}$, then $\operatorname{Icc}$ applied to $J$ is less than or equal to the closed ball of $\operatorname{tag}$ applied to $J$ and $r$ applied to $\operatorname{tag}$ applied to $J$.

BoxIntegral.TaggedPrepartition.biUnionPrepartitiondefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $x_{2}$ be a function from elements $J$ of $\operatorname{Box}$ applied to $x$ to prepartitions of $J$. Then $\operatorname{biUnionPrepartition}$ applied to $x_{1}$, $J$ and $x_{2}$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$.

BoxIntegral.TaggedPrepartition.disjUniondefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{TaggedPrepartition}$ applied to $I$ such that the union of $x_{1}$ is disjoint to the union of $x_{2}$. Then $\operatorname{disjUnion}$ applied to $x_{1}$, $x_{2}$ and $h$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$.

BoxIntegral.TaggedPrepartition.distortiondefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

the distortion of x1 (from the docstring)

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then the distortion of $x_{1}$ is an element of $\mathrm{NNReal}$ defined as the distortion of $\operatorname{toPrepartition}$ applied to $x_{1}$.

BoxIntegral.TaggedPrepartition.embedBoxdefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

no wording

English

Let $I$ and $J$ be elements of $\operatorname{Box}$ applied to $x$ such that $I \leq J$. Then $\operatorname{embedBox}$ applied to $I$, $J$ and $h$ is an embedding of $\operatorname{TaggedPrepartition}$ applied to $I$ and $\operatorname{TaggedPrepartition}$ applied to $J$.

BoxIntegral.TaggedPrepartition.filterdefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

the filter of x1 and p (from the name)

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $p$ be a function from elements of $\operatorname{Box}$ applied to $x$ to propositions. Then the filter of $x_{1}$ and $p$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as $\operatorname{mk}$ applied to the filter of $\operatorname{toPrepartition}$ applied to $x_{1}$ and $p$, $\operatorname{tag}$ and $\mathrm{BoxIntegral\_\_TaggedPrepartition\_\_tag\_mem\_Icc}$ applied to $x_{1}$.

BoxIntegral.TaggedPrepartition.iUniondefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

the union of x1 (from the name)

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Then the union of $x_{1}$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow \Real)$ defined as the union of $\operatorname{toPrepartition}$ applied to $x_{1}$.

BoxIntegral.TaggedPrepartition.infPrepartitiondefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

the infimum prepartition of x1 and x2 (from the name)

English

Let $x_{1}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $x_{2}$ be a prepartition of $I$. Then the infimum prepartition of $x_{1}$ and $x_{2}$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as $\operatorname{biUnionPrepartition}$ applied to $x_{1}$ and the function that maps $J$ to $\operatorname{restrict}$ applied to $x_{2}$ and $J$.

BoxIntegral.TaggedPrepartition.singledefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

no wording

English

Let $I$ and $J$ be elements of $\operatorname{Box}$ applied to $x$ such that $J \leq I$. Let $x_{1}$ be a function from elements of $x$ to real numbers such that $\MembershipmemMACRoT {\operatorname{Icc} (I)}{x_{1}}$. Then $\operatorname{single}$ applied to $I$, $J$, $\mathrm{hJ}$, $x_{1}$ and $h$ is an element of $\operatorname{TaggedPrepartition}$ applied to $I$ defined as $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $I$, $J$ and $\mathrm{hJ}$, the function that maps $x_{2}$ to $x_{1}$ and the function that maps $x_{3}$ to $h$.

BoxIntegral.TaggedPrepartition.tagdefMathlib.Analysis.BoxIntegral.Partition.Tagged, function or constant

Wording

the tag of x1 and x2 (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{TaggedPrepartition}$ applied to $I$. Let $x_{1}$ be an element of $\operatorname{Box}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then the tag of $x_{1}$ and $x_{2}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

Mathlib.Analysis.BoxIntegral.UnitPartition

BoxIntegral.hasIntegralVerticesdefMathlib.Analysis.BoxIntegral.UnitPartition, predicate

Wording

B has integral vertices (from the name)

English

Let $B$ be an element of $\operatorname{Box}$ applied to $x$. Then $B$ has integral vertices, if there exist functions $l$ and $u$ from elements of $x$ to integers, such that for all elements $i$ of $x$, $\operatorname{lower} (B , i)= l (i)$ and for all elements $i_{1}$ of $x$, $\operatorname{upper} (B , i_{1})= u (i_{1})$.

BoxIntegral.unitPartition.admissibleIndexdefMathlib.Analysis.BoxIntegral.UnitPartition, function or constant

Wording

the admissible index of n and B (from the name)

English

Let $n$ be a natural number. Let $B$ be an element of $\operatorname{Box}$ applied to $x$. Then the admissible index of $n$ and $B$ is a finite set of the set of functions from elements of $x$ to integers.

BoxIntegral.unitPartition.boxdefMathlib.Analysis.BoxIntegral.UnitPartition, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $x_{1}$ be a function from elements of $x$ to integers. Then $\operatorname{box}$ applied to $n$ and $x_{1}$ is an element of $\operatorname{Box}$ applied to $x$.

BoxIntegral.unitPartition.indexdefMathlib.Analysis.BoxIntegral.UnitPartition, function or constant

Wording

the index of x1 and i (from the name)

English

Let $n$ be a natural number. Let $x_{1}$ be a function from elements of $x$ to real numbers. Let $i$ be an element of $x$. Then the index of $x_{1}$ and $i$ is an integer defined as $\operatorname{ceil} (n \times x_{1} (i))- 1$.

BoxIntegral.unitPartition.prepartitiondefMathlib.Analysis.BoxIntegral.UnitPartition, function or constant

Wording

the prepartition of n and B (from the name)

English

Let $n$ be a natural number. Let $B$ be an element of $\operatorname{Box}$ applied to $x$. Then the prepartition of $n$ and $B$ is an element of $\operatorname{TaggedPrepartition}$ applied to $B$.

BoxIntegral.unitPartition.tagdefMathlib.Analysis.BoxIntegral.UnitPartition, function or constant

Wording

the tag of x1 and x2 (from the name)

English

Let $n$ be a natural number. Let $x_{1}$ be a function from elements of $x$ to integers. Let $x_{2}$ be an element of $x$. Then the tag of $x_{1}$ and $x_{2}$ is a real number defined as $\frac{ x_{1} (x_{2})+ 1}{n}$.

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

CStarAlgebra.approximateUnitdefMathlib.Analysis.CStarAlgebra.ApproximateUnit, function or constant

Wording

the approximate unit of A (from the name)

English

Let $A$ be a set. Then the approximate unit of $A$ is a filter of $A$ defined as the minimum of the filter of $\mathrm{CStarAlgebra\_\_isBasis\_nonneg\_sections}$ applied to $A$ and the principal filter of the closed ball of $0$ and $1$.

Filter.IsIncreasingApproximateUnitstructureMathlib.Analysis.CStarAlgebra.ApproximateUnit, predicate

Wording

l is a increasing approximate unit (from the name)

English

Let $l$ be a filter of $A$. Then we can say that $l$ is an increasing approximate unit.

Mathlib.Analysis.CStarAlgebra.Basic

CStarRingclassMathlib.Analysis.CStarAlgebra.Basic, predicate

Wording

E is a star ring (from the name)

English

Let $E$ be a set. Then we can say that $E$ is a star ring.

NormedStarGroupclassMathlib.Analysis.CStarAlgebra.Basic, predicate

Wording

E is a normed star group (from the name)

English

Let $E$ be a set. Then we can say that $E$ is a normed star group.

starNormedAddGroupHomdefMathlib.Analysis.CStarAlgebra.Basic, function or constant

Wording

the star normed additive group homomorphism (from the name)

English

The star normed additive group homomorphism is a normed additive group homomorphism of $E$ and $E$.

starₗᵢdefMathlib.Analysis.CStarAlgebra.Basic, function or constant

Wording

the star of x (from the name)

English

Let $x$ be a set. Then the star of $x$ is a linear isometry equivalence of $E$ and $E$.

Mathlib.Analysis.CStarAlgebra.CStarMatrix

CStarMatrixdefMathlib.Analysis.CStarAlgebra.CStarMatrix, type

Wording

star matrix of n and A (from the name)

English

Let $m$, $n$ and $A$ be sets. Then a star matrix of $n$ and $A$ is an element of the function that maps $m$, $n$ and $A$ to the set of matrixes of $n$ and $A$.

CStarMatrix.conjTransposedefMathlib.Analysis.CStarAlgebra.CStarMatrix, function or constant

Wording

the conjugate transpose of M (from the docstring)

English

Let $M$ be a star matrix of $n$ and $A$. Then the conjugate transpose of $M$ is a star matrix of $m$ and $A$ defined as the map of the transpose of $M$ and $\operatorname{star}$.

CStarMatrix.mapdefMathlib.Analysis.CStarAlgebra.CStarMatrix, function or constant

Wording

the map of M and f (from the name)

English

Let $M$ be a star matrix of $n$ and $A$. Let $f$ be a function from elements of $A$ to elements of $B$. Then the map of $M$ and $f$ is a star matrix of $n$ and $B$ defined as $\operatorname{ofMatrix}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $f$ applied to $M$ applied to $i_{1}$ and $j_{1}$.

CStarMatrix.mapₗdefMathlib.Analysis.CStarAlgebra.CStarMatrix, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a linear map of $A$ and $B$. Then the map of $f$ is a linear map of the set of star matrixes of $n$ and $A$ and the set of star matrixes of $n$ and $B$.

CStarMatrix.mapₙₐdefMathlib.Analysis.CStarAlgebra.CStarMatrix, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a non unital star algebra homomorphism of $A$ and $B$. Then the map of $f$ is a non unital star algebra homomorphism of the set of star matrixes of $n$ and $A$ and the set of star matrixes of $n$ and $B$.

CStarMatrix.ofMatrixdefMathlib.Analysis.CStarAlgebra.CStarMatrix, function or constant

Wording