Definitions: Mathlib.Topology, part 2 of 8

ContinuousLinearMapstructureMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, type

Wording

continuous linear map of M and x5 (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $M$ and $x_{5}$ be sets. Then the continuous linear maps of $M$ and $x_{5}$ are a basic type.

ContinuousLinearMap.coeLMdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

no wording

English

Let $S$ be a set. Then $\operatorname{coeLM}$ applied to $S$ is a linear map of the set of continuous linear maps of $M$ and $x_{5}$ and the set of linear maps of $M$ and $x_{5}$.

ContinuousLinearMap.coeLMₛₗdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

no wording

English

Let $x_{13}$ be a ring homomorphism of $R$ and $x$. Then $\mathrm{ContinuousLinearMap\_\_coeLM\_u209b\_\_u2097\_}$ applied to $x_{13}$ is a linear map of the set of continuous linear maps of $M$ and $x_{8}$ and the set of linear maps of $M$ and $x_{8}$.

ContinuousLinearMap.compdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a continuous linear map of $x_{12}$ and $x_{15}$. Let $f$ be a continuous linear map of $x_{9}$ and $x_{12}$. Then the composition of $g$ and $f$ is a continuous linear map of $x_{9}$ and $x_{15}$.

ContinuousLinearMap.copydefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a continuous linear map of $x_{5}$ and $x_{8}$. Let $\mathrm{f'}$ be a function from elements of $x_{5}$ to elements of $x_{8}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a continuous linear map of $x_{5}$ and $x_{8}$.

ContinuousLinearMap.homeomorphOfUnitdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the homeomorphism of T (from the name)

English

Let $T$ be a unit of the set of continuous linear maps of $x_{2}$ and $x_{2}$. Then the homeomorphism of $T$ is a homeomorphism of $x_{2}$ and $x_{2}$.

ContinuousLinearMap.iddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the identity map of x and x2 (from the docstring)

English

Let $x$ and $x_{2}$ be sets. Then the identity map of $x$ and $x_{2}$ is a continuous linear map of $x_{2}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the identity and $\mathrm{continuous\_id}$.

ContinuousLinearMap.lcompdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

no wording

English

Let $W$ be a set. Let $f$ be a continuous linear map of $U$ and $V$. Then $\operatorname{lcomp}$ applied to $W$ and $f$ is a linear map of the set of continuous linear maps of $V$ and $W$ and the set of continuous linear maps of $U$ and $W$.

ContinuousLinearMap.llcompdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

no wording

English

Let $R$, $U$, $V$ and $W$ be sets. Then $\operatorname{llcomp}$ applied to $R$, $U$, $V$ and $W$ is a linear map of the set of continuous linear maps of $U$ and $V$ and the set of linear maps of the set of continuous linear maps of $V$ and $W$ and the set of continuous linear maps of $U$ and $W$.

ContinuousLinearMap.smulRightdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the right scalar multiple of c and f (from the name)

English

Let $c$ be a continuous linear map of $x$ and $S$. Let $f$ be an element of $x_{3}$. Then the right scalar multiple of $c$ and $f$ is a continuous linear map of $x$ and $x_{3}$.

ContinuousLinearMap.smulRightₗdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the right scalar multiple of c (from the name)

English

Let $c$ be a continuous linear map of $M$ and $S$. Then the right scalar multiple of $c$ is a linear map of $x$ and the set of continuous linear maps of $M$ and $x$.

ContinuousLinearMap.toLinearMapRingHomdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the linear map ring homomorphism (from the name)

English

The linear map ring homomorphism is a ring homomorphism of the set of continuous linear maps of $x_{2}$ and $x_{2}$ and the set of linear maps of $x_{2}$ and $x_{2}$.

ContinuousLinearMap.toSpanSingletondefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the span singleton of x and x7 (from the name)

English

Let $x$ be a set. Let $x_{7}$ be an element of $x_{2}$. Then the span singleton of $x$ and $x_{7}$ is a continuous linear map of $x$ and $x_{2}$.

ContinuousLinearMap.toSpanSingletonLEdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Then $\operatorname{toSpanSingletonLE}$ applied to $R$, $S$ and $M$ is a linear equivalence of $M$ and the set of continuous linear maps of $R$ and $M$.

ContinuousLinearMapClassdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$, $M$ and $x_{3}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{ContinuousLinearMapClass}$ holds for $F$, $R$, $M$ and $x_{3}$, if $\mathrm{ContinuousSemilinearMapClass}$ holds for $F$, the identity ring homomorphism of $R$, $M$ and $x_{3}$.

ContinuousSemilinearMapClassclassMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $S$. Let $M$ and $x_{5}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ContinuousSemilinearMapClass}$ holds for $F$, $x_{2}$, $M$ and $x_{5}$.

StrongDualdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, type

Wording

strong dual of R and M (from the name)

English

Let $R$ and $M$ be sets. Then a strong dual of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of continuous linear maps of $M$ and $R$.

topDualPairingdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic, function or constant

Wording

the canonical pairing of x and E (from the docstring)

English

Let $x$ and $E$ be sets. Then the canonical pairing of $x$ and $E$ is a linear map of the set of continuous linear maps of $E$ and $x$ and the set of linear maps of $E$ and $x$ defined as $\operatorname{coeLM}$ applied to $x$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Extend

ContinuousLinearMap.extenddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Extend, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $E$ and $F$. Let $e$ be a continuous linear map of $E$ and $x_{2}$. Then $\operatorname{extend}$ applied to $f$ and $e$ is a continuous linear map of $x_{2}$ and $F$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible

ContinuousLinearMap.IsInvertibledefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible, predicate

Wording

f is invertible (from the docstring)

English

Let $f$ be a continuous linear map of $M$ and $x$. Then $f$ is invertible, if there exists a continuous linear equivalence $A$ of $M$ and $x$, such that the continuous linear map of $A$ is equal to $f$.

ContinuousLinearMap.inversedefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible, function or constant

Wording

the inverse of x8 (from the name)

English

Let $x_{8}$ be a continuous linear map of $M$ and $x$. Then the inverse of $x_{8}$ is a continuous linear map of $x$ and $M$ defined as $\mathrm{dite}$ applied to the proposition that $x_{8}$ is invertible, the function that maps $h$ to the continuous linear map of the inverse of $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $0$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

ContinuousLinearMap.coproddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the coproduct of x12 and x13 (from the name)

English

Let $x_{12}$ be a continuous linear map of $x$ and $M$. Let $x_{13}$ be a continuous linear map of $x_{1}$ and $M$. Then the coproduct of $x_{12}$ and $x_{13}$ is a continuous linear map of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $M$.

ContinuousLinearMap.coprodEquivdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the coproduct equivalence (from the name)

English

The coproduct equivalence is a linear equivalence of $\mathrm{Prod}$ applied to the set of continuous linear maps of $x$ and $M$ and the set of continuous linear maps of $x_{1}$ and $M$ and the set of continuous linear maps of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $M$.

ContinuousLinearMap.fstdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the first component of x1 and x5 (from the name)

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then the first component of $x_{1}$ and $x_{5}$ is a continuous linear map of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $x_{1}$.

ContinuousLinearMap.inldefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the left injection of x1 and x5 (from the name)

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then the left injection of $x_{1}$ and $x_{5}$ is a continuous linear map of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ defined as the product of the identity map of $R$ and $x_{1}$ and $0$.

ContinuousLinearMap.inrdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the right injection of x1 and x5 (from the name)

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then the right injection of $x_{1}$ and $x_{5}$ is a continuous linear map of $x_{5}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ defined as the product of $0$ and the identity map of $R$ and $x_{5}$.

ContinuousLinearMap.pidefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{4}$ to continuous linear maps of $M$ and $x_{5}$ applied to $i_{1}$. Then the product of $i_{1}$ is a continuous linear map of $M$ and the set of functions from elements $i$ of $x_{4}$ to elements of $x_{5}$ applied to $i$.

ContinuousLinearMap.piMapdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product map of f (from the name)

English

Let $f$ be a function from elements $i_{2}$ of $x_{1}$ to continuous linear maps of $x_{2}$ applied to $i_{2}$ and $x_{6}$ applied to $i_{2}$. Then the product map of $i_{2}$ is a continuous linear map of the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $x_{6}$ applied to $i_{1}$ defined as the function that maps $f$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the projection of $i$.

ContinuousLinearMap.proddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product of x13 and x14 (from the name)

English

Let $x_{13}$ be a continuous linear map of $x_{1}$ and $x_{5}$. Let $x_{14}$ be a continuous linear map of $x_{1}$ and $x_{9}$. Then the product of $x_{13}$ and $x_{14}$ is a continuous linear map of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{9}$.

ContinuousLinearMap.prodEquivdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of continuous linear maps of $M$ and $x_{4}$ and the set of continuous linear maps of $M$ and $x_{8}$ to the set of continuous linear maps of $M$ and $\mathrm{Prod}$ applied to $x_{4}$ and $x_{8}$.

ContinuousLinearMap.prodMapdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product map of x17 and x18 (from the name)

English

Let $x_{17}$ be a continuous linear map of $x_{1}$ and $x_{5}$. Let $x_{18}$ be a continuous linear map of $x_{9}$ and $x_{13}$. Then the product map of $x_{17}$ and $x_{18}$ is a continuous linear map of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{9}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{13}$ defined as the product of the composition of $x_{17}$ and the first component of $x_{1}$ and $x_{9}$ and the composition of $x_{18}$ and the second component of $x_{1}$ and $x_{9}$.

ContinuousLinearMap.prodₗdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the product of S (from the name)

English

Let $S$ be a set. Then the product of $S$ is a linear equivalence of $\mathrm{Prod}$ applied to the set of continuous linear maps of $M$ and $x_{4}$ and the set of continuous linear maps of $M$ and $x_{8}$ and the set of continuous linear maps of $M$ and $\mathrm{Prod}$ applied to $x_{4}$ and $x_{8}$.

ContinuousLinearMap.projdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the projection of i (from the name)

English

Let $i$ be an element of $x_{1}$. Then the projection of $i$ is a continuous linear map of the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $i_{1}$ and $x_{2}$ applied to $i$.

ContinuousLinearMap.singledefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Let $i$ be an element of $x_{1}$. Then $\operatorname{single}$ applied to $R$, $x_{2}$ and $i$ is a continuous linear map of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $x_{2}$ applied to $i_{1}$.

ContinuousLinearMap.snddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the second component of x1 and x5 (from the name)

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then the second component of $x_{1}$ and $x_{5}$ is a continuous linear map of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $x_{5}$.

Pi.compRightLdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd, function or constant

Wording

the right composition of x2 and f (from the name)

English

Let $R$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements of $x_{6}$ to elements of $x_{1}$. Then the right composition of $x_{2}$ and $f$ is a continuous linear map of the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to elements of $x_{2}$ applied to $f$ applied to $i_{1}$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive

PositiveContinuousLinearMapstructureMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, type

Wording

positive continuous linear map of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the positive continuous linear maps of $x$ and $x_{1}$ are a basic type.

PositiveContinuousLinearMap.compdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a positive continuous linear map of $x_{1}$ and $x_{2}$. Let $f$ be a positive continuous linear map of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a positive continuous linear map of $x$ and $x_{2}$.

PositiveContinuousLinearMap.iddefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, function or constant

Wording

the identity of R and x (from the docstring)

English

Let $R$ and $x$ be sets. Then the identity of $R$ and $x$ is a positive continuous linear map of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity of $R$ and $x$ and $\mathrm{continuous\_id}$.

PositiveContinuousLinearMap.mk₀defMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $x$ and $x_{1}$ such that for all elements $x_{11}$ of $x$, if $0 \leq x_{11}$, then $0 \leq f (x_{11})$. Then $\mathrm{PositiveContinuousLinearMap\_\_mk\_u2080\_}$ applied to $f$ and $\mathrm{hf}$ is a positive continuous linear map of $x$ and $x_{1}$.

PositiveContinuousLinearMap.ofClassdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, function or constant

Wording

the positive continuous linear map of f (from the name)

English

Let $f$ be an element of $F$. Then the positive continuous linear map of $f$ is a positive continuous linear map of $x$ and $x_{1}$.

PositiveContinuousLinearMap.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive, function or constant

Wording

the continuous linear map of self (from the name)

English

Let $\mathrm{self}$ be a positive continuous linear map of $x$ and $x_{1}$. Then the continuous linear map of $\mathrm{self}$ is a continuous linear map of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toPositiveLinearMap}$ applied to $\mathrm{self}$ and $\operatorname{cont}$ applied to $\mathrm{self}$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient

Submodule.liftQLdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient, function or constant

Wording

no wording

English

Let $S$ be a submodule of $R$ and $M$. Let $f$ be a continuous linear map of $M$ and $x_{4}$ such that $S$ is less than or equal to the kernel of $\operatorname{toLinearMap}$ applied to $f$. Then $\operatorname{liftQL}$ applied to $S$, $f$ and $h$ is a continuous linear map of the set of quotients of $M$ and $S$ and $x_{4}$.

Submodule.mkQLdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient, function or constant

Wording

no wording

English

Let $S$ be a submodule of $R$ and $M$. Then $\operatorname{mkQL}$ applied to $S$ is a continuous linear map of $M$ and the set of quotients of $M$ and $S$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

ContinuousLinearMap.codRestrictdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $x_{5}$ and $x_{6}$. Let $p$ be a submodule of $x_{1}$ and $x_{6}$ such that for all elements $x_{14}$ of $x_{5}$, $\MembershipmemMACRoT {p}{f (x_{14})}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $h$ is a continuous linear map of $x_{5}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {p}{x_{13}})}$.

ContinuousLinearMap.domRestrictdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

the restriction of f and p (from the docstring)

English

Let $f$ be a continuous linear map of $x_{5}$ and $x_{6}$. Let $p$ be a submodule of $x$ and $x_{5}$. Then the restriction of $f$ and $p$ is a continuous linear map of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {p}{x_{13}})}$ and $x_{6}$ defined as the composition of $f$ and the subtype of $p$.

ContinuousLinearMap.projKerOfRightInversedefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

the projection kernel of x14 and x15 (from the name)

English

Let $x_{14}$ be a continuous linear map of $x_{6}$ and $x_{7}$. Let $x_{15}$ be a continuous linear map of $x_{7}$ and $x_{6}$ such that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $x_{15}$ and $\operatorname{coe}$ applied to $x_{14}$. Then the projection kernel of $x_{14}$ and $x_{15}$ is a continuous linear map of $x_{6}$ and $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (x_{14}))}{x_{16}})}$.

ContinuousLinearMap.rangeRestrictdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $x_{5}$ and $x_{6}$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a continuous linear map of $x_{5}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toLinearMap} (f))}{x_{13}})}$.

ContinuousLinearMap.restrictdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $x_{5}$ and $x_{6}$ such that for all elements $x_{15}$ of $x_{5}$, if $x_{15}$ is an element of $p$, then $\MembershipmemMACRoT {q}{f (x_{15})}$. Then $\operatorname{restrict}$ applied to $f$ and $h$ is a continuous linear map of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {p}{x_{13}})}$ and $\SubtypeSet {x_{14}}{(\MembershipmemMACRoT {q}{x_{14}})}$.

Submodule.subtypeLdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict, function or constant

Wording

the subtype of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the subtype of $p$ is a continuous linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$ and $M$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars

ContinuousLinearMap.restrictScalarsdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a continuous linear map of $x$ and $x_{1}$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a continuous linear map of $x$ and $x_{1}$.

ContinuousLinearMap.restrictScalarsₗdefMathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars, function or constant

Wording

no wording

English

Let $A$, $x$, $x_{1}$, $R$ and $S$ be sets. Then $\mathrm{ContinuousLinearMap\_\_restrictScalars\_u2097\_}$ applied to $A$, $x$, $x_{1}$, $R$ and $S$ is a linear map of the set of continuous linear maps of $x$ and $x_{1}$ and the set of continuous linear maps of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\mathrm{ContinuousLinearMap\_\_restrictScalars\_add}$ and $\mathrm{ContinuousLinearMap\_\_restrictScalars\_smul}$.

Mathlib.Topology.Algebra.Module.Determinant

ContinuousLinearMap.detdefMathlib.Topology.Algebra.Module.Determinant, function or constant

Wording

the determinant of A (from the docstring)

English

Let $A$ be a continuous linear map of $M$ and $M$. Then the determinant of $A$ is an element of $R$ defined as $\operatorname{det}$ applied to $\operatorname{toLinearMap}$ applied to $A$.

Mathlib.Topology.Algebra.Module.Equiv.Basic

ContinuousLinearEquivstructureMathlib.Topology.Algebra.Module.Equiv.Basic, type

Wording

