InnerProductSpace.laplacianWithindefMathlib.Analysis.InnerProductSpace.Laplacian, function or constantEnglish
Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Let $x_{4}$ be an element of $E$. Then $\operatorname{laplacianWithin}$ applied to $f$, $s$ and $x_{4}$ is an element of $F$ defined as $\operatorname{tensorIteratedFDerivWithinTwo}$ applied to $\Real$, $f$, $s$, $x_{4}$ and the canonical covariant tensor of $E$.
bilinearIteratedFDerivTwodefMathlib.Analysis.InnerProductSpace.Laplacian, function or constantEnglish
Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{6}$ be an element of $E$. Then $\mathrm{bilinearIteratedFDerivTwo}$ applied to $x$, $f$ and $x_{6}$ is a linear map of $E$ and the set of linear maps of $E$ and $F$ defined as $\mathrm{ContinuousLinearMap\_\_toLinearMap\_u2081\_\_u2082\_\_\_app}$ applied to the derivative of $\mathrm{fderiv}$ applied to $f$ and $x_{6}$.
bilinearIteratedFDerivWithinTwodefMathlib.Analysis.InnerProductSpace.Laplacian, function or constantEnglish
Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Let $x_{6}$ be an element of $E$. Then $\mathrm{bilinearIteratedFDerivWithinTwo}$ applied to $x$, $f$, $s$ and $x_{6}$ is a linear map of $E$ and the set of linear maps of $E$ and $F$ defined as $\mathrm{ContinuousLinearMap\_\_toLinearMap\_u2081\_\_u2082\_\_\_app}$ applied to $\mathrm{fderivWithin}$ applied to $x$, $\mathrm{fderivWithin}$ applied to $x$, $f$ and $s$, $s$ and $x_{6}$.
tensorIteratedFDerivTwodefMathlib.Analysis.InnerProductSpace.Laplacian, function or constantEnglish
Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{6}$ be an element of $E$. Then $\mathrm{tensorIteratedFDerivTwo}$ applied to $x$, $f$ and $x_{6}$ is a linear map of the set of tensor products of $E$ and $E$ and $F$ defined as the lift of $\mathrm{bilinearIteratedFDerivTwo}$ applied to $x$, $f$ and $x_{6}$.
tensorIteratedFDerivWithinTwodefMathlib.Analysis.InnerProductSpace.Laplacian, function or constantEnglish
Let $x$ be a set. Let $f$ be a function from elements of $E$ to elements of $F$. Let $s$ be an element of $\wp E$. Let $x_{6}$ be an element of $E$. Then $\mathrm{tensorIteratedFDerivWithinTwo}$ applied to $x$, $f$, $s$ and $x_{6}$ is a linear map of the set of tensor products of $E$ and $E$ and $F$ defined as the lift of $\mathrm{bilinearIteratedFDerivWithinTwo}$ applied to $x$, $f$, $s$ and $x_{6}$.
IsCoercive.continuousLinearEquivOfBilindefMathlib.Analysis.InnerProductSpace.LaxMilgram, function or constantWording
the continuous linear equivalence of coercive (from the name)
English
Assume that $B$ is coercive. Then the continuous linear equivalence of $\mathrm{coercive}$ is a continuous linear equivalence of $V$ and $V$ defined as the continuous linear equivalence of the continuous linear map of $B$.
ContinuousLinearMap.reApplyInnerSelfdefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantEnglish
Let $T$ be a continuous linear map of $E$ and $E$. Let $x_{4}$ be an element of $E$. Then $\operatorname{reApplyInnerSelf}$ applied to $T$ and $x_{4}$ is a real number defined as $\operatorname{re}$ applied to $\operatorname{inner}$ applied to $x$, $T$ applied to $x_{4}$ and $x_{4}$.
InnerProductSpace.rankOnedefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantWording
the rank one of x (from the name)
English
Let $x$ be a set. Then the rank one of $x$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and the set of continuous linear maps of $F$ and $E$ defined as the flip of the composition of the right scalar multiple of $F$ and $E$ and the inner product of $x$.
LinearEquiv.isometryOfInnerdefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantWording
the isometry of f and h (from the name)
English
Let $f$ be a linear equivalence of $E$ and $\mathrm{E'}$ such that for all elements $x_{6}$ and $y$ of $E$, $\EqtMACRoH {\operatorname{inner} (x , f (x_{6}), f (y))}{\operatorname{inner} (x , x_{6} , y)}$. Then the isometry of $f$ and $h$ is a linear isometry equivalence of $E$ and $\mathrm{E'}$.
LinearMap.isometryOfInnerdefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantWording
the isometry of f and h (from the name)
English
Let $f$ be a linear map of $E$ and $\mathrm{E'}$ such that for all elements $x_{6}$ and $y$ of $E$, $\EqtMACRoH {\operatorname{inner} (x , f (x_{6}), f (y))}{\operatorname{inner} (x , x_{6} , y)}$. Then the isometry of $f$ and $h$ is a linear isometry of $E$ and $\mathrm{E'}$.
innerSLdefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantWording
the inner product of x (from the docstring)
English
Let $x$ be a set. Then the inner product of $x$ is a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $x$.
innerSLFlipdefMathlib.Analysis.InnerProductSpace.LinearMap, function or constantWording
the inner product of x (from the docstring)
English
Let $x$ be a set. Then the inner product of $x$ is a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $x$ defined as $\mathrm{ContinuousLinearMap\_\_flip\_u2097\_\_u1d62\_'\_\_app}$ applied to $E$, $E$, $x$, the identity ring homomorphism of $x$, the star ring end of $x$ and the inner product of $x$.
LinearPMap.IsFormalAdjointdefMathlib.Analysis.InnerProductSpace.LinearPMap, predicateEnglish
Let $T$ be a linear map of $E$ and $F$. Let $S$ be a linear map of $F$ and $E$. Then $\operatorname{IsFormalAdjoint}$ holds for $T$ and $S$, if for all elements $x_{6}$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{domain} (T)}{x_{8}})}$, for all elements $y$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{domain} (S)}{x_{7}})}$, $\EqtMACRoH {\operatorname{inner} (x , \operatorname{toFun'} (T , x_{6}), y)}{\operatorname{inner} (x , x_{6} , \operatorname{toFun'} (S , y))}$.
LinearPMap.adjointdefMathlib.Analysis.InnerProductSpace.LinearPMap, function or constantWording
the adjoint operator of T (from the docstring)
English
Let $T$ be a linear map of $E$ and $F$. Then the adjoint operator of $T$ is a linear map of $F$ and $E$ defined as $\operatorname{mk}$ applied to the domain of the adjoint operator of $T$ and $\mathrm{dite}$ applied to the proposition that the domain of $T$ is dense, the function that maps $\mathrm{hT}$ to $\operatorname{adjointAux}$ applied to $\mathrm{hT}$ and the function that maps $\mathrm{hT1}$ to $0$.
LinearPMap.adjointDomaindefMathlib.Analysis.InnerProductSpace.LinearPMap, function or constantWording
the domain of the adjoint operator of T (from the docstring)
English
Let $T$ be a linear map of $E$ and $F$. Then the domain of the adjoint operator of $T$ is a submodule of $x$ and $F$.
LinearPMap.adjointDomainMkCLMdefMathlib.Analysis.InnerProductSpace.LinearPMap, function or constantWording
the adjoint domain continuous linear map of T and y (from the name)
English
Let $T$ be a linear map of $E$ and $F$. Let $y$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{adjointDomain} (T)}{x_{7}})}$. Then the adjoint domain continuous linear map of $T$ and $y$ is a strong dual of $x$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{domain} (T)}{x_{6}})}$.
LinearPMap.adjointDomainMkCLMExtenddefMathlib.Analysis.InnerProductSpace.LinearPMap, function or constantEnglish
Let $T$ be a linear map of $E$ and $F$. Let $y$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{adjointDomain} (T)}{x_{6}})}$. Then $\operatorname{adjointDomainMkCLMExtend}$ applied to $T$ and $y$ is a strong dual of $x$ and $E$ defined as $\operatorname{extend}$ applied to the adjoint domain continuous linear map of $T$ and $y$ and the subtype of the domain of $T$.
Submodule.adjointdefMathlib.Analysis.InnerProductSpace.LinearPMap, function or constantWording
the adjoint of g (from the docstring)
English
Let $g$ be a submodule of $x$ and $\mathrm{Prod}$ applied to $E$ and $F$. Then the adjoint of $g$ is a submodule of $x$ and $\mathrm{Prod}$ applied to $F$ and $E$ defined as the map of $\operatorname{toLinearMap}$ applied to the linear equivalence of $2$ and $\operatorname{orthogonal}$ applied to the map of $\operatorname{toLinearMap}$ applied to the composition of the inverse of the skew swap of $F$ and $E$ and the inverse of the linear equivalence of $2$ and $g$.
OrthonormalBasis.mulOppositedefMathlib.Analysis.InnerProductSpace.MulOpposite, function or constantWording
the multiplicative opposite of b (from the docstring)
English
Let $b$ be an orthonormal basis of $x$ and $H$. Then the multiplicative opposite of $b$ is an orthonormal basis of $x$ and the set of multiplicative opposites of $H$ defined as the orthonormal basis of the multiplicative opposite of the basis of $b$ and $\operatorname{orthonormal}$ applied to $b$.
LinearMap.normDetdefMathlib.Analysis.InnerProductSpace.NormDet, function or constantWording
the norm determinant of f (from the docstring)
English
Let $f$ be a linear map of $U$ and $V$. Then the norm determinant of $f$ is an element of $\Real$ defined as $\mathrm{dite}$ applied to $\mathrm{Nonempty}$ applied to the set of orthonormal bases of $x$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{6}})}$, the function that maps $h_{1}$ to the norm of the determinant of $\operatorname{toMatrix}$ applied to the basis of $\mathrm{stdOrthonormalBasis}$ applied to $x$ and $U$, the basis of $\operatorname{some}$ applied to $h_{1}$ and $\operatorname{rangeRestrict}$ applied to $f$ and the function that maps $h_{2}$ to $0$.
InnerProductSpaceableclassMathlib.Analysis.InnerProductSpace.OfNorm, predicateEnglish
Let $E$ be a set. Then we can say that $\mathrm{InnerProductSpaceable}$ holds for $E$.
Orientation.finOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.Orientation, function or constantWording
the finite orthonormal basis of x2 (from the name)
English
Assume that $0 < n$. Assume that the rank of $\Real$ and $E$ is equal to $n$. Let $x_{2}$ be an orientation of $E$ and $\mathrm{Fin}$ applied to $n$. Then the finite orthonormal basis of $x_{2}$ is an orthonormal basis of $\Real$ and $E$ defined as $\operatorname{adjustToOrientation}$ applied to the reindexing of $\mathrm{stdOrthonormalBasis}$ applied to $\Real$ and $E$ and the finite congruence of $h$ and $x_{2}$.
OrthonormalBasis.adjustToOrientationdefMathlib.Analysis.InnerProductSpace.Orientation, function or constantEnglish
Let $e$ be an orthonormal basis of $\Real$ and $E$. Let $x_{5}$ be an orientation of $E$ and $x_{2}$. Then $\operatorname{adjustToOrientation}$ applied to $e$ and $x_{5}$ is an orthonormal basis of $\Real$ and $E$ defined as the orthonormal basis of $\operatorname{adjustToOrientation}$ applied to the basis of $e$ and $x_{5}$ and $\mathrm{OrthonormalBasis\_\_orthonormal\_adjustToOrientation}$ applied to $e$ and $x_{5}$.
ClosedSubmodule.orthogonaldefMathlib.Analysis.InnerProductSpace.Orthogonal, function or constantEnglish
Let $K$ be a closed submodule of $x$ and $E$. Then $\operatorname{orthogonal}$ applied to $K$ is a closed submodule of $x$ and $E$.
Submodule.IsOrthodefMathlib.Analysis.InnerProductSpace.Orthogonal, predicateEnglish
Let $U$ and $V$ be submodules of $x$ and $E$. Then $\operatorname{IsOrtho}$ holds for $U$ and $V$, if $U \leq \operatorname{orthogonal} (V)$.
Submodule.orthogonaldefMathlib.Analysis.InnerProductSpace.Orthogonal, function or constantEnglish
Let $K$ be a submodule of $x$ and $E$. Then $\operatorname{orthogonal}$ applied to $K$ is a submodule of $x$ and $E$.
LinearEquiv.isometryOfOrthonormaldefMathlib.Analysis.InnerProductSpace.Orthonormal, function or constantWording
the isometry of f (from the name)
English
Let $f$ be a linear equivalence of $E$ and $\mathrm{E'}$. Assume that $\operatorname{coe}$ applied to $v$ is orthonormal. Assume that $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $v$ is orthonormal. Then the isometry of $f$ is a linear isometry equivalence of $E$ and $\mathrm{E'}$.
LinearMap.isometryOfOrthonormaldefMathlib.Analysis.InnerProductSpace.Orthonormal, function or constantWording
the isometry of f (from the name)
English
Let $f$ be a linear map of $E$ and $\mathrm{E'}$. Assume that $\operatorname{coe}$ applied to $v$ is orthonormal. Assume that $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $v$ is orthonormal. Then the isometry of $f$ is a linear isometry of $E$ and $\mathrm{E'}$.
OrthonormaldefMathlib.Analysis.InnerProductSpace.Orthonormal, predicateWording
v is orthonormal (from the name)
English
Let $x$ be a set. Let $v$ be a function from elements of $x_{4}$ to elements of $E$. Then $v$ is orthonormal, if for all elements $i$ of $x_{4}$, the norm of $v$ applied to $i$ is equal to $1$ and the function that maps $i_{1}$ and $j$ to $\EqtMACRoH {\operatorname{inner} (x , v (i_{1}), v (j))}{0}$ is pairwise.
Orthonormal.equivdefMathlib.Analysis.InnerProductSpace.Orthonormal, function or constantWording
the equivalence of #3 (from the name)
English
Assume that $\operatorname{coe}$ applied to $v$ is orthonormal. Assume that $\operatorname{coe}$ applied to $\mathrm{v'}$ is orthonormal. Let $e$ be an equivalence from $x_{4}$ to $x_{5}$. Then the equivalence of $e$ is a linear isometry equivalence of $E$ and $\mathrm{E'}$.
basisOfOrthonormalOfCardEqFinrankdefMathlib.Analysis.InnerProductSpace.Orthonormal, function or constantWording
the basis of hv and card_eq (from the name)
English
Assume that $v$ is orthonormal. Assume that the cardinality of $x_{4}$ is equal to the rank of $x$ and $E$. Then the basis of $\mathrm{hv}$ and $\mathrm{card\_eq}$ is a basis of $x$ and $E$ defined as the basis of $\operatorname{linearIndependent}$ applied to $\mathrm{hv}$ and $\mathrm{card\_eq}$.
Complex.isometryOfOrthonormaldefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the isometry of v (from the name)
English
Let $v$ be an orthonormal basis of $\Real$ and $F$. Then the isometry of $v$ is a linear isometry equivalence of the set of complexes and $F$ defined as the composition of the representation of the orthonormal basis one and the inverse of the representation of $v$.
Complex.orthonormalBasisOneIdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the orthonormal basis one (from the name)
English
The orthonormal basis one is an orthonormal basis of $\Real$ and the set of complexes.
DirectSum.IsInternal.collectedOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, the function that maps $i_{3}$ to $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {A (i_{3})}{x_{10}})}$ and the function that maps $i_{4}$ to the subtype of $A$ applied to $i_{4}$. Assume that the function that maps $i_{2}$ to $A$ applied to $i_{2}$ is internal. Let $\mathrm{v\_family}$ be a function from elements $i_{1}$ of $x$ to orthonormal bases of $x_{1}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {A (i_{1})}{x_{9}})}$. Then $\operatorname{collectedOrthonormalBasis}$ applied to $\mathrm{hV}$, $\mathrm{hV\_sum}$, $i_{1}$ and $\mathrm{v\_family}$ is an orthonormal basis of $x_{1}$ and $E$.
DirectSum.IsInternal.isometryL2OfOrthogonalFamilydefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the isometry of hV and #2 (from the name)
English
Assume that $V$ is internal. Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, the function that maps $i_{1}$ to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {V (i_{1})}{x_{8}})}$ and the function that maps $i_{2}$ to the subtype of $V$ applied to $i_{2}$. Then the isometry of $\mathrm{hV}$ and $\mathrm{hV'}$ is a linear isometry equivalence of $E$ and $\mathrm{PiLp}$ applied to $2$ and the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {V (i)}{x_{7}})}$.
DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquivdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the sigma orthonormal basis index equivalence of hV and #3 (from the name)
English
Assume that the rank of $x_{1}$ and $E$ is equal to $n$. Assume that $V$ is internal. Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, the function that maps $i_{1}$ to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {V (i_{1})}{x_{8}})}$ and the function that maps $i_{2}$ to the subtype of $V$ applied to $i_{2}$. Then the sigma orthonormal basis index equivalence of $\mathrm{hV}$ and $\mathrm{hV'}$ is an equivalence from $\Sigma$ applied to the function that maps $i$ to $\mathrm{Fin}$ applied to the rank of $x_{1}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {V (i)}{x_{7}})}$ to $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_PiL2\_\_1554134833\_\_\_hygCtx\_\_\_hyg\_\_2}$, $\mathrm{hn}$, $\mathrm{hV}$ and $\mathrm{hV'}$.
DirectSum.IsInternal.subordinateOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the subordinate orthonormal basis of hV and #3 (from the name)
English
Assume that the rank of $x_{1}$ and $E$ is equal to $n$. Assume that $V$ is internal. Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {V (i)}{x_{7}})}$ and the function that maps $i_{1}$ to the subtype of $V$ applied to $i_{1}$. Then the subordinate orthonormal basis of $\mathrm{hV}$ and $\mathrm{hV'}$ is an orthonormal basis of $x_{1}$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_PiL2\_\_3752396123\_\_\_hygCtx\_\_\_hyg\_\_2}$, $\mathrm{hn}$, $\mathrm{hV}$ and $\mathrm{hV'}$.
DirectSum.IsInternal.subordinateOrthonormalBasisIndexdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the subordinate orthonormal basis index of a (from the name)
English
Assume that the rank of $x_{1}$ and $E$ is equal to $n$. Assume that $V$ is internal. Let $a$ be an element of $\mathrm{Fin}$ applied to $n$. Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, the function that maps $i$ to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {V (i)}{x_{7}})}$ and the function that maps $i_{1}$ to the subtype of $V$ applied to $i_{1}$. Then the subordinate orthonormal basis index of $a$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_PiL2\_\_3022897883\_\_\_hygCtx\_\_\_hyg\_\_2}$, $\mathrm{hn}$, $\mathrm{hV}$, $a$ and $\mathrm{hV'}$.
EuclideanSpacedefMathlib.Analysis.InnerProductSpace.PiL2, typeWording
Euclidean space of x and n (from the name)
English
Let $x$ and $n$ be sets. Then a Euclidean space of $x$ and $n$ is an element of the function that maps $x$ and $n$ to $\mathrm{PiLp}$ applied to $2$ and the function that maps $x_{1}$ to $x$.
EuclideanSpace.basisFundefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the basis of x and x1 (from the docstring)
English
Let $x$ and $x_{1}$ be sets. Then the basis of $x$ and $x_{1}$ is an orthonormal basis of $x_{1}$ and the set of Euclidean spaces of $x_{1}$ and $x$ defined as $\operatorname{ofRepr}$ applied to the identity of $x_{1}$ and the set of Euclidean spaces of $x_{1}$ and $x$.
EuclideanSpace.equivdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalence of $x$ and $x_{1}$ is a continuous linear equivalence of the set of Euclidean spaces of $x_{1}$ and $x$ and the set of functions from elements of $x$ to elements of $x_{1}$ defined as the continuous linear equivalence of $2$ and the function that maps $x_{3}$ to $x_{1}$.
EuclideanSpace.finAddEquivProddefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the finite additive equivalence product (from the name)
English
The finite additive equivalence product is a continuous linear equivalence of the set of Euclidean spaces of $x$ and $\mathrm{Fin}$ applied to $n + m$ and $\mathrm{Prod}$ applied to the set of Euclidean spaces of $x$ and $\mathrm{Fin}$ applied to $n$ and the set of Euclidean spaces of $x$ and $\mathrm{Fin}$ applied to $m$ defined as the composition of the continuous linear equivalence of $\operatorname{piLpCongrLeft}$ applied to $2$, $x$, $x$ and the inverse of the finite sum finite equivalence and the sum equivalence product.
EuclideanSpace.projdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the projection of i (from the name)
English
Let $i$ be an element of $x$. Then the projection of $i$ is a strong dual of $x_{1}$ and the set of Euclidean spaces of $x_{1}$ and $x$ defined as the projection of the function that maps $x_{3}$ to $x_{1}$ and $i$.
EuclideanSpace.projₗdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the projection of i (from the name)
English
Let $i$ be an element of $x$. Then the projection of $i$ is a linear map of the set of Euclidean spaces of $x_{1}$ and $x$ and $x_{1}$ defined as the projection of the function that maps $x_{3}$ to $x_{1}$ and $i$.
EuclideanSpace.restrict₂defMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Assume that $I \leq J$. Then $\mathrm{EuclideanSpace\_\_restrict\_u2082\_}$ applied to $\mathrm{hIJ}$ is a continuous linear map of the set of Euclidean spaces of $x_{1}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {J}{x_{3}})}$ and the set of Euclidean spaces of $x_{1}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {I}{x_{4}})}$.
EuclideanSpace.singledefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Let $i$ be an element of $x$. Let $a$ be an element of $x_{1}$. Then $\operatorname{single}$ applied to $i$ and $a$ is a Euclidean space of $x_{1}$ and $x$ defined as $\operatorname{single}$ applied to $2$, $i$ and $a$.
EuclideanSpace.sumEquivProddefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the sum equivalence product (from the name)
English
The sum equivalence product is a continuous linear equivalence of the set of Euclidean spaces of $x$ and $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$ and $\mathrm{Prod}$ applied to the set of Euclidean spaces of $x$ and $x_{2}$ and the set of Euclidean spaces of $x$ and $x_{3}$ defined as the composition of the continuous linear equivalence of $\operatorname{sumPiLpEquivProdLpPiLp}$ applied to $2$ and the function that maps $x_{6}$ to $x$ and the product continuous linear equivalence of $2$.
FiniteDimensional.orthonormalBasisSingletondefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the orthonormal basis singleton of v (from the name)
English
Let $x$ and $x_{1}$ be sets such that the rank of $x_{1}$ and $E$ is equal to $1$. Let $v$ be an element of $E$ such that the norm of $v$ is equal to $1$. Then the orthonormal basis singleton of $v$ is an orthonormal basis of $x_{1}$ and $E$.
LinearIsometry.extenddefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Let $L$ be a linear isometry of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $V$. Then $\operatorname{extend}$ applied to $L$ is a linear isometry of $V$ and $V$.
Matrix.toEuclideanLindefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
$\operatorname{toEuclideanLin}$ is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of linear maps of the set of Euclidean spaces of $x$ and $n$ and the set of Euclidean spaces of $x$ and $m$ defined as $\operatorname{toLpLin}$ applied to $2$ and $2$.
Module.Basis.toOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the orthonormal basis of v and hv (from the name)
English
Let $v$ be a basis of $x_{1}$ and $E$ such that $\operatorname{coe}$ applied to $v$ is orthonormal. Then the orthonormal basis of $v$ and $\mathrm{hv}$ is an orthonormal basis of $x_{1}$ and $E$.
OrthonormalBasisstructureMathlib.Analysis.InnerProductSpace.PiL2, typeWording
orthonormal basis of x1 and E (from the name)
English
Let $x$, $x_{1}$ and $E$ be sets. Then the orthonormal bases of $x_{1}$ and $E$ are a basic type.
OrthonormalBasis.equivdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the equivalence of e and #3 (from the name)
English
Let $b$ be an orthonormal basis of $x_{2}$ and $E$. Let $\mathrm{b'}$ be an orthonormal basis of $x_{2}$ and $\mathrm{E'}$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the equivalence of $\mathrm{b'}$ and $e$ is a linear isometry equivalence of $E$ and $\mathrm{E'}$ defined as the composition of the representation of $b$ and the composition of $\operatorname{piLpCongrLeft}$ applied to $2$, $x_{2}$, $x_{2}$ and $e$ and the inverse of the representation of $\mathrm{b'}$.
OrthonormalBasis.fromOrthogonalSpanSingletondefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Let $n$ be an element of $\Natural$. Assume that $v \neq 0$. Then $\operatorname{fromOrthogonalSpanSingleton}$ applied to $n$ and $\mathrm{hv}$ is an orthonormal basis of $x$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (x , \operatorname{singleton} (v)))}{x_{4}})}$ defined as the reindexing of $\mathrm{stdOrthonormalBasis}$ applied to $x$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (x , \operatorname{singleton} (v)))}{x_{4}})}$ and the finite congruence of $\mathrm{Submodule\_\_finrank\_orthogonal\_span\_singleton}$ applied to $\mathrm{hv}$.
OrthonormalBasis.mapdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the map of b and L (from the name)
English
Let $b$ be an orthonormal basis of $x_{1}$ and $E$. Let $L$ be a linear isometry equivalence of $E$ and $G$. Then the map of $b$ and $L$ is an orthonormal basis of $x_{1}$ and $G$ defined as $\operatorname{ofRepr}$ applied to the composition of the inverse of $L$ and the representation of $b$.
OrthonormalBasis.mkdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Assume that $v$ is orthonormal. Assume that the top is less than or equal to the span of $x_{1}$ and the range of $v$. Then $\operatorname{mk}$ applied to $\mathrm{hon}$ and $\mathrm{hsp}$ is an orthonormal basis of $x_{1}$ and $E$.
OrthonormalBasis.mkOfOrthogonalEqBotdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Assume that $v$ is orthonormal. Assume that $\operatorname{orthogonal}$ applied to the span of $x_{1}$ and the range of $v$ is equal to the bottom. Then $\operatorname{mkOfOrthogonalEqBot}$ applied to $\mathrm{hon}$ and $\mathrm{hsp}$ is an orthonormal basis of $x_{1}$ and $E$.
OrthonormalBasis.reindexdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the reindexing of b and e (from the name)
English
Let $b$ be an orthonormal basis of $x_{2}$ and $E$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $b$ and $e$ is an orthonormal basis of $x_{2}$ and $E$ defined as $\operatorname{ofRepr}$ applied to the composition of the representation of $b$ and $\operatorname{piLpCongrLeft}$ applied to $2$, $x_{2}$, $x_{2}$ and $e$.
OrthonormalBasis.reprdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the representation of self (from the name)
English
Let $\mathrm{self}$ be an orthonormal basis of $x_{1}$ and $E$. Then the representation of $\mathrm{self}$ is a linear isometry equivalence of $E$ and the set of Euclidean spaces of $x_{1}$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
OrthonormalBasis.singletondefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the singleton of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the singleton of $x$ and $x_{1}$ is an orthonormal basis of $x_{1}$ and $x_{1}$.
OrthonormalBasis.spandefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the span of h and s (from the name)
English
Assume that $\mathrm{v'}$ is orthonormal. Let $s$ be a finite set of $x$. Then the span of $h$ and $s$ is an orthonormal basis of $x_{1}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (x_{1} , \operatorname{image} (s , \mathrm{v'}))}{x_{7}})}$.
OrthonormalBasis.toBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the basis of b (from the name)
English
Let $b$ be an orthonormal basis of $x_{1}$ and $E$. Then the basis of $b$ is a basis of $x_{1}$ and $E$ defined as the basis of the composition of $\operatorname{toLinearEquiv}$ applied to the representation of $b$ and the linear equivalence of $2$.
Pi.orthonormalBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the orthonormal basis of B (from the name)
English
Let $B$ be a function from elements $i_{1}$ of $x$ to orthonormal bases of $x_{4}$ and $E$ applied to $i_{1}$. Then the orthonormal basis of $i_{1}$ is an orthonormal basis of $x_{4}$ and $\mathrm{PiLp}$ applied to $2$ and $E$ defined as the function that maps $B$ to $\operatorname{ofRepr}$ applied to the composition of $\operatorname{piLpCongrRight}$ applied to $2$ and the function that maps $i$ to the representation of $i_{1}$ applied to $i$ and the inverse of $\operatorname{piLpCurry}$ applied to $x_{4}$, $2$ and the function that maps $x_{8}$ and $x_{9}$ to $x_{4}$ and $B$.
PiLp.vecNotationdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantWording
the vector notation (from the name)
English
generation took over the time limit
stdOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.PiL2, function or constantEnglish
Let $x$ and $E$ be sets. Then $\mathrm{stdOrthonormalBasis}$ applied to $x$ and $E$ is an orthonormal basis of $x$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_PiL2\_\_2921777918\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x$ and $E$.
ContinuousLinearMap.IsPositivedefMathlib.Analysis.InnerProductSpace.Positive, predicateWording
T is positive (from the name)
English
Let $T$ be a continuous linear map of $E$ and $E$. Then $T$ is positive, if $\operatorname{toLinearMap}$ applied to $T$ is symmetric and for all elements $x_{4}$ of $E$, $0 \leq \operatorname{reApplyInnerSelf} (T , x_{4})$.
LinearMap.IsPositivedefMathlib.Analysis.InnerProductSpace.Positive, predicateWording
T is positive (from the name)
English
Let $T$ be a linear map of $E$ and $E$. Then $T$ is positive, if $T$ is symmetric and for all elements $x_{4}$ of $E$, $0 \leq \operatorname{re} (\operatorname{inner} (x , T (x_{4}), x_{4}))$.
LinearMap.tracePositiveLinearMapdefMathlib.Analysis.InnerProductSpace.Positive, function or constantWording
the trace positive linear map of x and E (from the name)
English
Let $x$ and $E$ be sets. Then the trace positive linear map of $x$ and $E$ is a positive linear map of the set of linear maps of $E$ and $E$ and $x$.
OrthonormalBasis.proddefMathlib.Analysis.InnerProductSpace.ProdL2, function or constantWording
the product of v and w (from the name)
English
Let $v$ be an orthonormal basis of $x$ and $E$. Let $w$ be an orthonormal basis of $x$ and $F$. Then the product of $v$ and $w$ is an orthonormal basis of $x$ and $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $E$ and $F$.
Submodule.orthogonalDecompositiondefMathlib.Analysis.InnerProductSpace.ProdL2, function or constantWording
the orthogonal decomposition of K (from the name)
English
Let $K$ be a submodule of $x$ and $E$. Then the orthogonal decomposition of $K$ is a linear isometry equivalence of $E$ and $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (K)}{x_{5}})}$.
Submodule.quotientEquivOrthogonaldefMathlib.Analysis.InnerProductSpace.ProdL2, function or constantEnglish
Let $K$ be a submodule of $x$ and $E$. Then $\operatorname{quotientEquivOrthogonal}$ applied to $K$ is a linear isometry equivalence of the set of quotients of $E$ and $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (K)}{x_{4}})}$.
Submodule.HasOrthogonalProjectionclassMathlib.Analysis.InnerProductSpace.Projection.Basic, predicateWording
K has orthogonal projections (from the name)
English
Let $K$ be a submodule of $x$ and $E$. Then we can say that $K$ has orthogonal projections.
Submodule.orthogonalProjectionOntodefMathlib.Analysis.InnerProductSpace.Projection.Basic, function or constantWording
the orthogonal projection onto a subspace of K (from the docstring)
English
Let $K$ be a submodule of $x$ and $E$. Then the orthogonal projection onto a subspace of $K$ is a continuous linear map of $E$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {K}{x_{4}})}$ defined as $\operatorname{projectionOntoL}$ applied to $K$, $\operatorname{orthogonal}$ applied to $K$ and $\mathrm{Submodule\_\_isTopCompl\_orthogonal}$ applied to $K$.
Submodule.starProjectiondefMathlib.Analysis.InnerProductSpace.Projection.Basic, function or constantWording
the orthogonal projection onto a subspace of U (from the docstring)
English
Let $U$ be a submodule of $x$ and $E$. Then the orthogonal projection onto a subspace of $U$ is a continuous linear map of $E$ and $E$ defined as the composition of the subtype of $U$ and the orthogonal projection onto a subspace of $U$.
Submodule.reflectiondefMathlib.Analysis.InnerProductSpace.Projection.Reflection, function or constantWording
the reflection of K (from the name)
English
Let $K$ be a submodule of $x$ and $E$. Then the reflection of $K$ is a linear isometry equivalence of $E$ and $E$.
ContinuousLinearMap.rayleighQuotientdefMathlib.Analysis.InnerProductSpace.Rayleigh, function or constantEnglish
Let $T$ be a continuous linear map of $E$ and $E$. Let $x_{4}$ be an element of $E$. Then $\operatorname{rayleighQuotient}$ applied to $T$ and $x_{4}$ is a real number defined as the quotient of $\operatorname{reApplyInnerSelf}$ applied to $T$ and $x_{4}$ and the exponentiation of the norm of $x_{4}$ to $2$.
RKHSclassMathlib.Analysis.InnerProductSpace.Reproducing, predicateEnglish
Let $x$, $X$ and $V$ be elements of $\mathrm{outParam}$ applied to the set of sets. Let $H$ be a set. Then we can say that $\mathrm{RKHS}$ holds for $x$, $H$, $X$ and $V$.
RKHS.OfKerneldefMathlib.Analysis.InnerProductSpace.Reproducing, typeWording
kernel of K (from the name)
English
Let $K$ be a matrix of $X$ and the set of continuous linear maps of $V$ and $V$. Then a kernel of $K$ is an element of the function that maps $K$ to the set of completions of $\mathrm{RKHS\_\_H\_u2080\_}$ applied to $K$.
RKHS.coeCLMdefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the coercion continuous linear map of x (from the name)
English
Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then the coercion continuous linear map of $x$ is a continuous linear map of $H$ and the set of functions from elements of $X$ to elements of $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RKHS.equivdefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the equivalence of h3 (from the name)
English
Assume that the kernel of $H$ is equal to the kernel of $\mathrm{H'}$. Then the equivalence of $h_{3}$ is a linear isometry equivalence of $H$ and $\mathrm{H'}$.
RKHS.evaldefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the evaluation of H and x7 (from the name)
English
Let $H$ be a set. Let $x_{7}$ be an element of $X$. Then the evaluation of $H$ and $x_{7}$ is a continuous linear map of $H$ and $V$ defined as the composition of the projection of $x_{7}$ and the coercion continuous linear map of $x$.
RKHS.kerFundefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the kernel function of H and x7 (from the name)
English
Let $H$ be a set. Let $x_{7}$ be an element of $X$. Then the kernel function of $H$ and $x_{7}$ is a continuous linear map of $V$ and $H$ defined as $\operatorname{adjoint}$ applied to the evaluation of $H$ and $x_{7}$.
RKHS.kerneldefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the kernel of H (from the docstring)
English
Let $H$ be a set. Then the kernel of $H$ is a matrix of $X$ and the set of continuous linear maps of $V$ and $V$ defined as $\operatorname{of}$ applied to the function that maps $x_{8}$ and $y_{1}$ to the composition of $\operatorname{adjoint}$ applied to the kernel function of $H$ and $x_{8}$ and the kernel function of $H$ and $y_{1}$.
RKHS.outerKerneldefMathlib.Analysis.InnerProductSpace.Reproducing, function or constantWording
the outer kernel of x and f (from the name)
English
Let $x$ be a set. Let $f$ be a function from elements of $X$ to elements of $V$. Then the outer kernel of $x$ and $f$ is a matrix of $X$ and the set of continuous linear maps of $V$ and $V$ defined as $\operatorname{of}$ applied to the function that maps $x_{5}$ and $y_{1}$ to $\operatorname{coe}$ applied to the rank one of $x$, $f$ applied to $x_{5}$ and $f$ applied to $y_{1}$.
RKHS.Add'.OfKernelAddEquivdefMathlib.Analysis.InnerProductSpace.Reproducing.Operations, function or constantWording
the kernel additive equivalence of K and #2 (from the name)
English
Let $K$ and $\mathrm{K'}$ be matrixes of $X$ and the set of continuous linear maps of $V$ and $V$. Then the kernel additive equivalence of $K$ and $\mathrm{K'}$ is a linear isometry equivalence of the set of kernels of $K + \mathrm{K'}$ and the set of sum spaces of the set of kernels of $K$ and the set of kernels of $\mathrm{K'}$.
RKHS.Add'.generatordefMathlib.Analysis.InnerProductSpace.Reproducing.Operations, function or constantWording
the generator of H and #2 (from the name)
English
Let $H$ and $\mathrm{H'}$ be sets. Then the generator of $H$ and $\mathrm{H'}$ is a continuous linear map of $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $H$ and $\mathrm{H'}$ and the set of functions from elements of $X$ to elements of $V$ defined as the composition of the coproduct of the coercion continuous linear map of $x$ and the coercion continuous linear map of $x$ and the continuous linear map of the product continuous linear equivalence of $2$.
RKHS.Add'.projectiondefMathlib.Analysis.InnerProductSpace.Reproducing.Operations, function or constantWording
the projection of H and #2 (from the name)
English
Let $H$ and $\mathrm{H'}$ be sets. Then the projection of $H$ and $\mathrm{H'}$ is a linear isometry of the set of sum spaces of $H$ and $\mathrm{H'}$ and $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $H$ and $\mathrm{H'}$ defined as the composition of the subtype of $\operatorname{orthogonal}$ applied to the kernel of $\operatorname{toLinearMap}$ applied to the generator of $H$ and $\mathrm{H'}$ and the linear isometry of $\operatorname{quotientEquivOrthogonal}$ applied to the kernel of $\operatorname{toLinearMap}$ applied to the generator of $H$ and $\mathrm{H'}$.
RKHS.Add'.sumSpacedefMathlib.Analysis.InnerProductSpace.Reproducing.Operations, typeWording
sum space of H and #2 (from the name)
English
Let $H$ and $\mathrm{H'}$ be sets. Then a sum space of $H$ and $\mathrm{H'}$ is an element of the function that maps $H$ and $\mathrm{H'}$ to the set of quotients of $\mathrm{WithLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $H$ and $\mathrm{H'}$ and the kernel of $\operatorname{toLinearMap}$ applied to the generator of $H$ and $\mathrm{H'}$.
LinearMap.singularValuesdefMathlib.Analysis.InnerProductSpace.SingularValues, function or constantWording
the singular value of T (from the name)
English
Let $T$ be a linear map of $E$ and $F$. Then the singular value of $T$ is an element of $\FinsuppMACRoQ {\Natural}{\Real}$.
LinearMap.IsSymmetric.diagonalizationdefMathlib.Analysis.InnerProductSpace.Spectrum, function or constantWording
the diagonalization of hT (from the name)
English
Assume that $T$ is symmetric. Then the diagonalization of $\mathrm{hT}$ is a linear isometry equivalence of $E$ and $\mathrm{PiLp}$ applied to $2$ and the function that maps $x_{4}$ to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{eigenspace} (T , \operatorname{val} (1 , x_{4}))}{x_{5}})}$ defined as the isometry of $\mathrm{LinearMap\_\_IsSymmetric\_\_direct\_sum\_isInternal}$ applied to $\mathrm{hT}$ and $\mathrm{LinearMap\_\_IsSymmetric\_\_orthogonalFamily\_eigenspaces'}$ applied to $\mathrm{hT}$.
LinearMap.IsSymmetric.eigenvaluesdefMathlib.Analysis.InnerProductSpace.Spectrum, function or constantWording
the eigenvalue of x4 (from the name)
English
Assume that $T$ is symmetric. Assume that the rank of $x$ and $E$ is equal to $n$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $n$. Then the eigenvalue of $x_{4}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{LinearMap\_\_IsSymmetric\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_Spectrum\_\_732640297\_\_\_hygCtx\_\_\_hyg\_\_14}$, $\mathrm{hT}$, $\mathrm{hn}$ and $x_{4}$.
LinearMap.IsSymmetric.eigenvectorBasisdefMathlib.Analysis.InnerProductSpace.Spectrum, function or constantWording
the eigenvector basis of hT and hn (from the name)
English
Assume that $T$ is symmetric. Assume that the rank of $x$ and $E$ is equal to $n$. Then the eigenvector basis of $\mathrm{hT}$ and $\mathrm{hn}$ is an orthonormal basis of $x$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{LinearMap\_\_IsSymmetric\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_Spectrum\_\_1103641225\_\_\_hygCtx\_\_\_hyg\_\_14}$, $\mathrm{hT}$ and $\mathrm{hn}$.
ClosedSubmodule.mulIdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the image of S (from the docstring)
English
Let $S$ be a closed submodule of $\Real$ and $H$. Then the image of $S$ is a closed submodule of $\Real$ and $H$ defined as $\operatorname{mapEquiv}$ applied to the scalar product by a non-zero complex number of $H$ and the imaginary unit and $S$.
ClosedSubmodule.symplCompdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the symplectic complement of S (from the docstring)
English
Let $S$ be a closed submodule of $\Real$ and $H$. Then the symplectic complement of $S$ is a closed submodule of $\Real$ and $H$ defined as $\operatorname{orthogonal}$ applied to the image of $S$.
Complex.UnitIdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the imaginary unit (from the docstring)
English
The imaginary unit is a unit of the set of complexes.
StandardSubspacestructureMathlib.Analysis.InnerProductSpace.StandardSubspace, typeWording
standard subspace of H (from the name)
English
Let $H$ be a set. Then the standard subspaces of $H$ are a basic type.
StandardSubspace.mulIdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the image of S (from the docstring)
English
Let $S$ be a standard subspace of $H$. Then the image of $S$ is a standard subspace of $H$.
StandardSubspace.symplCompdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the symplectic complement of S (from the docstring)
English
Let $S$ be a standard subspace of $H$. Then the symplectic complement of $S$ is a standard subspace of $H$.
StandardSubspace.toClosedSubmoduledefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the closed submodule of self (from the name)
English
Let $\mathrm{self}$ be a standard subspace of $H$. Then the closed submodule of $\mathrm{self}$ is a closed submodule of $\Real$ and $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
scalarSMulCLEdefMathlib.Analysis.InnerProductSpace.StandardSubspace, function or constantWording
the scalar product by a non-zero complex number of H and c (from the docstring)
English
Let $H$ be a set. Let $c$ be a unit of the set of complexes. Then the scalar product by a non-zero complex number of $H$ and $c$ is a continuous linear equivalence of $H$ and $H$ defined as $\operatorname{smulLeft}$ applied to $c$.
OrthogonalFamilydefMathlib.Analysis.InnerProductSpace.Subspace, predicateEnglish
Let $x$ be a set. Let $G$ be a function from elements of $x_{4}$ to sets. Let $V$ be a function from elements $i$ of $x_{4}$ to linear isometries of $G$ applied to $i$ and $E$. Then $\mathrm{OrthogonalFamily}$ holds for $x$, $G$, $i$ and $V$, if the function that maps $i$ and $j$ to the proposition that for all elements $v$ of $G$ applied to $i$, for all elements $w$ of $G$ applied to $j$, $\EqtMACRoH {\operatorname{inner} (x , i (i , v), i (j , w))}{0}$ is pairwise.
LinearMap.IsSymmetricdefMathlib.Analysis.InnerProductSpace.Symmetric, predicateWording
T is symmetric (from the name)
English
Let $T$ be a linear map of $E$ and $E$. Then $T$ is symmetric, if for all elements $x_{4}$ and $y$ of $E$, $\EqtMACRoH {\operatorname{inner} (x , T (x_{4}), y)}{\operatorname{inner} (x , x_{4} , T (y))}$.
LinearMap.IsSymmetricProjectionstructureMathlib.Analysis.InnerProductSpace.Symmetric, predicateWording
T is a symmetric projection (from the name)
English
Let $T$ be a linear map of $E$ and $E$. Then we can say that $T$ is a symmetric projection.
ContinuousLinearMap.lTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor 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 tensor of $G$ and $g$ is a continuous linear map of the set of tensor products of $G$ and $E$ and the set of tensor products of $G$ and $F$ defined as the composition of the continuous linear map of the continuous linear equivalence of the linear isometry equivalence version of $x$ and the composition of the tensor of $G$ and $g$ and the continuous linear map of the continuous linear equivalence of the linear isometry equivalence version of $x$.
ContinuousLinearMap.rTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor of G and f (from the name)
English
Let $G$ be a set. Let $f$ be a continuous linear map of $E$ and $F$. Then the tensor of $G$ and $f$ is a continuous linear map of the set of tensor products of $E$ and $G$ and the set of tensor products of $F$ and $G$.
LinearIsometry.lTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor of E and f (from the name)
English
Let $E$ be a set. Let $f$ be a linear isometry of $F$ and $G$. Then the tensor of $E$ and $f$ is a linear isometry of the set of tensor products of $E$ and $F$ and the set of tensor products of $E$ and $G$ defined as the map isometry of the identity linear isometry and $f$.
LinearIsometry.rTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor of G and f (from the name)
English
Let $G$ be a set. Let $f$ be a linear isometry of $E$ and $F$. Then the tensor of $G$ and $f$ is a linear isometry of the set of tensor products of $E$ and $G$ and the set of tensor products of $F$ and $G$ defined as the map isometry of $f$ and the identity linear isometry.
LinearIsometryEquiv.lTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor of E and f (from the name)
English
Let $E$ be a set. Let $f$ be a linear isometry equivalence of $F$ and $G$. Then the tensor of $E$ and $f$ is a linear isometry equivalence of the set of tensor products of $E$ and $F$ and the set of tensor products of $E$ and $G$ defined as the congruence isometry of the identity of $x$ and $E$ and $f$.
LinearIsometryEquiv.rTensordefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor of G and f (from the name)
English
Let $G$ be a set. Let $f$ be a linear isometry equivalence of $E$ and $F$. Then the tensor of $G$ and $f$ is a linear isometry equivalence of the set of tensor products of $E$ and $G$ and the set of tensor products of $F$ and $G$ defined as the congruence isometry of $f$ and the identity of $x$ and $G$.
OrthonormalBasis.tensorProductdefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the tensor product of x10 and x11 (from the name)
English
Let $x_{10}$ be an orthonormal basis of $x$ and $E$. Let $x_{11}$ be an orthonormal basis of $x$ and $F$. Then the tensor product of $x_{10}$ and $x_{11}$ is an orthonormal basis of $x$ and the set of tensor products of $E$ and $F$.
TensorProduct.assocIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the linear isometry equivalence version of x (from the docstring)
English
Let $x$, $E$, $F$ and $G$ be sets. Then the linear isometry equivalence version of $x$ is a linear isometry equivalence of the set of tensor products of the set of tensor products of $E$ and $F$ and $G$ and the set of tensor products of $E$ and the set of tensor products of $F$ and $G$ defined as the isometry of the associator of $F$ and $G$ and $\mathrm{TensorProduct\_\_inner\_assoc\_assoc}$.
TensorProduct.commIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the linear isometry equivalence version of x (from the docstring)
English
Let $x$, $E$ and $F$ be sets. Then the linear isometry equivalence version of $x$ is a linear isometry equivalence of the set of tensor products of $E$ and $F$ and the set of tensor products of $F$ and $E$ defined as the isometry of $\operatorname{comm}$ applied to $x$, $E$ and $F$ and $\mathrm{TensorProduct\_\_inner\_comm\_comm}$.
TensorProduct.congrIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the congruence isometry of f and g (from the name)
English
Let $f$ be a linear isometry equivalence of $E$ and $G$. Let $g$ be a linear isometry equivalence of $F$ and $H$. Then the congruence isometry of $f$ and $g$ is a linear isometry equivalence of the set of tensor products of $E$ and $F$ and the set of tensor products of $G$ and $H$.
TensorProduct.congrLdefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the congruence of f and g (from the name)
English
Let $f$ be a continuous linear equivalence of $E$ and $F$. Let $g$ be a continuous linear equivalence of $G$ and $H$. Then the congruence of $f$ and $g$ is a continuous linear equivalence of the set of tensor products of $E$ and $G$ and the set of tensor products of $F$ and $H$.
TensorProduct.lidIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantEnglish
Let $x$ and $E$ be sets. Then $\operatorname{lidIsometry}$ applied to $x$ and $E$ is a linear isometry equivalence of the set of tensor products of $x$ and $E$ and $E$ defined as the isometry of $\operatorname{lid}$ applied to $x$ and $E$ and $\mathrm{TensorProduct\_\_inner\_lid\_lid}$.
TensorProduct.mapInclIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the map inclusion isometry of #1 and #2 (from the name)
English
Let $\mathrm{E'}$ be a submodule of $x$ and $E$. Let $\mathrm{F'}$ be a submodule of $x$ and $F$. Then the map inclusion isometry of $\mathrm{E'}$ and $\mathrm{F'}$ is a linear isometry of the set of tensor products of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{E'}}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{F'}}{x_{7}})}$ and the set of tensor products of $E$ and $F$ defined as the map isometry of the subtype of $\mathrm{E'}$ and the subtype of $\mathrm{F'}$.
TensorProduct.mapIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the map isometry of f and g (from the name)
English
Let $f$ be a linear isometry of $E$ and $G$. Let $g$ be a linear isometry of $F$ and $H$. Then the map isometry of $f$ and $g$ is a linear isometry of the set of tensor products of $E$ and $F$ and the set of tensor products of $G$ and $H$ defined as the isometry of the tensor product of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{toLinearMap}$ applied to $g$ and $\mathrm{TensorProduct\_\_inner\_map\_map}$ applied to $f$ and $g$.
TensorProduct.mapLdefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantWording
the map 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 $G$ and $H$. Then the map of $f$ and $g$ is a continuous linear map of the set of tensor products of $E$ and $G$ and the set of tensor products of $F$ and $H$ defined as the composition of the tensor of $H$ and $f$ and the tensor of $E$ and $g$.
TensorProduct.mkLdefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantEnglish
Let $x$, $E$ and $F$ be sets. Then $\operatorname{mkL}$ applied to $x$, $E$ and $F$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and the set of tensor products of $E$ and $F$.
TensorProduct.ridIsometrydefMathlib.Analysis.InnerProductSpace.TensorProduct, function or constantEnglish
Let $x$ and $E$ be sets. Then $\operatorname{ridIsometry}$ applied to $x$ and $E$ is a linear isometry equivalence of the set of tensor products of $E$ and $x$ and $E$ defined as the isometry of $\operatorname{rid}$ applied to $x$ and $E$ and $\mathrm{TensorProduct\_\_inner\_rid\_rid}$.
Orientation.basisRightAngleRotationdefMathlib.Analysis.InnerProductSpace.TwoDim, function or constantWording
the basis right angle rotation of o and x2 (from the name)
English
Let $o$ be an orientation of $E$ and $\mathrm{Fin}$ applied to $2$. Let $x_{2}$ be an element of $E$ such that $x_{2} \neq 0$. Then the basis right angle rotation of $o$ and $x_{2}$ is a basis of $\Real$ and $E$.
Orientation.kahlerdefMathlib.Analysis.InnerProductSpace.TwoDim, function or constantEnglish
Let $o$ be an orientation of $E$ and $\mathrm{Fin}$ applied to $2$. Then $\operatorname{kahler}$ applied to $o$ is a linear map of $E$ and the set of linear maps of $E$ and the set of complexes defined as the sum of the composition of $\operatorname{llcomp}$ applied to $\Real$, $E$, $\Real$, the set of complexes and $\operatorname{toLinearMap}$ applied to the complex and the inner product of $\Real$ and the composition of $\operatorname{llcomp}$ applied to $\Real$, $E$, $\Real$, the set of complexes and $\operatorname{flip}$ applied to $\operatorname{lsmul}$ applied to $\Real$ and the set of complexes and $\operatorname{I}$ and the area form of $o$.
Orientation.rightAngleRotationdefMathlib.Analysis.InnerProductSpace.TwoDim, function or constantWording
the right angle rotation of o (from the name)
English
Let $o$ be an orientation of $E$ and $\mathrm{Fin}$ applied to $2$. Then the right angle rotation of $o$ is a linear isometry equivalence of $E$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{Orientation\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_InnerProductSpace\_\_TwoDim\_\_2712757639\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $o$.
HilbertBasisstructureMathlib.Analysis.InnerProductSpace.l2Space, typeWording
Hilbert basis of x1 and E (from the name)
English
Let $x$, $x_{1}$ and $E$ be sets. Then the Hilbert bases of $x_{1}$ and $E$ are a basic type.
HilbertBasis.mkdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantEnglish
Assume that $v$ is orthonormal. Assume that the top is less than or equal to the topological closure of the span of $x_{1}$ and the range of $v$. Then $\operatorname{mk}$ applied to $\mathrm{hv}$ and $\mathrm{hsp}$ is a Hilbert basis of $x_{1}$ and $E$ defined as $\operatorname{ofRepr}$ applied to the linear isometry equivalence of $\operatorname{isHilbertSum}$ applied to $\mathrm{hv}$ and $\mathrm{hsp}$.
HilbertBasis.mkOfOrthogonalEqBotdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantEnglish
Assume that $v$ is orthonormal. Assume that $\operatorname{orthogonal}$ applied to the span of $x_{1}$ and the range of $v$ is equal to the bottom. Then $\operatorname{mkOfOrthogonalEqBot}$ applied to $\mathrm{hv}$ and $\mathrm{hsp}$ is a Hilbert basis of $x_{1}$ and $E$.
HilbertBasis.reprdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantWording
the representation of self (from the name)
English
Let $\mathrm{self}$ be a Hilbert basis of $x_{1}$ and $E$. Then the representation of $\mathrm{self}$ is a linear isometry equivalence of $E$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{6} . x_{1} , 2)}{x_{5}})}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HilbertBasis.toOrthonormalBasisdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantWording
the orthonormal basis of b (from the name)
English
Let $b$ be a Hilbert basis of $x_{1}$ and $E$. Then the orthonormal basis of $b$ is an orthonormal basis of $x_{1}$ and $E$.
HilbertBasis.toSchauderBasisdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantEnglish
Let $b$ be a Hilbert basis of $x$ and $E$. Then $\operatorname{toSchauderBasis}$ applied to $b$ is an element of $\mathrm{SchauderBasis}$ applied to $x$ and $E$.
HilbertBasis.toUnconditionalSchauderBasisdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantEnglish
Let $b$ be a Hilbert basis of $x_{1}$ and $E$. Then $\operatorname{toUnconditionalSchauderBasis}$ applied to $b$ is an element of $\mathrm{UnconditionalSchauderBasis}$ applied to $x$, $x_{1}$ and $E$.
IsHilbertSumstructureMathlib.Analysis.InnerProductSpace.l2Space, predicateEnglish
Let $x_{1}$ be a set. Let $G$ be a function from elements of $x$ to sets. Let $V$ be a function from elements $i$ of $x$ to linear isometries of $G$ applied to $i$ and $E$. Then we can say that $\mathrm{IsHilbertSum}$ holds for $x_{1}$, $G$, $i$ and $V$.
IsHilbertSum.linearIsometryEquivdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantWording
the linear isometry equivalence of hV (from the name)
English
Assume that $\mathrm{IsHilbertSum}$ holds for $x_{1}$, $G$ and $V$. Then the linear isometry equivalence of $\mathrm{hV}$ is a linear isometry equivalence of $E$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{lp} (G , 2)}{x_{7}})}$ defined as the inverse of the linear isometry equivalence of the linear isometry of $\operatorname{OrthogonalFamily}$ applied to $\mathrm{hV}$ and $\mathrm{IsHilbertSum\_\_surjective\_isometry}$ applied to $\mathrm{hV}$.
OrthogonalFamily.linearIsometrydefMathlib.Analysis.InnerProductSpace.l2Space, function or constantWording
the linear isometry of hV (from the name)
English
Assume that $\mathrm{OrthogonalFamily}$ holds for $x_{1}$, $G$ and $V$. Then the linear isometry of $\mathrm{hV}$ is a linear isometry of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{lp} (G , 2)}{x_{7}})}$ and $E$.
OrthonormalBasis.toHilbertBasisdefMathlib.Analysis.InnerProductSpace.l2Space, function or constantWording
the Hilbert basis of b (from the name)
English
Let $b$ be an orthonormal basis of $x_{1}$ and $E$. Then the Hilbert basis of $b$ is a Hilbert basis of $x_{1}$ and $E$.
MeasureTheory.lconvolutiondefMathlib.Analysis.LConvolution, function or constantEnglish
Let $f$ and $g$ be functions from elements of $G$ to elements of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $G$. Let $x_{3}$ be an element of $G$. Then $\operatorname{lconvolution}$ applied to $f$, $g$, $x_{2}$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{lintegral}$ applied to $x_{2}$ and the function that maps $y$ to $f (y)\times g (\operatorname{neg} (y)+ x_{3})$.
MeasureTheory.mlconvolutiondefMathlib.Analysis.LConvolution, function or constantEnglish
Let $f$ and $g$ be functions from elements of $G$ to elements of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $G$. Let $x_{3}$ be an element of $G$. Then $\operatorname{mlconvolution}$ applied to $f$, $g$, $x_{2}$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{lintegral}$ applied to $x_{2}$ and the function that maps $y$ to $f (y)\times g (\operatorname{inv} (y)\times x_{3})$.
AbsConvexdefMathlib.Analysis.LocallyConvex.AbsConvex, predicateWording
x is absolutely convex (from the docstring)
English
generation took over the time limit
absConvexHulldefMathlib.Analysis.LocallyConvex.AbsConvex, function or constantWording
the absolute convex hull of x (from the docstring)
English
generation took over the time limit
closedAbsConvexHulldefMathlib.Analysis.LocallyConvex.AbsConvex, function or constantWording
the absolutely convex closed hull of x (from the docstring)
English
generation took over the time limit
AbsConvexOpenSetsdefMathlib.Analysis.LocallyConvex.AbsConvexOpen, typeWording
absolute value convex open set of x and E (from the name)
English
Let $x$ and $E$ be sets. Then an absolute value convex open set of $x$ and $E$ is an element of the function that maps $x$ and $E$ to $\SubtypeSet {s}{\mathrm{and} (\MembershipmemMACRoT {s}{0}, \mathrm{and} (\mathrm{IsOpen} (s), \mathrm{AbsConvex} (x)))}$.
gaugeSeminormFamilydefMathlib.Analysis.LocallyConvex.AbsConvexOpen, function or constantWording
the gauge seminorm family of x and E (from the name)
English
Let $x$ and $E$ be sets. Then the gauge seminorm family of $x$ and $E$ is a seminorm family of $E$ and the set of absolute value convex open sets of $x$ and $E$.
balancedCoredefMathlib.Analysis.LocallyConvex.BalancedCoreHull, function or constantEnglish
Let $x$ be a set. Let $s$ be an element of $\wp E$. Then $\mathrm{balancedCore}$ applied to $x$ and $s$ is an element of $\wp E$ defined as the union of $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is balanced and $t \leq s$.
balancedHulldefMathlib.Analysis.LocallyConvex.BalancedCoreHull, function or constantWording
the smallest balanced superset of x (from the docstring)
English
Let $x$ be a set. Then the smallest balanced superset of $x$ is a closure operator of $\wp E$ defined as the closure operator of the proposition that $\mathrm{Balanced}$ and the function that maps $x_{3}$ to $\operatorname{sInter}$.
BarrelledSpaceclassMathlib.Analysis.LocallyConvex.Barrelled, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{BarrelledSpace}$ holds for $x$ and $E$.
continuousLinearMapOfTendstodefMathlib.Analysis.LocallyConvex.Barrelled, function or constantWording
the continuous linear map of g and h10 (from the name)
English
Let $g$ be a function from elements of $x$ to continuous linear maps of $E$ and $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $n$ and $x_{12}$ to $g$ applied to $n$ and $x_{12}$, $l$ and the neighbourhood filter of $f$. Then the continuous linear map of $g$ and $h_{10}$ is a continuous linear map of $E$ and $F$.
BalanceddefMathlib.Analysis.LocallyConvex.Basic, predicateWording
A is balanced (from the name)
English
Let $x$ be a set. Let $A$ be an element of $\wp E$. Then $A$ is balanced, if for all elements $a$ of $x$, if the norm of $a$ is less than or equal to $1$, then $\HSMulhSMulMACRoAL {a}{A}\leq A$.
Bornology.IsVonNBoundeddefMathlib.Analysis.LocallyConvex.Bounded, predicateEnglish
Let $x$ be a set. Let $s$ be an element of $\wp E$. Then $\operatorname{IsVonNBounded}$ holds for $x$ and $s$, if for all elements $V$ of $\wp E$, if $V$ is an element of the neighbourhood filter of $0$, then $\mathrm{Absorbs}$ holds for $x$, $V$ and $s$.
QuasiCompleteSpaceclassMathlib.Analysis.LocallyConvex.Bounded, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{QuasiCompleteSpace}$ holds for $x$ and $E$.
LinearMap.clmOfExistsBoundedImagedefMathlib.Analysis.LocallyConvex.ContinuousOfBounded, function or constantWording
the continuous linear map of f and h4 (from the name)
English
Let $f$ be a linear map of $E$ and $F$ such that there exists an element $V$ of $\wp E$, such that $V$ is an element of the neighbourhood filter of $0$ and $\operatorname{IsVonNBounded}$ holds for $x_{1}$ and the image of $\operatorname{coe}$ applied to $f$ and $V$. Then the continuous linear map of $f$ and $h_{4}$ is a continuous linear map of $E$ and $F$.
ContinuousLinearEquiv.toCompactConvergenceCLMdefMathlib.Analysis.LocallyConvex.Montel, function or constantWording
the compact convergence continuous linear map of x4 (from the name)
English
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then the compact convergence continuous linear map of $x_{4}$ is a continuous linear equivalence of the set of continuous linear maps of $E$ and $F$ and the set of compact convergence continuous linear maps of $E$ and $F$.
MontelSpaceclassMathlib.Analysis.LocallyConvex.Montel, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{MontelSpace}$ holds for $x$ and $E$.
PointwiseConvergenceCLM.inducingFndefMathlib.Analysis.LocallyConvex.PointwiseConvergence, function or constantEnglish
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then $\operatorname{inducingFn}$ applied to $x_{4}$, $E$ and $F$ is a linear map of the set of pointwise convergence continuous linear maps of $E$ and $F$ and the set of functions from elements of $E$ to elements of $F$.
PointwiseConvergenceCLM.mkCLMdefMathlib.Analysis.LocallyConvex.PointwiseConvergence, function or constantWording
the continuous linear map of A (from the name)
English
Let $F$ and $G$ be sets. Let $A$ be a linear map of the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $D$ and $G$ such that for all elements $f$ of $D$, there exists a finite set $s$ of $E$, such that there exists an element $C$ of $\mathrm{NNReal}$, such that for all continuous linear maps $B$ of $E$ and $F$, there exists an element $g$ of $E$, such that there exists an element $\mathrm{\_hb}$ of $\MembershipmemMACRoT {s}{g}$, such that $\operatorname{norm} (\operatorname{coe} (A , B , f))\leq \HSMulhSMulMACRoAL {C}{\operatorname{norm} (B (g))}$. Then the continuous linear map of $A$ is a continuous linear map of the set of pointwise convergence continuous linear maps of $E$ and $F$ and the set of pointwise convergence continuous linear maps of $D$ and $G$.
PointwiseConvergenceCLM.seminormdefMathlib.Analysis.LocallyConvex.PointwiseConvergence, function or constantWording
the seminorm of x10 (from the name)
English
Let $x_{10}$ be an element of $E$. Then the seminorm of $x_{10}$ is a seminorm of $x_{1}$ and the set of pointwise convergence continuous linear maps of $E$ and $F$.
PointwiseConvergenceCLM.seminormFamilydefMathlib.Analysis.LocallyConvex.PointwiseConvergence, function or constantWording
the seminorm family of x4 (from the name)
English
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then the seminorm family of $x_{4}$ is a seminorm family of the set of pointwise convergence continuous linear maps of $E$ and $F$ and $E$ defined as $\operatorname{seminorm}$.
LinearMap.polardefMathlib.Analysis.LocallyConvex.Polar, function or constantEnglish
Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$. Let $s$ be an element of $\wp E$. Then $\operatorname{polar}$ applied to $B$ and $s$ is an element of $\wp F$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that for all elements $x_{6}$ of $E$, if $x_{6}$ is an element of $s$, then the norm of $\operatorname{coe}$ applied to $B$, $x_{6}$ and $y$ is less than or equal to $1$.
LinearMap.polarSubmoduledefMathlib.Analysis.LocallyConvex.Polar, function or constantWording
the polar submodule of B and m (from the name)
English
Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$. Let $m$ be an element of $S$. Then the polar submodule of $B$ and $m$ is a submodule of $x$ and $F$.
StrongDual.polardefMathlib.Analysis.LocallyConvex.Polar, function or constantEnglish
Let $R$ be a set. Let $x_{4}$ be an element of $\wp M$. Then $\operatorname{polar}$ applied to $R$ and $x_{4}$ is an element of the power set of the set of strong duals of $R$ and $M$ defined as $\operatorname{polar}$ applied to the flip of the canonical pairing of $R$ and $M$ and $x_{4}$.
StrongDual.polarSubmoduledefMathlib.Analysis.LocallyConvex.Polar, function or constantWording
the polar submodule of x and m (from the name)
English
Let $x$ be a set. Let $m$ be an element of $S$. Then the polar submodule of $x$ and $m$ is a submodule of $x$ and the set of strong duals of $x$ and $M$ defined as the polar submodule of the flip of the canonical pairing of $x$ and $M$ and $m$.
SeparatingDualclassMathlib.Analysis.LocallyConvex.SeparatingDual, predicateWording
V is a separating dual with respect to R (from the name)
English
Let $R$ and $V$ be sets. Then we can say that $V$ is a separating dual with respect to $R$.
LinearMap.leftDualEquivdefMathlib.Analysis.LocallyConvex.WeakDual, function or constantWording
the left dual equivalence of B and hl (from the name)
English
Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$ such that $B$ is a left separating. Then the left dual equivalence of $B$ and $\mathrm{hl}$ is a linear equivalence of $E$ and the set of strong duals of $x$ and the set of weak bilinears of the flip of $B$.
LinearMap.rightDualEquivdefMathlib.Analysis.LocallyConvex.WeakDual, function or constantWording
the right dual equivalence of B and hr (from the name)
English
Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$ such that $B$ is a right separating. Then the right dual equivalence of $B$ and $\mathrm{hr}$ is a linear equivalence of $F$ and the set of strong duals of $x$ and the set of weak bilinears of $B$.
LinearMap.toSeminormdefMathlib.Analysis.LocallyConvex.WeakDual, function or constantWording
the seminorm of f (from the name)
English
Let $f$ be a linear map of $E$ and $x$. Then the seminorm of $f$ is a seminorm of $x$ and $E$ defined as the composition of the norm of $x$ and $x$ and $f$.
LinearMap.toSeminormFamilydefMathlib.Analysis.LocallyConvex.WeakDual, function or constantWording
the seminorm family of B (from the name)
English
Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$. Then the seminorm family of $B$ is a seminorm family of $E$ and $F$ defined as the function that maps $y$ to the seminorm of $\operatorname{flip}$ applied to $B$ and $y$.
ContinuousLinearMap.WOTofCLMdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantEnglish
$\operatorname{WOTofCLM}$ is a continuous linear map of the set of continuous linear maps of $E$ and $F$ and $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $x_{1}$ and $\mathrm{ContinuousLinearMapWOT\_\_continuous\_ofCLM}$.
ContinuousLinearMapWOTstructureMathlib.Analysis.LocallyConvex.WeakOperatorTopology, typeEnglish
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then the elements of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ are a basic type.
ContinuousLinearMapWOT.addEquivdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the additive equivalence (from the name)
English
The additive equivalence is an additive equivalence of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ and the set of continuous linear maps of $E$ and $F$.
ContinuousLinearMapWOT.algEquivdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the algebra isomorphism of S (from the name)
English
Let $S$ be a set. Then the algebra isomorphism of $S$ is an algebra isomorphism of $\mathrm{ContinuousLinearMapWOT}$ applied to the identity ring homomorphism of $x$, $E$ and $E$ and the set of continuous linear maps of $E$ and $E$ defined as the algebra isomorphism of $S$ and the equivalence.
ContinuousLinearMapWOT.compdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{8}$, $F$ and $G$. Let $f$ be an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{6}$, $E$ and $F$. Then the composition of $g$ and $f$ is an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{7}$, $E$ and $G$ defined as $\operatorname{ofCLM}$ applied to the composition of the continuous linear map of $g$ and the continuous linear map of $f$.
ContinuousLinearMapWOT.equivdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the equivalence (from the name)
English
The equivalence is an equivalence from $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ to the set of continuous linear maps of $E$ and $F$.
ContinuousLinearMapWOT.iddefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the identity of x and F (from the docstring)
English
Let $x$ and $F$ be sets. Then the identity of $x$ and $F$ is an element of $\mathrm{ContinuousLinearMapWOT}$ applied to the identity ring homomorphism of $x$, $F$ and $F$ defined as $\operatorname{ofCLM}$ applied to the identity map of $x$ and $F$.
ContinuousLinearMapWOT.inducingFndefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantEnglish
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then $\operatorname{inducingFn}$ applied to $x_{4}$, $E$ and $F$ is a linear map of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ and the set of functions from elements of $\mathrm{Prod}$ applied to $E$ and the set of strong duals of $x_{1}$ and $F$ to elements of $x_{1}$.
ContinuousLinearMapWOT.linearEquivdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the linear equivalence of S (from the name)
English
Let $S$ be a set. Then the linear equivalence of $S$ is a linear equivalence of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ and the set of continuous linear maps of $E$ and $F$ defined as the linear equivalence of $S$ and the additive equivalence.
ContinuousLinearMapWOT.postcompCLMdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the postcomposition continuous linear map of g (from the name)
English
Let $g$ be an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{8}$, $F$ and $G$. Then the postcomposition continuous linear map of $g$ is a continuous linear map of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{6}$, $E$ and $F$ and $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{7}$, $E$ and $G$.
ContinuousLinearMapWOT.precompCLMdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the precomposition continuous linear map of f (from the name)
English
Let $f$ be an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{6}$, $E$ and $F$. Then the precomposition continuous linear map of $f$ is a continuous linear map of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{8}$, $F$ and $G$ and $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{7}$, $E$ and $G$.
ContinuousLinearMapWOT.ringEquivdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the ring isomorphism (from the name)
English
The ring isomorphism is a ring isomorphism of $\mathrm{ContinuousLinearMapWOT}$ applied to the identity ring homomorphism of $x$, $E$ and $E$ and the set of continuous linear maps of $E$ and $E$ defined as the ring isomorphism of the equivalence.
ContinuousLinearMapWOT.seminormdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the seminorm of x11 and y (from the name)
English
Let $x_{11}$ be an element of $E$. Let $y$ be a strong dual of $x_{1}$ and $F$. Then the seminorm of $x_{11}$ and $y$ is a seminorm of $x_{1}$ and $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$.
ContinuousLinearMapWOT.seminormFamilydefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the seminorm family of x4 (from the name)
English
Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then the seminorm family of $x_{4}$ is a seminorm family of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$ and $\mathrm{Prod}$ applied to $E$ and the set of strong duals of $x_{1}$ and $F$.
ContinuousLinearMapWOT.toCLMdefMathlib.Analysis.LocallyConvex.WeakOperatorTopology, function or constantWording
the continuous linear map of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{ContinuousLinearMapWOT}$ applied to $x_{4}$, $E$ and $F$. Then the continuous linear map of $\mathrm{self}$ is a continuous linear map of $E$ and $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
IsNormableSpaceclassMathlib.Analysis.LocallyConvex.WithSeminorms, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{IsNormableSpace}$ holds for $x$ and $E$.
IsNormableSpace.seminormdefMathlib.Analysis.LocallyConvex.WithSeminorms, function or constantWording
the seminorm of x and E (from the name)
English
Let $x$ and $E$ be sets. Then the seminorm of $x$ and $E$ is a seminorm of $x$ and $E$ defined as $\operatorname{choose}$ applied to $\operatorname{withSeminorms'}$.
PolynormableSpaceclassMathlib.Analysis.LocallyConvex.WithSeminorms, predicateEnglish
Let $x$ and $E$ be sets. Then we can say that $\mathrm{PolynormableSpace}$ holds for $x$ and $E$.
Seminorm.IsBoundeddefMathlib.Analysis.LocallyConvex.WithSeminorms, predicateEnglish
Let $p$ be a function from elements of $x_{2}$ to seminorms of $x$ and $E$. Let $q$ be a function from elements of $x_{3}$ to seminorms of $x_{1}$ and $F$. Let $f$ be a linear map of $E$ and $F$. Then $\operatorname{IsBounded}$ holds for $p$, $q$ and $f$, if for all elements $i$ of $x_{3}$, there exists a finite set $s$ of $x_{2}$, such that there exists an element $C$ of $\mathrm{NNReal}$, such that $\operatorname{comp} (q (i), f)\leq \HSMulhSMulMACRoAL {C}{\operatorname{sup} (s , p)}$.
SeminormFamilydefMathlib.Analysis.LocallyConvex.WithSeminorms, typeWording
seminorm family of E and x (from the name)
English
Let $R$, $E$ and $x$ be sets. Then a seminorm family of $E$ and $x$ is an element of the function that maps $R$, $E$ and $x$ to the set of functions from elements of $x$ to seminorms of $R$ and $E$.
SeminormFamily.basisSetsdefMathlib.Analysis.LocallyConvex.WithSeminorms, function or constantWording
the basis set of p (from the name)
English
Let $p$ be a seminorm family of $E$ and $x$. Then the basis set of $p$ is an element of $\wp (\wp E)$ defined as the union of the function that maps $s$ to the union of the function that maps $r$ to the union of the function that maps $h$ to $\operatorname{singleton}$ applied to the ball of $0$ and $r$.
SeminormFamily.compdefMathlib.Analysis.LocallyConvex.WithSeminorms, function or constantWording
the composition of q and f (from the name)
English
Let $q$ be a seminorm family of $F$ and $x_{2}$. Let $f$ be a linear map of $E$ and $F$. Then the composition of $q$ and $f$ is a seminorm family of $E$ and $x_{2}$ defined as the function that maps $i$ to the composition of $q$ applied to $i$ and $f$.
SeminormFamily.moduleFilterBasisdefMathlib.Analysis.LocallyConvex.WithSeminorms, function or constantWording
the module filter basis of p (from the name)
English
Let $p$ be a seminorm family of $F$ and $x_{1}$. Then the module filter basis of $p$ is a module filter basis of $x$ and $F$.
SeminormFamily.sigmadefMathlib.Analysis.LocallyConvex.WithSeminorms, function or constantWording
the sigma of p (from the name)
English
Let $p$ be a function from elements $i_{1}$ of $x_{1}$ to seminorm families of $E$ and $x_{5}$ applied to $i_{1}$. Then the sigma of $i_{1}$ is a seminorm family of $E$ and $\Sigma$ applied to the function that maps $i$ to $x_{5}$ applied to $i$.
WithSeminormsstructureMathlib.Analysis.LocallyConvex.WithSeminorms, predicateEnglish
Let $p$ be a seminorm family of $E$ and $x_{1}$. Then we can say that $\mathrm{WithSeminorms}$ holds for $p$.
Matrix.IsHermitian.cfcdefMathlib.Analysis.Matrix.HermitianFunctionalCalculus, function or constantEnglish
Assume that $A$ is hermitian. Let $f$ be a function from real numbers to real numbers. Then there is a matrix of $n$ and $x$. Proof. Let $\mathrm{hA}$ be arbitrary. Let $f$ be arbitrary. By x. By n. By x. By Matrix. By Unitary__conjStarAlgAut. By hA. By Matrix__IsHermitian__eigenvectorUnitary. By RCLike__ofReal. By f. By hA. By Matrix__IsHermitian__eigenvalues. By Function__comp. By Function__comp. By Matrix__diagonal. By DFunLike__coe__app.
LDL.diagdefMathlib.Analysis.Matrix.LDL, function or constantWording
the diagonal matrix of hS (from the docstring)
English
Assume that $S$ is a positive part. Then the diagonal matrix of $\mathrm{hS}$ is a matrix of $n$ and $x$ defined as the diagonal of $\operatorname{diagEntries}$ applied to $\mathrm{hS}$.
LDL.diagEntriesdefMathlib.Analysis.Matrix.LDL, function or constantWording
the diagonal entry of hS and x5 (from the name)
English
Assume that $S$ is a positive part. Let $x_{5}$ be an element of $n$. Then the diagonal entry of $\mathrm{hS}$ and $x_{5}$ is an element of $x$ defined as $\operatorname{inner}$ applied to $x$, $\operatorname{toLp}$ applied to $2$ and the star of the inverse of the lower triangular matrix of $\mathrm{hS}$ and $\operatorname{toLp}$ applied to $2$ and $\operatorname{mulVec}$ applied to the star of the inverse of the lower triangular matrix of $\mathrm{hS}$.
LDL.lowerdefMathlib.Analysis.Matrix.LDL, function or constantWording
the lower triangular matrix of hS (from the docstring)
English
Assume that $S$ is a positive part. Then the lower triangular matrix of $\mathrm{hS}$ is a matrix of $n$ and $x$ defined as $\operatorname{inv}$ applied to the inverse of the lower triangular matrix of $\mathrm{hS}$.
LDL.lowerInvdefMathlib.Analysis.Matrix.LDL, function or constantWording
the inverse of the lower triangular matrix of hS (from the docstring)
English
Assume that $S$ is a positive part. Then the inverse of the lower triangular matrix of $\mathrm{hS}$ is a matrix of $n$ and $x$ defined as $\operatorname{gramSchmidt}$ applied to $\operatorname{coe}$ applied to the basis function of $x$ and $n$.
Matrix.ofMeasurableEquivdefMathlib.Analysis.Matrix.MeasurableSpace, function or constantWording
the matrix of n and x (from the name)
English
Let $m$, $n$ and $x$ be sets. Then the matrix of $n$ and $x$ is a measurable equivalence of the set of functions from elements of $m$ and elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.
Matrix.tracePositiveLinearMapdefMathlib.Analysis.Matrix.Order, function or constantWording
the trace positive linear map of x and x1 (from the name)
English
Let $n$, $x$ and $x_{1}$ be sets. Then the trace positive linear map of $x$ and $x_{1}$ is a positive linear map of the set of matrixes of $n$ and $x_{1}$ and $x_{1}$.
Matrix.IsHermitian.eigenvaluesdefMathlib.Analysis.Matrix.Spectrum, function or constantWording
the eigenvalue of hA and x4 (from the name)
English
Assume that $A$ is hermitian. Let $x_{4}$ be an element of $n$. Then the eigenvalue of $\mathrm{hA}$ and $x_{4}$ is a real number.
Matrix.IsHermitian.eigenvalues₀defMathlib.Analysis.Matrix.Spectrum, function or constantWording
the eigenvalue of hA and x4 (from the name)
English
Assume that $A$ is hermitian. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to the cardinality of $n$. Then the eigenvalue of $\mathrm{hA}$ and $x_{4}$ is a real number.
Matrix.IsHermitian.eigenvectorBasisdefMathlib.Analysis.Matrix.Spectrum, function or constantWording
the eigenvector basis of hA (from the name)
English
Assume that $A$ is hermitian. Then the eigenvector basis of $\mathrm{hA}$ is an orthonormal basis of $x$ and the set of Euclidean spaces of $x$ and $n$.
Matrix.IsHermitian.eigenvectorUnitarydefMathlib.Analysis.Matrix.Spectrum, function or constantEnglish
Assume that $A$ is hermitian. Then $\operatorname{eigenvectorUnitary}$ applied to $\mathrm{hA}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x)}{x_{4}})}$ defined as the matrix of the basis of the basis of $n$ and $x$ and $\operatorname{coe}$ applied to the basis of the eigenvector basis of $\mathrm{hA}$.
ENNReal.LpAddConstdefMathlib.Analysis.MeanInequalitiesPow, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{LpAddConst}$ applied to $p$ is an element of $\mathrm{ENNReal}$ defined as $\iteMACRoG {(\MembershipmemMACRoT {\operatorname{Ioo} (0 , 1)}{p})}{(2 ^ {(\frac{ 1}{\operatorname{toReal} (p)}- 1)})}{1}$.
Complex.VerticalIntegrabledefMathlib.Analysis.MellinTransform, predicateEnglish
Let $f$ be a function from complexes to elements of $E$. Let $x_{1}$ be a real number. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $\Real$ and $\mathrm{Complex\_\_VerticalIntegrable\_\_\_auto\_1}$. Then $\operatorname{VerticalIntegrable}$ holds for $f$, $x_{1}$ and $x_{2}$, if $\operatorname{Integrable}$ holds for the function that maps $y$ to $f$ applied to the sum of the natural inclusion of the real numbers into the complex numbers of $x_{1}$ and the product of the natural inclusion of the real numbers into the complex numbers of $y$ and $\operatorname{I}$ and $x_{2}$.
HasMellindefMathlib.Analysis.MellinTransform, predicateEnglish
Let $f$ be a function from real numbers to elements of $E$. Let $s$ be a complex. Let $m$ be an element of $E$. Then $\mathrm{HasMellin}$ holds for $f$, $s$ and $m$, if $\mathrm{MellinConvergent}$ holds for $f$ and $s$ and $\EqtMACRoH {\mathrm{mellin} (f , s)}{m}$.
MellinConvergentdefMathlib.Analysis.MellinTransform, predicateEnglish
Let $f$ be a function from elements of $\Real$ to elements of $E$. Let $s$ be a complex. Then $\mathrm{MellinConvergent}$ holds for $f$ and $s$, if $\operatorname{IntegrableOn}$ holds for the function that maps $t$ to $\HSMulhSMulMACRoAL {(\operatorname{ofReal} (t)^ {(s - 1)})}{f (t)}$, $\operatorname{Ioi}$ applied to $0$ and the volume.
mellindefMathlib.Analysis.MellinTransform, function or constantEnglish
Let $f$ be a function from elements of $\Real$ to elements of $E$. Let $s$ be a complex. Then $\mathrm{mellin}$ applied to $f$ and $s$ is an element of $E$ defined as the Bochner integral of $\operatorname{restrict}$ applied to the volume and $\operatorname{Ioi}$ applied to $0$ and the function that maps $t$ to $\HSMulhSMulMACRoAL {(\operatorname{ofReal} (t)^ {(s - 1)})}{f (t)}$.
mellinInvdefMathlib.Analysis.MellinTransform, function or constantEnglish
Let $x_{2}$ and $x_{3}$ be elements of $\Real$. Let $f$ be a function from complexes to elements of $E$. Then $\mathrm{mellinInv}$ applied to $x_{2}$, $f$ and $x_{3}$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {(\frac{ 1}{2 \times \operatorname{pi}})}{\operatorname{integral} (\operatorname{volume} , \lambda y . \HSMulhSMulMACRoAL {(\operatorname{ofReal} (x_{3})^ {\operatorname{neg} (\operatorname{ofReal} (x_{2})+ \operatorname{ofReal} (y)\times \operatorname{I})})}{f (\operatorname{ofReal} (x_{2})+ \operatorname{ofReal} (y)\times \operatorname{I})})}$.
MeromorphicdefMathlib.Analysis.Meromorphic.Basic, predicateWording
f is meromorphic (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $E$. Then $f$ is meromorphic, if for all elements $x_{4}$ of $x$, $\mathrm{MeromorphicAt}$ holds for $f$ and $x_{4}$.
MeromorphicAtdefMathlib.Analysis.Meromorphic.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then $\mathrm{MeromorphicAt}$ holds for $f$ and $x_{4}$, if there exists a natural number $n$, such that $\mathrm{AnalyticAt}$ holds for $x$, the function that maps $z$ to $\HSMulhSMulMACRoAL {((z - x_{4})^ {n})}{f (z)}$ and $x_{4}$.
MeromorphicOndefMathlib.Analysis.Meromorphic.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $U$ be an element of $\wp x$. Then $\mathrm{MeromorphicOn}$ holds for $f$ and $U$, if for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $U$, then $\mathrm{MeromorphicAt}$ holds for $f$ and $x_{4}$.
MeromorphicOn.divisordefMathlib.Analysis.Meromorphic.Divisor, function or constantWording
the divisor of f and U (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $E$. Let $U$ be an element of $\wp x$. Then the divisor of $f$ and $U$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $\Integer$.
MeromorphicNFAtdefMathlib.Analysis.Meromorphic.NormalForm, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then $\mathrm{MeromorphicNFAt}$ holds for $f$ and $x_{4}$, if $\operatorname{EventuallyEq}$ holds for the neighbourhood filter of $x_{4}$, $f$ and $0$ or there exists an integer $n$ such that there exists a function $g$ from elements of $x$ to elements of $E$ such that $\mathrm{AnalyticAt}$ holds for $x$, $g$ and $x_{4}$ and $g (x_{4})\neq 0$ and $\operatorname{EventuallyEq}$ holds for the neighbourhood filter of $x_{4}$, $f$ and $\HSMulhSMulMACRoAL {\mathrm{pow} (\lambda x_{5} . x_{5} - x_{4} , n)}{g}$.
MeromorphicNFOndefMathlib.Analysis.Meromorphic.NormalForm, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $U$ be an element of $\wp x$. Then $\mathrm{MeromorphicNFOn}$ holds for $f$ and $U$, if for all elements $z$ of $x$, if $z$ is an element of $U$, then $\mathrm{MeromorphicNFAt}$ holds for $f$ and $z$.
toMeromorphicNFAtdefMathlib.Analysis.Meromorphic.NormalForm, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ and $x_{5}$ be elements of $x$. Then $\mathrm{toMeromorphicNFAt}$ applied to $f$, $x_{4}$ and $x_{5}$ is an element of $E$.
toMeromorphicNFOndefMathlib.Analysis.Meromorphic.NormalForm, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $U$ be an element of $\wp x$. Let $x_{4}$ be an element of $x$. Then $\mathrm{toMeromorphicNFOn}$ applied to $f$, $U$ and $x_{4}$ is an element of $E$ defined as $\mathrm{dite}$ applied to $\mathrm{MeromorphicOn}$ applied to $f$ and $U$, the function that maps $h$ and $z$ to $\mathrm{dite}$ applied to $\MembershipmemMACRoT {U}{z}$, the function that maps $\mathrm{hz}$ to $\mathrm{toMeromorphicNFAt}$ applied to $f$, $z$ and $z$ and the function that maps $\mathrm{hz1}$ to $f$ applied to $z$, the function that maps $h_{1}$ to $0$ and $x_{4}$.
meromorphicOrderAtdefMathlib.Analysis.Meromorphic.Order, function or constantWording
the order of f and x4 (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then the order of $f$ and $x_{4}$ is an element of $\mathrm{WithTop}$ applied to $\Integer$ defined as $\mathrm{dite}$ applied to $\mathrm{MeromorphicAt}$ applied to $f$ and $x_{4}$, the function that maps $\mathrm{hf}$ to the difference between the map of the function that maps $x_{5}$ to $x_{5}$ and $\mathrm{analyticOrderAt}$ applied to the function that maps $z$ to $\HSMulhSMulMACRoAL {((z - x_{4})^ {\operatorname{choose} (\mathrm{hf})})}{f (z)}$ and $x_{4}$ and $\operatorname{choose}$ applied to $\mathrm{hf}$ and the function that maps $\mathrm{hf1}$ to $0$.
meromorphicTrailingCoeffAtdefMathlib.Analysis.Meromorphic.TrailingCoefficient, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{4}$ be an element of $x$. Then $\mathrm{meromorphicTrailingCoeffAt}$ applied to $f$ and $x_{4}$ is an element of $E$.
AffineMap.ofMapMidpointdefMathlib.Analysis.Normed.Affine.AddTorsor, function or constantWording
the affine map of f (from the name)
English
Let $f$ be a function from elements of $P$ to elements of $Q$ such that for all elements $x_{8}$ of $P$, for all elements $y$ of $P$, $f$ applied to the midpoint of $x_{8}$ and $y$ is equal to the midpoint of $f$ applied to $x_{8}$ and $f$ applied to $y$ and $f$ is continuous. Then the affine map of $f$ is an affine map of $P$ and $Q$.
DilationEquiv.smulTorsordefMathlib.Analysis.Normed.Affine.AddTorsor, function or constantWording
the scalar multiple torsor of c and hk (from the name)
English
Let $c$ be an element of $P$. Assume that $k \neq 0$. Then the scalar multiple torsor of $c$ and $\mathrm{hk}$ is a dilation equivalence of $E$ and $P$.
ContinuousAffineMap.decompLinearIsometryEquivdefMathlib.Analysis.Normed.Affine.ContinuousAffineMap, function or constantWording
the decomposition linear isometry equivalence of V and W (from the name)
English
Let $x$, $R$, $V$ and $W$ be sets. Then the decomposition linear isometry equivalence of $V$ and $W$ is a linear isometry equivalence of the set of continuous affine maps of $V$ and $W$ and $\mathrm{Prod}$ applied to $W$ and the set of continuous linear maps of $V$ and $W$.
AffineIsometrystructureMathlib.Analysis.Normed.Affine.Isometry, typeWording
affine isometry of P and x2 (from the name)
English
Let $x$, $P$ and $x_{2}$ be sets. Then the affine isometries of $P$ and $x_{2}$ are a basic type.
AffineIsometry.compdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an affine isometry of $x_{3}$ and $x_{4}$. Let $f$ be an affine isometry of $P$ and $x_{3}$. Then the composition of $g$ and $f$ is an affine isometry of $P$ and $x_{4}$.
AffineIsometry.iddefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the identity affine isometry (from the docstring)
English
The identity affine isometry is an affine isometry of $P$ and $P$.
AffineIsometry.linearIsometrydefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the underlying linear map of f (from the docstring)
English
Let $f$ be an affine isometry of $P$ and $x_{2}$. Then the underlying linear map of $f$ is a linear isometry of $V$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the linear map between the corresponding vector spaces of $\operatorname{toAffineMap}$ applied to $f$ and $\mathrm{AffineIsometry\_\_norm\_map}$ applied to $f$.
AffineIsometry.toContinuousAffineMapdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the continuous affine map of f (from the name)
English
Let $f$ be an affine isometry of $P$ and $x_{2}$. Then the continuous affine map of $f$ is a continuous affine map of $P$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{toAffineMap}$ applied to $f$ and $\operatorname{continuous}$ applied to $f$.
AffineIsometryEquivstructureMathlib.Analysis.Normed.Affine.Isometry, typeWording
affine isometry equivalence of P and x2 (from the name)
English
Let $x$, $P$ and $x_{2}$ be sets. Then the affine isometry equivalences of $P$ and $x_{2}$ are a basic type.
AffineIsometryEquiv.constVAdddefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the constant sum of v (from the name)
English
Let $x$ and $P$ be sets. Let $v$ be an element of $V$. Then the constant sum of $v$ is an affine isometry equivalence of $P$ and $P$.
AffineIsometryEquiv.constVSubdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the constant difference of x and p (from the name)
English
Let $x$ be a set. Let $p$ be an element of $P$. Then the constant difference of $x$ and $p$ is an affine isometry equivalence of $P$ and $V$.
AffineIsometryEquiv.linearIsometryEquivdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the linear isometry equivalence of e (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the linear isometry equivalence of $e$ is a linear isometry equivalence of $V$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{linear}$ applied to $\operatorname{toAffineEquiv}$ applied to $e$ and $\mathrm{AffineIsometryEquiv\_\_norm\_map}$ applied to $e$.
AffineIsometryEquiv.mk'defMathlib.Analysis.Normed.Affine.Isometry, function or constantEnglish
Let $e$ be a function from elements of $x_{3}$ to elements of $x_{4}$. Let $\mathrm{e'}$ be a linear isometry equivalence of $x_{1}$ and $x_{2}$. Let $p$ be an element of $x_{3}$ such that for all elements $\mathrm{p'}$ of $x_{3}$, $e$ applied to $\mathrm{p'}$ is equal to the sum of $\mathrm{e'}$ applied to the vector difference of $\mathrm{p'}$ and $p$ and $e$ applied to $p$. Then $\operatorname{mk'}$ applied to $e$, $\mathrm{e'}$, $p$ and $h$ is an affine isometry equivalence of $x_{3}$ and $x_{4}$.
AffineIsometryEquiv.ofEqdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the affine isometry equivalence of x6 and x7 (from the name)
English
Let $x_{6}$ and $x_{7}$ be affine subspaces of $x$ and $P$ such that $\EqtMACRoH {x_{6}}{x_{7}}$. Then the affine isometry equivalence of $x_{6}$ and $x_{7}$ is an affine isometry equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6}}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7}}{x_{9}})}$.
AffineIsometryEquiv.ofTopdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the identity equivalence of x6 and h1 (from the docstring)
English
Let $x_{6}$ be an affine subspace of $x$ and $P$ such that $x_{6}$ is equal to the top. Then the identity equivalence of $x_{6}$ and $h_{1}$ is an affine isometry equivalence of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{6}}{x_{7}})}$ and $P$.
AffineIsometryEquiv.pointReflectiondefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the point reflection of x and x6 (from the name)
English
Let $x$ be a set. Let $x_{6}$ be an element of $P$. Then the point reflection of $x$ and $x_{6}$ is an affine isometry equivalence of $P$ and $P$ defined as the composition of the constant difference of $x$ and $x_{6}$ and the vector sum constant of $x$ and $x_{6}$.
AffineIsometryEquiv.refldefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the identity of x and P (from the name)
English
Let $x$ and $P$ be sets. Then the identity of $x$ and $P$ is an affine isometry equivalence of $P$ and $P$.
AffineIsometryEquiv.symmdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the inverse of $e$ is an affine isometry equivalence of $x_{2}$ and $P$.
AffineIsometryEquiv.toAffineIsometrydefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the affine isometry of e (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the affine isometry of $e$ is an affine isometry of $P$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the affine map of $\operatorname{toAffineEquiv}$ applied to $e$ and $\mathrm{AffineIsometryEquiv\_\_norm\_map}$ applied to $e$.
AffineIsometryEquiv.toContinuousAffineEquivdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the continuous affine equivalence of e (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the continuous affine equivalence of $e$ is a continuous affine equivalence of $P$ and $x_{2}$.
AffineIsometryEquiv.toHomeomorphdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the homeomorphism of $e$ is a homeomorphism of $P$ and $x_{2}$ defined as the homeomorphism of the isometry equivalence of $e$.
AffineIsometryEquiv.toIsometryEquivdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the isometry equivalence of e (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{2}$. Then the isometry equivalence of $e$ is an isometry equivalence of $P$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toAffineEquiv}$ applied to $e$ and $\operatorname{isometry}$ applied to $e$.
AffineIsometryEquiv.transdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be an affine isometry equivalence of $P$ and $x_{3}$. Let $\mathrm{e'}$ be an affine isometry equivalence of $x_{3}$ and $x_{4}$. Then the composition of $e$ and $\mathrm{e'}$ is an affine isometry equivalence of $P$ and $x_{4}$.
AffineIsometryEquiv.vaddConstdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the vector sum constant of x and p (from the name)
English
Let $x$ be a set. Let $p$ be an element of $P$. Then the vector sum constant of $x$ and $p$ is an affine isometry equivalence of $V$ and $P$.
AffineSubspace.equivMapOfInjectivedefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the equivalence map of E and x14 (from the name)
English
Let $E$ be an affine subspace of $x$ and $x_{3}$. Let $x_{14}$ be an affine map of $x_{3}$ and $x_{4}$ such that $\operatorname{coe}$ applied to $x_{14}$ is injective. Then the equivalence map of $E$ and $x_{14}$ is an affine equivalence of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {E}{x_{15}})}$ and $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {\operatorname{map} (x_{14} , E)}{x_{16}})}$.
AffineSubspace.isometryEquivMapdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the isometry equivalence map of x14 and E (from the name)
English
Let $x_{14}$ be an affine isometry of $x_{9}$ and $x_{2}$. Let $E$ be an affine subspace of $x$ and $x_{9}$. Then the isometry equivalence map of $x_{14}$ and $E$ is an affine isometry equivalence of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {E}{x_{15}})}$ and $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toAffineMap} (x_{14}), E)}{x_{16}})}$.
AffineSubspace.subtypeₐᵢdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the subtype of s (from the name)
English
Let $s$ be an affine subspace of $x$ and $P$. Then the subtype of $s$ is an affine isometry of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and $P$.
LinearIsometry.toAffineIsometrydefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the affine isometry of f (from the name)
English
Let $f$ be a linear isometry of $V$ and $x_{1}$. Then the affine isometry of $f$ is an affine isometry of $V$ and $x_{1}$.
LinearIsometryEquiv.toAffineIsometryEquivdefMathlib.Analysis.Normed.Affine.Isometry, function or constantWording
the affine isometry equivalence of e (from the name)
English
Let $e$ be a linear isometry equivalence of $V$ and $x_{1}$. Then the affine isometry equivalence of $e$ is an affine isometry equivalence of $V$ and $x_{1}$.
IsometryEquiv.toRealAffineIsometryEquivdefMathlib.Analysis.Normed.Affine.MazurUlam, function or constantWording
the real affine isometry equivalence of f (from the name)
English
Let $f$ be an isometry equivalence of $\mathrm{PE}$ and $\mathrm{PF}$. Then the real affine isometry equivalence of $f$ is an affine isometry equivalence of $\mathrm{PE}$ and $\mathrm{PF}$.
IsometryEquiv.toRealLinearIsometryEquivdefMathlib.Analysis.Normed.Affine.MazurUlam, function or constantWording
the real linear isometry equivalence of f (from the name)
English
Let $f$ be an isometry equivalence of $E$ and $F$. Then the real linear isometry equivalence of $f$ is a linear isometry equivalence of $E$ and $F$.
IsometryEquiv.toRealLinearIsometryEquivOfMapZerodefMathlib.Analysis.Normed.Affine.MazurUlam, function or constantWording
the real linear isometry equivalence of f and h0 (from the name)
English
Let $f$ be an isometry equivalence of $E$ and $F$ such that $\EqtMACRoH {f (0)}{0}$. Then the real linear isometry equivalence of $f$ and $h_{0}$ is a linear isometry equivalence of $E$ and $F$.
Affine.Simplex.EquilateraldefMathlib.Analysis.Normed.Affine.Simplex, predicateEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{Equilateral}$ holds for $s$, if there exists a real number $r$, such that for all elements $i$ and $j$ of $\mathrm{Fin}$ applied to $n + 1$, if $i \neq j$, then the distance of the point of $s$ and $i$ and the point of $s$ and $j$ is equal to $r$.
Affine.Simplex.RegulardefMathlib.Analysis.Normed.Affine.Simplex, predicateWording
s is regular (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then $s$ is regular, if for all permutations $x_{5}$ of $\mathrm{Fin}$ applied to $n + 1$, there exists an isometry equivalence $x_{6}$ of $P$ and $P$, such that $\operatorname{comp}$ applied to $\operatorname{points}$ applied to $s$ and $\operatorname{coe}$ applied to $x_{5}$ is equal to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $x_{6}$ and $\operatorname{points}$ applied to $s$.
Affine.Simplex.ScalenedefMathlib.Analysis.Normed.Affine.Simplex, predicateEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{Scalene}$ holds for $s$, if the function that maps $i$ to the distance of the point of $s$ and $\ProdfstMACRoZ {i}$ and the point of $s$ and $\ProdsndMACRoAA {i}$ is injective.
NormedSpace.expdefMathlib.Analysis.Normed.Algebra.Exponential, function or constantWording
the exponential map of x3 (from the docstring)
English
Let $x_{3}$ be an element of $x$. Then the exponential map of $x_{3}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{NormedSpace\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Normed\_\_Algebra\_\_Exponential\_\_267156490\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $x_{3}$.
NormedSpace.expSeriesdefMathlib.Analysis.Normed.Algebra.Exponential, function or constantWording
the exponential series of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the exponential series of $x$ and $x_{1}$ is a formal multilinear series of $x_{1}$ and $x_{1}$ defined as the function that maps $n$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (n !)}{\operatorname{mkPiAlgebraFin} (x , n , x_{1})}$.
NormedRing.algEquivComplexOfCompletedefMathlib.Analysis.Normed.Algebra.GelfandFormula, function or constantWording
the algebra isomorphism complex of hA (from the name)
English
Assume that for all elements $a$ of $A$, $a$ is a unit, if and only if $a \neq 0$. Then the algebra isomorphism complex of $\mathrm{hA}$ is an algebra isomorphism of the set of complexes and $A$.
NormedAlgebra.Complex.algEquivOfNormMuldefMathlib.Analysis.Normed.Algebra.GelfandMazur, function or constantWording
the algebra isomorphism of F (from the name)
English
Let $F$ be a set. Then the algebra isomorphism of $F$ is an algebra isomorphism of the set of complexes and $F$.
gelfandRadiusdefMathlib.Analysis.Normed.Algebra.GelfandRadius, function or constantWording
the Gelfand radius of a (from the name)
English
Let $a$ be an element of $A$. Then the Gelfand radius of $a$ is a real number defined as $\operatorname{limUnder}$ applied to $\operatorname{atTop}$ and the function that maps $k$ to the exponentiation of the norm of the exponentiation of $a$ to the value of $k$ to $\operatorname{inv}$ applied to the value of $k$.
NormedSpace.logdefMathlib.Analysis.Normed.Algebra.Logarithm, function or constantWording
the logarithm of x3 (from the docstring)
English
Let $x_{3}$ be an element of $x$. Then the logarithm of $x_{3}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{NormedSpace\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Analysis\_\_Normed\_\_Algebra\_\_Logarithm\_\_4281575742\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $x_{3}$.
NormedSpace.logSeriesdefMathlib.Analysis.Normed.Algebra.Logarithm, function or constantWording
the logarithm series of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the logarithm series of $x$ and $x_{1}$ is a formal multilinear series of $x_{1}$ and $x_{1}$ defined as the function that maps $n$ to $\HSMulhSMulMACRoAL {(\frac{ \operatorname{neg} (1)^ {(n + 1)}}{n})}{\operatorname{mkPiAlgebraFin} (x , n , x_{1})}$.
AlgHom.toContinuousLinearMapdefMathlib.Analysis.Normed.Algebra.Spectrum, function or constantWording
the continuous linear map of x4 (from the name)
English
Let $x_{4}$ be an algebra homomorphism of $A$ and $x$. Then the continuous linear map of $x_{4}$ is a strong dual of $x$ and $A$.
WeakDual.CharacterSpace.equivAlgHomdefMathlib.Analysis.Normed.Algebra.Spectrum, function or constantWording
the equivalence algebra homomorphism (from the name)
English
The equivalence algebra homomorphism is an equivalence from the set of elements of the character space of $x$ and $A$ to the set of algebra homomorphisms of $A$ and $x$.
spectralRadiusdefMathlib.Analysis.Normed.Algebra.Spectrum, function or constantWording
the spectral radius of x and a (from the name)
English
Let $x$ be a set. Let $a$ be an element of $A$. Then the spectral radius of $x$ and $a$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $k$ to the supremum of the function that maps $h$ to $\operatorname{ofNNReal}$ applied to the norm of $k$.
Unitization.splitMuldefMathlib.Analysis.Normed.Algebra.Unitization, function or constantWording
the split product of x and A (from the name)
English
Let $x$ and $A$ be sets. Then the split product of $x$ and $A$ is an algebra homomorphism of the set of unitizations of $x$ and $A$ and $\mathrm{Prod}$ applied to $x$ and the set of continuous linear maps of $A$ and $A$ defined as the product of $\operatorname{lift}$ applied to $0$ and $\operatorname{lift}$ applied to $\operatorname{Lmul}$ applied to $x$ and $A$.
WithLp.unitizationAlgEquivdefMathlib.Analysis.Normed.Algebra.UnitizationL1, function or constantWording
the unitization algebra isomorphism of R (from the name)
English
Let $R$ be a set. Then the unitization algebra isomorphism of $R$ is an algebra isomorphism of $\mathrm{WithLp}$ applied to $1$ and the set of unitizations of $x$ and $A$ and the set of unitizations of $x$ and $A$.
WithLp.unitization_addEquiv_proddefMathlib.Analysis.Normed.Algebra.UnitizationL1, function or constantWording
the unitization additive equivalence product of x and A (from the name)
English
Let $x$ and $A$ be sets. Then the unitization additive equivalence product of $x$ and $A$ is an additive equivalence of $\mathrm{WithLp}$ applied to $1$ and the set of unitizations of $x$ and $A$ and $\mathrm{WithLp}$ applied to $1$ and $\mathrm{Prod}$ applied to $x$ and $A$ defined as the composition of the additive equivalence of the linear equivalence of $1$ and the composition of the additive equivalence of $x$ and $A$ and the additive equivalence of the inverse of the linear equivalence of $1$.
DenselyNormedFieldclassMathlib.Analysis.Normed.Field.Basic, predicateWording
x is a densely normed field (from the name)
English
generation took over the time limit
NontriviallyNormedFieldclassMathlib.Analysis.Normed.Field.Basic, predicateWording
x is a nontrivially normed field (from the name)
English
generation took over the time limit
NormedDivisionRingclassMathlib.Analysis.Normed.Field.Basic, predicateWording
x is a normed division ring (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a normed division ring.
NormedFieldclassMathlib.Analysis.Normed.Field.Basic, predicateWording
x is a normed field (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a normed field.
IsKrasnerclassMathlib.Analysis.Normed.Field.Krasner, predicateEnglish
Let $K$ and $L$ be sets. Then we can say that $\mathrm{IsKrasner}$ holds for $K$ and $L$.
DilationEquiv.mulLeftdefMathlib.Analysis.Normed.Field.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 equivalence of $x$ and $x$.
DilationEquiv.mulRightdefMathlib.Analysis.Normed.Field.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 equivalence of $x$ and $x$.
Submonoid.unitClosedBalldefMathlib.Analysis.Normed.Field.UnitBall, function or constantWording
the unit closed ball of x (from the name)
English
Let $x$ be a set. Then the unit closed ball of $x$ is a submonoid of $x$.
Submonoid.unitSpheredefMathlib.Analysis.Normed.Field.UnitBall, function or constantWording
the unit sphere of x (from the name)
English
Let $x$ be a set. Then the unit sphere of $x$ is a submonoid of $x$.
Subsemigroup.unitBalldefMathlib.Analysis.Normed.Field.UnitBall, function or constantWording
the unit ball of x (from the name)
English
Let $x$ be a set. Then the unit ball of $x$ is a subsemigroup of $x$.
Subsemigroup.unitClosedBalldefMathlib.Analysis.Normed.Field.UnitBall, function or constantWording
the unit closed ball of x (from the name)
English
Let $x$ be a set. Then the unit closed ball of $x$ is a subsemigroup of $x$.
unitSphereToUnitsdefMathlib.Analysis.Normed.Field.UnitBall, function or constantWording
the unit sphere to unit of x (from the name)
English
Let $x$ be a set. Then the unit sphere to unit of $x$ is a monoid homomorphism of the set of elements of the sphere of $0$ and $1$ and $\UnitsMACRoAO {x}$.
AbsoluteValue.CompletiondefMathlib.Analysis.Normed.Field.WithAbs, typeWording
completion of v (from the name)
English
Let $v$ be an absolute value of $K$ and $\Real$. Then a completion of $v$ is an element of the function that maps $v$ to the set of completions of $\mathrm{WithAbs}$ applied to $v$.
IsometryEquiv.constVSubdefMathlib.Analysis.Normed.Group.AddTorsor, function or constantWording
the constant difference of x3 (from the name)
English
Let $x_{3}$ be an element of $P$. Then the constant difference of $x_{3}$ is an isometry equivalence of $P$ and $V$.
IsometryEquiv.vaddConstdefMathlib.Analysis.Normed.Group.AddTorsor, function or constantWording
the vector sum constant of x3 (from the name)
English
Let $x_{3}$ be an element of $P$. Then the vector sum constant of $x_{3}$ is an isometry equivalence of $V$ and $P$.
NormedAddTorsorclassMathlib.Analysis.Normed.Group.AddTorsor, predicateWording
V is a normed additive torsor (from the name)
English
Let $V$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $P$ be a set. Then we can say that $V$ is a normed additive torsor.
normAddGroupNormdefMathlib.Analysis.Normed.Group.Basic, function or constantWording
the norm of E (from the docstring)
English
Let $E$ be a set. Then the norm of $E$ is an additive group norm of $E$.
normAddGroupSeminormdefMathlib.Analysis.Normed.Group.Basic, function or constantWording
the norm of E (from the docstring)
English
Let $E$ be a set. Then the norm of $E$ is an additive group seminorm of $E$ defined as $\operatorname{mk}$ applied to $\operatorname{norm}$, $\mathrm{norm\_zero}$, $\mathrm{norm\_add\_le}$ and $\mathrm{norm\_neg}$.
normGroupNormdefMathlib.Analysis.Normed.Group.Basic, function or constantWording
the norm of E (from the docstring)
English
Let $E$ be a set. Then the norm of $E$ is a group norm of $E$.
normGroupSeminormdefMathlib.Analysis.Normed.Group.Basic, function or constantWording
the norm of E (from the docstring)
English
Let $E$ be a set. Then the norm of $E$ is a group seminorm of $E$ defined as $\operatorname{mk}$ applied to $\operatorname{norm}$, $\mathrm{norm\_one'}$, $\mathrm{norm\_mul\_le'}$ and $\mathrm{norm\_inv'}$.
ContinuousENormclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a continuous norm (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a continuous norm.
ENorm.enormdefMathlib.Analysis.Normed.Group.Defs, function or constantWording
the extended norm of x (from the name)
English
Let $x$ be an element of $E$. Then the extended norm of $x$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.
ENormedAddCommMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed additive commutative monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed additive commutative monoid.
ENormedAddMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed additive monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed additive monoid.
ENormedCommMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed commutative monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed commutative monoid.
ENormedMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed monoid.
ESeminormedAddCommMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed additive commutative monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed additive commutative monoid.
ESeminormedAddMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed additive monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed additive monoid.
ESeminormedCommMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed commutative monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed commutative monoid.
ESeminormedMonoidclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed monoid (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed monoid.
NNNorm.nnnormdefMathlib.Analysis.Normed.Group.Defs, function or constantWording
the norm of x (from the name)
English
Let $x$ be an element of $E$. Then the norm of $x$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.
Norm.normdefMathlib.Analysis.Normed.Group.Defs, function or constantWording
the norm of x (from the name)
English
Let $x$ be an element of $E$. Then the norm of $x$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.
NormedAddCommGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed additive commutative group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed additive commutative group.
NormedAddGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed additive group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed additive group.
NormedCommGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed commutative group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed commutative group.
NormedGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a normed group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a normed group.
SeminormedAddCommGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed additive commutative group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed additive commutative group.
SeminormedAddGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed additive group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed additive group.
SeminormedCommGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed commutative group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed commutative group.
SeminormedGroupclassMathlib.Analysis.Normed.Group.Defs, predicateWording
E is a seminormed group (from the name)
English
Let $E$ be a set. Then we can say that $E$ is a seminormed group.
AddMonoidHom.mkNormedAddGroupHomdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the normed additive group homomorphism of f and C (from the name)
English
Let $f$ be an additive monoid homomorphism of $V$ and $W$. Let $C$ be a real number such that for all elements $v$ of $V$, the norm of $f$ applied to $v$ is less than or equal to the product of $C$ and the norm of $v$. Then the normed additive group homomorphism of $f$ and $C$ is a normed additive group homomorphism of $V$ and $W$.
AddMonoidHom.mkNormedAddGroupHom'defMathlib.Analysis.Normed.Group.Hom, function or constantWording
the normed additive group homomorphism of f and C (from the name)
English
Let $f$ be an additive monoid homomorphism of $V$ and $W$. Let $C$ be an element of $\mathrm{NNReal}$ such that for all elements $x_{2}$ of $V$, the norm of $f$ applied to $x_{2}$ is less than or equal to the product of $C$ and the norm of $x_{2}$. Then the normed additive group homomorphism of $f$ and $C$ is a normed additive group homomorphism of $V$ and $W$.
NormedAddGroupHomstructureMathlib.Analysis.Normed.Group.Hom, typeWording
normed additive group homomorphism of V and W (from the name)
English
Let $V$ and $W$ be sets. Then the normed additive group homomorphisms of $V$ and $W$ are a basic type.
NormedAddGroupHom.Equalizer.liftdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the lift of x4 and h (from the name)
English
Let $x_{4}$ be a normed additive group homomorphism of $x$ and $V$ such that $\EqtMACRoH {\operatorname{comp} (f , x_{4})}{\operatorname{comp} (g , x_{4})}$. Then the lift of $x_{4}$ and $h$ is a normed additive group homomorphism of $x$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{5}})}$.
NormedAddGroupHom.Equalizer.liftEquivdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the lifting property of the equalizer (from the docstring)
English
The lifting property of the equalizer is an element of $\EquivMACRoAE {(\SubtypeSet {x_{4}}{(\EqtMACRoH {\operatorname{comp} (f , x_{4})}{\operatorname{comp} (g , x_{4})})})}{\mathrm{NormedAddGroupHom} (x , \SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{5}})})}$.
NormedAddGroupHom.Equalizer.mapdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the map of x12 and x13 (from the name)
English
Let $x_{12}$ be a normed additive group homomorphism of $x$ and $x_{1}$. Let $x_{13}$ be a normed additive group homomorphism of $x_{4}$ and $x_{5}$ such that $\EqtMACRoH {\operatorname{comp} (x_{13} , x_{8})}{\operatorname{comp} (x_{10} , x_{12})}$ and $\EqtMACRoH {\operatorname{comp} (x_{13} , x_{9})}{\operatorname{comp} (x_{11} , x_{12})}$. Then the map of $x_{12}$ and $x_{13}$ is a normed additive group homomorphism of $\SubtypeSet {x_{14}}{(\MembershipmemMACRoT {\operatorname{equalizer} (x_{8} , x_{9})}{x_{14}})}$ and $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {\operatorname{equalizer} (x_{10} , x_{11})}{x_{15}})}$.
NormedAddGroupHom.Equalizer.ιdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the inclusion of f and g (from the name)
English
Let $f$ and $g$ be normed additive group homomorphisms of $V$ and $W$. Then the inclusion of $f$ and $g$ is a normed additive group homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{equalizer} (f , g)}{x_{2}})}$ and $V$ defined as the inclusion of the equalizer of $f$ and $g$.
NormedAddGroupHom.NormNonincdefMathlib.Analysis.Normed.Group.Hom, predicateEnglish
Let $f$ be a normed additive group homomorphism of $V$ and $W$. Then $\operatorname{NormNoninc}$ holds for $f$, if for all elements $v$ of $V$, the norm of $f$ applied to $v$ is less than or equal to the norm of $v$.
NormedAddGroupHom.SurjectiveOnWithdefMathlib.Analysis.Normed.Group.Hom, predicateEnglish
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Let $K$ be an additive subgroup of $x_{1}$. Let $C$ be a real number. Then $\operatorname{SurjectiveOnWith}$ holds for $f$, $K$ and $C$, if for all elements $h$ of $x_{1}$, if $h$ is an element of $K$, then there exists an element $g$ of $x$, such that $\EqtMACRoH {f (g)}{h}$ and the norm of $g$ is less than or equal to the product of $C$ and the norm of $h$.
NormedAddGroupHom.coeAddHomdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the coercion additive homomorphism (from the name)
English
The coercion additive homomorphism is an additive monoid homomorphism of the set of normed additive group homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{NormedAddGroupHom\_\_coe\_zero}$ and $\mathrm{NormedAddGroupHom\_\_coe\_add}$.
NormedAddGroupHom.compdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a normed additive group homomorphism of $x_{1}$ and $x_{2}$. Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a normed additive group homomorphism of $x$ and $x_{2}$.
NormedAddGroupHom.compHomdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the composition homomorphism (from the name)
English
The composition homomorphism is an additive monoid homomorphism of the set of normed additive group homomorphisms of $x_{1}$ and $x_{2}$ and the set of additive monoid homomorphisms of the set of normed additive group homomorphisms of $x$ and $x_{1}$ and the set of normed additive group homomorphisms of $x$ and $x_{2}$.
NormedAddGroupHom.equalizerdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the equalizer of f and g (from the name)
English
Let $f$ and $g$ be normed additive group homomorphisms of $V$ and $W$. Then the equalizer of $f$ and $g$ is an additive subgroup of $V$ defined as the kernel of $f - g$.
NormedAddGroupHom.iddefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the identity of V (from the docstring)
English
Let $V$ be a set. Then the identity of $V$ is a normed additive group homomorphism of $V$ and $V$.
NormedAddGroupHom.incldefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the inclusion of s (from the docstring)
English
Let $s$ be an additive subgroup of $V$. Then the inclusion of $s$ is a normed additive group homomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $V$.
NormedAddGroupHom.kerdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the kernel of f (from the docstring)
English
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Then the kernel of $f$ is an additive subgroup of $x$ defined as the additive kernel of the additive monoid homomorphism of $f$.
NormedAddGroupHom.ker.liftdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the lift of f and g (from the name)
English
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Let $g$ be a normed additive group homomorphism of $x_{1}$ and $x_{2}$ such that $\EqtMACRoH {\operatorname{comp} (g , f)}{0}$. Then the lift of $f$ and $g$ is a normed additive group homomorphism of $x$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{ker} (g)}{x_{6}})}$.
NormedAddGroupHom.ofLipschitzdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the normed additive group homomorphism of f and h (from the name)
English
Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$ such that $\mathrm{LipschitzWith}$ holds for $K$ and $\operatorname{coe}$ applied to $f$. Then the normed additive group homomorphism of $f$ and $h$ is a normed additive group homomorphism of $x$ and $x_{1}$.
NormedAddGroupHom.opNormdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the operator norm of f (from the docstring)
English
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. 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_{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}$.
NormedAddGroupHom.rangedefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the range of f (from the name)
English
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Then the range of $f$ is an additive subgroup of $x_{1}$ defined as the range of the additive monoid homomorphism of $f$.
NormedAddGroupHom.toAddMonoidHomdefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the additive monoid homomorphism of f (from the name)
English
Let $f$ be a normed additive group homomorphism of $x$ and $x_{1}$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk'}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{NormedAddGroupHom\_\_map\_add'}$ applied to $f$.
NormedAddGroupHom.toFundefMathlib.Analysis.Normed.Group.Hom, function or constantWording
the normed additive group homomorphism of self and x2 (from the name)
English
Let $\mathrm{self}$ be a normed additive group homomorphism of $V$ and $W$. Let $x_{2}$ be an element of $V$. Then the normed additive group homomorphism of $\mathrm{self}$ and $x_{2}$ is an element of $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
NormedAddCommGroup.toCompldefMathlib.Analysis.Normed.Group.HomCompletion, function or constantWording
the complement (from the name)
English
The complement is a normed additive group homomorphism of $G$ and the set of completions of $G$.
NormedAddGroupHom.completiondefMathlib.Analysis.Normed.Group.HomCompletion, function or constantWording
the completion of f (from the name)
English
Let $f$ be a normed additive group homomorphism of $G$ and $H$. Then the completion of $f$ is a normed additive group homomorphism of the set of completions of $G$ and the set of completions of $H$.
NormedAddGroupHom.extensiondefMathlib.Analysis.Normed.Group.HomCompletion, function or constantWording
the extension of f (from the name)
English
Let $f$ be a normed additive group homomorphism of $G$ and $H$. Then the extension of $f$ is a normed additive group homomorphism of the set of completions of $G$ and $H$.
normedAddGroupHomCompletionHomdefMathlib.Analysis.Normed.Group.HomCompletion, function or constantWording
the normed additive group homomorphism completion homomorphism (from the name)
English
The normed additive group homomorphism completion homomorphism is an additive monoid homomorphism of the set of normed additive group homomorphisms of $G$ and $H$ and the set of normed additive group homomorphisms of the set of completions of $G$ and the set of completions of $H$.
nullAddSubgroupdefMathlib.Analysis.Normed.Group.NullSubmodule, function or constantWording
the additive null subgroup with respect to the norm of M (from the docstring)
English
Let $M$ be a set. Then the additive null subgroup with respect to the norm of $M$ is an additive subgroup of $M$.
nullSubgroupdefMathlib.Analysis.Normed.Group.NullSubmodule, function or constantWording
the null subgroup with respect to the norm of M (from the docstring)
English
Let $M$ be a set. Then the null subgroup with respect to the norm of $M$ is a subgroup of $M$.
nullSubmoduledefMathlib.Analysis.Normed.Group.NullSubmodule, function or constantWording
the null space with respect to the norm of x and E (from the docstring)
English
Let $x$ and $E$ be sets. Then the null space with respect to the norm of $x$ and $E$ is a submodule of $x$ and $E$.
AddSubgroup.normedMkdefMathlib.Analysis.Normed.Group.Quotient, function or constantEnglish
Let $S$ be an additive subgroup of $M$. Then $\operatorname{normedMk}$ applied to $S$ is a normed additive group homomorphism of $M$ and the set of quotients of $M$ and $S$.
AddSubgroup.quotientIsometryEquivOfEqdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient isometry equivalence of h (from the name)
English
Assume that $\EqtMACRoH {S}{T}$. Then the quotient isometry equivalence of $h$ is an isometry equivalence of the set of quotients of $M$ and $S$ and the set of quotients of $M$ and $T$.
NormedAddGroupHom.IsQuotientstructureMathlib.Analysis.Normed.Group.Quotient, predicateWording
f is a quotient (from the name)
English
Let $f$ be a normed additive group homomorphism of $M$ and $N$. Then we can say that $f$ is a quotient.
NormedAddGroupHom.liftdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the lift of S and f (from the name)
English
Let $S$ be an additive subgroup of $M$. Let $f$ be a normed additive group homomorphism of $M$ and $N$ such that for all elements $s$ of $M$, if $s$ is an element of $S$, then $\EqtMACRoH {f (s)}{0}$. Then the lift of $S$ and $f$ is a normed additive group homomorphism of the set of quotients of $M$ and $S$ and $N$.
QuotientAddGroup.addGroupSeminormdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the additive group seminorm (from the name)
English
The additive group seminorm is an additive group seminorm of the set of quotients of $M$ and $S$.
QuotientAddGroup.quotientBotIsometryEquivdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient bottom isometry equivalence (from the name)
English
The quotient bottom isometry equivalence is an isometry equivalence of the set of quotients of $M$ and the bottom and $M$.
QuotientAddGroup.quotientQuotientIsometryEquivQuotientdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient quotient isometry equivalence quotient of h (from the name)
English
Assume that $S \leq T$. Then the quotient quotient isometry equivalence quotient of $h$ is an isometry equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mk'}$ applied to $S$ and $T$ and the set of quotients of $M$ and $T$.
QuotientGroup.groupSeminormdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the group seminorm (from the name)
English
The group seminorm is a group seminorm of the set of quotients of $M$ and $S$.
QuotientGroup.quotientBotIsometryEquivdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient bottom isometry equivalence (from the name)
English
The quotient bottom isometry equivalence is an isometry equivalence of the set of quotients of $M$ and the bottom and $M$.
QuotientGroup.quotientQuotientIsometryEquivQuotientdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient quotient isometry equivalence quotient of h (from the name)
English
Assume that $S \leq T$. Then the quotient quotient isometry equivalence quotient of $h$ is an isometry equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mk'}$ applied to $S$ and $T$ and the set of quotients of $M$ and $T$.
Subgroup.quotientIsometryEquivOfEqdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient isometry equivalence of h (from the name)
English
Assume that $\EqtMACRoH {S}{T}$. Then the quotient isometry equivalence of $h$ is an isometry equivalence of the set of quotients of $M$ and $S$ and the set of quotients of $M$ and $T$.
Submodule.quotLIEOfEqdefMathlib.Analysis.Normed.Group.Quotient, function or constantEnglish
Let $S$ and $T$ be submodules of $R$ and $M$ such that $\EqtMACRoH {S}{T}$. Then $\operatorname{quotLIEOfEq}$ applied to $S$, $T$ and $h$ is a linear isometry equivalence of the set of quotients of $M$ and $S$ and the set of quotients of $M$ and $T$.
Submodule.quotientQuotientLIEQuotientdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient quotient Lie quotient of S and T (from the name)
English
Let $S$ and $T$ be submodules of $R$ and $M$ such that $S \leq T$. Then the quotient quotient Lie quotient of $S$ and $T$ is a linear isometry equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mkQ}$ applied to $S$ and $T$ and the set of quotients of $M$ and $T$.
Submodule.quotientQuotientLIEQuotientSupdefMathlib.Analysis.Normed.Group.Quotient, function or constantWording
the quotient quotient Lie quotient supremum of S and T (from the name)
English
Let $S$ and $T$ be submodules of $R$ and $M$. Then the quotient quotient Lie quotient supremum of $S$ and $T$ is a linear isometry equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mkQ}$ applied to $S$ and $T$ and the set of quotients of $M$ and $\MaxmaxMACRoAF {S}{T}$.
Function.IsRadialdefMathlib.Analysis.Normed.Group.RadialFunction, predicateWording
f is radial (from the docstring)
English
Let $f$ be a function from elements of $E$ to elements of $F$. Then $f$ is radial, if $\operatorname{FactorsThrough}$ holds for $f$ and the function that maps $x_{1}$ to the norm of $x_{1}$.
Function.radialPartdefMathlib.Analysis.Normed.Group.RadialFunction, function or constantWording
the radial part of f and x1 (from the docstring)
English
Let $f$ be a function from elements of $E$ to elements of $F$. Let $x_{1}$ be a real number. Then the radial part of $f$ and $x_{1}$ is an element of $F$ defined as $\operatorname{extend}$ applied to the function that maps $x_{1}$ to the norm of $x_{1}$, $f$, the function that maps $x_{2}$ to $\operatorname{choice}$ applied to $\mathrm{hF}$ and $x_{1}$.
SemiNormedGrpstructureMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
semi normed group (from the name)
English
The semi normed groups are a basic type.
SemiNormedGrp.HomstructureMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be semi normed groups. Then the homomorphisms of $M$ and $N$ are a basic type.
SemiNormedGrp.Hom.homdefMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the homomorphism of $f$ is a normed additive group homomorphism of the set of carriers of $M$ and the set of carriers of $N$ defined as the homomorphism of $f$.
SemiNormedGrp.Hom.hom'defMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $M$ and $N$. Then the homomorphism of $\mathrm{self}$ is a normed additive group homomorphism of the set of carriers of $M$ and the set of carriers of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
SemiNormedGrp.carrierdefMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a semi normed group. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
SemiNormedGrp.ofHomdefMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the semi normed group of f (from the name)
English
Let $f$ be a normed additive group homomorphism of $M$ and $N$. Then the semi normed group of $f$ is a homomorphism of $\operatorname{of}$ applied to $M$ and $\operatorname{of}$ applied to $N$ defined as the concrete category of $f$.
SemiNormedGrp₁structureMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
semi normed group (from the name)
English
The semi normed groups are a basic type.
SemiNormedGrp₁.HomstructureMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be semi normed groups. Then the homomorphisms of $M$ and $N$ are a basic type.
SemiNormedGrp₁.Hom.homdefMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the homomorphism of $f$ is an element of $\SubtypeSet {f_{1}}{\operatorname{NormNoninc} (f_{1})}$ defined as the homomorphism of $f$.
SemiNormedGrp₁.Hom.hom'defMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $M$ and $N$. Then the homomorphism of $\mathrm{self}$ is a normed additive group homomorphism of the set of carriers of $M$ and the set of carriers of $N$ defined as $\mathrm{SemiNormedGrp\_u2081\_\_\_Hom\_\_proj0}$ applied to $\mathrm{self}$.
SemiNormedGrp₁.carrierdefMathlib.Analysis.Normed.Group.SemiNormedGrp, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a semi normed group. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\mathrm{SemiNormedGrp\_u2081\_\_\_proj0}$ applied to $\mathrm{self}$.
SemiNormedGrp₁.mkHomdefMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the homomorphism of f and i (from the name)
English
Let $f$ be a normed additive group homomorphism of $M$ and $N$ such that $\operatorname{NormNoninc}$ holds for $f$. Then the homomorphism of $f$ and $i$ is a homomorphism of $\mathrm{SemiNormedGrp\_u2081\_\_\_of}$ applied to $M$ and $\mathrm{SemiNormedGrp\_u2081\_\_\_of}$ applied to $N$ defined as the concrete category of $f$.
SemiNormedGrp₁.mkIsodefMathlib.Analysis.Normed.Group.SemiNormedGrp, function or constantWording
the isomorphism of f (from the name)
English
Let $f$ be an isomorphism of $M$ and $N$ such that $\operatorname{NormNoninc}$ holds for the homomorphism of the homomorphism of $f$ and $\operatorname{NormNoninc}$ holds for the homomorphism of the inverse of $f$. Then the isomorphism of $f$ is an isomorphism of $\mathrm{SemiNormedGrp\_u2081\_\_\_of}$ applied to the set of carriers of $M$ and $\mathrm{SemiNormedGrp\_u2081\_\_\_of}$ applied to the set of carriers of $N$.
SemiNormedGrp.completiondefMathlib.Analysis.Normed.Group.SemiNormedGrp.Completion, function or constantWording
the completion (from the docstring)
English
The completion is a functor of the set of semi normed groups and the set of semi normed groups.
SemiNormedGrp.completion.incldefMathlib.Analysis.Normed.Group.SemiNormedGrp.Completion, function or constantWording
the inclusion (from the name)
English
The inclusion is a homomorphism of $V$ and the action of the completion and $V$.
SemiNormedGrp.completion.liftdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Completion, function or constantWording
the lift of f (from the name)
English
Let $f$ be a homomorphism of $V$ and $W$. Then the lift of $f$ is a homomorphism of the action of the completion and $V$ and $W$.
SemiNormedGrp.completion.mapHomdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Completion, function or constantWording
the map homomorphism of V and W (from the name)
English
Let $V$ and $W$ be semi normed groups. Then the map homomorphism of $V$ and $W$ is an additive monoid homomorphism of the set of homomorphisms of $V$ and $W$ and the set of homomorphisms of the action of the completion and $V$ and the action of the completion and $W$.
SemiNormedGrp.explicitCokerneldefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantWording
the explicit cokernel of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the explicit cokernel of $f$ is a semi normed group defined as $\operatorname{pt}$ applied to $\operatorname{cokernelCocone}$ applied to $f$.
SemiNormedGrp.explicitCokernel.mapdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantWording
the map of h (from the name)
English
Assume that the composition of $\mathrm{fab}$ and $\mathrm{fbd}$ is equal to the composition of $\mathrm{fac}$ and $\mathrm{fcd}$. Then the map of $h$ is a homomorphism of the explicit cokernel of $\mathrm{fab}$ and the explicit cokernel of $\mathrm{fcd}$.
SemiNormedGrp.explicitCokernelDescdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantEnglish
Assume that the composition of $f$ and $g$ is equal to $0$. Then $\operatorname{explicitCokernelDesc}$ applied to $w$ is a homomorphism of the explicit cokernel of $f$ and $Z$.
SemiNormedGrp.explicitCokernelIsodefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantWording
the explicit cokernel of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the explicit cokernel of $f$ is an isomorphism of the explicit cokernel of $f$ and the cokernel of $f$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimitCokernelCocone}$ applied to $f$ and $\operatorname{isColimit}$ applied to the parallel pair of $f$ and $0$.
SemiNormedGrp.explicitCokernelπdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantWording
the explicit cokernel projection of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the explicit cokernel projection of $f$ is a homomorphism of $Y$ and the explicit cokernel of $f$ defined as the component of the inclusion of $\operatorname{cokernelCocone}$ applied to $f$ and the one.
SemiNormedGrp.forkdefMathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels, function or constantWording
the fork of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $V$ and $W$. Then the fork of $f$ and $g$ is a fork of $f$ and $g$.
AddGroupNormstructureMathlib.Analysis.Normed.Group.Seminorm, typeWording
additive group norm of G (from the name)
English
Let $G$ be a set. Then the additive group norms of $G$ are a basic type.
AddGroupSeminormstructureMathlib.Analysis.Normed.Group.Seminorm, typeWording
additive group seminorm of G (from the name)
English
Let $G$ be a set. Then the additive group seminorms of $G$ are a basic type.
AddGroupSeminorm.compdefMathlib.Analysis.Normed.Group.Seminorm, function or constantWording
the composition of p and f (from the name)
English
Let $p$ be an additive group seminorm of $E$. Let $f$ be an additive monoid homomorphism of $F$ and $E$. Then the composition of $p$ and $f$ is an additive group seminorm of $F$.
AddGroupSeminorm.toFundefMathlib.Analysis.Normed.Group.Seminorm, function or constantWording
the additive group seminorm of self and x1 (from the name)
English
Let $\mathrm{self}$ be an additive group seminorm of $G$. Let $x_{1}$ be an element of $G$. Then the additive group seminorm of $\mathrm{self}$ and $x_{1}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
GroupNormstructureMathlib.Analysis.Normed.Group.Seminorm, typeWording
group norm of G (from the name)
English
Let $G$ be a set. Then the group norms of $G$ are a basic type.
GroupSeminormstructureMathlib.Analysis.Normed.Group.Seminorm, typeWording
group seminorm of G (from the name)
English
Let $G$ be a set. Then the group seminorms of $G$ are a basic type.
GroupSeminorm.compdefMathlib.Analysis.Normed.Group.Seminorm, function or constantWording
the composition of p and f (from the name)
English
Let $p$ be a group seminorm of $E$. Let $f$ be a monoid homomorphism of $F$ and $E$. Then the composition of $p$ and $f$ is a group seminorm of $F$.
GroupSeminorm.toFundefMathlib.Analysis.Normed.Group.Seminorm, function or constantWording
the group seminorm of self and x1 (from the name)
English
Let $\mathrm{self}$ be a group seminorm of $G$. Let $x_{1}$ be an element of $G$. Then the group seminorm of $\mathrm{self}$ and $x_{1}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
NonarchAddGroupNormstructureMathlib.Analysis.Normed.Group.Seminorm, typeEnglish
Let $G$ be a set. Then the elements of $\mathrm{NonarchAddGroupNorm}$ applied to $G$ are a basic type.
NonarchAddGroupNormClassclassMathlib.Analysis.Normed.Group.Seminorm, predicateEnglish
Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonarchAddGroupNormClass}$ holds for $F$ and $x$.
NonarchAddGroupSeminormstructureMathlib.Analysis.Normed.Group.Seminorm, typeEnglish
Let $G$ be a set. Then the elements of $\mathrm{NonarchAddGroupSeminorm}$ applied to $G$ are a basic type.
NonarchAddGroupSeminormClassclassMathlib.Analysis.Normed.Group.Seminorm, predicateEnglish
Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{NonarchAddGroupSeminormClass}$ holds for $F$ and $x$.
SeparationQuotient.liftNormedAddGroupHomdefMathlib.Analysis.Normed.Group.SeparationQuotient, function or constantWording
the lift of f and hf (from the docstring)
English
Let $f$ be a normed additive group homomorphism of $M$ and $N$ such that for all elements $x_{2}$ of $M$, if the norm of $x_{2}$ is equal to $0$, then $\EqtMACRoH {f (x_{2})}{0}$. Then the lift of $f$ and $\mathrm{hf}$ is a normed additive group homomorphism of the set of separation quotients of $M$ and $N$.
SeparationQuotient.liftNormedAddGroupHomEquivdefMathlib.Analysis.Normed.Group.SeparationQuotient, function or constantWording
the lift normed additive group homomorphism equivalence (from the name)
English
The lift normed additive group homomorphism equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{forall} (M , \lambda x_{2} . \mathrm{if} (\mathrm{Eq} (\operatorname{norm} (x_{2}), 0), \EqtMACRoH {f (x_{2})}{0}))})}{\mathrm{NormedAddGroupHom} (\mathrm{SeparationQuotient} (M), N)}$.
SeparationQuotient.normedMkdefMathlib.Analysis.Normed.Group.SeparationQuotient, function or constantEnglish
$\operatorname{normedMk}$ is a normed additive group homomorphism of $M$ and the set of separation quotients of $M$.
IsUltrametricDist.ball_openAddSubgroupdefMathlib.Analysis.Normed.Group.Ultra, function or constantWording
the ball open additive subgroup of S and hr (from the name)
English
Let $S$ be a set. Assume that $0 < r$. Then the ball open additive subgroup of $S$ and $\mathrm{hr}$ is an open additive subgroup of $S$.
IsUltrametricDist.ball_openSubgroupdefMathlib.Analysis.Normed.Group.Ultra, function or constantWording
the ball open subgroup of S and hr (from the name)
English
Let $S$ be a set. Assume that $0 < r$. Then the ball open subgroup of $S$ and $\mathrm{hr}$ is an open subgroup of $S$.
IsUltrametricDist.closedBall_openAddSubgroupdefMathlib.Analysis.Normed.Group.Ultra, function or constantWording
the closed ball open additive subgroup of S and hr (from the name)
English
Let $S$ be a set. Assume that $0 < r$. Then the closed ball open additive subgroup of $S$ and $\mathrm{hr}$ is an open additive subgroup of $S$.
IsUltrametricDist.closedBall_openSubgroupdefMathlib.Analysis.Normed.Group.Ultra, function or constantWording
the closed ball open subgroup of S and hr (from the name)
English
Let $S$ be a set. Assume that $0 < r$. Then the closed ball open subgroup of $S$ and $\mathrm{hr}$ is an open subgroup of $S$.