AddEquiv.lpBCFdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
$\operatorname{lpBCF}$ is an additive equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . E , \operatorname{top})}{x_{3}})}$ and the set of bounded continuous functions of $x$ and $E$.
AddEquiv.lpPiLpdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
$\operatorname{lpPiLp}$ is an additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{2}})}$ and $\mathrm{PiLp}$ applied to $p$ and $E$.
AlgEquiv.lpBCFdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{lpBCF}$ applied to $x$ and $x_{1}$ is an algebra isomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{7} . A , \operatorname{top})}{x_{6}})}$ and the set of bounded continuous functions of $x$ and $A$.
Equiv.lpPiLpdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
$\operatorname{lpPiLp}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{2}})})}{\mathrm{PiLp} (p , E)}$.
RingEquiv.lpBCFdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
$\operatorname{lpBCF}$ is a ring isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . R , \operatorname{top})}{x_{3}})}$ and the set of bounded continuous functions of $x$ and $R$.
lpBCFₗᵢdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
Let $E$ and $x_{1}$ be sets. Then $\mathrm{lpBCF\_u2097\_\_u1d62\_}$ applied to $E$ and $x_{1}$ is a linear isometry equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{7} . E , \operatorname{top})}{x_{6}})}$ and the set of bounded continuous functions of $x$ and $E$.
lpPiLpₗᵢdefMathlib.Analysis.Normed.Lp.LpEquiv, function or constantEnglish
Let $E$ be a function from elements of $x$ to sets. Let $x_{3}$ be a set. Then $\mathrm{lpPiLp\_u2097\_\_u1d62\_}$ applied to $E$ and $x_{3}$ is a linear isometry equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{6}})}$ and $\mathrm{PiLp}$ applied to $p$ and $E$.
Matrix.toLpLindefMathlib.Analysis.Normed.Lp.Matrix, function or constantEnglish
Let $p$ and $q$ be elements of $\mathrm{ENNReal}$. Then $\operatorname{toLpLin}$ applied to $p$ and $q$ is a linear equivalence of the set of matrixes of $n$ and $R$ and the set of linear maps of $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements of $n$ to elements of $R$ and $\mathrm{WithLp}$ applied to $q$ and the set of functions from elements of $m$ to elements of $R$ defined as the composition of $\operatorname{toLin'}$ and the arrow congruence of the inverse of the linear equivalence of $p$ and the inverse of the linear equivalence of $q$.
Matrix.toLpLinAlgEquivdefMathlib.Analysis.Normed.Lp.Matrix, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{toLpLinAlgEquiv}$ applied to $p$ is an algebra isomorphism of the set of matrixes of $n$ and $R$ and the set of ends of $R$ and $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements of $n$ to elements of $R$ defined as the algebra isomorphism of $\operatorname{toLpLin}$ applied to $p$ and $p$.
MeasurableEquiv.toLpdefMathlib.Analysis.Normed.Lp.MeasurableSpace, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $X$ be a set. Then $\operatorname{toLp}$ applied to $p$ and $X$ is a measurable equivalence of $X$ and $\mathrm{WithLp}$ applied to $p$ and $X$ defined as $\operatorname{mk}$ applied to the inverse of the equivalence of $p$ and $X$, $\mathrm{WithLp\_\_measurable\_toLp}$ applied to $p$ and $X$ and $\mathrm{WithLp\_\_measurable\_ofLp}$ applied to $p$ and $X$.
LinearIsometry.piLpExtendByZerodefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $E$ be sets. Let $f$ be an embedding of $x_{1}$ and $x_{4}$. Then $\operatorname{piLpExtendByZero}$ applied to $p$, $x$, $E$ and $f$ is a linear isometry of $\mathrm{PiLp}$ applied to $p$ and the function that maps $x_{8}$ to $E$ and $\mathrm{PiLp}$ applied to $p$ and the function that maps $x_{9}$ to $E$.
LinearIsometryEquiv.piLpCongrLeftdefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $E$ be sets. Let $e$ be an equivalence from $x_{1}$ to $x_{4}$. Then $\operatorname{piLpCongrLeft}$ applied to $p$, $x$, $E$ and $e$ is a linear isometry equivalence of $\mathrm{PiLp}$ applied to $p$ and the function that maps $x_{8}$ to $E$ and $\mathrm{PiLp}$ applied to $p$ and the function that maps $x_{9}$ to $E$.
LinearIsometryEquiv.piLpCongrRightdefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $e$ be a function from elements $i$ of $x_{1}$ to linear isometry equivalences of $x_{2}$ applied to $i$ and $x_{3}$ applied to $i$. Then $\operatorname{piLpCongrRight}$ applied to $p$, $i$ and $e$ is a linear isometry equivalence of $\mathrm{PiLp}$ applied to $p$ and $x_{2}$ and $\mathrm{PiLp}$ applied to $p$ and $x_{3}$.
LinearIsometryEquiv.piLpCurrydefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $x$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{6}$ be a function from elements $i_{2}$ of $x_{2}$ and elements of $x_{3}$ applied to $i_{2}$ to sets. Then $\operatorname{piLpCurry}$ applied to $x$, $p$, $i_{2}$ and $x_{6}$ is a linear isometry equivalence of $\mathrm{PiLp}$ applied to $p$ and the function that maps $i$ to $x_{6}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and $\mathrm{PiLp}$ applied to $p$ and the function that maps $i_{1}$ to $\mathrm{PiLp}$ applied to $p$ and $x_{6}$ applied to $i_{1}$.
PiLpdefMathlib.Analysis.Normed.Lp.PiLp, typeEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a function from elements of $x$ to sets. Then an element of $\mathrm{PiLp}$ applied to $p$ and $x_{1}$ is an element of the function that maps $p$ and $x_{1}$ to $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$.
PiLp.basisFundefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the basis function of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $x_{1}$ be sets. Then the basis function of $p$ is a basis of $x$ and $\mathrm{PiLp}$ applied to $p$ and the function that maps $x_{3}$ to $x$ defined as the basis of the linear equivalence of $p$.
PiLp.continuousLinearEquivdefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the continuous linear equivalence of p and x2 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Then the continuous linear equivalence of $p$ and $x_{2}$ is a continuous linear equivalence of $\mathrm{PiLp}$ applied to $p$ and $x_{2}$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$.
PiLp.equivOfUniquedefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the equivalence of p and x2 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Then the equivalence of $p$ and $x_{2}$ is a continuous linear equivalence of $\mathrm{PiLp}$ applied to $p$ and $x_{2}$ and $x_{2}$ applied to $\operatorname{default}$ defined as the composition of the continuous linear equivalence of $p$ and $x_{2}$ and the product of $x$ and $x_{2}$.
PiLp.equivₗᵢdefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the equivalence of x2 (from the name)
English
Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Then the equivalence of $x_{2}$ is a linear isometry equivalence of $\mathrm{PiLp}$ applied to the top and $x_{2}$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$ defined as $\operatorname{mk}$ applied to the linear equivalence of the top and $\mathrm{PiLp\_\_norm\_ofLp}$.
PiLp.homeomorphdefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the homeomorphism of p and x1 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a function from elements of $x$ to sets. Then the homeomorphism of $p$ and $x_{1}$ is a homeomorphism of $\mathrm{PiLp}$ applied to $p$ and $x_{1}$ and the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$.
PiLp.projdefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the projection of x2 and i (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Let $i$ be an element of $x_{1}$. Then the projection of $x_{2}$ and $i$ is a continuous linear map of $\mathrm{PiLp}$ applied to $p$ and $x_{2}$ and $x_{2}$ applied to $i$.
PiLp.projₗdefMathlib.Analysis.Normed.Lp.PiLp, function or constantWording
the projection of x2 and i (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Let $i$ be an element of $x_{1}$. Then the projection of $x_{2}$ and $i$ is a linear map of $\mathrm{PiLp}$ applied to $p$ and $x_{2}$ and $x_{2}$ applied to $i$ defined as the composition of the projection of $i$ and $\operatorname{toLinearMap}$ applied to the linear equivalence of $p$.
PiLp.singledefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x$. Let $a$ be an element of $x_{1}$ applied to $i$. Then $\operatorname{single}$ applied to $p$, $i$ and $a$ is an element of $\mathrm{PiLp}$ applied to $p$ and $x_{1}$ defined as $\operatorname{toLp}$ applied to $p$ and $\operatorname{single}$ applied to $i$ and $a$.
PiLp.sumPiLpEquivProdLpPiLpdefMathlib.Analysis.Normed.Lp.PiLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{4}$ be a function from elements of $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$ to sets. Then $\operatorname{sumPiLpEquivProdLpPiLp}$ applied to $p$ and $x_{4}$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements $i$ of $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$ to elements of $x_{4}$ applied to $i$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements $i_{1}$ of $x_{2}$ to elements of $x_{4}$ applied to $\operatorname{inl}$ applied to $i_{1}$ and $\mathrm{WithLp}$ applied to $p$ and the set of functions from elements $i_{2}$ of $x_{3}$ to elements of $x_{4}$ applied to $\operatorname{inr}$ applied to $i_{2}$.
IsometryEquiv.withLpProdAssocdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{withLpProdAssoc}$ applied to $p$, $x$, $x_{1}$ and $x_{2}$ is an isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
IsometryEquiv.withLpProdCommdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $x_{1}$ be sets. Then $\operatorname{withLpProdComm}$ applied to $p$, $x$ and $x_{1}$ is an isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$.
IsometryEquiv.withLpProdCongrdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be an isometry equivalence of $x$ and $x_{2}$. Let $g$ be an isometry equivalence of $x_{1}$ and $x_{3}$. Then $\operatorname{withLpProdCongr}$ applied to $p$, $f$ and $g$ is an isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.
IsometryEquiv.withLpProdUniquedefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $x_{1}$ be sets. Then $\operatorname{withLpProdUnique}$ applied to $p$, $x$ and $x_{1}$ is an isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.
IsometryEquiv.withLpUniqueProddefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $x_{1}$ be sets. Then $\operatorname{withLpUniqueProd}$ applied to $p$, $x$ and $x_{1}$ is an isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$ defined as the composition of $\operatorname{withLpProdComm}$ applied to $p$, $x$ and $x_{1}$ and $\operatorname{withLpProdUnique}$ applied to $p$, $x_{1}$ and $x$.
LinearIsometry.withLpProdMapdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a linear isometry of $x_{1}$ and $x_{3}$. Let $g$ be a linear isometry of $x_{2}$ and $x_{4}$. Then $\operatorname{withLpProdMap}$ applied to $p$, $f$ and $g$ is a linear isometry of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{3}$ and $x_{4}$.
LinearIsometryEquiv.withLpProdAssocdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be sets. Then $\operatorname{withLpProdAssoc}$ applied to $p$, $x$, $x_{1}$, $x_{2}$ and $x_{3}$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{3}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.
LinearIsometryEquiv.withLpProdCommdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{withLpProdComm}$ applied to $p$, $x$, $x_{1}$ and $x_{2}$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$.
LinearIsometryEquiv.withLpProdCongrdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a linear isometry equivalence of $x_{1}$ and $x_{3}$. Let $g$ be a linear isometry equivalence of $x_{2}$ and $x_{4}$. Then $\operatorname{withLpProdCongr}$ applied to $p$, $f$ and $g$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{3}$ and $x_{4}$.
LinearIsometryEquiv.withLpProdUniquedefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{withLpProdUnique}$ applied to $p$, $x$, $x_{1}$ and $x_{2}$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{1}$.
LinearIsometryEquiv.withLpUniqueProddefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{withLpUniqueProd}$ applied to $p$, $x$, $x_{1}$ and $x_{2}$ is a linear isometry equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{2}$ defined as the composition of $\operatorname{withLpProdComm}$ applied to $p$, $x$, $x_{1}$ and $x_{2}$ and $\operatorname{withLpProdUnique}$ applied to $p$, $x$, $x_{2}$ and $x_{1}$.
WithLp.fstdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the projection on the first coordinate in x2 (from the docstring)
English
Let $x_{2}$ be an element of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the projection on the first coordinate in $x_{2}$ is an element of $x$ defined as $\ProdfstMACRoZ {\operatorname{ofLp} (x_{2})}$.
WithLp.fstLdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the first component of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the first component of $p$ is a continuous linear map of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{1}$.
WithLp.fstₗdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the first component of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the first component of $p$ is a linear map of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{1}$.
WithLp.homeomorphProddefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the homeomorphism product of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$ and $x_{1}$ be sets. Then the homeomorphism product of $p$ is a homeomorphism of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
WithLp.idemFstdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
$\operatorname{idemFst}$ is an end of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
WithLp.idemSnddefMathlib.Analysis.Normed.Lp.ProdLp, function or constantEnglish
$\operatorname{idemSnd}$ is an end of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
WithLp.prodContinuousLinearEquivdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the product continuous linear equivalence of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the product continuous linear equivalence of $p$ is a continuous linear equivalence of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the linear equivalence of $p$, $\mathrm{WithLp\_\_prod\_continuous\_ofLp}$ applied to $p$, $x_{1}$ and $x_{2}$ and $\mathrm{WithLp\_\_prod\_continuous\_toLp}$ applied to $p$, $x_{1}$ and $x_{2}$.
WithLp.prodEquivₗᵢdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the product equivalence (from the name)
English
The product equivalence is a linear isometry equivalence of $\mathrm{WithLp}$ applied to the top and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
WithLp.snddefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the projection on the second coordinate in x2 (from the docstring)
English
Let $x_{2}$ be an element of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the projection on the second coordinate in $x_{2}$ is an element of $x_{1}$ defined as $\ProdsndMACRoAA {\operatorname{ofLp} (x_{2})}$.
WithLp.sndLdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the second component of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the second component of $p$ is a continuous linear map of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{2}$.
WithLp.sndₗdefMathlib.Analysis.Normed.Lp.ProdLp, function or constantWording
the second component of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the second component of $p$ is a linear map of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{2}$.
LinearEquiv.withLpCongrdefMathlib.Analysis.Normed.Lp.WithLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a linear equivalence of $V$ and $\mathrm{V'}$. Then $\operatorname{withLpCongr}$ applied to $p$ and $f$ is a linear equivalence of $\mathrm{WithLp}$ applied to $p$ and $V$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{V'}$ defined as the composition of the linear equivalence of $p$ and the composition of $f$ and the inverse of the linear equivalence of $p$.
LinearMap.withLpMapdefMathlib.Analysis.Normed.Lp.WithLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a linear map of $V$ and $\mathrm{V'}$. Then $\operatorname{withLpMap}$ applied to $p$ and $f$ is a linear map of $\mathrm{WithLp}$ applied to $p$ and $V$ and $\mathrm{WithLp}$ applied to $p$ and $\mathrm{V'}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $p$ and the composition of $f$ and $\operatorname{toLinearMap}$ applied to the linear equivalence of $p$.
WithLpstructureMathlib.Analysis.Normed.Lp.WithLp, typeEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $V$ be a set. Then the elements of $\mathrm{WithLp}$ applied to $p$ and $V$ are a basic type.
WithLp.addEquivdefMathlib.Analysis.Normed.Lp.WithLp, function or constantWording
the additive equivalence of p and V (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $V$ be a set. Then the additive equivalence of $p$ and $V$ is an additive equivalence of $\mathrm{WithLp}$ applied to $p$ and $V$ and $V$.
WithLp.congrdefMathlib.Analysis.Normed.Lp.WithLp, function or constantWording
the congruence of p and f (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be an equivalence from $V$ to $\mathrm{V'}$. Then the congruence of $p$ and $f$ is an element of $\EquivMACRoAE {\mathrm{WithLp} (p , V)}{\mathrm{WithLp} (p , \mathrm{V'})}$ defined as the composition of the equivalence of $p$ and $V$ and the composition of $f$ and the inverse of the equivalence of $p$ and $\mathrm{V'}$.
WithLp.equivdefMathlib.Analysis.Normed.Lp.WithLp, function or constantWording
the equivalence of p and V (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $V$ be a set. Then the equivalence of $p$ and $V$ is an element of $\EquivMACRoAE {\mathrm{WithLp} (p , V)}{V}$.
WithLp.linearEquivdefMathlib.Analysis.Normed.Lp.WithLp, function or constantWording
the linear equivalence of p (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $K$ and $V$ be sets. Then the linear equivalence of $p$ is a linear equivalence of $\mathrm{WithLp}$ applied to $p$ and $V$ and $V$.
WithLp.mapdefMathlib.Analysis.Normed.Lp.WithLp, function or constantWording
the map of f and x (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $f$ be a function from elements of $V$ to elements of $\mathrm{V'}$. Let $x$ be an element of $\mathrm{WithLp}$ applied to $p$ and $V$. Then the map of $f$ and $x$ is an element of $\mathrm{WithLp}$ applied to $p$ and $\mathrm{V'}$ defined as $\operatorname{toLp}$ applied to $p$ and $f$ applied to $\operatorname{ofLp}$ applied to $x$.
WithLp.ofLpdefMathlib.Analysis.Normed.Lp.WithLp, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WithLp}$ applied to $p$ and $V$. Then $\operatorname{ofLp}$ applied to $\mathrm{self}$ is an element of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
lp.dualPairingdefMathlib.Analysis.Normed.Lp.lpHolder, function or constantWording
the dual pairing of q and B (from the name)
English
Let $p$ and $q$ be elements of $\mathrm{ENNReal}$. Let $B$ be a function from elements $i_{1}$ of $x$ to continuous linear maps of $E$ applied to $i_{1}$ and the set of continuous linear maps of $F$ applied to $i_{1}$ and $H$ such that for all elements $i$ of $x$, the norm of $B$ applied to $i$ is less than or equal to $\operatorname{toReal}$ applied to $K$. Then the dual pairing of $q$ and $i_{1}$ is a continuous linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{9}})}$ and the set of continuous linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\mathrm{lp} (F , q)}{x_{10}})}$ and $H$ defined as the function that maps $\mathrm{hBK}$ to the composition of the postcomposition of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{lp} (F , q)}{x_{9}})}$ and the sum continuous linear map of $x$ and $H$ and the Holder of $1$ and $i_{1}$.
lp.holderdefMathlib.Analysis.Normed.Lp.lpHolder, function or constantWording
the Holder of hBK and e (from the name)
English
Let $r$ be an element of $\mathrm{ENNReal}$. Let $B$ be a function from elements $i_{1}$ of $x$ to continuous linear maps of $E$ applied to $i_{1}$ and the set of continuous linear maps of $F$ applied to $i_{1}$ and $G$ applied to $i_{1}$ such that for all elements $i$ of $x$, the norm of $B$ applied to $i$ is less than or equal to $K$. Let $e$ be an element of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{11}})}$. Let $f$ be an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\mathrm{lp} (F , q)}{x_{10}})}$. Then the Holder of $\mathrm{hBK}$ and $e$ is an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{lp} (G , r)}{x_{9}})}$ defined as the function that maps $i$ to $\operatorname{coe}$ applied to $i_{1}$ applied to $f$, $f$ and $f$.
lp.holderLdefMathlib.Analysis.Normed.Lp.lpHolder, function or constantWording
the Holder of r and B (from the name)
English
Let $r$ be an element of $\mathrm{ENNReal}$. Let $B$ be a function from elements $i_{1}$ of $x$ to continuous linear maps of $E$ applied to $i_{1}$ and the set of continuous linear maps of $F$ applied to $i_{1}$ and $G$ applied to $i_{1}$ such that for all elements $i$ of $x$, the norm of $B$ applied to $i$ is less than or equal to $\operatorname{toReal}$ applied to $K$. Then the Holder of $r$ and $i_{1}$ is a continuous linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{9}})}$ and the set of continuous linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\mathrm{lp} (F , q)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\mathrm{lp} (G , r)}{x_{11}})}$.
lp.holderₗdefMathlib.Analysis.Normed.Lp.lpHolder, function or constantWording
the Holder of r and B (from the name)
English
Let $r$ be an element of $\mathrm{ENNReal}$. Let $B$ be a function from elements $i_{1}$ of $x$ to continuous linear maps of $E$ applied to $i_{1}$ and the set of continuous linear maps of $F$ applied to $i_{1}$ and $G$ applied to $i_{1}$ such that for all elements $i$ of $x$, the norm of $B$ applied to $i$ is less than or equal to $K$. Then the Holder of $r$ and $i_{1}$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{9}})}$ and the set of linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\mathrm{lp} (F , q)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\mathrm{lp} (G , r)}{x_{11}})}$.
lp.mapCLMdefMathlib.Analysis.Normed.Lp.lpHolder, function or constantWording
the map continuous linear map of p and T (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $T$ be a function from elements $i_{1}$ of $x$ to continuous linear maps of $E$ applied to $i_{1}$ and $F$ applied to $i_{1}$. Assume that $0 \leq K$. Assume that for all elements $i$ of $x$, the norm of $T$ applied to $i$ is less than or equal to $K$. Then the map continuous linear map of $p$ and $i_{1}$ is a continuous linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\mathrm{lp} (F , p)}{x_{8}})}$.
MemℓpdefMathlib.Analysis.Normed.Lp.lpSpace, predicateEnglish
Let $f$ be a function from elements $i$ of $x$ to elements of $E$ applied to $i$. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{Mem\_u2113\_p}$ holds for $i$, $f$ and $p$, if $\iteMACRoG {\EqtMACRoH {f}{0}}{\operatorname{Finite} (\operatorname{ofPred} (\lambda i . \mathrm{Neq} (i (i), 0)))}{\iteMACRoG {(\EqtMACRoH {f}{\operatorname{top}})}{\mathrm{BddAbove} (\operatorname{range} (\lambda i_{1} . \operatorname{norm} (i (i_{1}))))}{\mathrm{Summable} (\lambda i_{2} . \operatorname{norm} (i (i_{2}))^ {\operatorname{toReal} (f)}, \operatorname{unconditional} (x))}}$.
PreLpdefMathlib.Analysis.Normed.Lp.lpSpace, typeEnglish
Let $E$ be a function from elements of $x$ to sets. Then an element of $\mathrm{PreLp}$ applied to $E$ is an element of the function that maps $E$ to the set of functions from elements $i$ of $x$ to elements of $E$ applied to $i$.
lpdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $E$ be a function from elements of $x$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{lp}$ applied to $E$ and $p$ is an additive subgroup of $\mathrm{PreLp}$ applied to $E$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $f$ to $\mathrm{Mem\_u2113\_p}$ applied to $f$ and $p$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Mem\_u2113\_p\_\_add}$ and $\mathrm{zero\_mem\_u2113\_p}$ and the function that maps $x_{4}$ to $\mathrm{Mem\_u2113\_p\_\_neg}$.
lp.coeFnAddMonoidHomdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the coercion function additive monoid homomorphism of E and p (from the name)
English
Let $E$ be a function from elements of $x$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Then the coercion function additive monoid homomorphism of $E$ and $p$ is an additive monoid homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{2}})}$ and the set of functions from elements $i$ of $x$ to elements of $E$ applied to $i$.
lp.evalCLMdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the evaluation continuous linear map of p and i (from the name)
English
Let $x$ be a set. Let $E$ be a function from elements of $x_{1}$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x_{1}$. Then the evaluation continuous linear map of $p$ and $i$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{5}})}$ and $E$ applied to $i$.
lp.evalₗdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the evaluation of p and i (from the name)
English
Let $E$ be a function from elements of $x_{1}$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x_{1}$. Then the evaluation of $p$ and $i$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{5}})}$ and $E$ applied to $i$.
lp.linearMapOfLEdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the linear map of E (from the name)
English
Let $x$ be a set. Let $E$ be a function from elements of $x_{1}$ to sets. Assume that $p \leq q$. Then the linear map of $E$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (E , q)}{x_{6}})}$.
lp.lsingledefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x_{1}$. Then $\operatorname{lsingle}$ applied to $p$ and $i$ is a linear map of $E$ applied to $i$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{6}})}$.
lp.singledefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x$. Let $a$ be an element of $E$ applied to $i$. Then $\operatorname{single}$ applied to $p$, $i$ and $a$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{3}})}$ defined as $\operatorname{single}$ applied to $i$ and $a$.
lp.singleAddMonoidHomdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the single additive monoid homomorphism of p and i (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x$. Then the single additive monoid homomorphism of $p$ and $i$ is an additive monoid homomorphism of $E$ applied to $i$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{3}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $p$ and $i$ and $\mathrm{lp\_\_single\_zero}$ applied to $p$ and $i$ and $\mathrm{lp\_\_single\_add}$ applied to $p$ and $i$.
lp.singleContinuousAddMonoidHomdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the single continuous additive monoid homomorphism of p and i (from the name)
English
Let $E$ be a function from elements of $x$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x$. Then the single continuous additive monoid homomorphism of $p$ and $i$ is a continuous additive monoid homomorphism of $E$ applied to $i$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{3}})}$.
lp.singleContinuousLinearMapdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the single continuous linear map of p and i (from the name)
English
Let $x$ be a set. Let $E$ be a function from elements of $x_{1}$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $i$ be an element of $x_{1}$. Then the single continuous linear map of $p$ and $i$ is a continuous linear map of $E$ applied to $i$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{6}})}$.
lp.toNormdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the norm of x2 (from the name)
English
Let $x_{2}$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (E , p)}{x_{5}})}$. Then the norm of $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . \Real , p)}{x_{3}})}$ defined as the function that maps $i$ to the norm of $i$.
lp.tsumCLMdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the sum continuous linear map of x1 and E (from the name)
English
Let $x$, $x_{1}$ and $E$ be sets. Then the sum continuous linear map of $x_{1}$ and $E$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{6} . E , 1)}{x_{5}})}$ and $E$.
lp.zeroBasisdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantWording
the zero basis (from the name)
English
The zero basis is a basis of $x$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . x , 0)}{x_{3}})}$.
lpInftySubalgebradefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $x$ be a set. Let $B$ be a function from elements of $I$ to sets. Then $\mathrm{lpInftySubalgebra}$ applied to $x$ and $B$ is a subalgebra of $x$ and $\mathrm{PreLp}$ applied to $B$.
lpInftySubringdefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $B$ be a function from elements of $I$ to sets. Then $\mathrm{lpInftySubring}$ applied to $B$ is a subring of $\mathrm{PreLp}$ applied to $B$.
lpSubmoduledefMathlib.Analysis.Normed.Lp.lpSpace, function or constantEnglish
Let $x$ be a set. Let $E$ be a function from elements of $x_{1}$ to sets. Let $p$ be an element of $\mathrm{ENNReal}$. Then $\mathrm{lpSubmodule}$ applied to $x$, $E$ and $p$ is a submodule of $x$ and $\mathrm{PreLp}$ applied to $E$.
AlternatingMap.mkContinuousdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $f$ be an alternating map of $F$ and $x_{1}$. Let $C$ be an element of $\Real$ such that for all functions $m$ from elements of $x_{1}$ to elements of $E$, $\operatorname{norm} (f (m))\leq C \times \FinsetProd {\FinsetunivMACRoAC}{i}{\operatorname{norm} (m (i))}$. Then $\operatorname{mkContinuous}$ applied to $f$, $C$ and $H$ is a continuous alternating map of $F$ and $x_{1}$.
AlternatingMap.mkContinuousAlternatingdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $f$ be an alternating map of the set of alternating maps of $G$ and $x_{10}$ and $x_{1}$. Let $C$ be an element of $\Real$ such that for all functions $x_{12}$ from elements of $x_{1}$ to elements of $E$, for all functions $x_{13}$ from elements of $x_{10}$ to elements of $F$, $\operatorname{norm} (\operatorname{coe} (f , x_{12} , x_{13}))\leq C \times \FinsetProd {\FinsetunivMACRoAC}{i}{\operatorname{norm} (x_{12} (i))}\times \FinsetProd {\FinsetunivMACRoAC}{i_{1}}{\operatorname{norm} (x_{13} (i_{1}))}$. Then $\operatorname{mkContinuousAlternating}$ applied to $f$, $C$ and $H$ is a continuous alternating map of the set of continuous alternating maps of $G$ and $x_{10}$ and $x_{1}$.
AlternatingMap.mkContinuousLineardefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $f$ be a linear map of $F$ and the set of alternating maps of $G$ and $x_{1}$. Let $C$ be an element of $\Real$ such that for all elements $x_{10}$ of $F$, for all functions $m$ from elements of $x_{1}$ to elements of $E$, $\operatorname{norm} (\operatorname{coe} (f , x_{10} , m))\leq C \times \operatorname{norm} (x_{10})\times \FinsetProd {\FinsetunivMACRoAC}{i}{\operatorname{norm} (m (i))}$. Then $\operatorname{mkContinuousLinear}$ applied to $f$, $C$ and $H$ is a continuous linear map of $F$ and the set of continuous alternating maps of $G$ and $x_{1}$.
ContinuousAlternatingMap.constOfIsEmptyLIEdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantWording
the constant of F and x1 (from the name)
English
Let $x$, $E$, $F$ and $x_{1}$ be sets. Then the constant of $F$ and $x_{1}$ is a linear isometry equivalence of $F$ and the set of continuous alternating maps of $F$ and $x_{1}$.
ContinuousAlternatingMap.fderivCompContinuousLinearMapdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantWording
the derivative composition continuous linear map of f and g (from the name)
English
Let $f$ be a continuous alternating map of $G$ and $x_{1}$. Let $g$ be a continuous linear map of $E$ and $F$. Then the derivative composition continuous linear map of $f$ and $g$ is a continuous linear map of the set of continuous linear maps of $E$ and $F$ and the set of continuous alternating maps of $G$ and $x_{1}$.
ContinuousAlternatingMap.fderivCompContinuousLinearMapCLMdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantWording
the derivative composition continuous linear map continuous linear map of G and g (from the name)
English
Let $G$ be a set. Let $g$ be a continuous linear map of $E$ and $F$. Then the derivative composition continuous linear map continuous linear map of $G$ and $g$ is a continuous linear map of the set of continuous alternating maps of $G$ and $x_{1}$ and the set of continuous linear maps of the set of continuous linear maps of $E$ and $F$ and the set of continuous alternating maps of $G$ and $x_{1}$.
ContinuousAlternatingMap.ofSubsingletonLIEdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantWording
the continuous alternating map of i (from the name)
English
Let $i$ be an element of $x_{1}$. Then the continuous alternating map of $i$ is a linear isometry equivalence of the set of continuous linear maps of $E$ and $F$ and the set of continuous alternating maps of $F$ and $x_{1}$.
ContinuousAlternatingMap.piLIEdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $x$ and $E$ be sets. Then $\operatorname{piLIE}$ applied to $x$ and $E$ is a linear isometry equivalence of the set of functions from elements $\mathrm{i'}$ of $x_{6}$ to continuous alternating maps of $F$ applied to $\mathrm{i'}$ and $x_{1}$ and the set of continuous alternating maps of the set of functions from elements $i$ of $x_{6}$ to elements of $F$ applied to $i$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the product linear equivalence and $\mathrm{ContinuousAlternatingMap\_\_opNorm\_pi}$.
ContinuousAlternatingMap.prodLIEdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $x$, $E$, $F$ and $G$ be sets. Then $\operatorname{prodLIE}$ applied to $x$, $E$, $F$ and $G$ is a linear isometry equivalence of $\mathrm{Prod}$ applied to the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $G$ and $x_{1}$ and the set of continuous alternating maps of $\mathrm{Prod}$ applied to $F$ and $G$ and $x_{1}$.
ContinuousAlternatingMap.restrictScalarsLIdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $x_{8}$ be a set. Then $\operatorname{restrictScalarsLI}$ applied to $x_{8}$ is a linear isometry of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $F$ and $x_{1}$.
ContinuousAlternatingMap.toContinuousMultilinearMapLIdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
$\operatorname{toContinuousMultilinearMapLI}$ is a linear isometry of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous multilinear maps of the function that maps $x_{8}$ to $E$ and $F$.
ContinuousLinearMap.flipAlternatingdefMathlib.Analysis.Normed.Module.Alternating.Basic, function or constantEnglish
Let $f$ be a continuous linear map of $F$ and the set of continuous alternating maps of $G$ and $x_{1}$. Then $\operatorname{flipAlternating}$ applied to $f$ is a continuous alternating map of the set of continuous linear maps of $F$ and $G$ and $x_{1}$.
ContinuousAlternatingMap.curryLeftdefMathlib.Analysis.Normed.Module.Alternating.Curry, function or constantWording
the left curry of f (from the name)
English
Let $f$ be a continuous alternating map of $F$ and $\mathrm{Fin}$ applied to $n + 1$. Then the left curry of $f$ is a continuous linear map of $E$ and the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n$.
ContinuousAlternatingMap.curryLeftLIdefMathlib.Analysis.Normed.Module.Alternating.Curry, function or constantEnglish
$\operatorname{curryLeftLI}$ is a linear isometry of the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n + 1$ and the set of continuous linear maps of $E$ and the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $f$ to the left curry of $f$ and $\mathrm{ContinuousAlternatingMap\_\_curryLeft\_add}$ and $\mathrm{ContinuousAlternatingMap\_\_curryLeft\_smul}$ and $\mathrm{ContinuousAlternatingMap\_\_norm\_curryLeft}$.
ContinuousAlternatingMap.alternatizeUncurryFindefMathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin, function or constantEnglish
Let $f$ be a continuous linear map of $E$ and the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{alternatizeUncurryFin}$ applied to $f$ is a continuous alternating map of $F$ and $\mathrm{Fin}$ applied to $n + 1$ defined as $\operatorname{alternatizeUncurryFinCLM}$ applied to $x$, $E$, $F$ and $f$.
ContinuousAlternatingMap.alternatizeUncurryFinCLMdefMathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin, function or constantEnglish
Let $x$, $E$ and $F$ be sets. Then $\operatorname{alternatizeUncurryFinCLM}$ applied to $x$, $E$ and $F$ is a continuous linear map of the set of continuous linear maps of $E$ and the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n$ and the set of continuous alternating maps of $F$ and $\mathrm{Fin}$ applied to $n + 1$.
Homeomorph.unitBalldefMathlib.Analysis.Normed.Module.Ball.Homeomorph, function or constantWording
the unit ball (from the name)
English
The unit ball is a homeomorphism of $E$ and the set of elements of the ball of $0$ and $1$ defined as the composition of the inverse of the universal set of $E$ and the homeomorphism source target of the universal set unit ball.
OpenPartialHomeomorph.unitBallBalldefMathlib.Analysis.Normed.Module.Ball.Homeomorph, function or constantWording
the unit ball ball of c and r (from the name)
English
Let $c$ be an element of $P$. Let $r$ be a real number such that $0 < r$. Then the unit ball ball of $c$ and $r$ is an open partial homeomorphism of $E$ and $P$.
OpenPartialHomeomorph.univBalldefMathlib.Analysis.Normed.Module.Ball.Homeomorph, function or constantWording
the universal set ball of c and r (from the name)
English
Let $c$ be an element of $P$. Let $r$ be a real number. Then the universal set ball of $c$ and $r$ is an open partial homeomorphism of $E$ and $P$.
OpenPartialHomeomorph.univUnitBalldefMathlib.Analysis.Normed.Module.Ball.Homeomorph, function or constantWording
the universal set unit ball (from the name)
English
The universal set unit ball is an open partial homeomorphism of $E$ and $E$.
homeomorphSphereProddefMathlib.Analysis.Normed.Module.Ball.RadialEquiv, function or constantWording
the homeomorphism sphere product of r (from the name)
English
Let $E$ be a set. Let $r$ be a real number such that $0 < r$. Then the homeomorphism sphere product of $r$ is a homeomorphism of the set of elements of the complement of $\operatorname{singleton}$ applied to $0$ and $\mathrm{Prod}$ applied to the set of elements of the sphere of $0$ and $r$ and the set of elements of $\operatorname{Ioi}$ applied to $0$.
homeomorphUnitSphereProddefMathlib.Analysis.Normed.Module.Ball.RadialEquiv, function or constantWording
the homeomorphism unit sphere product of E (from the name)
English
Let $E$ be a set. Then the homeomorphism unit sphere product of $E$ is a homeomorphism of the set of elements of the complement of $\operatorname{singleton}$ applied to $0$ and $\mathrm{Prod}$ applied to the set of elements of the sphere of $0$ and $1$ and the set of elements of $\operatorname{Ioi}$ applied to $0$.
GeneralSchauderBasisstructureMathlib.Analysis.Normed.Module.Bases, typeEnglish
Let $x$, $x_{1}$ and $X$ be sets. Let $L$ be a summation filter of $x$. Then the elements of $\mathrm{GeneralSchauderBasis}$ applied to $x$, $x_{1}$, $X$ and $L$ are a basic type.
GeneralSchauderBasis.basisdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the basis of self and x5 (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{GeneralSchauderBasis}$ applied to $x$, $x_{1}$, $X$ and $L$. Let $x_{5}$ be an element of $x$. Then the basis of $\mathrm{self}$ and $x_{5}$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.
GeneralSchauderBasis.coorddefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the coordinate of self and x5 (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{GeneralSchauderBasis}$ applied to $x$, $x_{1}$, $X$ and $L$. Let $x_{5}$ be an element of $x$. Then the coordinate of $\mathrm{self}$ and $x_{5}$ is a strong dual of $x_{1}$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{5}$.
GeneralSchauderBasis.projdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the projection of b and A (from the name)
English
Let $b$ be an element of $\mathrm{GeneralSchauderBasis}$ applied to $x_{4}$, $x$, $X$ and $L$. Let $A$ be a finite set of $x_{4}$. Then the projection of $b$ and $A$ is a continuous linear map of $X$ and $X$ defined as $\FinsetSum {A}{i}{\operatorname{smulRight} (\operatorname{coord} (b , i), \operatorname{basis} (b , i))}$.
SchauderBasisdefMathlib.Analysis.Normed.Module.Bases, typeEnglish
Let $x$ and $X$ be sets. Then an element of $\mathrm{SchauderBasis}$ applied to $x$ and $X$ is an element of the function that maps $x$ and $X$ to $\mathrm{GeneralSchauderBasis}$ applied to $\Natural$, $x$, $X$ and $\operatorname{conditional}$ applied to $\Natural$.
SchauderBasis.RankOneDecompositionstructureMathlib.Analysis.Normed.Module.Bases, typeWording
rank one decomposition of x and X (from the name)
English
Let $x$ and $X$ be sets. Then the rank one decompositions of $x$ and $X$ are a basic type.
SchauderBasis.RankOneDecomposition.PdefMathlib.Analysis.Normed.Module.Bases, function or constantEnglish
Let $\mathrm{self}$ be a rank one decomposition of $x$ and $X$. Let $x_{4}$ be a natural number. Then $\operatorname{P}$ applied to $\mathrm{self}$ and $x_{4}$ is a continuous linear map of $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
SchauderBasis.RankOneDecomposition.basisdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the basis of D (from the name)
English
Let $D$ be a rank one decomposition of $x$ and $X$. Then the basis of $D$ is an element of $\mathrm{SchauderBasis}$ applied to $x$ and $X$.
SchauderBasis.RankOneDecomposition.basisCoeffdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the basis coefficient of n and x4 (from the name)
English
Let $D$ be a rank one decomposition of $x$ and $X$. Let $n$ be a natural number. Let $x_{4}$ be an element of $X$. Then the basis coefficient of $n$ and $x_{4}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{SchauderBasis\_\_RankOneDecomposition\_\_exists\_coeff}$ applied to $D$, $n$ and $x_{4}$.
SchauderBasis.RankOneDecomposition.edefMathlib.Analysis.Normed.Module.Bases, function or constantEnglish
Let $\mathrm{self}$ be a rank one decomposition of $x$ and $X$. Let $x_{4}$ be a natural number. Then $\operatorname{e}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.
SchauderBasis.enormProjBounddefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the extended norm projection bound of b (from the name)
English
Let $b$ be an element of $\mathrm{SchauderBasis}$ applied to $x$ and $X$. Then the extended norm projection bound of $b$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $n$ to the extended norm of the projection of $b$ and $n$.
SchauderBasis.nnnormProjBounddefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the norm projection bound of b (from the name)
English
Let $b$ be an element of $\mathrm{SchauderBasis}$ applied to $x$ and $X$. Then the norm projection bound of $b$ is an element of $\mathrm{NNReal}$ defined as the supremum of the function that maps $n$ to the norm of the projection of $b$ and $n$.
SchauderBasis.projdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the projection of b and n (from the name)
English
Let $b$ be an element of $\mathrm{SchauderBasis}$ applied to $x$ and $X$. Let $n$ be a natural number. Then the projection of $b$ and $n$ is a continuous linear map of $X$ and $X$ defined as the projection of $b$ and the range of $n$.
SchauderBasis.succSubdefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the difference operator of P and n (from the docstring)
English
Let $P$ be a function from natural numbers to continuous linear maps of $X$ and $X$. Let $n$ be a natural number. Then the difference operator of $P$ and $n$ is a continuous linear map of $X$ and $X$ defined as $P (n + 1)- P (n)$.
UnconditionalSchauderBasisdefMathlib.Analysis.Normed.Module.Bases, typeEnglish
Let $x$, $x_{1}$ and $X$ be sets. Then an element of $\mathrm{UnconditionalSchauderBasis}$ applied to $x$, $x_{1}$ and $X$ is an element of the function that maps $x$, $x_{1}$ and $X$ to $\mathrm{GeneralSchauderBasis}$ applied to $x$, $x_{1}$, $X$ and $\operatorname{unconditional}$ applied to $x$.
UnconditionalSchauderBasis.enormProjBounddefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the extended norm projection bound of b (from the name)
English
Let $b$ be an element of $\mathrm{UnconditionalSchauderBasis}$ applied to $x_{4}$, $x$ and $X$. Then the extended norm projection bound of $b$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $A$ to the extended norm of the projection of $b$ and $A$.
UnconditionalSchauderBasis.nnnormProjBounddefMathlib.Analysis.Normed.Module.Bases, function or constantWording
the norm projection bound of b (from the name)
English
Let $b$ be an element of $\mathrm{UnconditionalSchauderBasis}$ applied to $x_{4}$, $x$ and $X$. Then the norm projection bound of $b$ is an element of $\mathrm{NNReal}$ defined as the supremum of the function that maps $A$ to the norm of the projection of $b$ and $A$.
NormedAlgebraclassMathlib.Analysis.Normed.Module.Basic, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{NormedAlgebra}$ holds for $x$ and $x_{1}$.
NormedSpaceclassMathlib.Analysis.Normed.Module.Basic, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{NormedSpace}$ holds for $x$ and $E$.
NormedSpace.CorestructureMathlib.Analysis.Normed.Module.Basic, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\operatorname{Core}$ holds for $x$ and $E$.
SeminormedSpace.CorestructureMathlib.Analysis.Normed.Module.Basic, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\operatorname{Core}$ holds for $x$ and $E$.
ContinuousLinearMap.equivProdOfSurjectiveOfIsCompldefMathlib.Analysis.Normed.Module.Complemented, function or constantWording
the equivalence product of f and g (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$. Let $g$ be a continuous linear map of $E$ and $G$. Assume that the range of $\operatorname{toLinearMap}$ applied to $f$ is equal to the top. Assume that the range of $\operatorname{toLinearMap}$ applied to $g$ is equal to the top. Assume that $\mathrm{IsCompl}$ holds for the kernel of $\operatorname{toLinearMap}$ applied to $f$ and the kernel of $\operatorname{toLinearMap}$ applied to $g$. Then the equivalence product of $f$ and $g$ is a continuous linear equivalence of $E$ and $\mathrm{Prod}$ applied to $F$ and $G$.
ContinuousLinearMap.HasLeftInversedefMathlib.Analysis.Normed.Module.ContinuousInverse, predicateWording
f has left inverses (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$. Then $f$ has left inverses, if there exists a continuous linear map $g$ of $F$ and $E$, such that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$.
ContinuousLinearMap.HasLeftInverse.complementdefMathlib.Analysis.Normed.Module.ContinuousInverse, function or constantWording
the complement of h (from the name)
English
Assume that $f$ has left inverses. Then the complement of $h$ is a submodule of $R$ and $F$ defined as the complement of $\mathrm{ContinuousLinearMap\_\_HasLeftInverse\_\_closedComplemented\_range}$ applied to $h$.
ContinuousLinearMap.HasLeftInverse.leftInversedefMathlib.Analysis.Normed.Module.ContinuousInverse, function or constantWording
the left inverse of h (from the name)
English
Assume that $f$ has left inverses. Then the left inverse of $h$ is a continuous linear map of $F$ and $E$ defined as $\operatorname{choose}$ applied to $h$.
ContinuousLinearMap.HasRightInversedefMathlib.Analysis.Normed.Module.ContinuousInverse, predicateWording
f has right inverses (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$. Then $f$ has right inverses, if there exists a continuous linear map $g$ of $F$ and $E$, such that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$.
ContinuousLinearMap.HasRightInverse.rightInversedefMathlib.Analysis.Normed.Module.ContinuousInverse, function or constantWording
the right inverse of h (from the name)
English
Assume that $f$ has right inverses. Then the right inverse of $h$ is a continuous linear map of $F$ and $E$ defined as $\operatorname{choose}$ applied to $h$.
NormedSpace.inclusionInDoubleDualdefMathlib.Analysis.Normed.Module.DoubleDual, function or constantWording
the inclusion of x and E (from the docstring)
English
Let $x$ and $E$ be sets. Then the inclusion of $x$ and $E$ is a continuous linear map of $E$ and the set of strong duals of $x$ and the set of strong duals of $x$ and $E$ defined as the continuous linear map of $x$ and $x$.
NormedSpace.inclusionInDoubleDualLidefMathlib.Analysis.Normed.Module.DoubleDual, function or constantWording
the inclusion of x (from the docstring)
English
Let $x$ be a set. Then the inclusion of $x$ is a linear isometry of $E$ and the set of strong duals of $x$ and the set of strong duals of $x$ and $E$.
NormedSpace.inclusionInDoubleDualWeakdefMathlib.Analysis.Normed.Module.DoubleDual, function or constantEnglish
Let $x$ and $X$ be sets. Then $\operatorname{inclusionInDoubleDualWeak}$ applied to $x$ and $X$ is a continuous linear map of the set of weak spaces of $x$ and $X$ and the set of weak duals of $x$ and the set of strong duals of $x$ and $X$.
AffineEquiv.toContinuousAffineEquivdefMathlib.Analysis.Normed.Module.FiniteDimension, function or constantWording
the continuous affine equivalence (from the name)
English
The continuous affine equivalence is an equivalence from the set of affine equivalences of $\mathrm{PE}$ and $\mathrm{PF}$ to the set of continuous affine equivalences of $\mathrm{PE}$ and $\mathrm{PF}$.
AffineIsometry.toAffineIsometryEquivdefMathlib.Analysis.Normed.Module.FiniteDimension, function or constantWording
the affine isometry equivalence of li and h2 (from the name)
English
Let $\mathrm{li}$ be an affine isometry of $x_{3}$ and $x_{4}$. Assume that the rank of $x$ and $x_{1}$ is equal to the rank of $x$ and $x_{2}$. Then the affine isometry equivalence of $\mathrm{li}$ and $h_{2}$ is an affine isometry equivalence of $x_{3}$ and $x_{4}$.
ContinuousLinearEquiv.piRingdefMathlib.Analysis.Normed.Module.FiniteDimension, function or constantWording
the product ring of x4 (from the name)
English
Let $x_{4}$ be a set. Then the product ring of $x_{4}$ is a continuous linear equivalence of the set of continuous linear maps of the set of functions from elements of $x_{4}$ to elements of $x$ and $E$ and the set of functions from elements of $x_{4}$ to elements of $E$.
LinearIsometry.toLinearIsometryEquivdefMathlib.Analysis.Normed.Module.FiniteDimension, function or constantWording
the linear isometry equivalence of li and h2 (from the name)
English
Let $\mathrm{li}$ be a linear isometry of $x$ and $F$. Assume that the rank of $x_{3}$ and $x$ is equal to the rank of $x_{3}$ and $F$. Then the linear isometry equivalence of $\mathrm{li}$ and $h_{2}$ is a linear isometry equivalence of $x$ and $F$.
lipschitzExtensionConstantdefMathlib.Analysis.Normed.Module.FiniteDimension, function or constantWording
the Lipschitz extension constant of #1 (from the name)
English
Let $\mathrm{E'}$ be a set. Then the Lipschitz extension constant of $\mathrm{E'}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Normed\_\_Module\_\_FiniteDimension\_\_3513382408\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $\mathrm{E'}$.
IsLprojectionstructureMathlib.Analysis.Normed.Module.MStructure, predicateEnglish
Let $X$ be a set. Let $P$ be an element of $M$. Then we can say that $\mathrm{IsLprojection}$ holds for $X$ and $P$.
IsMprojectionstructureMathlib.Analysis.Normed.Module.MStructure, predicateEnglish
Let $X$ be a set. Let $P$ be an element of $M$. Then we can say that $\mathrm{IsMprojection}$ holds for $X$ and $P$.
ContinuousLinearMap.flipMultilineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $f$ be a continuous linear map of $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$. Then $\operatorname{flipMultilinear}$ applied to $f$ is a continuous multilinear map of $E$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$.
ContinuousLinearMap.flipMultilinearEquivdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the flip multilinear equivalence of E (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the flip multilinear equivalence of $E$ is a continuous linear equivalence of the set of continuous linear maps of $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$ and the set of continuous multilinear maps of $E$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$.
ContinuousLinearMap.flipMultilinearEquivₗdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the flip multilinear equivalence of E (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the flip multilinear equivalence of $E$ is a linear equivalence of the set of continuous linear maps of $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$ and the set of continuous multilinear maps of $E$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $x$ and $G$ be sets. Let $E$ and $x_{2}$ be functions from elements of $x_{1}$ to sets. Then $\operatorname{compContinuousLinearMapContinuousMultilinear}$ applied to $x$, $E$, $x_{2}$ and $G$ is a continuous multilinear map of the function that maps $i$ to the set of continuous linear maps of $E$ applied to $i$ and $x_{2}$ applied to $i$ and the set of continuous linear maps of the set of continuous multilinear maps of $x_{2}$ and $G$ and the set of continuous multilinear maps of $E$ and $G$.
ContinuousMultilinearMap.compContinuousLinearMapLRightdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the right composition continuous linear map of g (from the name)
English
Let $g$ be a continuous multilinear map of $x_{2}$ and $G$. Then the right composition continuous linear map of $g$ is a continuous multilinear map of the function that maps $i$ to the set of continuous linear maps of $E$ applied to $i$ and $x_{2}$ applied to $i$ and the set of continuous multilinear maps of $E$ and $G$.
ContinuousMultilinearMap.compContinuousLinearMapMultilineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $x$ and $G$ be sets. Let $E$ and $x_{2}$ be functions from elements of $x_{1}$ to sets. Then $\operatorname{compContinuousLinearMapMultilinear}$ applied to $x$, $E$, $x_{2}$ and $G$ is a multilinear map of the function that maps $i$ to the set of continuous linear maps of $E$ applied to $i$ and $x_{2}$ applied to $i$ and the set of continuous linear maps of the set of continuous multilinear maps of $x_{2}$ and $G$ and the set of continuous multilinear maps of $E$ and $G$.
ContinuousMultilinearMap.fderivCompContinuousLinearMapdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the derivative composition continuous linear map of f and g (from the name)
English
Let $f$ be a continuous multilinear map of $x_{2}$ and $G$. Let $g$ be a function from elements $i_{1}$ of $x_{1}$ to continuous linear maps of $E$ applied to $i_{1}$ and $x_{2}$ applied to $i_{1}$. Then the derivative composition continuous linear map of $f$ and $i_{1}$ is a continuous linear map of the set of functions from elements $i$ of $x_{1}$ to continuous linear maps of $E$ applied to $i$ and $x_{2}$ applied to $i$ and the set of continuous multilinear maps of $E$ and $G$ defined as the function that maps $g$ to the derivative of the composition continuous multilinear map of $\operatorname{apply}$ applied to $x$, the set of continuous multilinear maps of $E$ and $G$ and $f$ and $\operatorname{compContinuousLinearMapContinuousMultilinear}$ applied to $x$, $E$, $x_{2}$ and $G$ and $i_{1}$.
ContinuousMultilinearMap.flipLineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $f$ be a continuous multilinear map of $E$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$. Then $\operatorname{flipLinear}$ applied to $f$ is a continuous linear map of $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$.
ContinuousMultilinearMap.iteratedFDerivdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the iterated derivative of k and x9 (from the name)
English
Let $f$ be a continuous multilinear map of $x_{2}$ and $G$. Let $k$ be an element of $\Natural$. Let $x_{9}$ be a function from elements $i_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $i_{1}$. Then the iterated derivative of $k$ and $i_{1}$ is a continuous multilinear map of the function that maps $x_{10}$ to the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$ and $G$ defined as the function that maps $x_{9}$ to $\FinsetSum {\FinsetunivMACRoAC}{e}{\operatorname{iteratedFDerivComponent} (f , \operatorname{toEquivRange} (e), \operatorname{compRightL} (x , x_{2} , \lambda a_{3} . \mathrm{not} (\MembershipmemMACRoT {\operatorname{range} (\operatorname{coe} (e))}{a_{3}}), i_{1}))}{x_{9}}$.
ContinuousMultilinearMap.iteratedFDerivComponentdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the iterated derivative component of f and e (from the name)
English
Let $f$ be a continuous multilinear map of $x_{2}$ and $G$. Let $e$ be an equivalence from $x_{9}$ to the set of elements of $s$. Then the iterated derivative component of $f$ and $e$ is a continuous multilinear map of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of continuous multilinear maps of the function that maps $x_{12}$ to the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $i_{1}$ and $G$.
ContinuousMultilinearMap.ofSubsingletonₗᵢdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the continuous multilinear map of i (from the name)
English
Let $x$ and $G$ be sets. Let $i$ be an element of $x_{1}$. Then the continuous multilinear map of $i$ is a linear isometry equivalence of the set of continuous linear maps of $G$ and $\mathrm{G'}$ and the set of continuous multilinear maps of the function that maps $x_{8}$ to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.opNormdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the operator norm of f (from the docstring)
English
Let $f$ be a continuous multilinear map of $E$ and $G$. Then the operator norm of $f$ is an element of $\Real$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that $0 \leq c$ and for all functions $m$ from elements $i_{1}$ of $x_{1}$ to elements of $E$ applied to $i_{1}$, $\operatorname{norm} (f (m))\leq c \times \FinsetProd {\FinsetunivMACRoAC}{i}{\operatorname{norm} (m (i))}$.
ContinuousMultilinearMap.piFieldEquivdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the product field equivalence of x1 and G (from the name)
English
Let $x$, $x_{1}$ and $G$ be sets. Then the product field equivalence of $x_{1}$ and $G$ is a linear isometry equivalence of $G$ and the set of continuous multilinear maps of the function that maps $x_{6}$ to $x$ and $G$.
ContinuousMultilinearMap.piₗᵢdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the product of x and E (from the name)
English
Let $x$ be a set. Let $E$ be a function from elements of $x_{1}$ to sets. Then the product of $x$ and $E$ is a linear isometry equivalence of the set of functions from elements $\mathrm{i'}$ of $x_{6}$ to continuous multilinear maps of $E$ and $\mathrm{E'}$ applied to $\mathrm{i'}$ and the set of continuous multilinear maps of $E$ and the set of functions from elements $i$ of $x_{6}$ to elements of $\mathrm{E'}$ applied to $i$.
ContinuousMultilinearMap.prodLdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the product of E (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the product of $E$ is a linear isometry equivalence of $\mathrm{Prod}$ applied to the set of continuous multilinear maps of $E$ and $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$ and the set of continuous multilinear maps of $E$ and $\mathrm{Prod}$ applied to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.restrdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the restriction of s and z (from the name)
English
Let $f$ be a continuous multilinear map of the function that maps $x_{7}$ to $G$ and $\mathrm{G'}$. Let $s$ be a finite set of $\mathrm{Fin}$ applied to $n$ such that $\FinsetcardMACRoM {s}= k$. Let $z$ be an element of $G$. Then the restriction of $s$ and $z$ is a continuous multilinear map of the function that maps $x_{6}$ to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.restrictScalarsₗᵢdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $x_{8}$ be a set. Then $\mathrm{ContinuousMultilinearMap\_\_restrictScalars\_u2097\_\_u1d62\_}$ applied to $x_{8}$ is a linear isometry of the set of continuous multilinear maps of $E$ and $G$ and the set of continuous multilinear maps of $E$ and $G$.
ContinuousMultilinearMap.seminormdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the seminorm of E (from the name)
English
Let $x$ and $G$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the seminorm of $E$ is a seminorm of $x$ and the set of continuous multilinear maps of $E$ and $G$.
ContinuousMultilinearMap.smulRightLdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantWording
the right scalar multiple of E (from the name)
English
Let $x$ and $G$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the right scalar multiple of $E$ is a continuous linear map of the set of continuous multilinear maps of $E$ and $x$ and the set of continuous linear maps of $G$ and the set of continuous multilinear maps of $E$ and $G$.
MultilinearMap.mkContinuousdefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $f$ be a multilinear map of $E$ and $G$. Let $C$ be an element of $\Real$ such that for all functions $m$ from elements $i_{1}$ of $x_{1}$ to elements of $E$ applied to $i_{1}$, $\operatorname{norm} (f (m))\leq C \times \FinsetProd {\FinsetunivMACRoAC}{i}{\operatorname{norm} (m (i))}$. Then $\operatorname{mkContinuous}$ applied to $f$, $C$ and $H$ is a continuous multilinear map of $E$ and $G$ defined as $\operatorname{mk}$ applied to $f$ and $\mathrm{MultilinearMap\_\_continuous\_of\_bound}$ applied to $f$, $C$ and $H$.
MultilinearMap.mkContinuousLineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $f$ be a linear map of $G$ and the set of multilinear maps of $E$ and $\mathrm{G'}$. Let $C$ be an element of $\Real$ such that for all elements $x_{10}$ of $G$, for all functions $m$ from elements $i_{2}$ of $x_{1}$ to elements of $E$ applied to $i_{2}$, $\operatorname{norm} (\operatorname{coe} (f , x_{10} , m))\leq C \times \operatorname{norm} (x_{10})\times \FinsetProd {\FinsetunivMACRoAC}{i_{1}}{\operatorname{norm} (m (i_{1}))}$. Then $\operatorname{mkContinuousLinear}$ applied to $f$, $C$ and $H$ is a continuous linear map of $G$ and the set of continuous multilinear maps of $E$ and $\mathrm{G'}$.
MultilinearMap.mkContinuousMultilineardefMathlib.Analysis.Normed.Module.Multilinear.Basic, function or constantEnglish
Let $f$ be a multilinear map of $E$ and the set of multilinear maps of $\mathrm{E'}$ and $G$. Let $C$ be an element of $\Real$ such that for all functions $x_{12}$ from elements $i_{5}$ of $x_{1}$ to elements of $E$ applied to $i_{5}$, for all functions $x_{13}$ from elements $i_{4}$ of $x_{2}$ to elements of $\mathrm{E'}$ applied to $i_{4}$, $\operatorname{norm} (\operatorname{coe} (f , x_{12} , x_{13}))\leq C \times \FinsetProd {\FinsetunivMACRoAC}{i_{2}}{\operatorname{norm} (x_{12} (i_{2}))}\times \FinsetProd {\FinsetunivMACRoAC}{i_{3}}{\operatorname{norm} (x_{13} (i_{3}))}$. Then $\operatorname{mkContinuousMultilinear}$ applied to $f$, $C$ and $H$ is a continuous multilinear map of $E$ and the set of continuous multilinear maps of $\mathrm{E'}$ and $G$.
ContinuousLinearMap.continuousMultilinearMapOptiondefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the continuous multilinear map option of B (from the name)
English
Let $B$ be a continuous linear map of $G$ and the set of continuous multilinear maps of $E$ and $F$. Then the continuous multilinear map option of $B$ is a continuous multilinear map of the function that maps $x_{10}$ to $\mathrm{Prod}$ applied to $G$ and the set of functions from elements $i$ of $x_{1}$ to elements of $E$ applied to $i$ and $F$.
ContinuousLinearMap.uncurryLeftdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $f$ be a continuous linear map of $\mathrm{Ei}$ applied to $0$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succ}$ applied to $i$ and $G$. Then $\operatorname{uncurryLeft}$ applied to $f$ is a continuous multilinear map of $\mathrm{Ei}$ and $G$.
ContinuousLinearMap.uncurryMiddefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a continuous linear map of $\mathrm{Ei}$ applied to $p$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $G$. Then $\operatorname{uncurryMid}$ applied to $p$ and $f$ is a continuous multilinear map of $\mathrm{Ei}$ and $G$.
ContinuousMultilinearMap.curryFinFinsetdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the curry finite finite set of hl and #5 (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Assume that $\FinsetcardMACRoM {s}= k$. Assume that the cardinality of the complement of $s$ is equal to $l$. Then the curry finite finite set of $\mathrm{hk}$ and $\mathrm{hl}$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{6}$ to $G$ and $\mathrm{G'}$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $G$ and the set of continuous multilinear maps of the function that maps $x_{8}$ to $G$ and $\mathrm{G'}$ defined as the composition of the domain domain congruence of the inverse of the finite sum equivalence of $\mathrm{hk}$ and $\mathrm{hl}$ and the curry sum equivalence of $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.curryLeftdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the left curry of f (from the name)
English
Let $f$ be a continuous multilinear map of $\mathrm{Ei}$ and $G$. Then the left curry of $f$ is a continuous linear map of $\mathrm{Ei}$ applied to $0$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succ}$ applied to $i$ and $G$ defined as $\operatorname{mkContinuousLinear}$ applied to the left curry of $\operatorname{toMultilinearMap}$ applied to $f$, the norm of $f$ and $\mathrm{ContinuousMultilinearMap\_\_norm\_map\_cons\_le}$ applied to $f$.
ContinuousMultilinearMap.curryMiddefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a continuous multilinear map of $\mathrm{Ei}$ and $G$. Then $\operatorname{curryMid}$ applied to $p$ and $f$ is a continuous linear map of $\mathrm{Ei}$ applied to $p$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $G$ defined as $\operatorname{mkContinuousLinear}$ applied to $\operatorname{curryMid}$ applied to $p$ and $\operatorname{toMultilinearMap}$ applied to $f$, the norm of $f$ and $\mathrm{ContinuousMultilinearMap\_\_norm\_map\_insertNth\_le}$ applied to $f$.
ContinuousMultilinearMap.curryMidEquivdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $x$ and $G$ be sets. Let $\mathrm{Ei}$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{curryMidEquiv}$ applied to $x$, $\mathrm{Ei}$, $G$ and $p$ is a linear isometry equivalence of the set of continuous multilinear maps of $\mathrm{Ei}$ and $G$ and the set of continuous linear maps of $\mathrm{Ei}$ applied to $p$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $G$.
ContinuousMultilinearMap.curryRightdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the right curry of f (from the name)
English
Let $f$ be a continuous multilinear map of $\mathrm{Ei}$ and $G$. Then the right curry of $f$ is a continuous multilinear map of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of continuous linear maps of $\mathrm{Ei}$ applied to $\operatorname{last}$ applied to $n$ and $G$.
ContinuousMultilinearMap.currySumdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the curry sum of f (from the name)
English
Let $f$ be a continuous multilinear map of the function that maps $x_{12}$ to $G$ and $\mathrm{G'}$. Then the curry sum of $f$ is a continuous multilinear map of the function that maps $x_{10}$ to $G$ and the set of continuous multilinear maps of the function that maps $x_{11}$ to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.currySumEquivdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the curry sum equivalence of G and #5 (from the name)
English
Let $x$, $x_{1}$, $x_{2}$, $G$ and $\mathrm{G'}$ be sets. Then the curry sum equivalence of $G$ and $\mathrm{G'}$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{10}$ to $G$ and $\mathrm{G'}$ and the set of continuous multilinear maps of the function that maps $x_{11}$ to $G$ and the set of continuous multilinear maps of the function that maps $x_{12}$ to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.domDomCongrₗᵢdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the domain domain congruence of #4 (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Let $x_{10}$ be an equivalence from $x_{1}$ to $x_{2}$. Then the domain domain congruence of $x_{10}$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{11}$ to $G$ and $\mathrm{G'}$ and the set of continuous multilinear maps of the function that maps $x_{12}$ to $G$ and $\mathrm{G'}$.
ContinuousMultilinearMap.uncurryRightdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $f$ be a continuous multilinear map of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of continuous linear maps of $\mathrm{Ei}$ applied to $\operatorname{last}$ applied to $n$ and $G$. Then $\operatorname{uncurryRight}$ applied to $f$ is a continuous multilinear map of $\mathrm{Ei}$ and $G$ defined as $\operatorname{mkContinuous}$ applied to $\operatorname{uncurryRight}$ applied to the composition multilinear map of $\operatorname{coeLM}$ applied to $x$ and $\operatorname{toMultilinearMap}$ applied to $f$, the norm of $f$ and the function that maps $m$ to $\mathrm{ContinuousMultilinearMap\_\_norm\_map\_init\_le}$ applied to $f$ and $m$.
ContinuousMultilinearMap.uncurrySumdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the uncurrying sum of f (from the name)
English
Let $f$ be a continuous multilinear map of the function that maps $x_{11}$ to $G$ and the set of continuous multilinear maps of the function that maps $x_{12}$ to $G$ and $\mathrm{G'}$. Then the uncurrying sum of $f$ is a continuous multilinear map of the function that maps $x_{10}$ to $G$ and $\mathrm{G'}$.
continuousMultilinearCurryFin0defMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $x$, $G$ and $\mathrm{G'}$ be sets. Then $\mathrm{continuousMultilinearCurryFin0}$ applied to $x$, $G$ and $\mathrm{G'}$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{6}$ to $G$ and $\mathrm{G'}$ and $\mathrm{G'}$.
continuousMultilinearCurryFin1defMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantEnglish
Let $x$, $G$ and $\mathrm{G'}$ be sets. Then $\mathrm{continuousMultilinearCurryFin1}$ applied to $x$, $G$ and $\mathrm{G'}$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{6}$ to $G$ and $\mathrm{G'}$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$ defined as the composition of the continuous multilinear curry right equivalence of the function that maps $x_{6}$ to $G$ and $\mathrm{continuousMultilinearCurryFin0}$ applied to $x$, $G$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$.
continuousMultilinearCurryLeftEquivdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the continuous multilinear curry left equivalence of Ei (from the name)
English
Let $x$ and $G$ be sets. Let $\mathrm{Ei}$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then the continuous multilinear curry left equivalence of $\mathrm{Ei}$ is a linear isometry equivalence of the set of continuous multilinear maps of $\mathrm{Ei}$ and $G$ and the set of continuous linear maps of $\mathrm{Ei}$ applied to $0$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{succ}$ applied to $i$ and $G$.
continuousMultilinearCurryRightEquivdefMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the continuous multilinear curry right equivalence of Ei (from the name)
English
Let $x$ and $G$ be sets. Let $\mathrm{Ei}$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then the continuous multilinear curry right equivalence of $\mathrm{Ei}$ is a linear isometry equivalence of the set of continuous multilinear maps of $\mathrm{Ei}$ and $G$ and the set of continuous multilinear maps of the function that maps $i$ to $\mathrm{Ei}$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of continuous linear maps of $\mathrm{Ei}$ applied to $\operatorname{last}$ applied to $n$ and $G$.
continuousMultilinearCurryRightEquiv'defMathlib.Analysis.Normed.Module.Multilinear.Curry, function or constantWording
the continuous multilinear curry right equivalence of n (from the name)
English
Let $x$, $G$ and $\mathrm{G'}$ be sets. Let $n$ be a natural number. Then the continuous multilinear curry right equivalence of $n$ is a linear isometry equivalence of the set of continuous multilinear maps of the function that maps $x_{6}$ to $G$ and $\mathrm{G'}$ and the set of continuous multilinear maps of the function that maps $x_{7}$ to $G$ and the set of continuous linear maps of $G$ and $\mathrm{G'}$ defined as the continuous multilinear curry right equivalence of the function that maps $x_{6}$ to $G$.
NormedSpace.normalizedefMathlib.Analysis.Normed.Module.Normalize, function or constantEnglish
Let $x_{2}$ be an element of $V$. Then $\operatorname{normalize}$ applied to $x_{2}$ is an element of $V$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (\operatorname{norm} (x_{2}))}{x_{2}}$.
PiTensorProduct.toDualContinuousMultilinearMapdefMathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm, function or constantWording
the dual continuous multilinear map of F (from the name)
English
Let $F$ be a set. Then the dual continuous multilinear map of $F$ is a linear map of the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ and the set of continuous linear maps of the set of continuous multilinear maps of $E$ and $F$ and $F$.
PiTensorProduct.liftEquivdefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the lift equivalence of E (from the name)
English
Let $x_{2}$ and $F$ be sets. Let $E$ be a function from elements of $x$ to sets. Then the lift equivalence of $E$ is a linear equivalence of the set of continuous multilinear maps of $E$ and $F$ and the set of continuous linear maps of the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ and $F$.
PiTensorProduct.liftIsometrydefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the lift isometry of E (from the name)
English
Let $x_{2}$ and $F$ be sets. Let $E$ be a function from elements of $x$ to sets. Then the lift isometry of $E$ is a linear isometry equivalence of the set of continuous multilinear maps of $E$ and $F$ and the set of continuous linear maps of the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ and $F$.
PiTensorProduct.mapLdefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the map of f (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ to continuous linear maps of $E$ applied to $i_{2}$ and $\mathrm{E'}$ applied to $i_{2}$. Then the map of $i_{2}$ is a continuous linear map of the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ and the set of product tensor products of $x_{2}$ and the function that maps $i_{1}$ to $\mathrm{E'}$ applied to $i_{1}$ defined as the function that maps $f$ to $\operatorname{liftIsometry}$ applied to $x_{2}$, $E$, the set of product tensor products of $x_{2}$ and the function that maps $i_{3}$ to $\mathrm{E'}$ applied to $i_{3}$, the composition continuous linear map of $\operatorname{tprodL}$ applied to $x_{2}$ and $i_{2}$ and $f$.
PiTensorProduct.mapLIncldefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the map inclusion of p (from the name)
English
Let $p$ be a function from elements $i_{2}$ of $x$ to submodules of $x_{2}$ and $E$ applied to $i_{2}$. Then the map inclusion of $i_{2}$ is a continuous linear map of the set of product tensor products of $x_{2}$ and the function that maps $i$ to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p (i)}{x_{6}})}$ and the set of product tensor products of $x_{2}$ and the function that maps $i_{1}$ to $E$ applied to $i_{1}$ defined as the function that maps $p$ to the map of the function that maps $i$ to the subtype of $i_{2}$ applied to $i$.
PiTensorProduct.mapLMonoidHomdefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the map monoid homomorphism (from the name)
English
The map monoid homomorphism is a monoid homomorphism of the set of functions from elements $i$ of $x$ to continuous linear maps of $E$ applied to $i$ and $E$ applied to $i$ and the set of continuous linear maps of the set of product tensor products of $x_{2}$ and the function that maps $i_{1}$ to $E$ applied to $i_{1}$ and the set of product tensor products of $x_{2}$ and the function that maps $i_{2}$ to $E$ applied to $i_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mapL}$ and $\mathrm{PiTensorProduct\_\_mapL\_one}$ and $\mathrm{PiTensorProduct\_\_mapL\_mul}$.
PiTensorProduct.mapLMultilineardefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantEnglish
Let $x_{2}$ be a set. Let $E$ and $\mathrm{E'}$ be functions from elements of $x$ to sets. Then $\operatorname{mapLMultilinear}$ applied to $x_{2}$, $E$ and $\mathrm{E'}$ is a continuous multilinear map of the function that maps $i$ to the set of continuous linear maps of $E$ applied to $i$ and $\mathrm{E'}$ applied to $i$ and the set of continuous linear maps of the set of product tensor products of $x_{2}$ and the function that maps $i_{1}$ to $E$ applied to $i_{1}$ and the set of product tensor products of $x_{2}$ and the function that maps $i_{2}$ to $\mathrm{E'}$ applied to $i_{2}$.
PiTensorProduct.projectiveSeminormdefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantWording
the projective seminorm (from the name)
English
The projective seminorm is a seminorm of $x_{2}$ and the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ defined as the seminorm of $\operatorname{norm}$.
PiTensorProduct.tprodLdefMathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm, function or constantEnglish
Let $x_{2}$ be a set. Then $\operatorname{tprodL}$ applied to $x_{2}$ is a continuous multilinear map of $E$ and the set of product tensor products of $x_{2}$ and the function that maps $i$ to $E$ applied to $i$ defined as $\operatorname{symm}$ applied to the lift isometry of $E$ and the identity map of $x_{2}$ and the set of product tensor products of $x_{2}$ and the function that maps $i_{7}$ to $E$ applied to $i_{7}$.
StrongDual.extendRCLikeLdefMathlib.Analysis.Normed.Module.RCLike.Extend, function or constantWording
the extension (from the docstring)
English
The extension is a continuous linear equivalence of the set of strong duals of $\Real$ and $F$ and the set of strong duals of $x$ and $F$.
StrongDual.extendRCLikeₗᵢdefMathlib.Analysis.Normed.Module.RCLike.Extend, function or constantEnglish
$\mathrm{StrongDual\_\_extendRCLike\_u2097\_\_u1d62\_}$ is a linear isometry equivalence of the set of strong duals of $\Real$ and $F$ and the set of strong duals of $x$ and $F$ defined as $\operatorname{mk}$ applied to the extension and $\mathrm{StrongDual\_\_norm\_extendRCLike}$.
SeminormstructureMathlib.Analysis.Normed.Module.Seminorm.Basic, typeWording
seminorm of x and E (from the name)
English
Let $x$ and $E$ be sets. Then the seminorms of $x$ and $E$ are a basic type.
Seminorm.balldefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantWording
the ball of x4 and r (from the name)
English
Let $p$ be a seminorm of $x$ and $E$. Let $x_{4}$ be an element of $E$. Let $r$ be a real number. Then the ball of $x_{4}$ and $r$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Lt} (p (y - x_{4}), r)$.
Seminorm.closedBalldefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantWording
the closed ball of x4 and r (from the name)
English
Let $p$ be a seminorm of $x$ and $E$. Let $x_{4}$ be an element of $E$. Let $r$ be a real number. Then the closed ball of $x_{4}$ and $r$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Leq} (p (y - x_{4}), r)$.
Seminorm.compdefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantWording
the composition of p and f (from the name)
English
Let $p$ be a seminorm of $x_{1}$ and $x_{2}$. Let $f$ be a linear map of $E$ and $x_{2}$. Then the composition of $p$ and $f$ is a seminorm of $x$ and $E$.
Seminorm.ofdefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantEnglish
Let $f$ be a function from elements of $E$ to real numbers such that for all elements $x_{5}$ of $E$, for all elements $y$ of $E$, $f (x_{5} + y)\leq f (x_{5})+ f (y)$ and for all elements $a$ of $x$, for all elements $x_{4}$ of $E$, $f$ applied to $\HSMulhSMulMACRoAL {a}{x_{4}}$ is equal to the product of the norm of $a$ and $f$ applied to $x_{4}$. Then $\operatorname{of}$ applied to $f$, $\mathrm{add\_le}$ and $\mathrm{smul}$ is a seminorm of $x$ and $E$.
Seminorm.ofSMulLEdefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantWording
the seminorm of f (from the name)
English
Let $f$ be a function from elements of $E$ to real numbers such that $f (0)= 0$, for all elements $x_{5}$ of $E$, for all elements $y$ of $E$, $f (x_{5} + y)\leq f (x_{5})+ f (y)$ and for all elements $r$ of $x$, for all elements $x_{4}$ of $E$, $f$ applied to $\HSMulhSMulMACRoAL {r}{x_{4}}$ is less than or equal to the product of the norm of $r$ and $f$ applied to $x_{4}$. Then the seminorm of $f$ is a seminorm of $x$ and $E$.
Seminorm.pullbackdefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantWording
the pullback of f (from the name)
English
Let $f$ be a linear map of $E$ and $x_{2}$. Then the pullback of $f$ is an additive monoid homomorphism of the set of seminorms of $x_{1}$ and $x_{2}$ and the set of seminorms of $x$ and $E$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $p$ to the composition of $p$ and $f$ and $\mathrm{Seminorm\_\_zero\_comp}$ applied to $f$ and the function that maps $p_{1}$ and $q$ to $\mathrm{Seminorm\_\_add\_comp}$ applied to $p_{1}$, $q$ and $f$.
Seminorm.restrictScalarsdefMathlib.Analysis.Normed.Module.Seminorm.Basic, function or constantEnglish
Let $x$ be a set. Let $p$ be a seminorm of $x_{1}$ and $E$. Then $\operatorname{restrictScalars}$ applied to $x$ and $p$ is a seminorm of $x$ and $E$.
SeminormClassclassMathlib.Analysis.Normed.Module.Seminorm.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $E$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SeminormClass}$ holds for $F$, $x$ and $E$.
normSeminormdefMathlib.Analysis.Normed.Module.Seminorm.Norm, function or constantWording
the norm of x and E (from the docstring)
English
Let $x$ and $E$ be sets. Then the norm of $x$ and $E$ is a seminorm of $x$ and $E$.
ContinuousLinearEquiv.coorddefMathlib.Analysis.Normed.Module.Span, function or constantWording
the coordinate of x4 (from the name)
English
Let $x$ be a set. Let $x_{4}$ be an element of $E$ such that $x_{4} \neq 0$. Then the coordinate of $x_{4}$ is a strong dual of $x$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{span} (x , \operatorname{singleton} (x_{4}))}{x_{5}})}$ defined as the continuous linear map of the inverse of the span nonzero singleton of $x_{4}$.
ContinuousLinearEquiv.toSpanNonzeroSingletondefMathlib.Analysis.Normed.Module.Span, function or constantWording
the span nonzero singleton of x4 (from the name)
English
Let $x$ be a set. Let $x_{4}$ be an element of $E$ such that $x_{4} \neq 0$. Then the span nonzero singleton of $x_{4}$ is a continuous linear equivalence of $x$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{span} (x , \operatorname{singleton} (x_{4}))}{x_{5}})}$.
LinearIsometryEquiv.toSpanUnitSingletondefMathlib.Analysis.Normed.Module.Span, function or constantWording
the span unit singleton of x4 and hx (from the name)
English
Let $x_{4}$ be an element of $E$ such that $\operatorname{norm} (x_{4})= 1$. Then the span unit singleton of $x_{4}$ and $\mathrm{hx}$ is a linear isometry equivalence of $x$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{span} (x , \operatorname{singleton} (x_{4}))}{x_{5}})}$.
NormedSpace.Dual.continuousLinearMapToWeakDualdefMathlib.Analysis.Normed.Module.WeakDual, function or constantWording
the continuous linear map to weak dual (from the name)
English
The continuous linear map to weak dual is a continuous linear map of the set of strong duals of $x$ and $E$ and the set of weak duals of $x$ and $E$.
WeakDual.extendRCLikeLdefMathlib.Analysis.Normed.Module.WeakDual, function or constantWording
the extension (from the docstring)
English
The extension is a continuous linear equivalence of the set of weak duals of $\Real$ and $F$ and the set of weak duals of $x$ and $F$.
WeakDual.polardefMathlib.Analysis.Normed.Module.WeakDual, function or constantWording
the polar set of x and s (from the docstring)
English
Let $x$ be a set. Let $s$ be an element of $\wp M$. Then the polar set of $x$ and $s$ is an element of the power set of the set of weak duals of $x$ and $M$ defined as the preimage of $\operatorname{coe}$ applied to the strong dual and $\operatorname{polar}$ applied to $x$ and $s$.
WeakDual.seminormFamilydefMathlib.Analysis.Normed.Module.WeakDual, function or constantWording
the seminorm family of x and E (from the name)
English
Let $x$ and $E$ be sets. Then the seminorm family of $x$ and $E$ is a seminorm family of the set of weak duals of $x$ and $E$ and $E$ defined as the seminorm family of the canonical pairing of $x$ and $E$.
ENormSMulClassclassMathlib.Analysis.Normed.MulAction, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{ENormSMulClass}$ holds for $x$ and $x_{1}$.
NormSMulClassclassMathlib.Analysis.Normed.MulAction, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{NormSMulClass}$ holds for $x$ and $x_{1}$.
ContinuousLinearEquiv.ofBijectivedefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the continuous linear equivalence of f (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$ such that the kernel of $\operatorname{toLinearMap}$ applied to $f$ is equal to the bottom and the range of $\operatorname{toLinearMap}$ applied to $f$ is equal to the top. Then the continuous linear equivalence of $f$ is a continuous linear equivalence of $E$ and $F$.
ContinuousLinearEquiv.toNonlinearRightInversedefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the nonlinear right inverse of f (from the name)
English
Let $f$ be a continuous linear equivalence of $E$ and $F$. Then the nonlinear right inverse of $f$ is a nonlinear right inverse of the continuous linear map of $f$.
ContinuousLinearMap.NonlinearRightInversestructureMathlib.Analysis.Normed.Operator.Banach, typeWording
nonlinear right inverse of f (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$. Then the nonlinear right inverses of $f$ are a basic type.
ContinuousLinearMap.NonlinearRightInverse.nnnormdefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the norm of self (from the name)
English
Let $\mathrm{self}$ be a nonlinear right inverse of $f$. Then the norm of $\mathrm{self}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
ContinuousLinearMap.NonlinearRightInverse.toFundefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the nonlinear right inverse of self and x9 (from the name)
English
Let $\mathrm{self}$ be a nonlinear right inverse of $f$. Let $x_{9}$ be an element of $F$. Then the nonlinear right inverse of $\mathrm{self}$ and $x_{9}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{9}$.
ContinuousLinearMap.antilipschitzConstant_of_injective_of_isClosed_rangedefMathlib.Analysis.Normed.Operator.Banach, function or constantEnglish
Let $f$ be a continuous linear map of $E$ and $F$ such that $\operatorname{coe}$ applied to $f$ is injective and the range of $\operatorname{coe}$ applied to $f$ is closed. Then $\mathrm{ContinuousLinearMap\_\_antilipschitzConstant\_of\_injective\_of\_isClosed\_range}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{hf'}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{choose}$ applied to $\mathrm{ContinuousLinearMap\_\_antilipschitz\_of\_injective\_of\_isClosed\_range}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{hf'}$.
ContinuousLinearMap.coprodSubtypeLEquivOfIsCompldefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the coproduct subtype equivalence of f (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$ such that $\mathrm{IsCompl}$ holds for the range of $\operatorname{toLinearMap}$ applied to $f$ and $G$ and the kernel of $\operatorname{toLinearMap}$ applied to $f$ is equal to the bottom. Then the coproduct subtype equivalence of $f$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $E$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {G}{x_{6}})}$ and $F$.
ContinuousLinearMap.equivRangedefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the equivalence range of hinj and hclo (from the name)
English
Assume that $\operatorname{coe}$ applied to $f$ is injective. Assume that the range of $\operatorname{coe}$ applied to $f$ is closed. Then the equivalence range of $\mathrm{hinj}$ and $\mathrm{hclo}$ is a continuous linear equivalence of $E$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toLinearMap} (f))}{x_{10}})}$.
ContinuousLinearMap.leftInverse_of_injective_of_isClosed_rangedefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the left inverse of f (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$ such that $\operatorname{coe}$ applied to $f$ is injective and the range of $\operatorname{coe}$ applied to $f$ is closed. Then the left inverse of $f$ is a continuous linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toLinearMap} (f))}{x_{6}})}$ and $E$.
ContinuousLinearMap.nonlinearRightInverseOfSurjectivedefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the nonlinear right inverse of f and hsurj (from the name)
English
Let $f$ be a continuous linear map of $E$ and $F$ such that the range of $\operatorname{toLinearMap}$ applied to $f$ is equal to the top. Then the nonlinear right inverse of $f$ and $\mathrm{hsurj}$ is a nonlinear right inverse of $f$ defined as $\operatorname{proj0}$ applied to $\mathrm{ContinuousLinearMap\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Normed\_\_Operator\_\_Banach\_\_754268252\_\_\_hygCtx\_\_\_hyg\_\_2}$, $f$ and $\mathrm{hsurj}$.
ContinuousLinearMap.ofIsClosedGraphdefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the continuous linear map of hg (from the name)
English
Assume that the graph of $g$ is closed. Then the continuous linear map of $\mathrm{hg}$ is a continuous linear map of $E$ and $F$ defined as $\operatorname{mk}$ applied to $g$ and $\mathrm{LinearMap\_\_continuous\_of\_isClosed\_graph}$ applied to $g$ and $\mathrm{hg}$.
ContinuousLinearMap.ofSeqClosedGraphdefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the continuous linear map of hg (from the name)
English
Assume that for all functions $u$ from natural numbers to elements of $E$, for all elements $x_{6}$ of $E$, for all elements $y$ of $F$, if $\operatorname{Tendsto}$ holds for $u$, $\operatorname{atTop}$ and the neighbourhood filter of $x_{6}$, then if $\operatorname{Tendsto}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $g$ and $u$, $\operatorname{atTop}$ and the neighbourhood filter of $y$, then $\EqtMACRoH {y}{g (x_{6})}$. Then the continuous linear map of $\mathrm{hg}$ is a continuous linear map of $E$ and $F$ defined as $\operatorname{mk}$ applied to $g$ and $\mathrm{LinearMap\_\_continuous\_of\_seq\_closed\_graph}$ applied to $g$ and $\mathrm{hg}$.
LinearEquiv.toContinuousLinearEquivOfContinuousdefMathlib.Analysis.Normed.Operator.Banach, function or constantWording
the continuous linear equivalence of e and h6 (from the name)
English
Let $e$ be a linear equivalence of $E$ and $F$ such that $\operatorname{coe}$ applied to $e$ is continuous. Then the continuous linear equivalence of $e$ and $h_{6}$ is a continuous linear equivalence of $E$ and $F$ defined as $\operatorname{mk}$ applied to $e$, $h_{6}$ and $\mathrm{LinearEquiv\_\_continuous\_symm}$ applied to $e$ and $h_{6}$.
ContinuousLinearMap.opNormdefMathlib.Analysis.Normed.Operator.Basic, function or constantWording
the operator norm of f (from the docstring)
English
Let $f$ be a continuous linear map of $E$ and $F$. Then the operator norm of $f$ is a real number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $c$ to the proposition that $0 \leq c$ and for all elements $x_{9}$ of $E$, the norm of $f$ applied to $x_{9}$ is less than or equal to the product of $c$ and the norm of $x_{9}$.
ContinuousLinearMap.restrictScalarsIsometrydefMathlib.Analysis.Normed.Operator.Basic, function or constantEnglish
Let $x$, $E$, $x_{1}$, $x_{7}$ and $x_{12}$ be sets. Then $\operatorname{restrictScalarsIsometry}$ applied to $x$, $E$, $x_{1}$, $x_{7}$ and $x_{12}$ is a linear isometry of the set of continuous linear maps of $E$ and $x_{1}$ and the set of continuous linear maps of $E$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\mathrm{ContinuousLinearMap\_\_restrictScalars\_u2097\_}$ applied to $x$, $E$, $x_{1}$, $x_{7}$ and $x_{12}$ and $\mathrm{ContinuousLinearMap\_\_norm\_restrictScalars}$.
ContinuousLinearMap.seminormdefMathlib.Analysis.Normed.Operator.Basic, function or constantWording
the seminorm (from the name)
English
The seminorm is a seminorm of $x_{1}$ and the set of continuous linear maps of $E$ and $F$.
LinearIsometry.toSpanSingletondefMathlib.Analysis.Normed.Operator.Basic, function or constantWording
the span singleton of E and hv (from the name)
English
Let $x$ and $E$ be sets. Assume that the norm of $v$ is equal to $1$. Then the span singleton of $E$ and $\mathrm{hv}$ is a linear isometry of $x$ and $E$.
ContinuousLinearMap.applydefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the continuous linear map of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the continuous linear map of $x$ and $x_{1}$ is a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of the set of continuous linear maps of $\mathrm{E'}$ and $x_{1}$ and $x_{1}$ defined as the flip of the identity map of $x$ and the set of continuous linear maps of $\mathrm{E'}$ and $x_{1}$.
ContinuousLinearMap.apply'defMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $\mathrm{F'}$ be a set. Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Then $\operatorname{apply'}$ applied to $\mathrm{F'}$ and $x_{4}$ is a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{F'}$ and $\mathrm{F'}$ defined as the flip of the identity map of $x_{1}$ and the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{F'}$.
ContinuousLinearMap.bilinearCompdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the bilinear composition of gE and gF (from the name)
English
Let $f$ be a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$. Let $\mathrm{gE}$ be a continuous linear map of $\mathrm{E''}$ and $\mathrm{E'}$. Let $\mathrm{gF}$ be a continuous linear map of $\mathrm{F''}$ and $\mathrm{F'}$. Then the bilinear composition of $\mathrm{gE}$ and $\mathrm{gF}$ is a continuous linear map of $\mathrm{E''}$ and the set of continuous linear maps of $\mathrm{F''}$ and $\mathrm{G'}$ defined as the flip of the composition of the flip of the composition of $f$ and $\mathrm{gE}$ and $\mathrm{gF}$.
ContinuousLinearMap.bilinearRestrictScalarsdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $x$ be a set. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then $\operatorname{bilinearRestrictScalars}$ applied to $x$ and $B$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$ defined as the composition of $\operatorname{restrictScalarsL}$ applied to $x_{1}$, $F$, $G$, $x$ and $x$ and $\operatorname{restrictScalars}$ applied to $x$ and $B$.
ContinuousLinearMap.compLdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the composition of x2 and #4 (from the name)
English
Let $x$, $\mathrm{E'}$, $x_{1}$ and $x_{2}$ be sets. Then the composition of $x_{1}$ and $x_{2}$ is a continuous linear map of the set of continuous linear maps of $x_{1}$ and $x_{2}$ and the set of continuous linear maps of the set of continuous linear maps of $\mathrm{E'}$ and $x_{1}$ and the set of continuous linear maps of $\mathrm{E'}$ and $x_{2}$ defined as $\operatorname{compSL}$ applied to $\mathrm{E'}$, $x_{1}$, $x_{2}$, the identity ring homomorphism of $x$ and the identity ring homomorphism of $x$.
ContinuousLinearMap.compSLdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $\mathrm{E'}$, $\mathrm{F'}$ and $\mathrm{G'}$ be sets. Let $x_{6}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{7}$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Then $\operatorname{compSL}$ applied to $\mathrm{E'}$, $\mathrm{F'}$, $\mathrm{G'}$, $x_{6}$ and $x_{7}$ is a continuous linear map of the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$ and the set of continuous linear maps of the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{F'}$ and the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{G'}$.
ContinuousLinearMap.compSLₗdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $\mathrm{E'}$, $\mathrm{F'}$ and $\mathrm{G'}$ be sets. Let $x_{6}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{7}$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Then $\mathrm{ContinuousLinearMap\_\_compSL\_u2097\_}$ applied to $\mathrm{E'}$, $\mathrm{F'}$, $\mathrm{G'}$, $x_{6}$ and $x_{7}$ is a linear map of the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$ and the set of linear maps of the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{F'}$ and the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{G'}$.
ContinuousLinearMap.deriv₂defMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the derivative of f (from the name)
English
Let $f$ be a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $x_{1}$ and $x_{2}$. Then the derivative of $f$ is a continuous linear map of $\mathrm{Prod}$ applied to $\mathrm{E'}$ and $x_{1}$ and the set of continuous linear maps of $\mathrm{Prod}$ applied to $\mathrm{E'}$ and $x_{1}$ and $x_{2}$ defined as the sum of the bilinear composition of the first component of $\mathrm{E'}$ and $x_{1}$ and the second component of $\mathrm{E'}$ and $x_{1}$ and the bilinear composition of the second component of $\mathrm{E'}$ and $x_{1}$ and the first component of $\mathrm{E'}$ and $x_{1}$.
ContinuousLinearMap.flipdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the flip of f (from the name)
English
Let $f$ be a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$. Then the flip of $f$ is a continuous linear map of $\mathrm{F'}$ and the set of continuous linear maps of $\mathrm{E'}$ and $\mathrm{G'}$.
ContinuousLinearMap.flipₗᵢdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the flip of x1 and x2 (from the name)
English
Let $x$, $E$, $x_{1}$ and $x_{2}$ be sets. Then the flip of $x_{1}$ and $x_{2}$ is a linear isometry equivalence of the set of continuous linear maps of $E$ and the set of continuous linear maps of $x_{1}$ and $x_{2}$ and the set of continuous linear maps of $x_{1}$ and the set of continuous linear maps of $E$ and $x_{2}$.
ContinuousLinearMap.flipₗᵢ'defMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the flip of x12 and x13 (from the name)
English
Let $E$, $F$ and $G$ be sets. Let $x_{12}$ be a ring homomorphism of $x_{1}$ and $x_{2}$. Let $x_{13}$ be a ring homomorphism of $x$ and $x_{2}$. Then the flip of $x_{12}$ and $x_{13}$ is a linear isometry equivalence of the set of continuous linear maps of $E$ and the set of continuous linear maps of $F$ and $G$ and the set of continuous linear maps of $F$ and the set of continuous linear maps of $E$ and $G$.
ContinuousLinearMap.precompLdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the precomposition of x1 and L (from the name)
English
Let $x_{1}$ be a set. Let $L$ be a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $x_{2}$ and $x_{3}$. Then the precomposition of $x_{1}$ and $L$ is a continuous linear map of the set of continuous linear maps of $x_{1}$ and $\mathrm{E'}$ and the set of continuous linear maps of $x_{2}$ and the set of continuous linear maps of $x_{1}$ and $x_{3}$ defined as the flip of the precomposition of $x_{1}$ and the flip of $L$.
ContinuousLinearMap.precompRdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the precomposition of x1 and L (from the name)
English
Let $x_{1}$ be a set. Let $L$ be a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $x_{2}$ and $x_{3}$. Then the precomposition of $x_{1}$ and $L$ is a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of the set of continuous linear maps of $x_{1}$ and $x_{2}$ and the set of continuous linear maps of $x_{1}$ and $x_{3}$ defined as the composition of the composition of $x_{2}$ and $x_{3}$ and $L$.
ContinuousLinearMap.smulRightLdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the right scalar multiple of x1 and #3 (from the name)
English
Let $x$, $\mathrm{E'}$ and $x_{1}$ be sets. Then the right scalar multiple of $\mathrm{E'}$ and $x_{1}$ is a continuous linear map of the set of strong duals of $x$ and $\mathrm{E'}$ and the set of continuous linear maps of $x_{1}$ and the set of continuous linear maps of $\mathrm{E'}$ and $x_{1}$.
ContinuousLinearMap.smulRightLₗdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantWording
the right scalar multiple of x1 and #3 (from the name)
English
Let $x$, $\mathrm{E'}$ and $x_{1}$ be sets. Then the right scalar multiple of $\mathrm{E'}$ and $x_{1}$ is a linear map of the set of strong duals of $x$ and $\mathrm{E'}$ and the set of linear maps of $x_{1}$ and the set of continuous linear maps of $\mathrm{E'}$ and $x_{1}$.
LinearMap.mkContinuousOfExistsBound₂defMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $f$ be a linear map of $E$ and the set of linear maps of $F$ and $G$ such that there exists a real number $C$, such that for all elements $x_{14}$ of $E$, for all elements $y$ of $F$, the norm of $\operatorname{coe}$ applied to $f$, $x_{14}$ and $y$ is less than or equal to the product of $C$, the norm of $x_{14}$ and the norm of $y$. Then $\mathrm{LinearMap\_\_mkContinuousOfExistsBound\_u2082\_}$ applied to $f$ and $h_{1}$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$.
LinearMap.mkContinuous₂defMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $f$ be a linear map of $E$ and the set of linear maps of $F$ and $G$. Let $C$ be a real number such that for all elements $x_{14}$ of $E$, for all elements $y$ of $F$, the norm of $\operatorname{coe}$ applied to $f$, $x_{14}$ and $y$ is less than or equal to the product of $C$, the norm of $x_{14}$ and the norm of $y$. Then $\mathrm{LinearMap\_\_mkContinuous\_u2082\_}$ applied to $f$, $C$ and $\mathrm{hC}$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$.
LinearMap.mkContinuous₂OfExistsdefMathlib.Analysis.Normed.Operator.Bilinear, function or constantEnglish
Let $f$ be a linear map of $\mathrm{E'}$ and the set of linear maps of $\mathrm{F'}$ and $\mathrm{G'}$ such that there exists a continuous linear map $g$ of $\mathrm{E'}$ and the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$, such that for all elements $a$ of $\mathrm{E'}$, for all elements $b$ of $\mathrm{F'}$, $\EqtMACRoH {\operatorname{coe} (f , a , b)}{\operatorname{coe} (g , a , b)}$. Then $\mathrm{LinearMap\_\_mkContinuous\_u2082\_OfExists}$ applied to $f$ and $\mathrm{hf}$ is a continuous linear map of $\mathrm{E'}$ and the set of continuous linear maps of $\mathrm{F'}$ and $\mathrm{G'}$.
IsBoundedBilinearMapstructureMathlib.Analysis.Normed.Operator.BoundedLinearMaps, predicateWording
f is a bounded bilinear map (from the name)
English
Let $x$ be a set. Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $E$ and $F$ to elements of $G$. Then we can say that $f$ is a bounded bilinear map.
IsBoundedBilinearMap.derivdefMathlib.Analysis.Normed.Operator.BoundedLinearMaps, function or constantWording
the derivative of h and p (from the docstring)
English
Assume that $f$ is a bounded bilinear map. Let $p$ be an element of $\mathrm{Prod}$ applied to $E$ and $F$. Then the derivative of $h$ and $p$ is a continuous linear map of $\mathrm{Prod}$ applied to $E$ and $F$ and $G$ defined as $\mathrm{ContinuousLinearMap\_\_deriv\_u2082\_\_\_app}$ applied to the continuous linear map of $h$ and $p$.
IsBoundedBilinearMap.linearDerivdefMathlib.Analysis.Normed.Operator.BoundedLinearMaps, function or constantWording
the linear derivative of h and p (from the name)
English
Assume that $f$ is a bounded bilinear map. Let $p$ be an element of $\mathrm{Prod}$ applied to $E$ and $F$. Then the linear derivative of $h$ and $p$ is a linear map of $\mathrm{Prod}$ applied to $E$ and $F$ and $G$ defined as $\operatorname{toLinearMap}$ applied to $\mathrm{ContinuousLinearMap\_\_deriv\_u2082\_\_\_app}$ applied to the continuous linear map of $h$ and $p$.
IsBoundedBilinearMap.toContinuousLinearMapdefMathlib.Analysis.Normed.Operator.BoundedLinearMaps, function or constantWording
the continuous linear map of hf (from the name)
English
Assume that $f$ is a bounded bilinear map. Then the continuous linear map of $\mathrm{hf}$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$.
IsBoundedLinearMapstructureMathlib.Analysis.Normed.Operator.BoundedLinearMaps, predicateWording
f is a bounded linear map (from the name)
English
Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Then we can say that $f$ is a bounded linear map.
IsBoundedLinearMap.toContinuousLinearMapdefMathlib.Analysis.Normed.Operator.BoundedLinearMaps, function or constantWording
the continuous linear map of f and hf (from the name)
English
Let $f$ be a function from elements of $E$ to elements of $F$ such that $f$ is a bounded linear map. Then the continuous linear map of $f$ and $\mathrm{hf}$ is a continuous linear map of $E$ and $F$.
IsBoundedLinearMap.toLinearMapdefMathlib.Analysis.Normed.Operator.BoundedLinearMaps, function or constantWording
the linear map of f and h (from the name)
English
Let $f$ be a function from elements of $E$ to elements of $F$ such that $f$ is a bounded linear map. Then the linear map of $f$ and $h$ is a linear map of $E$ and $F$ defined as $\operatorname{mk'}$ applied to $f$ and $\operatorname{toIsLinearMap}$ applied to $h$.
ContinuousLinearMap.mkOfIsCompactOperatordefMathlib.Analysis.Normed.Operator.Compact.Basic, function or constantEnglish
Assume that $\operatorname{coe}$ applied to $f$ is a compact operator. Then $\operatorname{mkOfIsCompactOperator}$ applied to $\mathrm{hf}$ is a continuous linear map of $x_{5}$ and $x_{6}$ defined as $\operatorname{mk}$ applied to $f$ and $\operatorname{continuous}$ applied to $\mathrm{hf}$.
IsCompactOperatordefMathlib.Analysis.Normed.Operator.Compact.Basic, predicateWording
f is a compact operator (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is a compact operator, if there exists an element $K$ of $\wp x_{1}$, such that $K$ is compact and the preimage of $f$ and $K$ is an element of the neighbourhood filter of $0$.
compactOperatordefMathlib.Analysis.Normed.Operator.Compact.Basic, function or constantWording
the compact operator of x4 (from the name)
English
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{5}$ and $x_{6}$ be sets. Then the compact operator of $x_{4}$ is a submodule of $x_{1}$ and the set of continuous linear maps of $x_{5}$ and $x_{6}$.
ContinuousLinearMap.ofMemClosureImageCoeBoundeddefMathlib.Analysis.Normed.Operator.Completeness, function or constantWording
the continuous linear map of f (from the name)
English
Let $f$ be a function from elements of $\mathrm{E'}$ to elements of $F$. Assume that $s$ is bounded. Assume that $f$ is an element of the closure of the image of $\operatorname{coe}$ and $s$. Then the continuous linear map of $f$ is a continuous linear map of $\mathrm{E'}$ and $F$.
ContinuousLinearMap.ofTendstoOfBoundedRangedefMathlib.Analysis.Normed.Operator.Completeness, function or constantWording
the continuous linear map of f and g (from the name)
English
Let $f$ be a function from elements of $\mathrm{E'}$ to elements of $F$. Let $g$ be a function from elements of $x_{9}$ to continuous linear maps of $\mathrm{E'}$ and $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $a$ and $x_{10}$ to $g$ applied to $a$ and $x_{10}$, $l$ and the neighbourhood filter of $f$ and the range of $g$ is bounded. Then the continuous linear map of $f$ and $g$ is a continuous linear map of $\mathrm{E'}$ and $F$.
ContinuousLinearEquiv.ofHomothetydefMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantWording
the continuous linear equivalence of f and a (from the name)
English
Let $f$ be a linear equivalence of $E$ and $F$. Let $a$ be a real number such that $0 < a$ and for all elements $x_{10}$ of $E$, the norm of $f$ applied to $x_{10}$ is equal to the product of $a$ and the norm of $x_{10}$. Then the continuous linear equivalence of $f$ and $a$ is a continuous linear equivalence of $E$ and $F$.
ContinuousLinearMap.ofHomothetydefMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantWording
the continuous linear map of f and a (from the name)
English
Let $f$ be a linear map of $E$ and $F$. Let $a$ be a real number such that for all elements $x_{9}$ of $E$, the norm of $f$ applied to $x_{9}$ is equal to the product of $a$ and the norm of $x_{9}$. Then the continuous linear map of $f$ and $a$ is a continuous linear map of $E$ and $F$.
LinearEquiv.toContinuousLinearEquivOfBoundsdefMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantWording
the continuous linear equivalence of C_to and C_inv (from the name)
English
Let $e$ be a linear equivalence of $E$ and $F$. Let $\mathrm{C\_to}$ and $\mathrm{C\_inv}$ be real numbers such that for all elements $x_{11}$ of $E$, the norm of $e$ applied to $x_{11}$ is less than or equal to the product of $\mathrm{C\_to}$ and the norm of $x_{11}$ and for all elements $x_{10}$ of $F$, the norm of $\operatorname{symm}$ applied to $e$ and $x_{10}$ is less than or equal to the product of $\mathrm{C\_inv}$ and the norm of $x_{10}$. Then the continuous linear equivalence of $\mathrm{C\_to}$ and $\mathrm{C\_inv}$ is a continuous linear equivalence of $E$ and $F$.
LinearMap.mkContinuousdefMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantEnglish
Let $f$ be a linear map of $E$ and $F$. Let $C$ be a real number such that for all elements $x_{9}$ of $E$, the norm of $f$ applied to $x_{9}$ is less than or equal to the product of $C$ and the norm of $x_{9}$. Then $\operatorname{mkContinuous}$ applied to $f$, $C$ and $h$ is a continuous linear map of $E$ and $F$.
LinearMap.mkContinuousOfExistsBounddefMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantEnglish
Let $f$ be a linear map of $E$ and $F$ such that there exists a real number $C$, such that for all elements $x_{9}$ of $E$, the norm of $f$ applied to $x_{9}$ is less than or equal to the product of $C$ and the norm of $x_{9}$. Then $\operatorname{mkContinuousOfExistsBound}$ applied to $f$ and $h$ is a continuous linear map of $E$ and $F$.
LinearMap.toContinuousLinearMap₁defMathlib.Analysis.Normed.Operator.ContinuousLinearMap, function or constantWording
the continuous linear map of f (from the name)
English
Let $f$ be a linear map of $x$ and $E$. Then the continuous linear map of $f$ is a continuous linear map of $x$ and $E$.
LinearEquiv.extenddefMathlib.Analysis.Normed.Operator.Extend, function or constantEnglish
Let $f$ be a linear equivalence of $E$ and $F$. Let $x_{16}$ be a linear map of $E$ and $x_{2}$. Let $x_{17}$ be a linear map of $F$ and $x_{3}$. Assume that $\operatorname{coe}$ applied to $x_{16}$ is a dense range. Assume that there exists a real number $C_{1}$, such that for all elements $x_{19}$ of $E$, the norm of $x_{17}$ applied to $f$ applied to $x_{19}$ is less than or equal to the product of $C_{1}$ and the norm of $x_{16}$ applied to $x_{19}$. Assume that $\operatorname{coe}$ applied to $x_{17}$ is a dense range. Assume that there exists a real number $C$, such that for all elements $x_{18}$ of $F$, the norm of $x_{16}$ applied to $\operatorname{symm}$ applied to $f$ and $x_{18}$ is less than or equal to the product of $C$ and the norm of $x_{17}$ applied to $x_{18}$. Then $\operatorname{extend}$ applied to $f$, $x_{16}$, $x_{17}$, $h_{6}$, $h_{7}$, $h_{8}$ and $h_{9}$ is a continuous linear equivalence of $x_{2}$ and $x_{3}$.
LinearEquiv.extendOfIsometrydefMathlib.Analysis.Normed.Operator.Extend, function or constantEnglish
Let $f$ be a linear equivalence of $E$ and $F$. Let $x_{16}$ be a linear map of $E$ and $x_{2}$. Let $x_{17}$ be a linear map of $F$ and $x_{3}$. Assume that $\operatorname{coe}$ applied to $x_{16}$ is a dense range. Assume that $\operatorname{coe}$ applied to $x_{17}$ is a dense range. Assume that for all elements $x_{18}$ of $E$, the norm of $x_{17}$ applied to $f$ applied to $x_{18}$ is equal to the norm of $x_{16}$ applied to $x_{18}$. Then $\operatorname{extendOfIsometry}$ applied to $f$, $x_{16}$, $x_{17}$, $h_{4}$, $h_{5}$ and $\mathrm{h\_norm}$ is a linear isometry equivalence of $x_{2}$ and $x_{3}$.
LinearIsometry.completiondefMathlib.Analysis.Normed.Operator.Extend, function or constantWording
the completion of f (from the name)
English
Let $f$ be a linear isometry of $E$ and $F$. Then the completion of $f$ is a linear isometry of the set of completions of $E$ and the set of completions of $F$.
LinearIsometry.fromCompletiondefMathlib.Analysis.Normed.Operator.Extend, function or constantEnglish
Let $f$ be a linear isometry of $E$ and $F$. Then $\operatorname{fromCompletion}$ applied to $f$ is a linear isometry of the set of completions of $E$ and $F$.
LinearMap.compLeftInversedefMathlib.Analysis.Normed.Operator.Extend, function or constantWording
the composition left inverse of f and g (from the name)
English
Let $f$ be a linear map of $E$ and $F$. Let $g$ be a linear map of $E$ and $x_{2}$. Then the composition left inverse of $f$ and $g$ is a continuous linear map of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{range} (g)}{x_{12}})}$ and $F$.
LinearMap.extendOfIsometrydefMathlib.Analysis.Normed.Operator.Extend, function or constantEnglish
Let $f$ be a linear map of $E$ and $F$. Assume that $\operatorname{coe}$ applied to $e$ is a dense range. Assume that for all elements $x_{12}$ of $E$, the norm of $f$ applied to $x_{12}$ is equal to the norm of $e$ applied to $x_{12}$. Then $\operatorname{extendOfIsometry}$ applied to $f$, $\mathrm{h\_dense}$ and $\mathrm{h\_norm}$ is a linear isometry of $x_{2}$ and $F$.
LinearMap.extendOfNormdefMathlib.Analysis.Normed.Operator.Extend, function or constantEnglish
Let $f$ be a linear map of $E$ and $F$. Let $e$ be a linear map of $E$ and $x_{2}$. Then $\operatorname{extendOfNorm}$ applied to $f$ and $e$ is a continuous linear map of $x_{2}$ and $F$ defined as $\operatorname{extend}$ applied to the composition left inverse of $f$ and $e$ and the subtype of the range of $e$.
ContinuousLinearMap.FredholmPackagestructureMathlib.Analysis.Normed.Operator.Fredholm.Basic, typeEnglish
Let $u$ be a continuous linear map of $E$ and $F$. Then the elements of $\operatorname{FredholmPackage}$ applied to $u$ are a basic type.
ContinuousLinearMap.FredholmPackage.decCodomdefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{FredholmPackage}$ applied to $u$. Then $\operatorname{decCodom}$ applied to $\mathrm{self}$ is an element of $\mathrm{FredholmDecomposition}$ applied to $x$ and $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
ContinuousLinearMap.FredholmPackage.decDomdefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{FredholmPackage}$ applied to $u$. Then $\operatorname{decDom}$ applied to $\mathrm{self}$ is an element of $\mathrm{FredholmDecomposition}$ applied to $x$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ContinuousLinearMap.FredholmPackage.equivdefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantWording
the equivalence of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{FredholmPackage}$ applied to $u$. Then the equivalence of $\mathrm{self}$ is a continuous linear equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\mathrm{FredholmDecomposition\_\_X\_u2081\_} (\operatorname{decDom} (\mathrm{self}))}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{FredholmDecomposition\_\_X\_u2081\_} (\operatorname{decCodom} (\mathrm{self}))}{x_{9}})}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
ContinuousLinearMap.FredholmPackage.quasiInversedefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Let $\mathrm{pkg}$ be an element of $\operatorname{FredholmPackage}$ applied to $u$. Then $\operatorname{quasiInverse}$ applied to $\mathrm{pkg}$ is a continuous linear map of $F$ and $E$ defined as the composition of the subtype of $\mathrm{FredholmDecomposition\_\_X\_u2081\_}$ applied to $\operatorname{decDom}$ applied to $\mathrm{pkg}$ and the composition of the continuous linear map of the inverse of the equivalence of $\mathrm{pkg}$ and the projection of $\operatorname{decCodom}$ applied to $\mathrm{pkg}$.
ContinuousLinearMap.IsFredholmstructureMathlib.Analysis.Normed.Operator.Fredholm.Basic, predicateEnglish
Let $u$ be a continuous linear map of $E$ and $F$. Then we can say that $\operatorname{IsFredholm}$ holds for $u$.
ContinuousLinearMap.IsFredholm.fredholmPackagedefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Assume that $\operatorname{IsFredholm}$ holds for $u$. Assume that the kernel of $\operatorname{toLinearMap}$ applied to $u$ is a top complement with respect to $x_{8}$. Assume that the range of $\operatorname{toLinearMap}$ applied to $u$ is a top complement with respect to $x_{9}$. Then $\operatorname{fredholmPackage}$ applied to $\mathrm{u\_fred}$, $\mathrm{h\_dom}$ and $\mathrm{h\_codom}$ is an element of $\operatorname{FredholmPackage}$ applied to $u$.
FredholmDecompositionstructureMathlib.Analysis.Normed.Operator.Fredholm.Basic, typeEnglish
Let $x$ and $E$ be sets. Then the elements of $\mathrm{FredholmDecomposition}$ applied to $x$ and $E$ are a basic type.
FredholmDecomposition.X₀defMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{FredholmDecomposition}$ applied to $x$ and $E$. Then $\mathrm{FredholmDecomposition\_\_X\_u2080\_}$ applied to $\mathrm{self}$ is a submodule of $x$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FredholmDecomposition.X₁defMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{FredholmDecomposition}$ applied to $x$ and $E$. Then $\mathrm{FredholmDecomposition\_\_X\_u2081\_}$ applied to $\mathrm{self}$ is a submodule of $x$ and $E$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
FredholmDecomposition.projdefMathlib.Analysis.Normed.Operator.Fredholm.Basic, function or constantWording
the projection of dec (from the name)
English
Let $\mathrm{dec}$ be an element of $\mathrm{FredholmDecomposition}$ applied to $x$ and $E$. Then the projection of $\mathrm{dec}$ is a continuous linear map of $E$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{FredholmDecomposition\_\_X\_u2081\_} (\mathrm{dec})}{x_{5}})}$ defined as $\operatorname{projectionOntoL}$ applied to $\mathrm{FredholmDecomposition\_\_X\_u2081\_}$ applied to $\mathrm{dec}$, $\mathrm{FredholmDecomposition\_\_X\_u2080\_}$ applied to $\mathrm{dec}$ and $\operatorname{isTopCompl}$ applied to $\mathrm{dec}$.
LinearIsometrystructureMathlib.Analysis.Normed.Operator.LinearIsometry, typeWording
linear isometry of E and x4 (from the name)
English
Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $E$ and $x_{4}$ be sets. Then the linear isometries of $E$ and $x_{4}$ are a basic type.
LinearIsometry.compdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a linear isometry of $x_{2}$ and $x_{3}$. Let $f$ be a linear isometry of $E$ and $x_{2}$. Then the composition of $g$ and $f$ is a linear isometry of $E$ and $x_{3}$.
LinearIsometry.equivRangedefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the equivalence range of f (from the name)
English
Let $f$ be a linear isometry of $F$ and $E$. Then the equivalence range of $f$ is a linear isometry equivalence of $F$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toLinearMap} (f))}{x_{8}})}$.
LinearIsometry.iddefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the identity linear isometry (from the docstring)
English
The identity linear isometry is a linear isometry of $E$ and $E$.
LinearIsometry.submoduleMapdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the submodule map of p and e (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Let $e$ be a linear isometry of $M$ and $x$. Then the submodule map of $p$ and $e$ is a linear isometry of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{ofClass} (e), p)}{x_{7}})}$.
LinearIsometry.toContinuousLinearMapdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the continuous linear map of f (from the name)
English
Let $f$ be a linear isometry of $E$ and $x_{1}$. Then the continuous linear map of $f$ is a continuous linear map of $E$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{continuous}$ applied to $f$.
LinearIsometryClassdefMathlib.Analysis.Normed.Operator.LinearIsometry, predicateEnglish
Let $x$ be a set. Let $R$, $E$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{LinearIsometryClass}$ holds for $x$, $R$, $E$ and $x_{1}$, if $\mathrm{SemilinearIsometryClass}$ holds for $x$, the identity ring homomorphism of $R$, $E$ and $x_{1}$.
LinearIsometryEquivstructureMathlib.Analysis.Normed.Operator.LinearIsometry, typeWording
linear isometry equivalence of E and x5 (from the name)
English
Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $E$ and $x_{5}$ be sets. Then the linear isometry equivalences of $E$ and $x_{5}$ are a basic type.
LinearIsometryEquiv.negdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the negation operation of R (from the docstring)
English
Let $R$ be a set. Then the negation operation of $R$ is a linear isometry equivalence of $E$ and $E$.
LinearIsometryEquiv.ofBoundsdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry equivalence of e (from the name)
English
Let $e$ be a linear equivalence of $E$ and $x_{1}$ such that for all elements $x_{10}$ of $E$, the norm of $e$ applied to $x_{10}$ is less than or equal to the norm of $x_{10}$ and for all elements $y$ of $x_{1}$, the norm of $\operatorname{symm}$ applied to $e$ and $y$ is less than or equal to the norm of $y$. Then the linear isometry equivalence of $e$ is a linear isometry equivalence of $E$ and $x_{1}$.
LinearIsometryEquiv.ofEqdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry equivalence of p and q (from the name)
English
Let $p$ and $q$ be submodules of $\mathrm{R'}$ and $E$ such that $\EqtMACRoH {p}{q}$. Then the linear isometry equivalence of $p$ and $q$ is a linear isometry equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {q}{x_{4}})}$.
LinearIsometryEquiv.ofLinearIsometrydefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry equivalence of f and g (from the name)
English
Let $f$ be a linear isometry of $E$ and $x_{1}$. Let $g$ be a linear map of $x_{1}$ and $E$ such that the composition of $\operatorname{toLinearMap}$ applied to $f$ and $g$ is equal to the identity and the composition of $g$ and $\operatorname{toLinearMap}$ applied to $f$ is equal to the identity. Then the linear isometry equivalence of $f$ and $g$ is a linear isometry equivalence of $E$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the linear equivalence of $\operatorname{toLinearMap}$ applied to $f$ and $g$ and the function that maps $x_{10}$ to $\mathrm{LinearIsometry\_\_norm\_map}$ applied to $f$ and $x_{10}$.
LinearIsometryEquiv.ofSurjectivedefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry equivalence of f and hfr (from the name)
English
Let $f$ be a linear isometry of $F$ and $x_{1}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the linear isometry equivalence of $f$ and $\mathrm{hfr}$ is a linear isometry equivalence of $F$ and $x_{1}$.
LinearIsometryEquiv.ofTopdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry equivalence of p (from the name)
English
Let $E$ be a set. Let $p$ be a submodule of $R$ and $E$ such that $p$ is equal to the top. Then the linear isometry equivalence of $p$ is a linear isometry equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $E$.
LinearIsometryEquiv.prodAssocdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the product associator of x and x1 (from the name)
English
Let $R$, $E$, $x$ and $x_{1}$ be sets. Then the product associator of $x$ and $x_{1}$ is a linear isometry equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $E$ and $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $E$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
LinearIsometryEquiv.prodCommdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantEnglish
Let $R$, $E$ and $x$ be sets. Then $\operatorname{prodComm}$ applied to $R$, $E$ and $x$ is a linear isometry equivalence of $\mathrm{Prod}$ applied to $E$ and $x$ and $\mathrm{Prod}$ applied to $x$ and $E$.
LinearIsometryEquiv.refldefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the identity of R and E (from the name)
English
Let $R$ and $E$ be sets. Then the identity of $R$ and $E$ is a linear isometry equivalence of $E$ and $E$.
LinearIsometryEquiv.submoduleMapdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the submodule map of p and e (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Let $e$ be a linear isometry equivalence of $M$ and $x_{1}$. Then the submodule map of $p$ and $e$ is a linear isometry equivalence of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {p}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toLinearMap} (\operatorname{toLinearEquiv} (\operatorname{toContinuousLinearEquiv} (e))), p)}{x_{11}})}$.
LinearIsometryEquiv.symmdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{1}$. Then the inverse of $e$ is a linear isometry equivalence of $x_{1}$ and $E$.
LinearIsometryEquiv.toContinuousLinearEquivdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the continuous linear equivalence of e (from the name)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{1}$. Then the continuous linear equivalence of $e$ is a continuous linear equivalence of $E$ and $x_{1}$.
LinearIsometryEquiv.toHomeomorphdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{1}$. Then the homeomorphism of $e$ is a homeomorphism of $E$ and $x_{1}$ defined as the homeomorphism of the isometry equivalence of $e$.
LinearIsometryEquiv.toIsometryEquivdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the isometry equivalence of e (from the name)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{1}$. Then the isometry equivalence of $e$ is an isometry equivalence of $E$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the equivalence of $\operatorname{toLinearEquiv}$ applied to $e$ and $\operatorname{isometry}$ applied to $e$.
LinearIsometryEquiv.toLinearIsometrydefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry of e (from the name)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{1}$. Then the linear isometry of $e$ is a linear isometry of $E$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $e$ and $\mathrm{LinearIsometryEquiv\_\_norm\_map'}$ applied to $e$.
LinearIsometryEquiv.transdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be a linear isometry equivalence of $E$ and $x_{2}$. Let $\mathrm{e'}$ be a linear isometry equivalence of $x_{2}$ and $x_{3}$. Then the composition of $e$ and $\mathrm{e'}$ is a linear isometry equivalence of $E$ and $x_{3}$.
LinearIsometryEquiv.uliftdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the lift of R and E (from the name)
English
Let $R$ and $E$ be sets. Then the lift of $R$ and $E$ is a linear isometry equivalence of $\mathrm{ULift}$ applied to $E$ and $E$.
LinearIsometryEquivClassdefMathlib.Analysis.Normed.Operator.LinearIsometry, predicateEnglish
Let $x$ be a set. Let $R$, $E$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{LinearIsometryEquivClass}$ holds for $x$, $R$, $E$ and $x_{1}$, if $\mathrm{SemilinearIsometryEquivClass}$ holds for $x$, the identity ring homomorphism of $R$, $E$ and $x_{1}$.
LinearMap.toLinearIsometrydefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the linear isometry of f and hf (from the name)
English
Let $f$ be a linear map of $E$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is an isometry. Then the linear isometry of $f$ and $\mathrm{hf}$ is a linear isometry of $E$ and $x_{1}$.
MulOpposite.opLinearIsometryEquivdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the opposite linear isometry equivalence of R and H (from the name)
English
Let $R$ and $H$ be sets. Then the opposite linear isometry equivalence of $R$ and $H$ is a linear isometry equivalence of $H$ and the set of multiplicative opposites of $H$.
SemilinearIsometryClassclassMathlib.Analysis.Normed.Operator.LinearIsometry, predicateEnglish
Let $x$ be a set. Let $x_{4}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $x_{1}$. Let $E$ and $x_{5}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SemilinearIsometryClass}$ holds for $x$, $x_{4}$, $E$ and $x_{5}$.
SemilinearIsometryEquivClassclassMathlib.Analysis.Normed.Operator.LinearIsometry, predicateEnglish
Let $x$ be a set. Let $x_{4}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $x_{1}$. Let $E$ and $x_{6}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SemilinearIsometryEquivClass}$ holds for $x$, $x_{4}$, $E$ and $x_{6}$.
Submodule.subtypeₗᵢdefMathlib.Analysis.Normed.Operator.LinearIsometry, function or constantWording
the subtype of p (from the name)
English
Let $p$ be a submodule of $\mathrm{R'}$ and $E$. Then the subtype of $p$ is a linear isometry of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $E$.
ContinuousLinearMap.lsmuldefMathlib.Analysis.Normed.Operator.Mul, function or constantEnglish
Let $x$ and $R$ be sets. Then $\operatorname{lsmul}$ applied to $x$ and $R$ is a continuous linear map of $R$ and the set of continuous linear maps of $E$ and $E$.
ContinuousLinearMap.muldefMathlib.Analysis.Normed.Operator.Mul, function or constantWording
the product of x and R (from the name)
English
Let $x$ and $R$ be sets. Then the product of $x$ and $R$ is a continuous linear map of $R$ and the set of continuous linear maps of $R$ and $R$.
ContinuousLinearMap.mulLeftRightdefMathlib.Analysis.Normed.Operator.Mul, function or constantWording
the right multiplicative left of x and R (from the name)
English
Let $x$ and $R$ be sets. Then the right multiplicative left of $x$ and $R$ is a continuous linear map of $R$ and the set of continuous linear maps of $R$ and the set of continuous linear maps of $R$ and $R$ defined as the composition of the flip of the composition of the composition of $R$ and $R$ and the flip of the product of $x$ and $R$ and the product of $x$ and $R$.
ContinuousLinearMap.mulₗᵢdefMathlib.Analysis.Normed.Operator.Mul, function or constantWording
the product of x and R (from the name)
English
Let $x$ and $R$ be sets. Then the product of $x$ and $R$ is a linear isometry of $R$ and the set of continuous linear maps of $R$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to the product of $x$ and $R$ and the function that maps $x_{4}$ to $\mathrm{ContinuousLinearMap\_\_opNorm\_mul\_apply}$ applied to $x$, $R$ and $x_{4}$.
ContinuousLinearMap.toSpanSingletonLIEdefMathlib.Analysis.Normed.Operator.Mul, function or constantEnglish
Let $x$ and $E$ be sets. Then $\operatorname{toSpanSingletonLIE}$ applied to $x$ and $E$ is a linear isometry equivalence of $E$ and the set of continuous linear maps of $x$ and $E$.
NonUnitalAlgHom.LmuldefMathlib.Analysis.Normed.Operator.Mul, function or constantEnglish
Let $x$ and $R$ be sets. Then $\operatorname{Lmul}$ applied to $x$ and $R$ is a non unital algebra homomorphism of $R$ and the set of continuous linear maps of $R$ and $R$.
RegularNormedAlgebraclassMathlib.Analysis.Normed.Operator.Mul, predicateEnglish
Let $x$ and $R$ be sets. Then we can say that $\mathrm{RegularNormedAlgebra}$ holds for $x$ and $R$.
IsCoercivedefMathlib.Analysis.Normed.Operator.NormedSpace, predicateWording
B is coercive (from the name)
English
Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $\Real$. Then $B$ is coercive, if there exists a real number $C$, such that $0 < C$ and for all elements $u$ of $E$, the product of the product of $C$ and the norm of $u$ and the norm of $u$ is less than or equal to $\operatorname{coe}$ applied to $B$, $u$ and $u$.
LinearIsometry.inldefMathlib.Analysis.Normed.Operator.NormedSpace, function or constantWording
the left injection of E and F (from the name)
English
Let $x$, $E$ and $F$ be sets. Then the left injection of $E$ and $F$ is a linear isometry of $E$ and $\mathrm{Prod}$ applied to $E$ and $F$.
LinearIsometry.inrdefMathlib.Analysis.Normed.Operator.NormedSpace, function or constantWording
the right injection of E and F (from the name)
English
Let $x$, $E$ and $F$ be sets. Then the right injection of $E$ and $F$ is a linear isometry of $F$ and $\mathrm{Prod}$ applied to $E$ and $F$.
LinearIsometry.postcompdefMathlib.Analysis.Normed.Operator.NormedSpace, function or constantWording
the postcomposition of a (from the name)
English
Let $a$ be a linear isometry of $F$ and $G$. Then the postcomposition of $a$ is a linear isometry of the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $E$ and $G$.
LinearIsometry.singledefMathlib.Analysis.Normed.Operator.NormedSpace, function or constantEnglish
Let $x_{3}$ be a set. Let $E$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then $\operatorname{single}$ applied to $x_{3}$, $E$ and $i$ is a linear isometry of $E$ applied to $i$ and the set of functions from elements $j$ of $x$ to elements of $E$ applied to $j$.
ContinuousLinearMap.prodMapLdefMathlib.Analysis.Normed.Operator.Prod, function or constantWording
the product map of x4 and x5 (from the name)
English
Let $x$, $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ be sets. Then the product map of $x_{4}$ and $x_{5}$ is a continuous linear map of $\mathrm{Prod}$ applied to the set of continuous linear maps of $x_{2}$ and $x_{3}$ and the set of continuous linear maps of $x_{4}$ and $x_{5}$ and the set of continuous linear maps of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{4}$ and $\mathrm{Prod}$ applied to $x_{3}$ and $x_{5}$.
ContinuousLinearMap.prodₗᵢdefMathlib.Analysis.Normed.Operator.Prod, function or constantWording
the product of R (from the name)
English
Let $R$ be a set. Then the product of $R$ is a linear isometry equivalence of $\mathrm{Prod}$ applied to the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $E$ and $G$ and the set of continuous linear maps of $E$ and $\mathrm{Prod}$ applied to $F$ and $G$.
HasSolidNormclassMathlib.Analysis.Normed.Order.Lattice, predicateWording
x has solid norms (from the name)
English
Let $x$ be a set. Then we can say that $x$ has solid norms.
NonUnitalNormedCommRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a non unital normed commutative ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a non unital normed commutative ring.
NonUnitalNormedRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a non unital normed ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a non unital normed ring.
NonUnitalSeminormedCommRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a non unital seminormed commutative ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a non unital seminormed commutative ring.
NonUnitalSeminormedRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a non unital seminormed ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a non unital seminormed ring.
NormMulClassclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a norm multiplicative class (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a norm multiplicative class.
NormOneClassclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a norm one class (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a norm one class.
NormedCommRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a normed commutative ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a normed commutative ring.
NormedRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a normed ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a normed ring.
RingHom.IsBoundeddefMathlib.Analysis.Normed.Ring.Basic, predicateWording
f is bounded (from the name)
English
Let $f$ be a ring homomorphism of $x$ and $x_{2}$. Then $f$ is bounded, if there exists a real number $C$, such that $0 < C$ and for all elements $x_{4}$ of $x$, the norm of $f$ applied to $x_{4}$ is less than or equal to the product of $C$ and the norm of $x_{4}$.
RingHomIsometricclassMathlib.Analysis.Normed.Ring.Basic, predicateEnglish
Let $x_{6}$ be a ring homomorphism of $x$ and $x_{1}$. Then we can say that $\mathrm{RingHomIsometric}$ holds for $x_{6}$.
SeminormedCommRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a seminormed commutative ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a seminormed commutative ring.
SeminormedRingclassMathlib.Analysis.Normed.Ring.Basic, predicateWording
x is a seminormed ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a seminormed ring.
nnnormHomdefMathlib.Analysis.Normed.Ring.Basic, function or constantWording
the norm homomorphism (from the name)
English
The norm homomorphism is a monoid with zero homomorphism of $x$ and $\mathrm{NNReal}$.
normHomdefMathlib.Analysis.Normed.Ring.Basic, function or constantWording
the norm homomorphism (from the name)
English
The norm homomorphism is a monoid with zero homomorphism of $x$ and $\Real$.
Dilation.mulLeftdefMathlib.Analysis.Normed.Ring.Lemmas, function or constantWording
the left multiplicative of a and ha (from the name)
English
Let $a$ be an element of $x$ such that $a \neq 0$. Then the left multiplicative of $a$ and $\mathrm{ha}$ is a dilation of $x$ and $x$.
Dilation.mulRightdefMathlib.Analysis.Normed.Ring.Lemmas, function or constantWording
the right multiplicative of a and ha (from the name)
English
Let $a$ be an element of $x$ such that $a \neq 0$. Then the right multiplicative of $a$ and $\mathrm{ha}$ is a dilation of $x$ and $x$.
Units.adddefMathlib.Analysis.Normed.Ring.Units, function or constantWording
the sum of x1 and t (from the name)
English
Let $x_{1}$ be a unit of $R$. Let $t$ be an element of $R$ such that the norm of $t$ is less than $\operatorname{inv}$ applied to the norm of the underlying value in the base of $\operatorname{inv}$ applied to $x_{1}$. Then the sum of $x_{1}$ and $t$ is a unit of $R$.
Units.ofNearbydefMathlib.Analysis.Normed.Ring.Units, function or constantWording
the unit of x1 and y (from the name)
English
Let $x_{1}$ be a unit of $R$. Let $y$ be an element of $R$ such that the norm of the difference between $y$ and the underlying value in the base of $x_{1}$ is less than $\operatorname{inv}$ applied to the norm of the underlying value in the base of $\operatorname{inv}$ applied to $x_{1}$. Then the unit of $x_{1}$ and $y$ is a unit of $R$.
AbsoluteValue.LiesOverclassMathlib.Analysis.Normed.Ring.WithAbs, predicateEnglish
Let $w$ be an absolute value of $L$ and $S$. Let $v$ be an absolute value of $K$ and $S$. Then we can say that $\operatorname{LiesOver}$ holds for $w$ and $v$.
AbsoluteValue.underdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantEnglish
Let $K$ be a set. Let $w$ be an absolute value of $L$ and $S$. Then $\operatorname{under}$ applied to $K$ and $w$ is an absolute value of $K$ and $S$ defined as the composition of $w$ and $\mathrm{FaithfulSMul\_\_algebraMap\_injective}$ applied to $K$ and $L$.
WithAbsstructureMathlib.Analysis.Normed.Ring.WithAbs, typeEnglish
Let $v$ be an absolute value of $R$ and $S$. Then the elements of $\mathrm{WithAbs}$ applied to $v$ are a basic type.
WithAbs.algEquivdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantWording
the algebra isomorphism of R and v (from the name)
English
Let $R$ be a set. Let $v$ be an absolute value of $T$ and $S$. Then the algebra isomorphism of $R$ and $v$ is an algebra isomorphism of $\mathrm{WithAbs}$ applied to $v$ and $T$ defined as the algebra isomorphism of $R$ and $\operatorname{toEquiv}$ applied to the equivalence of $v$.
WithAbs.congrdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantWording
the congruence of w and f (from the name)
English
Let $v$ be an absolute value of $R$ and $S$. Let $w$ be an absolute value of $T$ and $S$. Let $f$ be a ring isomorphism of $R$ and $T$. Then the congruence of $w$ and $f$ is a ring isomorphism of $\mathrm{WithAbs}$ applied to $v$ and $\mathrm{WithAbs}$ applied to $w$.
WithAbs.equivdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantWording
the equivalence of v (from the name)
English
Let $v$ be an absolute value of $R$ and $S$. Then the equivalence of $v$ is a ring isomorphism of $\mathrm{WithAbs}$ applied to $v$ and $R$.
WithAbs.linearEquivdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantWording
the linear equivalence of R and v (from the name)
English
Let $R$ be a set. Let $v$ be an absolute value of $T$ and $S$. Then the linear equivalence of $R$ and $v$ is a linear equivalence of $\mathrm{WithAbs}$ applied to $v$ and $T$ defined as the linear equivalence of $R$ and the additive equivalence of the equivalence of $v$.
WithAbs.mapdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantWording
the map of w and f (from the name)
English
Let $v$ be an absolute value of $R$ and $S$. Let $w$ be an absolute value of $T$ and $S$. Let $f$ be a ring homomorphism of $R$ and $T$. Then the map of $w$ and $f$ is a ring homomorphism of $\mathrm{WithAbs}$ applied to $v$ and $\mathrm{WithAbs}$ applied to $w$ defined as the composition of the ring homomorphism of the inverse of the equivalence of $w$ and the composition of $f$ and the ring homomorphism of the equivalence of $v$.
WithAbs.ofAbsdefMathlib.Analysis.Normed.Ring.WithAbs, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WithAbs}$ applied to $v$. Then $\operatorname{ofAbs}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
AlgebraNormstructureMathlib.Analysis.Normed.Unbundled.AlgebraNorm, typeWording
algebra norm of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the algebra norms of $R$ and $S$ are a basic type.
AlgebraNorm.isScalarTower_restrictiondefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the restriction of hinj and f (from the docstring)
English
Assume that $\operatorname{coe}$ applied to the algebra map of $A$ and $S$ is injective. Let $f$ be an algebra norm of $R$ and $S$. Then the restriction of $\mathrm{hinj}$ and $f$ is an algebra norm of $R$ and $A$.
AlgebraNorm.restrictiondefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the restriction of A and f (from the docstring)
English
Let $A$ be a subalgebra of $R$ and $S$. Let $f$ be an algebra norm of $R$ and $S$. Then the restriction of $A$ and $f$ is an algebra norm of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$.
AlgebraNorm.toRingSeminorm'defMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the ring seminorm of f (from the name)
English
Let $f$ be an algebra norm of $R$ and $S$. Then the ring seminorm of $f$ is a ring seminorm of $S$ defined as $\operatorname{toRingSeminorm}$ applied to $\operatorname{toRingNorm}$ applied to $f$.
AlgebraNorm.toSeminormdefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the seminorm of self (from the name)
English
Let $\mathrm{self}$ be an algebra norm of $R$ and $S$. Then the seminorm of $\mathrm{self}$ is a seminorm of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\operatorname{toRingSeminorm}$ applied to $\operatorname{toRingNorm}$ applied to $\mathrm{self}$ and $\operatorname{smul'}$ applied to $\mathrm{self}$.
AlgebraNormClassclassMathlib.Analysis.Normed.Unbundled.AlgebraNorm, predicateEnglish
Let $F$ be a set. Let $R$ and $S$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{AlgebraNormClass}$ holds for $F$, $R$ and $S$.
MulAlgebraNormstructureMathlib.Analysis.Normed.Unbundled.AlgebraNorm, typeWording
multiplicative algebra norm of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the multiplicative algebra norms of $R$ and $S$ are a basic type.
MulAlgebraNorm.toAlgebraNormdefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the algebra norm of f (from the name)
English
Let $f$ be a multiplicative algebra norm of $R$ and $S$. Then the algebra norm of $f$ is an algebra norm of $R$ and $S$.
MulAlgebraNorm.toSeminormdefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the seminorm of self (from the name)
English
Let $\mathrm{self}$ be a multiplicative algebra norm of $R$ and $S$. Then the seminorm of $\mathrm{self}$ is a seminorm of $R$ and $S$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\operatorname{toMulRingSeminorm}$ applied to $\operatorname{toMulRingNorm}$ applied to $\mathrm{self}$ and $\operatorname{smul'}$ applied to $\mathrm{self}$.
MulAlgebraNormClassclassMathlib.Analysis.Normed.Unbundled.AlgebraNorm, predicateEnglish
Let $F$ be a set. Let $R$ and $S$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{MulAlgebraNormClass}$ holds for $F$, $R$ and $S$.
MulRingNorm.toRingNormdefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the ring norm of f (from the name)
English
Let $f$ be a multiplicative ring norm of $R$. Then the ring norm of $f$ is a ring norm of $R$.
NormedAlgebra.toMulAlgebraNormdefMathlib.Analysis.Normed.Unbundled.AlgebraNorm, function or constantWording
the multiplicative algebra norm of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the multiplicative algebra norm of $K$ and $L$ is a multiplicative algebra norm of $K$ and $L$.
Module.Basis.normdefMathlib.Analysis.Normed.Unbundled.FiniteExtension, function or constantWording
the norm of B and x5 (from the name)
English
Let $B$ be a basis of $K$ and $L$. Let $x_{5}$ be an element of $L$. Then the norm of $B$ and $x_{5}$ is a real number defined as the supremum of the universal set and the function that maps $i$ to the norm of $\operatorname{coe}$ applied to the representation of $B$, $x_{5}$ and $i$.
IsUltrametricDist.algNormOfAlgEquivdefMathlib.Analysis.Normed.Unbundled.InvariantExtension, function or constantWording
the algebra norm of x3 (from the name)
English
Let $x_{3}$ be an algebra isomorphism of $L$ and $L$. Then the algebra norm of $x_{3}$ is an algebra norm of $K$ and $L$.
IsUltrametricDist.invariantExtensiondefMathlib.Analysis.Normed.Unbundled.InvariantExtension, function or constantWording
the invariant extension of K and L (from the name)
English
Let $K$ and $L$ be sets. Then the invariant extension of $K$ and $L$ is an algebra norm of $K$ and $L$.
AlgebraNorm.toMulAlgebraNormdefMathlib.Analysis.Normed.Unbundled.IsPowMulUnique, function or constantWording
the multiplicative algebra norm of f and hf (from the name)
English
Let $f$ be an algebra norm of $K$ and $L$ such that $\operatorname{coe}$ applied to $f$ is a power product. Then the multiplicative algebra norm of $f$ and $\mathrm{hf}$ is a multiplicative algebra norm of $K$ and $L$.
MulRingNormstructureMathlib.Analysis.Normed.Unbundled.RingSeminorm, typeWording
multiplicative ring norm of R (from the name)
English
Let $R$ be a set. Then the multiplicative ring norms of $R$ are a basic type.
MulRingNorm.mulRingNormEquivAbsoluteValuedefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the multiplicative ring norm equivalence absolute value (from the name)
English
The multiplicative ring norm equivalence absolute value is an equivalence from the set of multiplicative ring norms of $R$ to the set of absolute values of $R$ and $\Real$.
MulRingNorm.ofAbsoluteValuedefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the multiplicative ring norm of v (from the name)
English
Let $v$ be an absolute value of $R$ and $\Real$. Then the multiplicative ring norm of $v$ is a multiplicative ring norm of $R$.
MulRingNorm.toAbsoluteValuedefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the absolute value of N (from the name)
English
Let $N$ be a multiplicative ring norm of $R$. Then the absolute value of $N$ is an absolute value of $R$ and $\Real$.
MulRingNorm.toAddGroupNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the additive group norm of self (from the name)
English
Let $\mathrm{self}$ be a multiplicative ring norm of $R$. Then the additive group norm of $\mathrm{self}$ is an additive group norm of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\operatorname{toMulRingSeminorm}$ applied to $\mathrm{self}$ and $\mathrm{MulRingNorm\_\_eq\_zero\_of\_map\_eq\_zero'}$ applied to $\mathrm{self}$.
MulRingSeminormstructureMathlib.Analysis.Normed.Unbundled.RingSeminorm, typeWording
multiplicative ring seminorm of R (from the name)
English
Let $R$ be a set. Then the multiplicative ring seminorms of $R$ are a basic type.
MulRingSeminorm.toMonoidWithZeroHomdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the monoid with zero homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a multiplicative ring seminorm of $R$. Then the monoid with zero homomorphism of $\mathrm{self}$ is a monoid with zero homomorphism of $R$ and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\mathrm{self}$ and $\mathrm{AddGroupSeminorm\_\_map\_zero'}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\mathrm{self}$, $\mathrm{MulRingSeminorm\_\_map\_one'}$ applied to $\mathrm{self}$ and $\mathrm{MulRingSeminorm\_\_map\_mul'}$ applied to $\mathrm{self}$.
NormedField.toAbsoluteValuedefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the absolute value of R (from the name)
English
Let $R$ be a set. Then the absolute value of $R$ is an absolute value of $R$ and $\Real$.
NormedField.toMulRingNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the multiplicative ring norm of R (from the name)
English
Let $R$ be a set. Then the multiplicative ring norm of $R$ is a multiplicative ring norm of $R$.
NormedRing.toRingNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the ring norm of R (from the name)
English
Let $R$ be a set. Then the ring norm of $R$ is a ring norm of $R$.
RingNormstructureMathlib.Analysis.Normed.Unbundled.RingSeminorm, typeWording
ring norm of R (from the name)
English
Let $R$ be a set. Then the ring norms of $R$ are a basic type.
RingNorm.toAddGroupNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the additive group norm of self (from the name)
English
Let $\mathrm{self}$ be a ring norm of $R$. Then the additive group norm of $\mathrm{self}$ is an additive group norm of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddGroupSeminorm}$ applied to $\operatorname{toRingSeminorm}$ applied to $\mathrm{self}$ and $\mathrm{RingNorm\_\_eq\_zero\_of\_map\_eq\_zero'}$ applied to $\mathrm{self}$.
RingSeminormstructureMathlib.Analysis.Normed.Unbundled.RingSeminorm, typeWording
ring seminorm of R (from the name)
English
Let $R$ be a set. Then the ring seminorms of $R$ are a basic type.
RingSeminorm.toRingNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the ring norm of f and hnt (from the name)
English
Let $f$ be a ring seminorm of $K$ such that $f \neq 0$. Then the ring norm of $f$ and $\mathrm{hnt}$ is a ring norm of $K$.
SeminormedRing.toRingSeminormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the ring seminorm of R (from the name)
English
Let $R$ be a set. Then the ring seminorm of $R$ is a ring seminorm of $R$.
normRingNormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the norm of R (from the docstring)
English
Let $R$ be a set. Then the norm of $R$ is a ring norm of $R$.
normRingSeminormdefMathlib.Analysis.Normed.Unbundled.RingSeminorm, function or constantWording
the norm of R (from the docstring)
English
Let $R$ be a set. Then the norm of $R$ is a ring seminorm of $R$.
normFromBoundeddefMathlib.Analysis.Normed.Unbundled.SeminormFromBounded, function or constantEnglish
Assume that $f (0)= 0$. Assume that $0 \leq f$. Assume that for all elements $x_{2}$ and $y$ of $R$, $f (x_{2} \times y)\leq c \times f (x_{2})\times f (y)$. Assume that for all elements $a$ and $b$ of $R$, $f (a + b)\leq f (a)+ f (b)$. Assume that for all elements $x_{1}$ of $R$, $f (\operatorname{neg} (x_{1}))= f (x_{1})$. Assume that the preimage of $f$ and $\operatorname{singleton}$ applied to $0$ is equal to $\operatorname{singleton}$ applied to $0$. Then $\mathrm{normFromBounded}$ applied to $\mathrm{f\_zero}$, $\mathrm{f\_nonneg}$, $\mathrm{f\_mul}$, $\mathrm{f\_add}$, $\mathrm{f\_neg}$ and $\mathrm{f\_ker}$ is a ring norm of $R$.
seminormFromBoundeddefMathlib.Analysis.Normed.Unbundled.SeminormFromBounded, function or constantEnglish
Assume that $f (0)= 0$. Assume that $0 \leq f$. Assume that for all elements $x_{2}$ and $y$ of $R$, $f (x_{2} \times y)\leq c \times f (x_{2})\times f (y)$. Assume that for all elements $a$ and $b$ of $R$, $f (a + b)\leq f (a)+ f (b)$. Assume that for all elements $x_{1}$ of $R$, $f (\operatorname{neg} (x_{1}))= f (x_{1})$. Then $\mathrm{seminormFromBounded}$ applied to $\mathrm{f\_zero}$, $\mathrm{f\_nonneg}$, $\mathrm{f\_mul}$, $\mathrm{f\_add}$ and $\mathrm{f\_neg}$ is a ring seminorm of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{seminormFromBounded'}$ applied to $f$, $\mathrm{seminormFromBounded\_zero}$ applied to $\mathrm{f\_zero}$, $\mathrm{seminormFromBounded\_add}$ applied to $\mathrm{f\_nonneg}$, $\mathrm{f\_mul}$ and $\mathrm{f\_add}$ and $\mathrm{seminormFromBounded\_neg}$ applied to $\mathrm{f\_neg}$ and $\mathrm{seminormFromBounded\_mul}$ applied to $\mathrm{f\_nonneg}$ and $\mathrm{f\_mul}$.
seminormFromBounded'defMathlib.Analysis.Normed.Unbundled.SeminormFromBounded, function or constantEnglish
Let $f$ be a function from elements of $R$ to real numbers. Let $x_{1}$ be an element of $R$. Then $\mathrm{seminormFromBounded'}$ applied to $f$ and $x_{1}$ is a real number defined as the supremum of the function that maps $y$ to $\frac{ f (x_{1} \times y)}{f (y)}$.
algNormFromConstdefMathlib.Analysis.Normed.Unbundled.SeminormFromConst, function or constantWording
the algebra norm from constant of hg_k and hg_pm (from the name)
English
Assume that $g (k)\neq 0$. Assume that $\operatorname{coe}$ applied to $g$ is a power product. Then the algebra norm from constant of $\mathrm{hg\_k}$ and $\mathrm{hg\_pm}$ is an algebra norm of $F$ and $K$.
normFromConstdefMathlib.Analysis.Normed.Unbundled.SeminormFromConst, function or constantWording
the norm from constant of hg_k and hg_pm (from the name)
English
Assume that $g (k)\neq 0$. Assume that $\operatorname{coe}$ applied to $g$ is a power product. Then the norm from constant of $\mathrm{hg\_k}$ and $\mathrm{hg\_pm}$ is a ring norm of $K$.
seminormFromConstdefMathlib.Analysis.Normed.Unbundled.SeminormFromConst, function or constantWording
the seminorm from constant of hc and hpm (from the name)
English
Assume that $f (c)\neq 0$. Assume that $\operatorname{coe}$ applied to $f$ is a power product. Then the seminorm from constant of $\mathrm{hc}$ and $\mathrm{hpm}$ is a ring seminorm of $R$.
seminormFromConst'defMathlib.Analysis.Normed.Unbundled.SeminormFromConst, function or constantWording
the seminorm from constant of f and x1 (from the name)
English
Let $c$ and $x_{1}$ be elements of $R$. Let $f$ be a ring seminorm of $R$. Then the seminorm from constant of $f$ and $x_{1}$ is a real number defined as the infimum of $\mathrm{seminormFromConst\_seq}$ applied to $x_{1}$.
seminormFromConst_seqdefMathlib.Analysis.Normed.Unbundled.SeminormFromConst, function or constantWording
the seminorm from constant sequence of x1 and x2 (from the name)
English
Let $c$ and $x_{1}$ be elements of $R$. Let $f$ be a ring seminorm of $R$. Let $x_{2}$ be a natural number. Then the seminorm from constant sequence of $x_{1}$ and $x_{2}$ is a real number defined as $\frac{ f (x_{1} \times c ^ {x_{2}})}{f (c)^ {x_{2}}}$.
smoothingFundefMathlib.Analysis.Normed.Unbundled.SmoothingSeminorm, function or constantEnglish
Let $x_{1}$ be a ring seminorm of $R$. Let $x_{2}$ be an element of $R$. Then $\mathrm{smoothingFun}$ applied to $x_{1}$ and $x_{2}$ is a real number defined as the infimum of the function that maps $n$ to the exponentiation of $x_{1}$ applied to the exponentiation of $x_{2}$ to the value of $n$ to the quotient of $1$ and the value of $n$.
smoothingSeminormdefMathlib.Analysis.Normed.Unbundled.SmoothingSeminorm, function or constantEnglish
Let $x_{1}$ be a ring seminorm of $R$ such that $x_{1} (1)\leq 1$ and $\operatorname{coe}$ applied to $x_{1}$ is a nonarchimedean. Then $\mathrm{smoothingSeminorm}$ applied to $x_{1}$, $h$ and $\mathrm{hna}$ is a ring seminorm of $R$.
smoothingSeminormSeqdefMathlib.Analysis.Normed.Unbundled.SmoothingSeminorm, function or constantEnglish
Let $x_{1}$ be a ring seminorm of $R$. Let $x_{2}$ be an element of $R$. Let $x_{3}$ be a natural number. Then $\mathrm{smoothingSeminormSeq}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a real number defined as $x_{1} (x_{2} ^ {x_{3}})^ {\frac{ 1}{x_{3}}}$.