continuous linear equivalence of M and x6 (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $M$ and $x_{6}$ be sets. Then the continuous linear equivalences of $M$ and $x_{6}$ are a basic type.

ContinuousLinearEquiv.arrowCongrEquivdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the arrow congruence equivalence of x32 and x33 (from the name)

English

Let $x_{32}$ be a continuous linear equivalence of $x_{10}$ and $x_{13}$. Let $x_{33}$ be a continuous linear equivalence of $x_{19}$ and $x_{16}$. Then the arrow congruence equivalence of $x_{32}$ and $x_{33}$ is an equivalence from the set of continuous linear maps of $x_{10}$ and $x_{19}$ to the set of continuous linear maps of $x_{13}$ and $x_{16}$.

ContinuousLinearEquiv.arrowCongrEquivₛₗdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the arrow congruence equivalence of x32 and x33 (from the name)

English

Let $x_{32}$ be a continuous linear equivalence of $x_{10}$ and $x_{13}$. Let $x_{33}$ be a continuous linear equivalence of $x_{19}$ and $x_{16}$. Then the arrow congruence equivalence of $x_{32}$ and $x_{33}$ is a linear equivalence of the set of continuous linear maps of $x_{10}$ and $x_{19}$ and the set of continuous linear maps of $x_{13}$ and $x_{16}$.

ContinuousLinearEquiv.equivOfInversedefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the equivalence of x14 and x15 (from the name)

English

Let $x_{14}$ be a continuous linear map of $x_{6}$ and $x_{9}$. Let $x_{15}$ be a continuous linear map of $x_{9}$ and $x_{6}$ such that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to $x_{15}$ and $\operatorname{coe}$ applied to $x_{14}$ and $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $x_{15}$ and $\operatorname{coe}$ applied to $x_{14}$. Then the equivalence of $x_{14}$ and $x_{15}$ is a continuous linear equivalence of $x_{6}$ and $x_{9}$.

ContinuousLinearEquiv.equivOfInverse'defMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the equivalence of x14 and x15 (from the name)

English

Let $x_{14}$ be a continuous linear map of $x_{6}$ and $x_{9}$. Let $x_{15}$ be a continuous linear map of $x_{9}$ and $x_{6}$ such that the composition of $x_{14}$ and $x_{15}$ is equal to the identity map of $x_{1}$ and $x_{9}$ and the composition of $x_{15}$ and $x_{14}$ is equal to the identity map of $x$ and $x_{6}$. Then the equivalence of $x_{14}$ and $x_{15}$ is a continuous linear equivalence of $x_{6}$ and $x_{9}$.

ContinuousLinearEquiv.equivOfRightInversedefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the equivalence of x8 and x9 (from the name)

English

Let $x_{8}$ be a continuous linear map of $M$ and $x_{4}$. Let $x_{9}$ be a continuous linear map of $x_{4}$ and $M$ such that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $x_{9}$ and $\operatorname{coe}$ applied to $x_{8}$. Then the equivalence of $x_{8}$ and $x_{9}$ is a continuous linear equivalence of $M$ and $\mathrm{Prod}$ applied to $x_{4}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{toLinearMap} (x_{8}))}{x_{10}})}$.

ContinuousLinearEquiv.negdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the negation map of R (from the docstring)

English

Let $R$ be a set. Then the negation map of $R$ is a continuous linear equivalence of $M$ and $M$.

ContinuousLinearEquiv.ofIsHomeomorphdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the continuous linear equivalence of f and hf (from the name)

English

Let $f$ be a linear equivalence of $M$ and $x_{2}$ such that $\operatorname{coe}$ applied to $f$ is a homeomorphism. Then the continuous linear equivalence of $f$ and $\mathrm{hf}$ is a continuous linear equivalence of $M$ and $x_{2}$.

ContinuousLinearEquiv.ofUnitdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the continuous linear equivalence of f (from the name)

English

Let $f$ be a unit of the set of continuous linear maps of $M$ and $M$. Then the continuous linear equivalence of $f$ is a continuous linear equivalence of $M$ and $M$.

ContinuousLinearEquiv.refldefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the identity map of x and x2 (from the docstring)

English

Let $x$ and $x_{2}$ be sets. Then the identity map of $x$ and $x_{2}$ is a continuous linear equivalence of $x_{2}$ and $x_{2}$.

ContinuousLinearEquiv.restrictScalarsdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a continuous linear equivalence of $M$ and $M$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a continuous linear equivalence of $M$ and $M$.

ContinuousLinearEquiv.skewProddefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the skew product of f and #3 (from the name)

English

Let $e$ be a continuous linear equivalence of $M$ and $x_{3}$. Let $\mathrm{e'}$ be a continuous linear equivalence of $x_{6}$ and $x_{9}$. Let $f$ be a continuous linear map of $M$ and $x_{9}$. Then the skew product of $\mathrm{e'}$ and $f$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $M$ and $x_{6}$ and $\mathrm{Prod}$ applied to $x_{3}$ and $x_{9}$.

ContinuousLinearEquiv.smulLeftdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the left scalar multiple (from the name)

English

The left scalar multiple is a monoid homomorphism of $G$ and the set of continuous linear equivalences of $x_{2}$ and $x_{2}$.

ContinuousLinearEquiv.symmdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the inverse of e (from the docstring)

English

Let $e$ be a continuous linear equivalence of $x_{6}$ and $x_{9}$. Then the inverse of $e$ is a continuous linear equivalence of $x_{9}$ and $x_{6}$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toLinearEquiv}$ applied to $e$, $\mathrm{ContinuousLinearEquiv\_\_continuous\_invFun}$ applied to $e$ and $\mathrm{ContinuousLinearEquiv\_\_continuous\_toFun}$ applied to $e$.

ContinuousLinearEquiv.toContinuousAddEquivdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the continuous additive equivalence of e (from the name)

English

Let $e$ be a continuous linear equivalence of $x_{2}$ and $M$. Then the continuous additive equivalence of $e$ is a continuous additive equivalence of $x_{2}$ and $M$.

ContinuousLinearEquiv.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the continuous linear map of e (from the name)

English

Let $e$ be a continuous linear equivalence of $x_{6}$ and $x_{9}$. Then the continuous linear map of $e$ is a continuous linear map of $x_{6}$ and $x_{9}$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $e$ and $\mathrm{ContinuousLinearEquiv\_\_continuous\_toFun}$ applied to $e$.

ContinuousLinearEquiv.toHomeomorphdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be a continuous linear equivalence of $x_{6}$ and $x_{9}$. Then the homeomorphism of $e$ is a homeomorphism of $x_{6}$ and $x_{9}$ defined as $\operatorname{mk}$ applied to the equivalence of $\operatorname{toLinearEquiv}$ applied to $e$, $\mathrm{ContinuousLinearEquiv\_\_continuous\_toFun}$ applied to $e$ and $\mathrm{ContinuousLinearEquiv\_\_continuous\_invFun}$ applied to $e$.

ContinuousLinearEquiv.toLinearEquivMonoidHomdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence monoid homomorphism (from the name)

English

The linear equivalence monoid homomorphism is a monoid homomorphism of the set of continuous linear equivalences of $V$ and $V$ and the set of linear equivalences of $V$ and $V$.

ContinuousLinearEquiv.toUnitdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the unit of f (from the name)

English

Let $f$ be a continuous linear equivalence of $M$ and $M$. Then the unit of $f$ is a unit of the set of continuous linear maps of $M$ and $M$.

ContinuousLinearEquiv.transdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the composition of x24 and x25 (from the name)

English

Let $x_{24}$ be a continuous linear equivalence of $x_{12}$ and $x_{15}$. Let $x_{25}$ be a continuous linear equivalence of $x_{15}$ and $x_{18}$. Then the composition of $x_{24}$ and $x_{25}$ is a continuous linear equivalence of $x_{12}$ and $x_{18}$.

ContinuousLinearEquiv.uliftdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the lift (from the name)

English

The lift is a continuous linear equivalence of $\mathrm{ULift}$ applied to $x_{2}$ and $x_{2}$.

ContinuousLinearEquiv.unitsEquivdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the unit equivalence of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the unit equivalence of $R$ and $M$ is a multiplicative equivalence of the set of units of the set of continuous linear maps of $M$ and $M$ and the set of continuous linear equivalences of $M$ and $M$.

ContinuousLinearEquiv.unitsEquivAutdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the unit equivalence automorphism of R (from the name)

English

Let $R$ be a set. Then the unit equivalence automorphism of $R$ is an equivalence from $\UnitsMACRoAO {R}$ to the set of continuous linear equivalences of $R$ and $R$.

ContinuousLinearEquivClassdefMathlib.Topology.Algebra.Module.Equiv.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$, $M$ and $x_{3}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{ContinuousLinearEquivClass}$ holds for $F$, $R$, $M$ and $x_{3}$, if $\mathrm{ContinuousSemilinearEquivClass}$ holds for $F$, the identity ring homomorphism of $R$, $M$ and $x_{3}$.

ContinuousSemilinearEquivClassclassMathlib.Topology.Algebra.Module.Equiv.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $S$. Let $M$ and $x_{6}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ContinuousSemilinearEquivClass}$ holds for $F$, $x_{2}$, $M$ and $x_{6}$.

MulOpposite.opContinuousLinearEquivdefMathlib.Topology.Algebra.Module.Equiv.Basic, function or constant

Wording

the opposite continuous linear equivalence of R (from the name)

English

Let $R$ be a set. Then the opposite continuous linear equivalence of $R$ is a continuous linear equivalence of $M$ and the set of multiplicative opposites of $M$.

Mathlib.Topology.Algebra.Module.Equiv.Pi

ContinuousLinearEquiv.finTwoArrowdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\operatorname{finTwoArrow}$ applied to $R$ and $M$ is a continuous linear equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $M$ and $\mathrm{Prod}$ applied to $M$ and $M$.

ContinuousLinearEquiv.funUniquedefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

no wording

English

Let $x$, $R$ and $M$ be sets. Then $\operatorname{funUnique}$ applied to $x$, $R$ and $M$ is a continuous linear equivalence of the set of functions from elements of $x$ to elements of $M$ and $M$.

ContinuousLinearEquiv.piCongrLeftdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

the left product congruence of x3 and e (from the name)

English

Let $R$ be a set. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Let $e$ be an equivalence from $x_{2}$ to $x_{1}$. Then the left product congruence of $x_{3}$ and $e$ is a continuous linear equivalence of the set of functions from elements $\mathrm{i'}$ of $x_{2}$ to elements of $x_{3}$ applied to $e$ applied to $\mathrm{i'}$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{3}$ applied to $i$.

ContinuousLinearEquiv.piCongrRightdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

the right product congruence of f (from the name)

English

Let $f$ be a function from elements $i_{2}$ of $x_{1}$ to continuous linear equivalences of $M$ applied to $i_{2}$ and $N$ applied to $i_{2}$. Then the right product congruence of $i_{2}$ is a continuous linear equivalence of the set of functions from elements $i$ of $x_{1}$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $N$ applied to $i_{1}$.

ContinuousLinearEquiv.piFinTwodefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

no wording

English

Let $R$ be a set. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $R$ and $M$ is a continuous linear equivalence of the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $2$ to elements of $M$ applied to $i$ and $\mathrm{Prod}$ applied to $M$ applied to $0$ and $M$ applied to $1$.

ContinuousLinearEquiv.piUniquedefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

the product of R and f (from the docstring)

English

Let $R$ be a set. Let $f$ be a function from elements of $x_{1}$ to sets. Then the product of $R$ and $f$ is a continuous linear equivalence of the set of functions from elements $t$ of $x_{1}$ to elements of $f$ applied to $t$ and $f$ applied to $\operatorname{default}$.

ContinuousLinearEquiv.sumPiEquivProdPidefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

the sum product equivalence product product of A (from the name)

English

Let $R$, $S$ and $T$ be sets. Let $A$ be a function from elements of $\mathrm{Sum}$ applied to $S$ and $T$ to sets. Then the sum product equivalence product product of $A$ is a continuous linear equivalence of the set of functions from elements $\mathrm{st}$ of $\mathrm{Sum}$ applied to $S$ and $T$ to elements of $A$ applied to $\mathrm{st}$ and $\mathrm{Prod}$ applied to the set of functions from elements $s$ of $S$ to elements of $A$ applied to $\operatorname{inl}$ applied to $s$ and the set of functions from elements $t$ of $T$ to elements of $A$ applied to $\operatorname{inr}$ applied to $t$.

ContinuousLinearMap.finConsdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

no wording

English

Let $f$ be a continuous linear map of $N$ and $M$ applied to $0$. Let $\mathrm{fs}$ be a continuous linear map of $N$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $M$ applied to $\operatorname{succ}$ applied to $i_{1}$. Then $\operatorname{finCons}$ applied to $f$ and $\mathrm{fs}$ is a continuous linear map of $N$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $M$ applied to $i$ defined as the composition of the continuous linear map of $\operatorname{consEquivL}$ applied to $R$ and $M$ and the product of $f$ and $\mathrm{fs}$.

ContinuousLinearMap.iInfKerProjEquivdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

the infimum kernel projection equivalence of x2 (from the name)

English

Let $R$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Assume that $I$ is disjoint to $J$. Assume that $\operatorname{univ} \leq \UnionunionMACRoAB {I}{J}$. Then the infimum kernel projection equivalence of $x_{2}$ is a continuous linear equivalence of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{iInf} (\lambda i . \mathrm{iInf} (\lambda h . \operatorname{ker} (\operatorname{toLinearMap} (\operatorname{proj} (i)))))}{x_{7}})}$ and the set of functions from elements $i_{1}$ of $I$ to elements of $x_{2}$ applied to $i_{1}$.

Fin.consEquivLdefMathlib.Topology.Algebra.Module.Equiv.Pi, function or constant

Wording

no wording

English

Let $R$ be a set. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then $\operatorname{consEquivL}$ applied to $R$ and $M$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $M$ applied to $0$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $M$ applied to $\operatorname{succ}$ applied to $i$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $M$ applied to $i_{1}$.

Mathlib.Topology.Algebra.Module.Equiv.Prod

ContinuousLinearEquiv.prodAssocdefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

the product associator of x5 and x9 (from the name)

English

Let $R$, $x_{1}$, $x_{5}$ and $x_{9}$ be sets. Then the product associator of $x_{5}$ and $x_{9}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $x_{9}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{9}$.

ContinuousLinearEquiv.prodCommdefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

no wording

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then $\operatorname{prodComm}$ applied to $R$, $x_{1}$ and $x_{5}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{1}$.

ContinuousLinearEquiv.prodCongrdefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

the product congruence of e and #2 (from the name)

English

Let $e$ be a continuous linear equivalence of $x_{1}$ and $x_{5}$. Let $\mathrm{e'}$ be a continuous linear equivalence of $x_{9}$ and $x_{13}$. Then the product congruence of $e$ and $\mathrm{e'}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{9}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{13}$.

ContinuousLinearEquiv.prodProdProdCommdefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

no wording

English

Let $R$, $x_{1}$, $x_{5}$, $x_{9}$ and $x_{13}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $R$, $x_{1}$, $x_{5}$, $x_{9}$ and $x_{13}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $\mathrm{Prod}$ applied to $x_{9}$ and $x_{13}$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{9}$ and $\mathrm{Prod}$ applied to $x_{5}$ and $x_{13}$.

ContinuousLinearEquiv.prodUniquedefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

no wording

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then $\operatorname{prodUnique}$ applied to $R$, $x_{1}$ and $x_{5}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $x_{1}$.

ContinuousLinearEquiv.uniqueProddefMathlib.Topology.Algebra.Module.Equiv.Prod, function or constant

Wording

the unique product of x1 and x5 (from the name)

English

Let $R$, $x_{1}$ and $x_{5}$ be sets. Then the unique product of $x_{1}$ and $x_{5}$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $x_{5}$ and $x_{1}$ and $x_{1}$.

Mathlib.Topology.Algebra.Module.Equiv.Submodule

ContinuousLinearEquiv.ofEqdefMathlib.Topology.Algebra.Module.Equiv.Submodule, function or constant

Wording

the continuous linear equivalence of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $\EqtMACRoH {p}{q}$. Then the continuous linear equivalence of $p$ and $q$ is a continuous linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {q}{x_{5}})}$.

ContinuousLinearEquiv.ofSubmodule'defMathlib.Topology.Algebra.Module.Equiv.Submodule, function or constant

Wording

the continuous linear equivalence of f and U (from the name)

English

Let $f$ be a continuous linear equivalence of $M$ and $x_{5}$. Let $U$ be a submodule of $x_{4}$ and $x_{5}$. Then the continuous linear equivalence of $f$ and $U$ is a continuous linear equivalence of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{comap} (\operatorname{toLinearMap} (\operatorname{toLinearEquiv} (f)), U)}{x_{12}})}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {U}{x_{13}})}$.

ContinuousLinearEquiv.ofSubmodulesdefMathlib.Topology.Algebra.Module.Equiv.Submodule, function or constant

Wording

the continuous linear equivalence of p and q (from the name)

English

Let $e$ be a continuous linear equivalence of $M$ and $x_{5}$. Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $x_{4}$ and $x_{5}$ such that the map of $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $e$ and $p$ is equal to $q$. Then the continuous linear equivalence of $p$ and $q$ is a continuous linear equivalence of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {p}{x_{12}})}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {q}{x_{13}})}$ defined as the composition of the submodule map of $e$ and $p$ and the continuous linear equivalence of the map of $\operatorname{toLinearMap}$ applied to $\operatorname{toLinearEquiv}$ applied to $e$ and $p$ and $q$.

ContinuousLinearEquiv.submoduleMapdefMathlib.Topology.Algebra.Module.Equiv.Submodule, function or constant

Wording

the submodule map of e and p (from the name)

English

Let $e$ be a continuous linear equivalence of $M$ and $x_{5}$. Let $p$ be a submodule of $R$ and $M$. Then the submodule map of $e$ and $p$ is a continuous linear equivalence of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {p}{x_{12}})}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toLinearMap} (\operatorname{toLinearEquiv} (e)), p)}{x_{13}})}$.

Submodule.topContEquivdefMathlib.Topology.Algebra.Module.Equiv.Submodule, function or constant

Wording

the top submodule (from the docstring)

English

The top submodule is a continuous linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{4}})}$ and $M$.

Mathlib.Topology.Algebra.Module.FiniteDimension

ContinuousLinearEquiv.ofFinrankEqdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the continuous linear equivalence of cond (from the name)

English

Assume that the rank of $x$ and $E$ is equal to the rank of $x$ and $F$. Then the continuous linear equivalence of $\mathrm{cond}$ is a continuous linear equivalence of $E$ and $F$ defined as the continuous linear equivalence of the linear equivalence of $F$ and $\mathrm{cond}$.

ContinuousLinearMap.toContinuousLinearEquivOfDetNeZerodefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the continuous linear equivalence of f and hf (from the name)

English

Let $f$ be a continuous linear map of $E$ and $E$ such that the determinant of $f$ is distinct from $0$. Then the continuous linear equivalence of $f$ and $\mathrm{hf}$ is a continuous linear equivalence of $E$ and $E$ defined as the continuous linear equivalence of the equivalence of $\operatorname{toLinearMap}$ applied to $f$ and $\mathrm{hf}$.

LinearEquiv.toContinuousLinearEquivdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the continuous linear equivalence of e (from the name)

English

Let $e$ be a linear equivalence of $E$ and $F$. Then the continuous linear equivalence of $e$ is a continuous linear equivalence of $E$ and $F$.

LinearMap.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the continuous linear map induced by a linear map (from the docstring)

English

The continuous linear map induced by a linear map is a linear equivalence of the set of linear maps of $E$ and $\mathrm{F'}$ and the set of continuous linear maps of $E$ and $\mathrm{F'}$.

Module.Basis.constrLdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

no wording

English

Let $v$ be a basis of $x$ and $E$. Let $f$ be a function from elements of $x_{7}$ to elements of $F$. Then $\operatorname{constrL}$ applied to $v$ and $f$ is a continuous linear map of $E$ and $F$ defined as $\operatorname{toContinuousLinearMap}$ applied to $\operatorname{constr}$ applied to $v$, $x$ and $f$.

Module.Basis.equivFunLdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the equivalence function of v (from the name)

English

Let $v$ be a basis of $x$ and $E$. Then the equivalence function of $v$ is a continuous linear equivalence of $E$ and the set of functions from elements of $x_{4}$ to elements of $x$.

Module.End.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.FiniteDimension, function or constant

Wording

the continuous linear map of E (from the name)

English

Let $E$ be a set. Then the continuous linear map of $E$ is an algebra isomorphism of the set of linear maps of $E$ and $E$ and the set of continuous linear maps of $E$ and $E$.

Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear

IsBilinearMap.toContinuousBilinearMapdefMathlib.Topology.Algebra.Module.FiniteDimensionBilinear, function or constant

Wording

the continuous bilinear map of h11 (from the name)

English

Assume that $f$ is a bilinear map. Then the continuous bilinear map of $h_{11}$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$ defined as the continuous bilinear map of the linear map of $h_{11}$.

LinearMap.toContinuousBilinearMapdefMathlib.Topology.Algebra.Module.FiniteDimensionBilinear, function or constant

Wording

the continuous bilinear map of f (from the name)

English

Let $f$ be a linear map of $E$ and the set of linear maps of $F$ and $G$. Then the continuous bilinear map of $f$ is a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$.

Mathlib.Topology.Algebra.Module.IsWeak

LinearMap.IsWeakclassMathlib.Topology.Algebra.Module.IsWeak, predicate

Wording

B is weak (from the name)

English

Let $B$ be a linear map of $E$ and the set of linear maps of $F$ and $x$. Then we can say that $B$ is weak.

LinearMap.IsWeak.evaldefMathlib.Topology.Algebra.Module.IsWeak, function or constant

Wording

the evaluation 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 evaluation of $B$ is a linear map of $F$ and the set of strong duals of $x$ and $E$.

Mathlib.Topology.Algebra.Module.LinearPMap

LinearPMap.HasCorestructureMathlib.Topology.Algebra.Module.LinearPMap, predicate

Wording

no wording

English

Let $f$ be a linear map of $E$ and $F$. Let $S$ be a submodule of $R$ and $E$. Then we can say that $\operatorname{HasCore}$ holds for $f$ and $S$.

LinearPMap.IsClosabledefMathlib.Topology.Algebra.Module.LinearPMap, predicate

Wording

no wording

English

Let $f$ be a linear map of $E$ and $F$. Then $\operatorname{IsClosable}$ holds for $f$, if there exists a linear map $\mathrm{f'}$ of $E$ and $F$, such that the topological closure of the graph of $f$ is equal to the graph of $\mathrm{f'}$.

LinearPMap.IsCloseddefMathlib.Topology.Algebra.Module.LinearPMap, predicate

Wording

f is closed (from the name)

English

Let $f$ be a linear map of $E$ and $F$. Then $f$ is closed, if the graph of $f$ is closed.

LinearPMap.closuredefMathlib.Topology.Algebra.Module.LinearPMap, function or constant

Wording

the closure of f (from the name)

English

Let $f$ be a linear map of $E$ and $F$. Then the closure of $f$ is a linear map of $E$ and $F$ defined as $\mathrm{dite}$ applied to $\operatorname{IsClosable}$ applied to $f$, the function that maps $\mathrm{hf}$ to $\operatorname{choose}$ applied to $\mathrm{hf}$ and the function that maps $\mathrm{hf1}$ to $f$.

Mathlib.Topology.Algebra.Module.LocallyConvex

LocallyConvexSpaceclassMathlib.Topology.Algebra.Module.LocallyConvex, predicate

Wording

no wording

English

Let $x$ and $E$ be sets. Then we can say that $\mathrm{LocallyConvexSpace}$ holds for $x$ and $E$.

Mathlib.Topology.Algebra.Module.ModuleTopology

IsModuleTopologyclassMathlib.Topology.Algebra.Module.ModuleTopology, predicate

Wording

A is a module topology with respect to R (from the name)

English

Let $R$ and $A$ be sets. Then we can say that $A$ is a module topology with respect to $R$.

Mathlib.Topology.Algebra.Module.Multilinear.Basic

ContinuousLinearMap.compContinuousMultilinearMapdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the composition continuous multilinear map of g and f (from the name)

English

Let $g$ be a continuous linear map of $x_{2}$ and $x_{3}$. Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Then the composition continuous multilinear map of $g$ and $f$ is a continuous multilinear map of $x_{1}$ and $x_{3}$.

ContinuousMultilinearMapstructureMathlib.Topology.Algebra.Module.Multilinear.Basic, type

Wording

continuous multilinear map of x1 and x2 (from the name)

English

Let $R$ and $x_{2}$ be sets. Let $x_{1}$ be a function from elements of $x$ to sets. Then the continuous multilinear maps of $x_{1}$ and $x_{2}$ are a basic type.

ContinuousMultilinearMap.applyAddHomdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

Let $m$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\operatorname{applyAddHom}$ applied to $i$ and $m$ is an additive monoid homomorphism of the set of continuous multilinear maps of $x_{1}$ and $x_{2}$ and $x_{2}$.

ContinuousMultilinearMap.codRestrictdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Let $p$ be a submodule of $R$ and $x_{2}$ such that for all functions $v$ from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$, $\MembershipmemMACRoT {p}{f (v)}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $h$ is a continuous multilinear map of $x_{1}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {p}{x_{10}})}$.

ContinuousMultilinearMap.compContinuousLinearMapdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the composition continuous linear map of g and f (from the name)

English

Let $g$ be a continuous multilinear map of $x_{2}$ and $x_{3}$. Let $f$ be a function from elements $i$ of $x$ to continuous linear maps of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$. Then the composition continuous linear map of $g$ and $i$ is a continuous multilinear map of $x_{1}$ and $x_{3}$.

ContinuousMultilinearMap.constOfIsEmptydefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the constant of x1 and m (from the name)

English

Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Let $m$ be an element of $x_{2}$. Then the constant of $x_{1}$ and $m$ is a continuous multilinear map of $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.curry0defMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the curry of f (from the name)

English

Let $f$ be a continuous multilinear map of the function that maps $x_{9}$ to $x$ and $x_{1}$. Then the curry of $f$ is an element of $x_{1}$ defined as $f$ applied to $0$.

ContinuousMultilinearMap.domDomCongrdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the domain domain congruence of e and f (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{10}$. Let $f$ be a continuous multilinear map of the function that maps $x_{12}$ to $x_{1}$ and $x_{2}$. Then the domain domain congruence of $e$ and $f$ is a continuous multilinear map of the function that maps $x_{11}$ to $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.domDomCongrEquivdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the domain domain congruence equivalence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{10}$. Then the domain domain congruence equivalence of $e$ is an equivalence from the set of continuous multilinear maps of the function that maps $x_{11}$ to $x_{1}$ and $x_{2}$ to the set of continuous multilinear maps of the function that maps $x_{12}$ to $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.linearDerivdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the derivative of f and x12 (from the docstring)

English

Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Let $x_{12}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Then the derivative of $f$ and $i_{1}$ is a continuous linear map of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $x_{2}$ defined as the function that maps $x_{12}$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{toContinuousLinearMap} (i_{1} , i), \operatorname{proj} (i))}{x_{12}}$.

ContinuousMultilinearMap.mkPiAlgebradefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product algebra of x and A (from the name)

English

Let $R$, $x$ and $A$ be sets. Then the product algebra of $x$ and $A$ is a continuous multilinear map of the function that maps $x_{6}$ to $A$ and $A$.

ContinuousMultilinearMap.mkPiAlgebraFindefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Let $n$ be a natural number. Then $\operatorname{mkPiAlgebraFin}$ applied to $R$, $n$ and $A$ is a continuous multilinear map of the function that maps $x_{4}$ to $A$ and $A$.

ContinuousMultilinearMap.mkPiRingdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product ring of z (from the name)

English

Let $R$ and $x$ be sets. Let $z$ be an element of $M$. Then the product ring of $z$ is a continuous multilinear map of the function that maps $x_{7}$ to $R$ and $M$ defined as the right scalar multiple of the product algebra of $x$ and $R$ and $z$.

ContinuousMultilinearMap.ofSubsingletondefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the continuous multilinear map of i (from the name)

English

Let $R$, $x_{1}$ and $x_{2}$ be sets. Let $i$ be an element of $x$. Then the continuous multilinear map of $i$ is an equivalence from the set of continuous linear maps of $x_{1}$ and $x_{2}$ to the set of continuous multilinear maps of the function that maps $x_{10}$ to $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.pidefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{6}$ to continuous multilinear maps of $x_{1}$ and $\mathrm{M'}$ applied to $i_{1}$. Then the product of $i_{1}$ is a continuous multilinear map of $x_{1}$ and the set of functions from elements $i$ of $x_{6}$ to elements of $\mathrm{M'}$ applied to $i$.

ContinuousMultilinearMap.piEquivdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from the set of functions from elements $i$ of $x_{6}$ to continuous multilinear maps of $x_{1}$ and $\mathrm{M'}$ applied to $i$ to the set of continuous multilinear maps of $x_{1}$ and the set of functions from elements $i_{1}$ of $x_{6}$ to elements of $\mathrm{M'}$ applied to $i_{1}$.

ContinuousMultilinearMap.piLinearEquivdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product linear equivalence (from the name)

English

The product linear equivalence is a linear equivalence of the set of functions from elements $i$ of $x_{7}$ to continuous multilinear maps of $x_{1}$ and $\mathrm{M'}$ applied to $i$ and the set of continuous multilinear maps of $x_{1}$ and the set of functions from elements $i_{1}$ of $x_{7}$ to elements of $\mathrm{M'}$ applied to $i_{1}$.

ContinuousMultilinearMap.proddefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Let $g$ be a continuous multilinear map of $x_{1}$ and $x_{3}$. Then the product of $f$ and $g$ is a continuous multilinear map of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

ContinuousMultilinearMap.prodEquivdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the product equivalence (from the name)

English

The product equivalence is an equivalence from $\mathrm{Prod}$ applied to the set of continuous multilinear maps of $x_{1}$ and $x_{2}$ and the set of continuous multilinear maps of $x_{1}$ and $x_{3}$ to the set of continuous multilinear maps of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

ContinuousMultilinearMap.restrictScalarsdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a continuous multilinear map of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toMultilinearMap}$ applied to $f$ and $\operatorname{cont}$ applied to $f$.

ContinuousMultilinearMap.smulRightdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the right scalar multiple of f and z (from the name)

English

Let $f$ be a continuous multilinear map of $x_{1}$ and $R$. Let $z$ be an element of $x_{2}$. Then the right scalar multiple of $f$ and $z$ is a continuous multilinear map of $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

the continuous linear map of m and i1 (from the name)

English

Let $f$ be a continuous multilinear map of $x_{1}$ and $x_{2}$. Let $m$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then the continuous linear map of $i_{1}$ and $m$ is a continuous linear map of $x_{1}$ applied to $i$ and $x_{2}$.

ContinuousMultilinearMap.toMultilinearMapLineardefMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

$\operatorname{toMultilinearMapLinear}$ is a linear map of the set of continuous multilinear maps of $x_{1}$ and $x_{2}$ and the set of multilinear maps of $x_{1}$ and $x_{2}$.

ContinuousMultilinearMap.uncurry0defMathlib.Topology.Algebra.Module.Multilinear.Basic, function or constant

Wording

no wording

English

Let $R$ and $x$ be sets. Let $x_{9}$ be an element of $x_{1}$. Then $\operatorname{uncurry0}$ applied to $R$, $x$ and $x_{9}$ is a continuous multilinear map of the function that maps $x_{10}$ to $x$ and $x_{1}$ defined as the constant of the function that maps $x_{10}$ to $x$ and $x_{9}$.

Mathlib.Topology.Algebra.Module.Multilinear.Topology

ContinuousLinearEquiv.continuousMultilinearMapCongrLeftdefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the left continuous multilinear map congruence of F and f (from the name)

English

Let $F$ be a set. Let $f$ be a function from elements $i$ of $x_{1}$ to continuous linear equivalences of $E$ applied to $i$ and $x_{2}$ applied to $i$. Then the left continuous multilinear map congruence of $F$ and $i$ is a continuous linear equivalence of the set of continuous multilinear maps of $x_{2}$ and $F$ and the set of continuous multilinear maps of $E$ and $F$.

ContinuousLinearEquiv.continuousMultilinearMapCongrRightdefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the right continuous multilinear map congruence of E and g (from the name)

English

Let $E$ be a function from elements of $x_{1}$ to sets. Let $g$ be a continuous linear equivalence of $F$ and $G$. Then the right continuous multilinear map congruence of $E$ and $g$ is a continuous linear equivalence of the set of continuous multilinear maps of $E$ and $F$ and the set of continuous multilinear maps of $E$ and $G$.

ContinuousLinearMap.compContinuousMultilinearMapLdefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the composition continuous multilinear map of E (from the name)

English

Let $x$, $F$ and $G$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Then the composition continuous multilinear map of $E$ is a continuous linear map of the set of continuous linear maps of $F$ and $G$ and the set of continuous linear maps of the set of continuous multilinear maps of $E$ and $F$ and the set of continuous multilinear maps of $E$ and $G$.

ContinuousMultilinearMap.applydefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the continuous multilinear map of E and m (from the name)

English

Let $x$ and $F$ be sets. Let $E$ be a function from elements of $x_{1}$ to sets. Let $m$ be a function from elements $i$ of $x_{1}$ to elements of $E$ applied to $i$. Then the continuous multilinear map of $E$ and $i$ is a continuous linear map of the set of continuous multilinear maps of $E$ and $F$ and $F$.

ContinuousMultilinearMap.compContinuousLinearMapLdefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the composition continuous linear map of f (from the name)

English

Let $f$ be a function from elements $i$ of $x_{1}$ to continuous linear maps of $E$ applied to $i$ and $x_{9}$ applied to $i$. Then the composition continuous linear map of $i$ is a continuous linear map of the set of continuous multilinear maps of $x_{9}$ and $F$ and the set of continuous multilinear maps of $E$ and $F$.

ContinuousMultilinearMap.domDomCongrLdefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

the domain domain congruence of e (from the name)

English

Let $e$ be an equivalence from $x_{1}$ to $x_{9}$. Then the domain domain congruence of $e$ is a continuous linear map of the set of continuous multilinear maps of the function that maps $x_{10}$ to $F$ and $G$ and the set of continuous multilinear maps of the function that maps $x_{11}$ to $F$ and $G$.

ContinuousMultilinearMap.restrictScalarsLineardefMathlib.Topology.Algebra.Module.Multilinear.Topology, function or constant

Wording

no wording

English

Let $x_{9}$ be a set. Then $\operatorname{restrictScalarsLinear}$ applied to $x_{9}$ is a continuous linear map of the set of continuous multilinear maps of $E$ and $F$ and the set of continuous multilinear maps of $E$ and $F$.

Mathlib.Topology.Algebra.Module.PerfectPairing

LinearMap.IsContPerfPairclassMathlib.Topology.Algebra.Module.PerfectPairing, predicate

Wording

no wording

English

Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Then we can say that $\operatorname{IsContPerfPair}$ holds for $p$.

LinearMap.toContPerfPairdefMathlib.Topology.Algebra.Module.PerfectPairing, function or constant

Wording

no wording

English

Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Then $\operatorname{toContPerfPair}$ applied to $p$ is a linear equivalence of $M$ and the set of strong duals of $R$ and $N$.

Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

WeakDual.CharacterSpace.toAlgHomdefMathlib.Topology.Algebra.Module.Spaces.CharacterSpace, function or constant

Wording

the algebra homomorphism of x6 (from the name)

English

Let $x_{6}$ be an element of the character space of $x$ and $A$. Then the algebra homomorphism of $x_{6}$ is an algebra homomorphism of $A$ and $x$.

WeakDual.CharacterSpace.toCLMdefMathlib.Topology.Algebra.Module.Spaces.CharacterSpace, function or constant

Wording

the continuous linear map of x6 (from the name)

English

Let $x_{6}$ be an element of the character space of $x$ and $A$. Then the continuous linear map of $x_{6}$ is a continuous linear map of $A$ and $x$ defined as $x_{6}$.

WeakDual.CharacterSpace.toNonUnitalAlgHomdefMathlib.Topology.Algebra.Module.Spaces.CharacterSpace, function or constant

Wording

the non unital algebra homomorphism of x6 (from the name)

English

Let $x_{6}$ be an element of the character space of $x$ and $A$. Then the non unital algebra homomorphism of $x_{6}$ is a non unital algebra homomorphism of $A$ and $x$.

WeakDual.characterSpacedefMathlib.Topology.Algebra.Module.Spaces.CharacterSpace, function or constant

Wording

the character space of x and A (from the docstring)

English

Let $x$ and $A$ be sets. Then the character space of $x$ and $A$ is an element of the power set of the set of weak duals of $x$ and $A$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $x_{6} \neq 0$ and for all elements $x_{7}$ of $A$, for all elements $y$ of $A$, $\EqtMACRoH {x_{6} (x_{7} \times y)}{x_{6} (x_{7})\times x_{6} (y)}$.

WeakDual.gelfandTransformdefMathlib.Topology.Algebra.Module.Spaces.CharacterSpace, function or constant

Wording

the Gelfand transform of x and A (from the name)

English

Let $x$ and $A$ be sets. Then the Gelfand transform of $x$ and $A$ is an algebra homomorphism of $A$ and the set of continuous maps of the set of elements of the character space of $x$ and $A$ and $x$.

Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM

CompactConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, type

Wording

compact convergence continuous linear map of E and F (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then a compact convergence continuous linear map of $E$ and $F$ is an element of the function that maps $x_{4}$, $E$ and $F$ to the set of uniform convergence continuous linear maps of $F$ and $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that $S$ is compact.

CompactConvergenceCLM.piEquivLdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, function or constant

Wording

the product equivalence of F (from the name)

English

Let $x$ and $E$ be sets. Let $F$ be a function from elements of $x_{5}$ to sets. Then the product equivalence of $F$ is a continuous linear equivalence of the set of functions from elements $i$ of $x_{5}$ to compact convergence continuous linear maps of $E$ and $F$ applied to $i$ and the set of compact convergence continuous linear maps of $E$ and the set of functions from elements $i_{1}$ of $x_{5}$ to elements of $F$ applied to $i_{1}$.

ContinuousLinearEquiv.compactConvergenceCLMCongrdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, function or constant

Wording

the compact convergence continuous linear map congruence of x14 and x15 (from the name)

English

Let $x_{14}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{15}$ be a continuous linear equivalence of $H$ and $G$. Then the compact convergence continuous linear map congruence of $x_{14}$ and $x_{15}$ is a continuous linear equivalence of the set of compact convergence continuous linear maps of $E$ and $H$ and the set of compact convergence continuous linear maps of $F$ and $G$ defined as $\operatorname{compactConvergenceCLMCongrSL}$ applied to $x_{14}$ and $x_{15}$.

ContinuousLinearEquiv.compactConvergenceCLMCongrSLdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, function or constant

Wording

no wording

English

Let $x_{28}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{29}$ be a continuous linear equivalence of $H$ and $G$. Then $\operatorname{compactConvergenceCLMCongrSL}$ applied to $x_{28}$ and $x_{29}$ is a continuous linear equivalence of the set of compact convergence continuous linear maps of $E$ and $H$ and the set of compact convergence continuous linear maps of $F$ and $G$.

ContinuousLinearMap.postcompCompactConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, function or constant

Wording

the postcomposition compact convergence continuous linear map of E and L (from the name)

English

Let $E$ be a set. Let $L$ be a continuous linear map of $F$ and $G$. Then the postcomposition compact convergence continuous linear map of $E$ and $L$ is a continuous linear map of the set of compact convergence continuous linear maps of $E$ and $F$ and the set of compact convergence continuous linear maps of $E$ and $G$ defined as the postcomposition uniform convergence continuous linear map of $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that $S$ is compact and $L$.

ContinuousLinearMap.precompCompactConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM, function or constant

Wording

the precomposition compact convergence continuous linear map of G and L (from the name)

English

Let $G$ be a set. Let $L$ be a continuous linear map of $E$ and $F$. Then the precomposition compact convergence continuous linear map of $G$ and $L$ is a continuous linear map of the set of compact convergence continuous linear maps of $F$ and $G$ and the set of compact convergence continuous linear maps of $E$ and $G$.

Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

ContinuousLinearEquiv.arrowCongrdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the arrow congruence of x14 and x15 (from the name)

English

Let $x_{14}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{15}$ be a continuous linear equivalence of $H$ and $G$. Then the arrow congruence of $x_{14}$ and $x_{15}$ is a continuous linear equivalence of the set of continuous linear maps of $E$ and $H$ and the set of continuous linear maps of $F$ and $G$ defined as $\operatorname{arrowCongrSL}$ applied to $x_{14}$ and $x_{15}$.

ContinuousLinearEquiv.arrowCongrSLdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

no wording

English

Let $x_{28}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{29}$ be a continuous linear equivalence of $H$ and $G$. Then $\operatorname{arrowCongrSL}$ applied to $x_{28}$ and $x_{29}$ is a continuous linear equivalence of the set of continuous linear maps of $E$ and $H$ and the set of continuous linear maps of $F$ and $G$.

ContinuousLinearEquiv.conjContinuousAlgEquivdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the conjugate continuous algebra isomorphism of e (from the name)

English

Let $e$ be a continuous linear equivalence of $G$ and $H$. Then the conjugate continuous algebra isomorphism of $e$ is a continuous algebra isomorphism of the set of continuous linear maps of $G$ and $G$ and the set of continuous linear maps of $H$ and $H$.

ContinuousLinearMap.applyₗdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x_{10}$ be a ring homomorphism of $x$ and $x_{1}$. Then $\mathrm{ContinuousLinearMap\_\_apply\_u2097\_}$ applied to $F$ and $x_{10}$ is a linear map of $E$ and the set of continuous linear maps of the set of continuous linear maps of $E$ and $F$ and $F$.

ContinuousLinearMap.coprodEquivLdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the coproduct equivalence of S (from the name)

English

Let $S$ be a set. Then the coproduct equivalence of $S$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to the set of continuous linear maps of $E$ and $G$ and the set of continuous linear maps of $F$ and $G$ and the set of continuous linear maps of $\mathrm{Prod}$ applied to $E$ and $F$ and $G$.

ContinuousLinearMap.piEquivLdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the product equivalence of F (from the name)

English

Let $x$ and $E$ be sets. Let $F$ be a function from elements of $x_{2}$ to sets. Then the product equivalence of $F$ is a continuous linear equivalence of the set of functions from elements $i$ of $x_{2}$ to continuous linear maps of $E$ and $F$ applied to $i$ and the set of continuous linear maps of $E$ and the set of functions from elements $i_{1}$ of $x_{2}$ to elements of $F$ applied to $i_{1}$.

ContinuousLinearMap.postcompdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the postcomposition of E and L (from the name)

English

Let $E$ be a set. Let $L$ be a continuous linear map of $F$ and $G$. Then the postcomposition of $E$ and $L$ is a continuous linear map of the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $E$ and $G$.

ContinuousLinearMap.precompdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the precomposition of G and L (from the name)

English

Let $G$ be a set. Let $L$ be a continuous linear map of $E$ and $F$. Then the precomposition of $G$ and $L$ is a continuous linear map of the set of continuous linear maps of $F$ and $G$ and the set of continuous linear maps of $E$ and $G$.

ContinuousLinearMap.prodLdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the product of S (from the name)

English

Let $S$ be a set. Then the product of $S$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $E$ and $G$ and the set of continuous linear maps of $E$ and $\mathrm{Prod}$ applied to $F$ and $G$.

ContinuousLinearMap.restrictScalarsLdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

no wording

English

Let $x$, $E$, $F$, $x_{8}$ and $x_{13}$ be sets. Then $\operatorname{restrictScalarsL}$ applied to $x$, $E$, $F$, $x_{8}$ and $x_{13}$ is a continuous linear map of the set of continuous linear maps of $E$ and $F$ and the set of continuous linear maps of $E$ and $F$.

ContinuousLinearMap.toBilinFormdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the bilinear form of L (from the name)

English

Let $L$ be a continuous linear map of $E$ and the set of continuous linear maps of $E$ and $x$. Then the bilinear form of $L$ is a bilinear form of $x$ and $E$ defined as $\mathrm{ContinuousLinearMap\_\_toLinearMap\_u2081\_\_u2082\_\_\_app}$ applied to $L$.

ContinuousLinearMap.toLinearMap₁₂defMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

the linear map (from the name)

English

The linear map is a linear map of the set of continuous linear maps of $E$ and the set of continuous linear maps of $F$ and $G$ and the set of linear maps of $E$ and the set of linear maps of $F$ and $G$.

ContinuousLinearMap.toSpanSingletonCLEdefMathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap, function or constant

Wording

no wording

English

$\operatorname{toSpanSingletonCLE}$ is a continuous linear equivalence of $E$ and the set of continuous linear maps of $x$ and $E$.

Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM

ContinuousLinearMap.toPointwiseConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the pointwise convergence continuous linear map of x4 (from the name)

English

Let $x_{1}$, $E$ and $F$ be sets. Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Then the pointwise convergence continuous linear map of $x_{4}$ is a continuous linear map of the set of continuous linear maps of $E$ and $F$ and the set of pointwise convergence continuous linear maps of $E$ and $F$.

PointwiseConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, type

Wording

pointwise convergence continuous linear map of E and F (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then a pointwise convergence continuous linear map of $E$ and $F$ is an element of the function that maps $x_{4}$, $E$ and $F$ to the set of uniform convergence continuous linear maps of $F$ and $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that the set of elements of $s$ is finite.

PointwiseConvergenceCLM.coeLMdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

no wording

English

Let $x$, $E$ and $F$ be sets. Then $\operatorname{coeLM}$ applied to $x$, $E$ and $F$ is a linear map of the set of pointwise convergence continuous linear maps of $E$ and $F$ and the set of linear maps of $E$ and $F$ defined as $\operatorname{coeLM}$ applied to $x$.

PointwiseConvergenceCLM.coeLMₛₗdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

no wording

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $E$ and $F$ be sets. Then $\mathrm{PointwiseConvergenceCLM\_\_coeLM\_u209b\_\_u2097\_}$ 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 linear maps of $E$ and $F$ defined as $\mathrm{ContinuousLinearMap\_\_coeLM\_u209b\_\_u2097\_}$ applied to $x_{4}$.

PointwiseConvergenceCLM.equivWeakDualdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the equivalence weak dual of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the equivalence weak dual of $x$ and $E$ is a continuous linear equivalence of the set of pointwise convergence continuous linear maps of $E$ and $x$ and the set of weak duals of $x$ and $E$.

PointwiseConvergenceCLM.evalCLMdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the evaluation continuous linear map of x4 and a (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $F$ be a set. Let $a$ be an element of $E$. Then the evaluation continuous linear map of $x_{4}$ and $a$ is a continuous linear map of the set of pointwise convergence continuous linear maps of $E$ and $F$ and $F$.

PointwiseConvergenceCLM.piEquivLdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the product equivalence of F (from the name)

English

Let $x$ and $E$ be sets. Let $F$ be a function from elements of $x_{5}$ to sets. Then the product equivalence of $F$ is a continuous linear equivalence of the set of functions from elements $i$ of $x_{5}$ to pointwise convergence continuous linear maps of $E$ and $F$ applied to $i$ and the set of pointwise convergence continuous linear maps of $E$ and the set of functions from elements $i_{1}$ of $x_{5}$ to elements of $F$ applied to $i_{1}$.

PointwiseConvergenceCLM.postcompdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the postcomposition of E and L (from the name)

English

Let $E$ be a set. Let $L$ be a continuous linear map of $F$ and $G$. Then the postcomposition of $E$ and $L$ 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 $E$ and $G$.

PointwiseConvergenceCLM.precompdefMathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM, function or constant

Wording

the precomposition of G and L (from the name)

English

Let $G$ be a set. Let $L$ be a continuous linear map of $E$ and $F$. Then the precomposition of $G$ and $L$ is a continuous linear map of the set of pointwise convergence continuous linear maps of $F$ and $G$ and the set of pointwise convergence continuous linear maps of $E$ and $G$.

Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

ContinuousLinearEquiv.uniformConvergenceCLMCongrdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the uniform convergence continuous linear map congruence of x16 and x17 (from the name)

English

Let $x_{14}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{15}$ be a continuous linear equivalence of $H$ and $G$. Let $x_{16}$ be an element of $\wp (\wp E)$. Let $x_{17}$ be an element of $\wp (\wp F)$ such that for all elements $t$ of $\wp F$, $t$ is an element of $x_{17}$, if and only if the preimage of $\operatorname{coe}$ applied to $x_{14}$ and $t$ is an element of $x_{16}$. Then the uniform convergence continuous linear map congruence of $x_{16}$ and $x_{17}$ is a continuous linear equivalence of the set of uniform convergence continuous linear maps of $H$ and $x_{16}$ and the set of uniform convergence continuous linear maps of $G$ and $x_{17}$ defined as $\operatorname{uniformConvergenceCLMCongrSL}$ applied to $x_{14}$, $x_{15}$, $x_{16}$, $x_{17}$ and $h_{4}$.

ContinuousLinearEquiv.uniformConvergenceCLMCongrSLdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

no wording

English

Let $x_{28}$ be a continuous linear equivalence of $E$ and $F$. Let $x_{29}$ be a continuous linear equivalence of $H$ and $G$. Let $x_{30}$ be an element of $\wp (\wp E)$. Let $x_{31}$ be an element of $\wp (\wp F)$ such that for all elements $t$ of $\wp F$, $t$ is an element of $x_{31}$, if and only if the preimage of $\operatorname{coe}$ applied to $x_{28}$ and $t$ is an element of $x_{30}$. Then $\operatorname{uniformConvergenceCLMCongrSL}$ applied to $x_{28}$, $x_{29}$, $x_{30}$, $x_{31}$ and $h_{14}$ is a continuous linear equivalence of the set of uniform convergence continuous linear maps of $H$ and $x_{30}$ and the set of uniform convergence continuous linear maps of $G$ and $x_{31}$.

ContinuousLinearMap.postcompUniformConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the postcomposition uniform convergence continuous linear map of x18 and L (from the name)

English

Let $x_{18}$ be an element of $\wp (\wp E)$. Let $L$ be a continuous linear map of $F$ and $G$. Then the postcomposition uniform convergence continuous linear map of $x_{18}$ and $L$ is a continuous linear map of the set of uniform convergence continuous linear maps of $F$ and $x_{18}$ and the set of uniform convergence continuous linear maps of $G$ and $x_{18}$.

ContinuousLinearMap.precompUniformConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the precomposition uniform convergence continuous linear map of x19 and L (from the name)

English

Let $G$ be a set. Let $x_{18}$ be an element of $\wp (\wp E)$. Let $x_{19}$ be an element of $\wp (\wp F)$. Let $L$ be a continuous linear map of $E$ and $F$ such that $\operatorname{MapsTo}$ holds for the function that maps $x_{20}$ to the image of $\operatorname{coe}$ applied to $L$ and $x_{20}$, $x_{18}$ and $x_{19}$. Then the precomposition uniform convergence continuous linear map of $x_{19}$ and $L$ is a continuous linear map of the set of uniform convergence continuous linear maps of $G$ and $x_{19}$ and the set of uniform convergence continuous linear maps of $G$ and $x_{18}$.

ContinuousLinearMap.toUniformConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the uniform convergence continuous linear map of x4 and x11 (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $F$ be a set. Let $x_{11}$ be an element of $\wp (\wp E)$. Then the uniform convergence continuous linear map of $x_{4}$ and $x_{11}$ is a linear equivalence of the set of continuous linear maps of $E$ and $F$ and the set of uniform convergence continuous linear maps of $F$ and $x_{11}$ defined as the identity map of $x_{1}$ and the set of continuous linear maps of $E$ and $F$.

UniformConvergenceCLMdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, type

Wording

uniform convergence continuous linear map of F and x11 (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $F$ be a set. Let $x_{11}$ be an element of $\wp (\wp E)$. Then a uniform convergence continuous linear map of $F$ and $x_{11}$ is an element of the function that maps $x_{4}$, $F$ and $x_{11}$ to the set of continuous linear maps of $E$ and $F$.

UniformConvergenceCLM.ofFundefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the uniform convergence continuous linear map of x4 and x11 (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{1}$. Let $F$ be a set. Let $x_{11}$ be an element of $\wp (\wp E)$. Then the uniform convergence continuous linear map of $x_{4}$ and $x_{11}$ is an equivalence from the set of continuous linear maps of $E$ and $F$ to the set of uniform convergence continuous linear maps of $F$ and $x_{11}$.

UniformConvergenceCLM.piEquivLdefMathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM, function or constant

Wording

the product equivalence of F and x9 (from the name)

English

Let $x$ be a set. Let $F$ be a function from elements of $x_{2}$ to sets. Let $x_{9}$ be an element of $\wp (\wp E)$. Then the product equivalence of $F$ and $x_{9}$ is a continuous linear equivalence of the set of functions from elements $i$ of $x_{2}$ to uniform convergence continuous linear maps of $F$ applied to $i$ and $x_{9}$ and the set of uniform convergence continuous linear maps of the set of functions from elements $i_{1}$ of $x_{2}$ to elements of $F$ applied to $i_{1}$ and $x_{9}$.

Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

WeakBilindefMathlib.Topology.Algebra.Module.Spaces.WeakBilin, type

Wording

weak bilinear of x6 (from the name)

English

Let $x_{6}$ be a linear map of $E$ and the set of linear maps of $F$ and $x$. Then a weak bilinear of $x_{6}$ is an element of the function that maps $x_{6}$ to $E$.

WeakBilin.evaldefMathlib.Topology.Algebra.Module.Spaces.WeakBilin, function or constant

Wording

the evaluation 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 evaluation of $B$ is a linear map of $F$ and the set of strong duals of $x$ and the set of weak bilinears of $B$.

Mathlib.Topology.Algebra.Module.Spaces.WeakDual

StrongDual.toWeakDualdefMathlib.Topology.Algebra.Module.Spaces.WeakDual, function or constant

Wording

the weak dual (from the name)

English

The weak dual is a linear equivalence of the set of strong duals of $x$ and $E$ and the set of weak duals of $x$ and $E$ defined as the identity map of $x$ and the set of strong duals of $x$ and $E$.

WeakDualdefMathlib.Topology.Algebra.Module.Spaces.WeakDual, type

Wording

weak dual of x and E (from the name)

English

Let $x$ and $E$ be sets. Then a weak dual of $x$ and $E$ is an element of the function that maps $x$ and $E$ to the set of weak bilinears of the canonical pairing of $x$ and $E$.

WeakDual.toStrongDualdefMathlib.Topology.Algebra.Module.Spaces.WeakDual, function or constant

Wording

the strong dual (from the name)

English

The strong dual is a linear equivalence of the set of weak duals of $x$ and $E$ and the set of strong duals of $x$ and $E$ defined as the inverse of the weak dual.

WeakSpacedefMathlib.Topology.Algebra.Module.Spaces.WeakDual, type

Wording

weak space of x and E (from the name)

English

Let $x$ and $E$ be sets. Then a weak space of $x$ and $E$ is an element of the function that maps $x$ and $E$ to the set of weak bilinears of the flip of the canonical pairing of $x$ and $E$.

WeakSpace.mapdefMathlib.Topology.Algebra.Module.Spaces.WeakDual, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a continuous linear map of $E$ and $F$. Then the map of $f$ is a continuous linear map of the set of weak spaces of $x$ and $E$ and the set of weak spaces of $x$ and $F$.

toWeakSpacedefMathlib.Topology.Algebra.Module.Spaces.WeakDual, function or constant

Wording

the weak space of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the weak space of $x$ and $E$ is a linear equivalence of $E$ and the set of weak spaces of $x$ and $E$ defined as the identity map of $x$ and $E$.

toWeakSpaceCLMdefMathlib.Topology.Algebra.Module.Spaces.WeakDual, function or constant

Wording

the weak space continuous linear map of x and E (from the name)

English

Let $x$ and $E$ be sets. Then the weak space continuous linear map of $x$ and $E$ is a continuous linear map of $E$ and the set of weak spaces of $x$ and $E$.

Mathlib.Topology.Algebra.Module.Star

StarModule.decomposeProdAdjointLdefMathlib.Topology.Algebra.Module.Star, function or constant

Wording

no wording

English

Let $R$ and $A$ be sets. Then $\operatorname{decomposeProdAdjointL}$ applied to $R$ and $A$ is a continuous linear equivalence of $A$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\mathrm{skewAdjoint} (A)}{x_{8}})}$.

selfAdjointPartLdefMathlib.Topology.Algebra.Module.Star, function or constant

Wording

the self-adjoint part of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the self-adjoint part of $R$ and $A$ is a continuous linear map of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{7}})}$.

skewAdjointPartLdefMathlib.Topology.Algebra.Module.Star, function or constant

Wording

the skew adjoint part of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the skew adjoint part of $R$ and $A$ is a continuous linear map of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{skewAdjoint} (A)}{x_{7}})}$.

starLdefMathlib.Topology.Algebra.Module.Star, function or constant

Wording

the star of R (from the name)

English

Let $R$ be a set. Then the star of $R$ is a continuous linear equivalence of $A$ and $A$.

starL'defMathlib.Topology.Algebra.Module.Star, function or constant

Wording

the star of R (from the name)

English

Let $R$ be a set. Then the star of $R$ is a continuous linear equivalence of $A$ and $A$.

Mathlib.Topology.Algebra.Module.TransferInstance

AddEquiv.continuousLinearEquivdefMathlib.Topology.Algebra.Module.TransferInstance, function or constant

Wording

the continuous linear equivalence of R and e (from the name)

English

Let $R$ be a set. Let $e$ be an additive equivalence of $x$ and $x_{1}$. Then the continuous linear equivalence of $R$ and $e$ is a continuous linear equivalence of $x$ and $x_{1}$.

Shrink.continuousLinearEquivdefMathlib.Topology.Algebra.Module.TransferInstance, function or constant

Wording

the continuous linear equivalence of R and x (from the name)

English

Let $R$ and $x$ be sets. Then the continuous linear equivalence of $R$ and $x$ is a continuous linear equivalence of the set of shrinks of $x$ and $x$ defined as the continuous linear equivalence of $R$ and the additive equivalence.

Mathlib.Topology.Algebra.Monoid

AddSubmonoid.topologicalClosuredefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be an additive submonoid of $M$. Then the topological closure of $s$ is an additive submonoid of $M$.

AddSubsemigroup.topologicalClosuredefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be an additive subsemigroup of $M$. Then the topological closure of $s$ is an additive subsemigroup of $M$.

ContinuousMap.addLeftdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $X$. Then $\operatorname{addLeft}$ applied to $x_{2}$ is a continuous map of $X$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $x_{2} + x_{3}$ and $\mathrm{continuous\_const\_add}$ applied to $x_{2}$.

ContinuousMap.addRightdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $X$. Then $\operatorname{addRight}$ applied to $x_{2}$ is a continuous map of $X$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $x_{3} + x_{2}$ and $\mathrm{continuous\_add\_const}$ applied to $x_{2}$.

ContinuousMap.mulLeftdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the left multiplicative of x2 (from the name)

English

Let $x_{2}$ be an element of $X$. Then the left multiplicative of $x_{2}$ is a continuous map of $X$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $x_{2} \times x_{3}$ and $\mathrm{continuous\_const\_mul}$ applied to $x_{2}$.

ContinuousMap.mulRightdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the right multiplicative of x2 (from the name)

English

Let $x_{2}$ be an element of $X$. Then the right multiplicative of $x_{2}$ is a continuous map of $X$ and $X$ defined as $\operatorname{mk}$ applied to the function that maps $x_{3}$ to $x_{3} \times x_{2}$ and $\mathrm{continuous\_mul\_const}$ applied to $x_{2}$.

Filter.Tendsto.addUnitsdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the additive unit of h3 and h4 (from the name)

English

Assume that $\operatorname{Tendsto}$ holds for the function that maps $x_{6}$ to the underlying value in the base of $f$ applied to $x_{6}$, $l$ and the neighbourhood filter of $x_{3}$. Assume that $\operatorname{Tendsto}$ holds for the function that maps $x_{5}$ to the underlying value in the base of $\operatorname{neg}$ applied to $f$ applied to $x_{5}$, $l$ and the neighbourhood filter of $x_{4}$. Then the additive unit of $h_{3}$ and $h_{4}$ is an additive unit of $N$.

Filter.Tendsto.unitsdefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the unit of h3 and h4 (from the name)

English

Assume that $\operatorname{Tendsto}$ holds for the function that maps $x_{6}$ to the underlying value in the base of $f$ applied to $x_{6}$, $l$ and the neighbourhood filter of $x_{3}$. Assume that $\operatorname{Tendsto}$ holds for the function that maps $x_{5}$ to the underlying value in the base of $\operatorname{inv}$ applied to $f$ applied to $x_{5}$, $l$ and the neighbourhood filter of $x_{4}$. Then the unit of $h_{3}$ and $h_{4}$ is a unit of $N$.

Submonoid.topologicalClosuredefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a submonoid of $M$. Then the topological closure of $s$ is a submonoid of $M$.

Subsemigroup.topologicalClosuredefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a subsemigroup of $M$. Then the topological closure of $s$ is a subsemigroup of $M$.

addHomOfMemClosureRangeCoedefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the additive homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is an element of the closure of the range of the function that maps $f_{1}$ and $x_{6}$ to $f_{1}$ applied to $x_{6}$. Then the additive homomorphism of $f$ and $\mathrm{hf}$ is an additive homomorphism of $x$ and $x_{1}$.

addHomOfTendstodefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the additive homomorphism of f and g (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $a$ and $x_{7}$ to $g$ applied to $a$ and $x_{7}$, $l$ and the neighbourhood filter of $f$. Then the additive homomorphism of $f$ and $g$ is an additive homomorphism of $x_{1}$ and $x_{2}$.

addMonoidHomOfMemClosureRangeCoedefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the additive monoid homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is an element of the closure of the range of the function that maps $f_{1}$ and $x_{6}$ to $f_{1}$ applied to $x_{6}$. Then the additive monoid homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of $x$ and $x_{1}$.

addMonoidHomOfTendstodefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the additive monoid homomorphism of f and g (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $a$ and $x_{7}$ to $g$ applied to $a$ and $x_{7}$, $l$ and the neighbourhood filter of $f$. Then the additive monoid homomorphism of $f$ and $g$ is an additive monoid homomorphism of $x_{1}$ and $x_{2}$.

monoidHomOfMemClosureRangeCoedefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the monoid homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is an element of the closure of the range of the function that maps $f_{1}$ and $x_{6}$ to $f_{1}$ applied to $x_{6}$. Then the monoid homomorphism of $f$ and $\mathrm{hf}$ is a monoid homomorphism of $x$ and $x_{1}$.

monoidHomOfTendstodefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the monoid homomorphism of f and g (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $a$ and $x_{7}$ to $g$ applied to $a$ and $x_{7}$, $l$ and the neighbourhood filter of $f$. Then the monoid homomorphism of $f$ and $g$ is a monoid homomorphism of $x_{1}$ and $x_{2}$.

mulHomOfMemClosureRangeCoedefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the multiplicative homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is an element of the closure of the range of the function that maps $f_{1}$ and $x_{6}$ to $f_{1}$ applied to $x_{6}$. Then the multiplicative homomorphism of $f$ and $\mathrm{hf}$ is a multiplicative homomorphism of $x$ and $x_{1}$.

mulHomOfTendstodefMathlib.Topology.Algebra.Monoid, function or constant

Wording

the multiplicative homomorphism of f and g (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $F$ such that $\operatorname{Tendsto}$ holds for the function that maps $a$ and $x_{7}$ to $g$ applied to $a$ and $x_{7}$, $l$ and the neighbourhood filter of $f$. Then the multiplicative homomorphism of $f$ and $g$ is a multiplicative homomorphism of $x_{1}$ and $x_{2}$.

Mathlib.Topology.Algebra.Monoid.Defs

ContinuousAddclassMathlib.Topology.Algebra.Monoid.Defs, predicate

Wording

M is a continuous sum (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a continuous sum.

ContinuousMulclassMathlib.Topology.Algebra.Monoid.Defs, predicate

Wording

M is a continuous product (from the name)

English

Let $M$ be a set. Then we can say that $M$ is a continuous product.

SeparatelyContinuousAddclassMathlib.Topology.Algebra.Monoid.Defs, predicate

Wording

M is a separately continuous sum (from the name)

English

generation took over the time limit

SeparatelyContinuousMulclassMathlib.Topology.Algebra.Monoid.Defs, predicate

Wording

M is a separately continuous product (from the name)

English

generation took over the time limit

Mathlib.Topology.Algebra.MulAction

ContinuousSMulclassMathlib.Topology.Algebra.MulAction, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{ContinuousSMul}$ holds for $M$ and $X$.

ContinuousVAddclassMathlib.Topology.Algebra.MulAction, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{ContinuousVAdd}$ holds for $M$ and $X$.

Mathlib.Topology.Algebra.NonUnitalAlgebra

NonUnitalAlgebra.elementaldefMathlib.Topology.Algebra.NonUnitalAlgebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{4}$ be an element of $A$. Then $\operatorname{elemental}$ applied to $R$ and $x_{4}$ is a non unital subalgebra of $R$ and $A$ defined as the topological closure of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{4}$.

NonUnitalSubalgebra.topologicalClosuredefMathlib.Topology.Algebra.NonUnitalAlgebra, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a non unital subalgebra of $R$ and $A$. Then the topological closure of $s$ is a non unital subalgebra of $R$ and $A$.

Mathlib.Topology.Algebra.NonUnitalStarAlgebra

NonUnitalStarAlgebra.elementaldefMathlib.Topology.Algebra.NonUnitalStarAlgebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{6}$ be an element of $A$. Then $\operatorname{elemental}$ applied to $R$ and $x_{6}$ is a non unital star subalgebra of $R$ and $A$ defined as the topological closure of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{6}$.

NonUnitalStarSubalgebra.topologicalClosuredefMathlib.Topology.Algebra.NonUnitalStarAlgebra, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a non unital star subalgebra of $R$ and $A$. Then the topological closure of $s$ is a non unital star subalgebra of $R$ and $A$.

Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Ideal.openAddSubgroupdefMathlib.Topology.Algebra.Nonarchimedean.AdicTopology, function or constant

Wording

the open additive subgroup of I and n (from the name)

English

Let $I$ be an ideal of $R$. Let $n$ be a natural number. Then the open additive subgroup of $I$ and $n$ is an open additive subgroup of $R$.

IsAdicdefMathlib.Topology.Algebra.Nonarchimedean.AdicTopology, predicate

Wording

J is adic (from the name)

English

Let $J$ be an ideal of $R$. Then $J$ is adic, if $\EqtMACRoH {H}{\operatorname{adicTopology} (J)}$.

WithIdealclassMathlib.Topology.Algebra.Nonarchimedean.AdicTopology, predicate

Wording

no wording

English

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

WithIdeal.idefMathlib.Topology.Algebra.Nonarchimedean.AdicTopology, function or constant

Wording

no wording

English

$\operatorname{i}$ is an ideal of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

WithIdeal.uniformEquivdefMathlib.Topology.Algebra.Nonarchimedean.AdicTopology, function or constant

Wording

the uniform equivalence of e and h (from the name)

English

Let $e$ be a ring isomorphism of $R$ and $S$ such that the map of the ring homomorphism of $e$ and $\operatorname{i}$ is equal to $\operatorname{i}$. Then the uniform equivalence of $e$ and $h$ is a uniform equivalence of $R$ and $S$.

Mathlib.Topology.Algebra.Nonarchimedean.Bases

RingFilterBasis.SubmodulesBasisstructureMathlib.Topology.Algebra.Nonarchimedean.Bases, predicate

Wording

no wording

English

Assume that $R$ is a ring filter basis. Let $B$ be a function from elements of $x$ to submodules of $R$ and $M$. Then we can say that $\operatorname{SubmodulesBasis}$ holds for $\mathrm{BR}$ and $B$.

RingFilterBasis.moduleFilterBasisdefMathlib.Topology.Algebra.Nonarchimedean.Bases, function or constant

Wording

the module filter basis of BR and hB (from the name)

English

Assume that $R$ is a ring filter basis. Assume that $\operatorname{SubmodulesBasis}$ holds for $\mathrm{BR}$ and $B$. Then the module filter basis of $\mathrm{BR}$ and $\mathrm{hB}$ is a module filter basis of $R$ and $M$ defined as the image of $\operatorname{submodulesBasisIsBasis}$ applied to $\mathrm{BR}$ and $\mathrm{hB}$.

RingSubgroupsBasisstructureMathlib.Topology.Algebra.Nonarchimedean.Bases, predicate

Wording

no wording

English

Let $B$ be a function from elements of $x$ to additive subgroups of $A$. Then we can say that $\mathrm{RingSubgroupsBasis}$ holds for $B$.

RingSubgroupsBasis.openAddSubgroupdefMathlib.Topology.Algebra.Nonarchimedean.Bases, function or constant

Wording

the open additive subgroup of hB and i (from the name)

English

Assume that $\mathrm{RingSubgroupsBasis}$ holds for $B$. Let $i$ be an element of $x$. Then the open additive subgroup of $\mathrm{hB}$ and $i$ is an open additive subgroup of $A$.

SubmodulesBasisstructureMathlib.Topology.Algebra.Nonarchimedean.Bases, predicate

Wording

no wording

English

Let $B$ be a function from elements of $x$ to submodules of $R$ and $M$. Then we can say that $\mathrm{SubmodulesBasis}$ holds for $B$.

SubmodulesBasis.openAddSubgroupdefMathlib.Topology.Algebra.Nonarchimedean.Bases, function or constant

Wording

the open additive subgroup of hB and i (from the name)

English

Assume that $\mathrm{SubmodulesBasis}$ holds for $B$. Let $i$ be an element of $x$. Then the open additive subgroup of $\mathrm{hB}$ and $i$ is an open additive subgroup of $M$.

SubmodulesBasis.toModuleFilterBasisdefMathlib.Topology.Algebra.Nonarchimedean.Bases, function or constant

Wording

the image of hB (from the docstring)

English

Assume that $\mathrm{SubmodulesBasis}$ holds for $B$. Then the image of $\mathrm{hB}$ is a module filter basis of $R$ and $M$.

SubmodulesRingBasisstructureMathlib.Topology.Algebra.Nonarchimedean.Bases, predicate

Wording

no wording

English

Let $B$ be a function from elements of $x$ to submodules of $R$ and $A$. Then we can say that $\mathrm{SubmodulesRingBasis}$ holds for $B$.

Mathlib.Topology.Algebra.Nonarchimedean.Basic

NonarchimedeanAddGroupclassMathlib.Topology.Algebra.Nonarchimedean.Basic, predicate

Wording

G is a nonarchimedean additive group (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a nonarchimedean additive group.

NonarchimedeanGroupclassMathlib.Topology.Algebra.Nonarchimedean.Basic, predicate

Wording

G is a nonarchimedean group (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a nonarchimedean group.

NonarchimedeanRingclassMathlib.Topology.Algebra.Nonarchimedean.Basic, predicate

Wording

R is a nonarchimedean ring (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a nonarchimedean ring.

Mathlib.Topology.Algebra.OpenSubgroup

IsTopologicalAddGroup.addNegClosureNhdstructureMathlib.Topology.Algebra.OpenSubgroup, predicate

Wording

no wording

English

Let $T$ and $W$ be elements of $\wp G$. Then we can say that $\operatorname{addNegClosureNhd}$ holds for $T$ and $W$.

IsTopologicalGroup.mulInvClosureNhdstructureMathlib.Topology.Algebra.OpenSubgroup, predicate

Wording

no wording

English

Let $T$ and $W$ be elements of $\wp G$. Then we can say that $\operatorname{mulInvClosureNhd}$ holds for $T$ and $W$.

OpenAddSubgroupstructureMathlib.Topology.Algebra.OpenSubgroup, type

Wording

open additive subgroup of G (from the name)

English

Let $G$ be a set. Then the open additive subgroups of $G$ are a basic type.

OpenAddSubgroup.comapdefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the preimage of f and H (from the name)

English

Let $f$ be an additive monoid homomorphism of $G$ and $N$ such that $\operatorname{coe}$ applied to $f$ is continuous. Let $H$ be an open additive subgroup of $N$. Then the preimage of $f$ and $H$ is an open additive subgroup of $G$.

OpenAddSubgroup.iInfOfFinitedefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the intersection of U (from the docstring)

English

Let $U$ be a function from elements of $x_{2}$ to open additive subgroups of $G$. Then the intersection of $U$ is an open additive subgroup of $G$.

OpenAddSubgroup.proddefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the product of U and V (from the name)

English

Let $U$ be an open additive subgroup of $G$. Let $V$ be an open additive subgroup of $H$. Then the product of $U$ and $V$ is an open additive subgroup of $\mathrm{Prod}$ applied to $G$ and $H$.

OpenAddSubgroup.toOpensdefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the open of U (from the name)

English

Let $U$ be an open additive subgroup of $G$. Then the open of $U$ is an open of $G$ defined as $\operatorname{mk}$ applied to $U$ and $\operatorname{isOpen'}$ applied to $U$.

OpenNormalAddSubgroupstructureMathlib.Topology.Algebra.OpenSubgroup, type

Wording

open normal additive subgroup of G (from the name)

English

Let $G$ be a set. Then the open normal additive subgroups of $G$ are a basic type.

OpenNormalSubgroupstructureMathlib.Topology.Algebra.OpenSubgroup, type

Wording

open normal subgroup of G (from the name)

English

Let $G$ be a set. Then the open normal subgroups of $G$ are a basic type.

OpenSubgroupstructureMathlib.Topology.Algebra.OpenSubgroup, type

Wording

open subgroup of G (from the name)

English

Let $G$ be a set. Then the open subgroups of $G$ are a basic type.

OpenSubgroup.comapdefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the preimage of f and H (from the name)

English

Let $f$ be a monoid homomorphism of $G$ and $N$ such that $\operatorname{coe}$ applied to $f$ is continuous. Let $H$ be an open subgroup of $N$. Then the preimage of $f$ and $H$ is an open subgroup of $G$.

OpenSubgroup.iInfOfFinitedefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the intersection of U (from the docstring)

English

Let $U$ be a function from elements of $x_{2}$ to open subgroups of $G$. Then the intersection of $U$ is an open subgroup of $G$.

OpenSubgroup.proddefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the product of U and V (from the name)

English

Let $U$ be an open subgroup of $G$. Let $V$ be an open subgroup of $H$. Then the product of $U$ and $V$ is an open subgroup of $\mathrm{Prod}$ applied to $G$ and $H$.

OpenSubgroup.toOpensdefMathlib.Topology.Algebra.OpenSubgroup, function or constant

Wording

the open of U (from the name)

English

Let $U$ be an open subgroup of $G$. Then the open of $U$ is an open of $G$ defined as $\operatorname{mk}$ applied to $U$ and $\operatorname{isOpen'}$ applied to $U$.

Mathlib.Topology.Algebra.Order.UpperLower

HasUpperLowerClosureclassMathlib.Topology.Algebra.Order.UpperLower, predicate

Wording

x has upper lower closures (from the name)

English

Let $x$ be a set. Then we can say that $x$ has upper lower closures.

Mathlib.Topology.Algebra.PontryaginDual

PontryaginDualdefMathlib.Topology.Algebra.PontryaginDual, type

Wording

no wording

English

Let $A$ be a set. Then an element of $\mathrm{PontryaginDual}$ applied to $A$ is an element of the function that maps $A$ to the set of continuous monoid homomorphisms of $A$ and the set of circles.

PontryaginDual.mapdefMathlib.Topology.Algebra.PontryaginDual, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a continuous monoid homomorphism of $A$ and $B$. Then the map of $f$ is a continuous monoid homomorphism of $\mathrm{PontryaginDual}$ applied to $B$ and $\mathrm{PontryaginDual}$ applied to $A$ defined as the left composition of the set of circles and $f$.

PontryaginDual.mapHomdefMathlib.Topology.Algebra.PontryaginDual, function or constant

Wording

the map homomorphism of A and G (from the name)

English

Let $A$ and $G$ be sets. Then the map homomorphism of $A$ and $G$ is a continuous monoid homomorphism of the set of continuous monoid homomorphisms of $A$ and $G$ and the set of continuous monoid homomorphisms of $\mathrm{PontryaginDual}$ applied to $G$ and $\mathrm{PontryaginDual}$ applied to $A$.

Mathlib.Topology.Algebra.ProperAction.Basic

ProperSMulclassMathlib.Topology.Algebra.ProperAction.Basic, predicate

Wording

no wording

English

Let $G$ and $X$ be sets. Then we can say that $\mathrm{ProperSMul}$ holds for $G$ and $X$.

ProperVAddclassMathlib.Topology.Algebra.ProperAction.Basic, predicate

Wording

no wording

English

Let $G$ and $X$ be sets. Then we can say that $\mathrm{ProperVAdd}$ holds for $G$ and $X$.

Mathlib.Topology.Algebra.ProperConstSMul

ProperConstSMulclassMathlib.Topology.Algebra.ProperConstSMul, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{ProperConstSMul}$ holds for $M$ and $X$.

ProperConstVAddclassMathlib.Topology.Algebra.ProperConstSMul, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{ProperConstVAdd}$ holds for $M$ and $X$.

Mathlib.Topology.Algebra.RestrictedProduct.Basic

RestrictedProductdefMathlib.Topology.Algebra.RestrictedProduct.Basic, type

Wording

restricted product of A and i (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $A$ be a function from elements $i$ of $x$ to elements of $\wp R (i)$. Let $x_{1}$ be a filter of $x$. Then a restricted product of $i$ and $A$ is an element of the function that maps $R$, $A$, $x_{1}$ and $x_{1}$ to $\SubtypeSet {x_{2}}{\operatorname{Eventually} (\lambda i . \MembershipmemMACRoT {i (i)}{x_{2} (i)}, A)}{x_{1}}$.

RestrictedProduct.coeAddMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the coercion additive monoid homomorphism (from the name)

English

The coercion additive monoid homomorphism is an additive monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{1}$ and the set of functions from elements $i_{2}$ of $x$ to elements of $R$ applied to $i_{2}$.

RestrictedProduct.coeMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the coercion monoid homomorphism (from the name)

English

The coercion monoid homomorphism is a monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{1}$ and the set of functions from elements $i_{2}$ of $x$ to elements of $R$ applied to $i_{2}$.

RestrictedProduct.evalAddMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the evaluation additive monoid homomorphism of R and j (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the evaluation additive monoid homomorphism of $R$ and $j$ is an additive monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{1}$ and $R$ applied to $j$.

RestrictedProduct.evalMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the evaluation monoid homomorphism of R and j (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the evaluation monoid homomorphism of $R$ and $j$ is a monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{1}$ and $R$ applied to $j$.

RestrictedProduct.evalRingHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the evaluation ring homomorphism of R and j (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the evaluation ring homomorphism of $R$ and $j$ is a ring homomorphism of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{1}$ and $R$ applied to $j$.

RestrictedProduct.inclusiondefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the inclusion of A and h (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $A$ be a function from elements $i_{4}$ of $x$ to elements of $\wp R (i_{4})$. Assume that $x_{1} \leq x_{2}$. Let $x_{3}$ be a restricted product of the function that maps $i_{3}$ to $A$ applied to $i_{3}$ and $x_{2}$. Then the inclusion of $i_{4}$ and $h$ is a restricted product of the function that maps $i_{1}$ to $A$ applied to $i_{1}$ and $x_{1}$ defined as the function that maps $x_{3}$ to the coercion of $h$ and $x_{3}$.

RestrictedProduct.mapdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the map of x2 and h (from the name)

English

Let $x_{2}$ be a function from elements $i_{5}$ of $x$ and elements of $G$ applied to $i_{5}$ to elements of $H$ applied to $i_{5}$ such that $\operatorname{Eventually}$ holds for the function that maps $i_{4}$ to $\operatorname{MapsTo}$ applied to $x_{2}$ applied to $i_{4}$, $C$ applied to $i_{4}$ and $D$ applied to $i_{4}$ and $x_{1}$. Let $x_{3}$ be a restricted product of the function that maps $i_{3}$ to $C$ applied to $i_{3}$ and $x_{1}$. Then the map of $i_{5}$ and $h$ is a restricted product of the function that maps $i_{1}$ to $D$ applied to $i_{1}$ and $x_{1}$ defined as the function that maps $x_{3}$ to $\operatorname{mapAlong}$ applied to $G$, $H$, $\mathrm{id}$, $\mathrm{Filter\_\_tendsto\_id}$, $i_{5}$, $x_{2}$, $h$ and $x_{3}$.

RestrictedProduct.mapAlongdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements of $x$ to sets. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{Tendsto}$ holds for $f$, $x_{5}$ and $x_{4}$. Let $x_{8}$ be a function from elements $j_{3}$ of $x_{1}$ and elements of $x_{2}$ applied to $f$ applied to $j_{3}$ to elements of $x_{3}$ applied to $j_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $j_{2}$ to $\operatorname{MapsTo}$ applied to $x_{8}$ applied to $j_{2}$, $x_{6}$ applied to $f$ applied to $j_{2}$ and $x_{7}$ applied to $j_{2}$ and $x_{5}$. Let $x_{9}$ be a restricted product of the function that maps $i_{1}$ to $x_{6}$ applied to $i_{1}$ and $x_{4}$. Then $\operatorname{mapAlong}$ applied to $x_{2}$, $x_{3}$, $f$, $\mathrm{hf}$, $j_{3}$, $x_{8}$, $h$ and $x_{9}$ is a restricted product of the function that maps $j_{1}$ to $x_{7}$ applied to $j_{1}$ and $x_{5}$ defined as the function that maps $j$ to $j_{3}$ applied to $x_{9}$ and $h$ applied to $f$ applied to $x_{9}$.

RestrictedProduct.mapAlongAddMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements of $x$ to sets. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{Tendsto}$ holds for $f$, $x_{5}$ and $x_{4}$. Let $x_{14}$ be a function from elements $j_{3}$ of $x_{1}$ to additive monoid homomorphisms of $x_{2}$ applied to $f$ applied to $j_{3}$ and $x_{3}$ applied to $j_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $j_{2}$ to $\operatorname{MapsTo}$ applied to $\operatorname{coe}$ applied to $x_{14}$ applied to $j_{2}$, $x_{10}$ applied to $f$ applied to $j_{2}$ and $x_{11}$ applied to $j_{2}$ and $x_{5}$. Then $\operatorname{mapAlongAddMonoidHom}$ applied to $x_{2}$, $x_{3}$, $f$, $\mathrm{hf}$, $j_{3}$, $x_{14}$ and $h_{2}$ is an additive monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $x_{10}$ applied to $i_{1}$ and $x_{4}$ and the set of restricted products of the function that maps $j_{1}$ to $x_{11}$ applied to $j_{1}$ and $x_{5}$.

RestrictedProduct.mapAlongMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements of $x$ to sets. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{Tendsto}$ holds for $f$, $x_{5}$ and $x_{4}$. Let $x_{14}$ be a function from elements $j_{3}$ of $x_{1}$ to monoid homomorphisms of $x_{2}$ applied to $f$ applied to $j_{3}$ and $x_{3}$ applied to $j_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $j_{2}$ to $\operatorname{MapsTo}$ applied to $\operatorname{coe}$ applied to $x_{14}$ applied to $j_{2}$, $x_{10}$ applied to $f$ applied to $j_{2}$ and $x_{11}$ applied to $j_{2}$ and $x_{5}$. Then $\operatorname{mapAlongMonoidHom}$ applied to $x_{2}$, $x_{3}$, $f$, $\mathrm{hf}$, $j_{3}$, $x_{14}$ and $h_{2}$ is a monoid homomorphism of the set of restricted products of the function that maps $i_{1}$ to $x_{10}$ applied to $i_{1}$ and $x_{4}$ and the set of restricted products of the function that maps $j_{1}$ to $x_{11}$ applied to $j_{1}$ and $x_{5}$.

RestrictedProduct.mapAlongRingHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements of $x$ to sets. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{Tendsto}$ holds for $f$, $x_{5}$ and $x_{4}$. Let $x_{14}$ be a function from elements $j_{3}$ of $x_{1}$ to ring homomorphisms of $x_{2}$ applied to $f$ applied to $j_{3}$ and $x_{3}$ applied to $j_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $j_{2}$ to $\operatorname{MapsTo}$ applied to $\operatorname{coe}$ applied to $x_{14}$ applied to $j_{2}$, $x_{10}$ applied to $f$ applied to $j_{2}$ and $x_{11}$ applied to $j_{2}$ and $x_{5}$. Then $\operatorname{mapAlongRingHom}$ applied to $x_{2}$, $x_{3}$, $f$, $\mathrm{hf}$, $j_{3}$, $x_{14}$ and $h_{2}$ is a ring homomorphism of the set of restricted products of the function that maps $i_{1}$ to $x_{10}$ applied to $i_{1}$ and $x_{4}$ and the set of restricted products of the function that maps $j_{1}$ to $x_{11}$ applied to $j_{1}$ and $x_{5}$.

RestrictedProduct.mkdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a function from elements $i_{3}$ of $x$ to elements of $R$ applied to $i_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $i_{2}$ to $\MembershipmemMACRoT {A (i_{2})}{x_{2} (i_{2})}$ and $x_{1}$. Then $\operatorname{mk}$ applied to $i_{3}$, $x_{2}$ and $\mathrm{hx}$ is a restricted product of the function that maps $i_{1}$ to $A$ applied to $i_{1}$ and $x_{1}$ defined as the function that maps $\mathrm{hx}$ to $i_{3}$ applied to $\mathrm{hx}$.

RestrictedProduct.mulSingledefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from elements $i_{3}$ of $x$ to elements of $S$ applied to $i_{3}$. Let $i$ be an element of $x$. Let $x_{4}$ be an element of $G$ applied to $i$. Then $\operatorname{mulSingle}$ applied to $i_{3}$, $A$, $i$ and $x_{4}$ is a restricted product of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the cofinite filter defined as the function that maps $x_{4}$ to $\operatorname{mulSingle}$ applied to $A$, $i$ and $x_{4}$.

RestrictedProduct.mulSingleMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the multiplicative single monoid homomorphism of A and i3 (from the name)

English

Let $A$ be a function from elements $i_{3}$ of $x$ to elements of $S$ applied to $i_{3}$. Let $i$ be an element of $x$. Then the multiplicative single monoid homomorphism of $i_{3}$ and $A$ is a monoid homomorphism of $G$ applied to $i$ and the set of restricted products of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the cofinite filter.

RestrictedProduct.singledefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

no wording

English

Let $A$ be a function from elements $i_{3}$ of $x$ to elements of $S$ applied to $i_{3}$. Let $i$ be an element of $x$. Let $x_{4}$ be an element of $G$ applied to $i$. Then $\operatorname{single}$ applied to $i_{3}$, $A$, $i$ and $x_{4}$ is a restricted product of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the cofinite filter defined as the function that maps $x_{4}$ to $\operatorname{single}$ applied to $A$, $i$ and $x_{4}$.

RestrictedProduct.singleAddMonoidHomdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the single additive monoid homomorphism of A and i3 (from the name)

English

Let $A$ be a function from elements $i_{3}$ of $x$ to elements of $S$ applied to $i_{3}$. Let $i$ be an element of $x$. Then the single additive monoid homomorphism of $i_{3}$ and $A$ is an additive monoid homomorphism of $G$ applied to $i$ and the set of restricted products of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the cofinite filter.

RestrictedProduct.structureMapdefMathlib.Topology.Algebra.RestrictedProduct.Basic, function or constant

Wording

the structure map of i3 and x1 (from the name)

English

Let $R$ be a function from elements of $x$ to sets. Let $A$ be a function from elements $i_{3}$ of $x$ to elements of $\wp R (i_{3})$. Let $x_{1}$ be a filter of $x$. Let $x_{2}$ be a function from elements $i_{2}$ of $x$ to elements of $A$ applied to $i_{2}$. Then the structure map of $A$ and $x_{1}$ is a restricted product of the function that maps $i_{1}$ to $A$ applied to $i_{1}$ and $x_{1}$ defined as the function that maps $i$ and $x_{2}$ to $x_{1}$ applied to $i_{2}$ and $x_{2}$.

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

RestrictedProduct.homeoBotdefMathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace, function or constant

Wording

the homeomorphism bottom (from the name)

English

The homeomorphism bottom is a homeomorphism of the set of functions from elements $i$ of $x$ to elements of $R$ applied to $i$ and the set of restricted products of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the bottom.

RestrictedProduct.homeoTopdefMathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace, function or constant

Wording

the homeomorphism top (from the name)

English

The homeomorphism top is a homeomorphism of the set of functions from elements $i$ of $x$ to elements of $A$ applied to $i$ and the set of restricted products of the function that maps $i_{2}$ to $A$ applied to $i_{2}$ and the top.

Mathlib.Topology.Algebra.RestrictedProduct.Units

RestrictedProduct.coeUnitsdefMathlib.Topology.Algebra.RestrictedProduct.Units, function or constant

Wording

the homomorphism from the units (from the docstring)

English

The homomorphism from the units is a monoid homomorphism of the set of units of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{3}$ and the set of functions from elements $i_{2}$ of $x$ to units of $R$ applied to $i_{2}$ defined as the composition of the monoid homomorphism of the product unit and the map of the coercion monoid homomorphism.

RestrictedProduct.mkUnitdefMathlib.Topology.Algebra.RestrictedProduct.Units, function or constant

Wording

the unit of x4 and i3 (from the name)

English

Let $x_{4}$ be a function from elements $i_{3}$ of $x$ to units of $R$ applied to $i_{3}$ such that $\operatorname{Eventually}$ holds for the function that maps $i_{2}$ to the proposition that $x_{4}$ applied to $i_{2}$ is an element of the unit of the submonoid of $B$ applied to $i_{2}$ and $x_{3}$. Then the unit of $i_{3}$ and $x_{4}$ is a unit of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{3}$.

RestrictedProduct.unitsEquivdefMathlib.Topology.Algebra.RestrictedProduct.Units, function or constant

Wording

the ring isomorphism between the units of R (from the docstring)

English

Let $R$ be a function from elements of $x$ to sets. Then the ring isomorphism between the units of $R$ is a multiplicative equivalence of the set of units of the set of restricted products of the function that maps $i_{1}$ to $B$ applied to $i_{1}$ and $x_{3}$ and the set of restricted products of the function that maps $i_{3}$ to the unit of the submonoid of $B$ applied to $i_{3}$ and $x_{3}$.

Mathlib.Topology.Algebra.Ring.Basic

AbsoluteValue.compdefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the composition of v and hf (from the name)

English

Let $v$ be an absolute value of $R$ and $S$. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the composition of $v$ and $\mathrm{hf}$ is an absolute value of $T$ and $S$.

ContinuousAddEquiv.mulLeftdefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the left multiplicative of r (from the name)

English

Let $r$ be a unit of $R$. Then the left multiplicative of $r$ is a continuous additive equivalence of $R$ and $R$.

ContinuousAddEquiv.mulRightdefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the right multiplicative of r (from the name)

English

Let $r$ be a unit of $R$. Then the right multiplicative of $r$ is a continuous additive equivalence of $R$ and $R$.

IsSemitopologicalRingclassMathlib.Topology.Algebra.Ring.Basic, predicate

Wording

no wording

English

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

IsSemitopologicalSemiringclassMathlib.Topology.Algebra.Ring.Basic, predicate

Wording

no wording

English

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

IsTopologicalRingclassMathlib.Topology.Algebra.Ring.Basic, predicate

Wording

R is a topological ring (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a topological ring.

IsTopologicalSemiringclassMathlib.Topology.Algebra.Ring.Basic, predicate

Wording

R is a topological semiring (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a topological semiring.

NonUnitalSubring.topologicalClosuredefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the topological closure of S (from the name)

English

Let $S$ be a non unital subring of $R$. Then the topological closure of $S$ is a non unital subring of $R$.

NonUnitalSubsemiring.topologicalClosuredefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a non unital subsemiring of $R$. Then the topological closure of $s$ is a non unital subsemiring of $R$.

RingTopologystructureMathlib.Topology.Algebra.Ring.Basic, type

Wording

ring topology of R (from the name)

English

Let $R$ be a set. Then the ring topologies of $R$ are a basic type.

RingTopology.coinduceddefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $R$ to elements of $S$. Then $\operatorname{coinduced}$ applied to $f$ is a ring topology of $S$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $b$ to $\mathrm{Leq} (\operatorname{coinduced} (f , t), \operatorname{toTopologicalSpace} (b))$.

RingTopology.toAddGroupTopologydefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the additive group topology of t (from the name)

English

Let $t$ be a ring topology of $R$. Then the additive group topology of $t$ is an additive group topology of $R$.

RingTopology.toAddGroupTopology.orderEmbeddingdefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the order embedding (from the name)

English

The order embedding is an order embedding of the set of ring topologies of $R$ and the set of additive group topologies of $R$.

Subring.topologicalClosuredefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the topological closure of S (from the name)

English

Let $S$ be a subring of $R$. Then the topological closure of $S$ is a subring of $R$.

Subsemiring.topologicalClosuredefMathlib.Topology.Algebra.Ring.Basic, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a subsemiring of $R$. Then the topological closure of $s$ is a subsemiring of $R$.

Mathlib.Topology.Algebra.Ring.Ideal

Ideal.closuredefMathlib.Topology.Algebra.Ring.Ideal, function or constant

Wording

the closure of I (from the docstring)

English

Let $I$ be an ideal of $R$. Then the closure of $I$ is an ideal of $R$.

Ideal.connectedComponentOfZerodefMathlib.Topology.Algebra.Ring.Ideal, function or constant

Wording

the connected component of zero of R (from the docstring)

English

Let $R$ be a set. Then the connected component of zero of $R$ is an ideal of $R$.

Mathlib.Topology.Algebra.SeparationQuotient.Basic

SeparationQuotient.liftCLMdefMathlib.Topology.Algebra.SeparationQuotient.Basic, function or constant

Wording

the lift continuous linear map of f and hf (from the name)

English

Let $f$ be a continuous linear map of $M$ and $N$ such that for all elements $x_{9}$ and $y$ of $M$, if $\mathrm{Inseparable}$ holds for $x_{9}$ and $y$, then $\EqtMACRoH {f (x_{9})}{f (y)}$. Then the lift continuous linear map of $f$ and $\mathrm{hf}$ is a continuous linear map of the set of separation quotients of $M$ and $N$.

SeparationQuotient.mkAddMonoidHomdefMathlib.Topology.Algebra.SeparationQuotient.Basic, function or constant

Wording

the additive monoid homomorphism (from the name)

English

The additive monoid homomorphism is an additive monoid homomorphism of $M$ and the set of separation quotients of $M$.

SeparationQuotient.mkCLMdefMathlib.Topology.Algebra.SeparationQuotient.Basic, function or constant

Wording

the continuous linear map of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the continuous linear map of $R$ and $M$ is a continuous linear map of $M$ and the set of separation quotients of $M$.

SeparationQuotient.mkMonoidHomdefMathlib.Topology.Algebra.SeparationQuotient.Basic, function or constant

Wording

the monoid homomorphism (from the name)

English

The monoid homomorphism is a monoid homomorphism of $M$ and the set of separation quotients of $M$.

SeparationQuotient.mkRingHomdefMathlib.Topology.Algebra.SeparationQuotient.Basic, function or constant

Wording

the ring homomorphism (from the name)

English

The ring homomorphism is a ring homomorphism of $R$ and the set of separation quotients of $R$.

Mathlib.Topology.Algebra.SeparationQuotient.Hom

SeparationQuotient.liftContinuousAddMonoidHomdefMathlib.Topology.Algebra.SeparationQuotient.Hom, function or constant

Wording

the lift of f and hf (from the docstring)

English

Let $f$ be a continuous additive monoid homomorphism of $M$ and $N$ such that for all elements $x_{4}$ and $y$ of $M$, if $\mathrm{Inseparable}$ holds for $x_{4}$ and $y$, then $\EqtMACRoH {f (x_{4})}{f (y)}$. Then the lift of $f$ and $\mathrm{hf}$ is a continuous additive monoid homomorphism of the set of separation quotients of $M$ and $N$.

SeparationQuotient.liftContinuousMonoidHomdefMathlib.Topology.Algebra.SeparationQuotient.Hom, function or constant

Wording

the lift of f and hf (from the docstring)

English

Let $f$ be a continuous monoid homomorphism of $M$ and $N$ such that for all elements $x_{4}$ and $y$ of $M$, if $\mathrm{Inseparable}$ holds for $x_{4}$ and $y$, then $\EqtMACRoH {f (x_{4})}{f (y)}$. Then the lift of $f$ and $\mathrm{hf}$ is a continuous monoid homomorphism of the set of separation quotients of $M$ and $N$.

Mathlib.Topology.Algebra.SeparationQuotient.Section

SeparationQuotient.outCLMdefMathlib.Topology.Algebra.SeparationQuotient.Section, function or constant

Wording

no wording

English

Let $K$ and $E$ be sets. Then $\operatorname{outCLM}$ applied to $K$ and $E$ is a continuous linear map of the set of separation quotients of $E$ and $E$ defined as $\operatorname{choose}$ applied to $\mathrm{SeparationQuotient\_\_exists\_out\_continuousLinearMap}$ applied to $K$ and $E$.

Mathlib.Topology.Algebra.Star

ContinuousStarclassMathlib.Topology.Algebra.Star, predicate

Wording

R is a continuous star (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a continuous star.

starContinuousMapdefMathlib.Topology.Algebra.Star, function or constant

Wording

the star operation bundled as a continuous map (from the docstring)

English

The star operation bundled as a continuous map is a continuous map of $R$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{star}$ and $\mathrm{ContinuousStar\_\_continuous\_star}$.

Mathlib.Topology.Algebra.StarSubalgebra

StarAlgebra.elementaldefMathlib.Topology.Algebra.StarSubalgebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{6}$ be an element of $A$. Then $\operatorname{elemental}$ applied to $R$ and $x_{6}$ is a star subalgebra of $R$ and $A$ defined as the closure of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{6}$.

StarSubalgebra.topologicalClosuredefMathlib.Topology.Algebra.StarSubalgebra, function or constant

Wording

the closure of s (from the docstring)

English

Let $s$ be a star subalgebra of $R$ and $A$. Then the closure of $s$ is a star subalgebra of $R$ and $A$.

Mathlib.Topology.Algebra.Support

HasCompactMulSupportdefMathlib.Topology.Algebra.Support, predicate

Wording

f has compact multiplicative supports (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ has compact multiplicative supports, if the topological support of $f$ is compact.

HasCompactMulSupport.submonoiddefMathlib.Topology.Algebra.Support, function or constant

Wording

the submonoid of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the submonoid of $x$ and $x_{1}$ is a submonoid of the set of functions from elements of $x$ to elements of $x_{1}$.

HasCompactSupportdefMathlib.Topology.Algebra.Support, predicate

Wording

f has compact supports (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ has compact supports, if $\mathrm{tsupport}$ applied to $f$ is compact.

HasCompactSupport.addSubmonoiddefMathlib.Topology.Algebra.Support, function or constant

Wording

the additive submonoid of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the additive submonoid of $x$ and $x_{1}$ is an additive submonoid of the set of functions from elements of $x$ to elements of $x_{1}$.

mulTSupportdefMathlib.Topology.Algebra.Support, function or constant

Wording

the topological support of f (from the docstring)

English

Let $f$ be a function from elements of $X$ to elements of $x$. Then the topological support of $f$ is an element of $\wp X$ defined as the closure of the multiplicative support of $f$.

tsupportdefMathlib.Topology.Algebra.Support, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $x$. Then $\mathrm{tsupport}$ applied to $f$ is an element of $\wp X$ defined as the closure of the support of $f$.

Mathlib.Topology.Algebra.TopologicallyNilpotent

IsTopologicallyNilpotentdefMathlib.Topology.Algebra.TopologicallyNilpotent, predicate

Wording

a is topologically nilpotent (from the docstring)

English

generation took over the time limit

topologicalNilradicaldefMathlib.Topology.Algebra.TopologicallyNilpotent, function or constant

Wording

the topological nilradical of R (from the docstring)

English

Let $R$ be a set. Then the topological nilradical of $R$ is an ideal of $R$.

Mathlib.Topology.Algebra.UniformField

CompletableTopFieldclassMathlib.Topology.Algebra.UniformField, predicate

Wording

no wording

English

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

UniformSpace.Completion.hatInvdefMathlib.Topology.Algebra.UniformField, function or constant

Wording

no wording

English

Let $x_{2}$ be a completion of $K$. Then $\operatorname{hatInv}$ applied to $x_{2}$ is a completion of $K$ defined as $\operatorname{extend}$ applied to $\mathrm{UniformSpace\_\_Completion\_\_isDenseInducing\_coe}$, the function that maps $x_{2}$ to the coercion of $\operatorname{inv}$ applied to $x_{2}$ and $x_{2}$.

Mathlib.Topology.Algebra.UniformMulAction

UniformContinuousConstSMulclassMathlib.Topology.Algebra.UniformMulAction, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{UniformContinuousConstSMul}$ holds for $M$ and $X$.

UniformContinuousConstVAddclassMathlib.Topology.Algebra.UniformMulAction, predicate

Wording

no wording

English

Let $M$ and $X$ be sets. Then we can say that $\mathrm{UniformContinuousConstVAdd}$ holds for $M$ and $X$.

Mathlib.Topology.Algebra.UniformRing

IsDenseInducing.extendRingHomdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

no wording

English

Assume that $\mathrm{IsUniformInducing}$ holds for $\operatorname{coe}$ applied to $i$. Assume that $\operatorname{coe}$ applied to $i$ is a dense range. Assume that $\mathrm{UniformContinuous}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{extendRingHom}$ applied to $\mathrm{ue}$, $\mathrm{dr}$ and $\mathrm{hf}$ is a ring homomorphism of $x_{3}$ and $x_{6}$.

UniformSpace.Completion.coeRingHomdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

the coercion ring homomorphism (from the name)

English

The coercion ring homomorphism is a ring homomorphism of $x$ and the set of completions of $x$.

UniformSpace.Completion.extensionHomdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

the completion extension of f and hf (from the docstring)

English

Let $f$ be a ring homomorphism of $x$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the completion extension of $f$ and $\mathrm{hf}$ is a ring homomorphism of the set of completions of $x$ and $x_{3}$.

UniformSpace.Completion.mapRingEquivdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

the map ring isomorphism of f (from the name)

English

Let $f$ be a ring isomorphism of $x$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to the inverse of $f$ are continuous. Then the map ring isomorphism of $f$ is a ring isomorphism of the set of completions of $x$ and the set of completions of $x_{3}$.

UniformSpace.Completion.mapRingHomdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

the completion map of f and hf (from the docstring)

English

Let $f$ be a ring homomorphism of $x$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the completion map of $f$ and $\mathrm{hf}$ is a ring homomorphism of the set of completions of $x$ and the set of completions of $x_{3}$.

UniformSpace.sepQuotHomeomorphRingQuotdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{sepQuotHomeomorphRingQuot}$ applied to $x$ is a homeomorphism of the set of separation quotients of $x$ and the set of quotients of $x$ and the closure of the bottom.

UniformSpace.sepQuotRingEquivRingQuotdefMathlib.Topology.Algebra.UniformRing, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{sepQuotRingEquivRingQuot}$ applied to $x$ is a ring isomorphism of the set of separation quotients of $x$ and the set of quotients of $x$ and the closure of the bottom.

Mathlib.Topology.Algebra.ValuativeRel.Completion

Valuation.extensiondefMathlib.Topology.Algebra.ValuativeRel.Completion, function or constant

Wording

the extension of v (from the docstring)

English

Let $v$ be a valuation of $K$ and $x$. Then the extension of $v$ is a valuation of the set of completions of $K$ and $x$.

Valuation.valueGroup₀ExtensionEquivdefMathlib.Topology.Algebra.ValuativeRel.Completion, function or constant

Wording

the value group extension equivalence of v (from the name)

English

Let $v$ be a valuation of $K$ and $x$. Then the value group extension equivalence of $v$ is a multiplicative equivalence of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the extension of $v$.

Valuation.valueGroup₀ExtensionHomdefMathlib.Topology.Algebra.ValuativeRel.Completion, function or constant

Wording

the value group extension homomorphism of v (from the name)

English

Let $v$ be a valuation of $K$ and $x$. Then the value group extension homomorphism of $v$ is a monoid with zero homomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the extension of $v$.

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

IsValuativeTopologyclassMathlib.Topology.Algebra.ValuativeRel.ValuativeTopology, predicate

Wording

R is a valuative topology (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a valuative topology.

Mathlib.Topology.Algebra.Valued.NormedValued

NormedField.valuationdefMathlib.Topology.Algebra.Valued.NormedValued, function or constant

Wording

the valuation (from the docstring)

English

The valuation is a valuation of $K$ and $\mathrm{NNReal}$.

Valuation.absoluteValuedefMathlib.Topology.Algebra.Valued.NormedValued, function or constant

Wording

the absolute value of v (from the name)

English

Let $v$ be a valuation of $L$ and $x_{1}$. Then the absolute value of $v$ is an absolute value of $L$ and $\Real$.

Valuation.normdefMathlib.Topology.Algebra.Valued.NormedValued, function or constant

Wording

the norm of v and x3 (from the name)

English

Let $v$ be a valuation of $R$ and $x_{1}$. Let $x_{3}$ be an element of $R$. Then the norm of $v$ and $x_{3}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{hom'}$ applied to $v$ and $\operatorname{restrict}$ applied to $v$ and $x_{3}$.

Mathlib.Topology.Algebra.Valued.ValuationTopology

ValuedclassMathlib.Topology.Algebra.Valued.ValuationTopology, predicate

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{Valued}$ holds for $R$ and $x_{1}$.

Valued.vdefMathlib.Topology.Algebra.Valued.ValuationTopology, function or constant

Wording

no wording

English

$\operatorname{v}$ is a valuation of $R$ and $x_{1}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Mathlib.Topology.Algebra.Valued.ValuedField

Valued.ResidueFielddefMathlib.Topology.Algebra.Valued.ValuedField, type

Wording

residue field of K (from the name)

English

Let $K$ be a set. Then a residue field of $K$ is an element of the function that maps $K$ to the set of residue fields of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{integer} (K)}{x_{3}})}$.

Valued.extensiondefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the extension of the valuation of x3 (from the docstring)

English

Let $x_{3}$ be a completion of $K$. Then the extension of the valuation of $x_{3}$ is a value group of $\operatorname{toMonoidWithZeroHom}$ applied to $\operatorname{v}$.

Valued.extensionValuationdefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the extension (from the docstring)

English

The extension is a valuation of the set of completions of $K$ and $x_{1}$.

Valued.integerdefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the integer of K (from the name)

English

Let $K$ be a set. Then the integer of $K$ is a subring of $K$ defined as the integer of $\operatorname{v}$.

Valued.maximalIdealdefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the maximal ideal of K (from the name)

English

Let $K$ be a set. Then the maximal ideal of $K$ is an ideal of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{integer} (K)}{x_{3}})}$ defined as the maximal ideal of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{integer} (K)}{x_{3}})}$.

Valued.valueGroup₀_equiv_extensionValuationdefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the value group equivalence extension valuation (from the name)

English

The value group equivalence extension valuation is a multiplicative equivalence of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $\operatorname{v}$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the extension.

Valued.valueGroup₀_hom_extensionValuationdefMathlib.Topology.Algebra.Valued.ValuedField, function or constant

Wording

the value group homomorphism extension valuation (from the name)

English

The value group homomorphism extension valuation is a monoid with zero homomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $\operatorname{v}$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to the extension.

Mathlib.Topology.Algebra.Valued.WithVal

NumberField.RingOfIntegers.withValEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

no wording

English

Let $v$ be a valuation of $K$ and $x$. Let $R$ be a set. Then $\operatorname{withValEquiv}$ applied to $v$ and $R$ is a ring isomorphism of the set of rings of integer of $\mathrm{WithVal}$ applied to $v$ and $R$ defined as the equivalence of $R$.

Rat.ringOfIntegersWithValEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the ring of v (from the name)

English

Let $v$ be a valuation of $\Rational$ and $x$. Then the ring of $v$ is a ring isomorphism of the set of rings of integer of $\mathrm{WithVal}$ applied to $v$ and $\Integer$ defined as $\operatorname{withValEquiv}$ applied to $v$ and $\Integer$.

Valuation.CompletiondefMathlib.Topology.Algebra.Valued.WithVal, type

Wording

completion of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then a completion of $v$ is an element of the function that maps $v$ to the set of completions of $\mathrm{WithVal}$ applied to $v$.

Valuation.IsEquiv.orderRingIsodefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the order ring isomorphism of h (from the name)

English

Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Then the order ring isomorphism of $h$ is an order ring isomorphism of $\mathrm{WithVal}$ applied to $v$ and $\mathrm{WithVal}$ applied to $w$.

Valuation.IsEquiv.uniformEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the uniform equivalence of h (from the name)

English

Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Then the uniform equivalence of $h$ is a uniform equivalence of $\mathrm{WithVal}$ applied to $v$ and $\mathrm{WithVal}$ applied to $w$.

WithValstructureMathlib.Topology.Algebra.Valued.WithVal, type

Wording

no wording

English

Let $v$ be a valuation of $R$ and $x$. Then the elements of $\mathrm{WithVal}$ applied to $v$ are a basic type.

WithVal.algEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the algebra isomorphism of R and v (from the name)

English

Let $R$ be a set. Let $v$ be a valuation of $S$ and $x$. Then the algebra isomorphism of $R$ and $v$ is an algebra isomorphism of $\mathrm{WithVal}$ applied to $v$ and $S$ defined as the algebra isomorphism of $R$ and $\operatorname{toEquiv}$ applied to the equivalence of $v$.

WithVal.congrdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the congruence of w and f (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Let $w$ be a valuation of $S$ and $x_{4}$. Let $f$ be a ring isomorphism of $R$ and $S$. Then the congruence of $w$ and $f$ is a ring isomorphism of $\mathrm{WithVal}$ applied to $v$ and $\mathrm{WithVal}$ applied to $w$.

WithVal.equivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the equivalence of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the equivalence of $v$ is a ring isomorphism of $\mathrm{WithVal}$ applied to $v$ and $R$.

WithVal.linearEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the linear equivalence of R and v (from the name)

English

Let $R$ be a set. Let $v$ be a valuation of $S$ and $x$. Then the linear equivalence of $R$ and $v$ is a linear equivalence of $\mathrm{WithVal}$ applied to $v$ and $S$ defined as the linear equivalence of $R$ and the additive equivalence of the equivalence of $v$.

WithVal.mapdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the map of w and f (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Let $w$ be a valuation of $S$ and $x_{4}$. Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $w$ and $f$ is a ring homomorphism of $\mathrm{WithVal}$ applied to $v$ and $\mathrm{WithVal}$ applied to $w$ defined as the composition of the ring homomorphism of the inverse of the equivalence of $w$ and the composition of $f$ and the ring homomorphism of the equivalence of $v$.

WithVal.ofValdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{WithVal}$ applied to $v$. Then $\operatorname{ofVal}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

WithVal.uniformEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the uniform equivalence of hV and h (from the name)

English

Assume that $\EqtMACRoH {\operatorname{v}}{w}$. Assume that $\operatorname{IsEquiv}$ holds for $v$ and $w$. Then the uniform equivalence of $\mathrm{hV}$ and $h$ is a uniform equivalence of $\mathrm{WithVal}$ applied to $v$ and $R$.

WithVal.valuationdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the valuation of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the valuation of $v$ is a valuation of $\mathrm{WithVal}$ applied to $v$ and $x$ defined as the preimage of the ring homomorphism of the equivalence of $v$ and $v$.

WithVal.valueGroupEquivdefMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the value group equivalence of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the value group equivalence of $v$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (\operatorname{v}))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{valueGroup} (\operatorname{toMonoidWithZeroHom} (v))}{x_{4}})}$.

WithVal.valueGroupOrderIso₀defMathlib.Topology.Algebra.Valued.WithVal, function or constant

Wording

the value group order isomorphism of v (from the name)

English

Let $v$ be a valuation of $R$ and $x$. Then the value group order isomorphism of $v$ is an order monoid isomorphism of the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $\operatorname{v}$ and the set of value groups of $\operatorname{toMonoidWithZeroHom}$ applied to $v$.

Mathlib.Topology.ApproximateUnit

Filter.IsApproximateUnitstructureMathlib.Topology.ApproximateUnit, predicate

Wording

l is a approximate unit (from the name)

English

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

Mathlib.Topology.Baire.BaireMeasurable

BaireMeasurableSetdefMathlib.Topology.Baire.BaireMeasurable, predicate

Wording

s is a Baire measurable set (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is a Baire measurable set, if $s$ is a measurable set.

Mathlib.Topology.Bases

FirstCountableTopologyclassMathlib.Topology.Bases, predicate

Wording

x is a first countable topology (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a first countable topology.

SecondCountableTopologyclassMathlib.Topology.Bases, predicate

Wording

x is a second countable topology (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a second countable topology.

TopologicalSpace.IsSeparabledefMathlib.Topology.Bases, predicate

Wording

s is separable (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is separable, if there exists an element $c$ of $\wp x$, such that $c$ is countable and $s$ is less than or equal to the closure of $c$.

TopologicalSpace.IsTopologicalBasisstructureMathlib.Topology.Bases, predicate

Wording

s is a topological basis (from the name)

English

Let $s$ be an element of $\wp (\wp x)$. Then we can say that $s$ is a topological basis.

TopologicalSpace.SeparableSpaceclassMathlib.Topology.Bases, predicate

Wording

x is a separable space (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a separable space.

TopologicalSpace.countableBasisdefMathlib.Topology.Bases, function or constant

Wording

the countable basis of x (from the name)

English

Let $x$ be a set. Then the countable basis of $x$ is an element of $\wp (\wp x)$ defined as $\operatorname{choose}$ applied to $\mathrm{TopologicalSpace\_\_exists\_countable\_basis}$ applied to $x$.

TopologicalSpace.denseSeqdefMathlib.Topology.Bases, function or constant

Wording

the dense sequence of x and x1 (from the name)

English

Let $x$ be a set. Let $x_{1}$ be a natural number. Then the dense sequence of $x$ and $x_{1}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{TopologicalSpace\_\_exists\_dense\_seq}$ applied to $x$ and $x_{1}$.

Mathlib.Topology.Bornology.Absorbs

AbsorbentdefMathlib.Topology.Bornology.Absorbs, predicate

Wording

M is absorbent (from the docstring)

English

Let $M$ be a set. Let $s$ be an element of $\wp x$. Then $M$ is absorbent, if for all elements $x_{3}$ of $x$, $\mathrm{Absorbs}$ holds for $M$, $s$ and $\operatorname{singleton}$ applied to $x_{3}$.

AbsorbsdefMathlib.Topology.Bornology.Absorbs, predicate

Wording

no wording

English

Let $M$ be a set. Let $s$ and $t$ be elements of $\wp x$. Then $\mathrm{Absorbs}$ holds for $M$, $s$ and $t$, if $\operatorname{Eventually}$ holds for the function that maps $a$ to $\mathrm{Leq} (t , \HSMulhSMulMACRoAL {a}{s})$ and $\operatorname{cobounded}$ applied to $M$.

Filter.absorbingdefMathlib.Topology.Bornology.Absorbs, function or constant

Wording

no wording

English

Let $x$ be a set. Let $u$ be an element of $\wp x_{1}$. Then $\operatorname{absorbing}$ applied to $x$ and $u$ is a filter of $x_{1}$.

Mathlib.Topology.Bornology.Basic

BornologyclassMathlib.Topology.Bornology.Basic, predicate

Wording

x is a bornology (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a bornology.

Bornology.IsBoundeddefMathlib.Topology.Bornology.Basic, predicate

Wording

s is bounded (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is bounded, if the complement of $s$ is cobounded.

Bornology.IsCoboundeddefMathlib.Topology.Bornology.Basic, predicate

Wording

s is cobounded (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is cobounded, if $\MembershipmemMACRoT {\operatorname{cobounded} (x)}{s}$.

Bornology.coboundeddefMathlib.Topology.Bornology.Basic, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{cobounded}$ applied to $x$ is a filter of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Extend

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars

Mathlib.Topology.Algebra.Module.Determinant

Mathlib.Topology.Algebra.Module.Equiv.Basic

Mathlib.Topology.Algebra.Module.Equiv.Pi

Mathlib.Topology.Algebra.Module.Equiv.Prod

Mathlib.Topology.Algebra.Module.Equiv.Submodule

Mathlib.Topology.Algebra.Module.FiniteDimension

Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear

Mathlib.Topology.Algebra.Module.IsWeak

Mathlib.Topology.Algebra.Module.LinearPMap

Mathlib.Topology.Algebra.Module.LocallyConvex

Mathlib.Topology.Algebra.Module.ModuleTopology

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Mathlib.Topology.Algebra.Module.Multilinear.Topology

Mathlib.Topology.Algebra.Module.PerfectPairing

Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace

Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM

Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM

Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Mathlib.Topology.Algebra.Module.Spaces.WeakDual

Mathlib.Topology.Algebra.Module.Star

Mathlib.Topology.Algebra.Module.TransferInstance

Mathlib.Topology.Algebra.Monoid

Mathlib.Topology.Algebra.Monoid.Defs

Mathlib.Topology.Algebra.MulAction

Mathlib.Topology.Algebra.NonUnitalAlgebra

Mathlib.Topology.Algebra.NonUnitalStarAlgebra

Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Mathlib.Topology.Algebra.Nonarchimedean.Bases

Mathlib.Topology.Algebra.Nonarchimedean.Basic

Mathlib.Topology.Algebra.OpenSubgroup

Mathlib.Topology.Algebra.Order.UpperLower

Mathlib.Topology.Algebra.PontryaginDual

Mathlib.Topology.Algebra.ProperAction.Basic

Mathlib.Topology.Algebra.ProperConstSMul

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Mathlib.Topology.Algebra.RestrictedProduct.Units

Mathlib.Topology.Algebra.Ring.Basic

Mathlib.Topology.Algebra.Ring.Ideal

Mathlib.Topology.Algebra.SeparationQuotient.Basic

Mathlib.Topology.Algebra.SeparationQuotient.Hom

Mathlib.Topology.Algebra.SeparationQuotient.Section

Mathlib.Topology.Algebra.Star

Mathlib.Topology.Algebra.StarSubalgebra

Mathlib.Topology.Algebra.Support

Mathlib.Topology.Algebra.TopologicallyNilpotent

Mathlib.Topology.Algebra.UniformField

Mathlib.Topology.Algebra.UniformMulAction

Mathlib.Topology.Algebra.UniformRing

Mathlib.Topology.Algebra.ValuativeRel.Completion

Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Mathlib.Topology.Algebra.Valued.NormedValued

Mathlib.Topology.Algebra.Valued.ValuationTopology

Mathlib.Topology.Algebra.Valued.ValuedField

Mathlib.Topology.Algebra.Valued.WithVal

Mathlib.Topology.ApproximateUnit

Mathlib.Topology.Baire.BaireMeasurable

Mathlib.Topology.Bases

Mathlib.Topology.Bornology.Absorbs

Mathlib.Topology.Bornology.Basic

Mathlib.Topology.Bornology.BoundedOperation