Definitions: Mathlib.Topology, part 1 of 8

AffineSubspace.ofEqdefMathlib.Topology.Algebra.AffineSubspace, function or constant

Wording

the affine subspace of h2 (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the affine subspace of $h_{2}$ is a continuous affine equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {s}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {t}{x_{6}})}$.

AffineSubspace.subtypeAdefMathlib.Topology.Algebra.AffineSubspace, function or constant

Wording

the subtype of s (from the name)

English

Let $s$ be an affine subspace of $R$ and $P$. Then the subtype of $s$ is a continuous affine map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {s}{x_{5}})}$ and $P$.

ContinuousAffineEquiv.affineSubspaceMapdefMathlib.Topology.Algebra.AffineSubspace, function or constant

Wording

the affine subspace map of e and s (from the name)

English

Let $e$ be a continuous affine equivalence of $P$ and $Q$. Let $s$ be an affine subspace of $R$ and $P$. Then the affine subspace map of $e$ and $s$ is a continuous affine equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {s}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toAffineMap} (\operatorname{toAffineEquiv} (e)), s)}{x_{10}})}$.

Mathlib.Topology.Algebra.Algebra

Algebra.elementaldefMathlib.Topology.Algebra.Algebra, 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 subalgebra of $R$ and $A$ defined as the topological closure of $\operatorname{adjoin}$ applied to $R$ and $\operatorname{singleton}$ applied to $x_{4}$.

ContinuousAlgHomstructureMathlib.Topology.Algebra.Algebra, type

Wording

continuous algebra homomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the continuous algebra homomorphisms of $A$ and $B$ are a basic type.

ContinuousAlgHom.codRestrictdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

no wording

English

Let $f$ be a continuous algebra homomorphism of $A$ and $B$. Let $p$ be a subalgebra of $R$ and $B$ such that for all elements $x_{8}$ of $A$, $\MembershipmemMACRoT {p}{f (x_{8})}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $h$ is a continuous algebra homomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {p}{x_{7}})}$.

ContinuousAlgHom.compdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a continuous algebra homomorphism of $B$ and $C$. Let $f$ be a continuous algebra homomorphism of $A$ and $B$. Then the composition of $g$ and $f$ is a continuous algebra homomorphism of $A$ and $C$.

ContinuousAlgHom.copydefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a continuous algebra homomorphism of $A$ and $B$. Let $\mathrm{f'}$ be a function from elements of $A$ to elements of $B$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a continuous algebra homomorphism of $A$ and $B$.

ContinuousAlgHom.fstdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the first component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the first component of $A$ and $B$ is a continuous algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$ defined as $\operatorname{mk}$ applied to the first component of $A$ and $B$ and $\mathrm{continuous\_fst}$.

ContinuousAlgHom.iddefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the identity map of R and A (from the docstring)

English

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

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

Wording

the product of x10 and x11 (from the name)

English

Let $x_{10}$ be a continuous algebra homomorphism of $A$ and $B$. Let $x_{11}$ be a continuous algebra homomorphism of $A$ and $C$. Then the product of $x_{10}$ and $x_{11}$ is a continuous algebra homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

ContinuousAlgHom.prodEquivdefMathlib.Topology.Algebra.Algebra, 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 algebra homomorphisms of $A$ and $B$ and the set of continuous algebra homomorphisms of $A$ and $C$ to the set of continuous algebra homomorphisms of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

ContinuousAlgHom.prodMapdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the product map of x13 and x14 (from the name)

English

Let $x_{13}$ be a continuous algebra homomorphism of $A$ and $B$. Let $x_{14}$ be a continuous algebra homomorphism of $C$ and $D$. Then the product map of $x_{13}$ and $x_{14}$ is a continuous algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $C$ and $\mathrm{Prod}$ applied to $B$ and $D$ defined as the product of the composition of $x_{13}$ and the first component of $A$ and $C$ and the composition of $x_{14}$ and the second component of $A$ and $C$.

ContinuousAlgHom.rangeRestrictdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

no wording

English

Let $f$ be a continuous algebra homomorphism of $A$ and $B$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a continuous algebra homomorphism of $A$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{toAlgHom} (f))}{x_{7}})}$.

ContinuousAlgHom.restrictScalarsdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a continuous algebra homomorphism of $B$ and $C$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a continuous algebra homomorphism of $B$ and $C$.

ContinuousAlgHom.snddefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the second component of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the second component of $A$ and $B$ is a continuous algebra homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$ defined as $\operatorname{mk}$ applied to the second component of $A$ and $B$ and $\mathrm{continuous\_snd}$.

ContinuousAlgHom.toAlgHomMonoidHomdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the algebra homomorphism monoid homomorphism (from the name)

English

The algebra homomorphism monoid homomorphism is a monoid homomorphism of the set of continuous algebra homomorphisms of $A$ and $A$ and the set of algebra homomorphisms of $A$ and $A$.

ContinuousAlgHom.toContinuousLinearMapdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the continuous linear map of e (from the name)

English

Let $e$ be a continuous algebra homomorphism of $A$ and $B$. Then the continuous linear map of $e$ is a continuous linear map of $A$ and $B$.

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

Wording

the topological closure of s (from the docstring)

English

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

Subalgebra.valAdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the value of p (from the name)

English

Let $p$ be a subalgebra of $R$ and $A$. Then the value of $p$ is a continuous algebra homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$ and $A$.

algebraMapCLMdefMathlib.Topology.Algebra.Algebra, function or constant

Wording

the inclusion of the base ring of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the inclusion of the base ring of $R$ and $A$ is a continuous linear map of $R$ and $A$.

Mathlib.Topology.Algebra.Algebra.Equiv

ContinuousAlgEquivstructureMathlib.Topology.Algebra.Algebra.Equiv, type

Wording

continuous algebra isomorphism of A and B (from the name)

English

Let $R$, $A$ and $B$ be sets. Then the continuous algebra isomorphisms of $A$ and $B$ are a basic type.

ContinuousAlgEquiv.castdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the cast of h (from the name)

English

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is a continuous algebra isomorphism of $A$ applied to $i$ and $A$ applied to $j$.

ContinuousAlgEquiv.refldefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the identity isomorphism of R and A (from the docstring)

English

Let $R$ and $A$ be sets. Then the identity isomorphism of $R$ and $A$ is a continuous algebra isomorphism of $A$ and $A$ defined as $\operatorname{mk}$ applied to the identity, $\mathrm{continuous\_id}$ and $\mathrm{continuous\_id}$.

ContinuousAlgEquiv.symmdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the inverse of e (from the docstring)

English

Let $e$ be a continuous algebra isomorphism of $A$ and $B$. Then the inverse of $e$ is a continuous algebra isomorphism of $B$ and $A$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toAlgEquiv}$ applied to $e$, $\mathrm{ContinuousAlgEquiv\_\_continuous\_invFun}$ applied to $e$ and $\mathrm{ContinuousAlgEquiv\_\_continuous\_toFun}$ applied to $e$.

ContinuousAlgEquiv.toContinuousAlgHomdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the continuous algebra homomorphism of e (from the name)

English

Let $e$ be a continuous algebra isomorphism of $A$ and $B$. Then the continuous algebra homomorphism of $e$ is a continuous algebra homomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to the algebra homomorphism of $\operatorname{toAlgEquiv}$ applied to $e$ and $\mathrm{ContinuousAlgEquiv\_\_continuous\_toFun}$ applied to $e$.

ContinuousAlgEquiv.toContinuousLinearEquivdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the continuous linear equivalence of e (from the name)

English

Let $e$ be a continuous algebra isomorphism of $A$ and $B$. Then the continuous linear equivalence of $e$ is a continuous linear equivalence of $A$ and $B$.

ContinuousAlgEquiv.toHomeomorphdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the homeomorphism of self (from the name)

English

Let $\mathrm{self}$ be a continuous algebra isomorphism of $A$ and $B$. Then the homeomorphism of $\mathrm{self}$ is a homeomorphism of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toAlgEquiv}$ applied to $\mathrm{self}$, $\mathrm{ContinuousAlgEquiv\_\_continuous\_toFun}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousAlgEquiv\_\_continuous\_invFun}$ applied to $\mathrm{self}$.

ContinuousAlgEquiv.transdefMathlib.Topology.Algebra.Algebra.Equiv, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a continuous algebra isomorphism of $A$ and $B$. Let $x_{11}$ be a continuous algebra isomorphism of $B$ and $C$. Then the composition of $x_{10}$ and $x_{11}$ is a continuous algebra isomorphism of $A$ and $C$.

ContinuousAlgEquivClassclassMathlib.Topology.Algebra.Algebra.Equiv, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$, $A$ and $B$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ContinuousAlgEquivClass}$ holds for $F$, $R$, $A$ and $B$.

Mathlib.Topology.Algebra.AsymptoticCone

AffineSpace.asymptoticNhdsdefMathlib.Topology.Algebra.AsymptoticCone, function or constant

Wording

the asymptotic neighbourhood filter of v (from the name)

English

Let $k$ and $P$ be sets. Let $v$ be an element of $V$. Then the asymptotic neighbourhood filter of $v$ is a filter of $P$ defined as the supremum of the function that maps $p$ to the sum of $\HSMulhSMulMACRoAL {\operatorname{atTop}}{\mathrm{nhds} (v)}$ and $\operatorname{pure}$ applied to $p$.

asymptoticConedefMathlib.Topology.Algebra.AsymptoticCone, function or constant

Wording

the asymptotic cone of k and s (from the name)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then the asymptotic cone of $k$ and $s$ is an element of $\wp V$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to $\operatorname{Frequently}$ applied to the function that maps $p$ to $\MembershipmemMACRoT {s}{p}$ and the asymptotic neighbourhood filter of $v$.

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

ProfiniteAddGrpstructureMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, type

Wording

profinite additive group (from the name)

English

The profinite additive groups are a basic type.

ProfiniteAddGrp.ContinuousMulEquiv.toProfiniteAddGrpIsodefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group isomorphism of e (from the name)

English

Let $e$ be a continuous additive equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $X$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $Y$. Then the profinite additive group isomorphism of $e$ is an isomorphism of $X$ and $Y$.

ProfiniteAddGrp.HomstructureMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be profinite additive groups. Then the homomorphisms of $A$ and $B$ are a basic type.

ProfiniteAddGrp.Hom.homdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $M$ and $N$. Then the homomorphism of $f$ is a continuous additive monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $M$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $N$ defined as the homomorphism of $f$.

ProfiniteAddGrp.Hom.hom'defMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a continuous additive monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $A$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ProfiniteAddGrp.limitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the abbreviation for the limit of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite additive groups. Then the abbreviation for the limit of $F$ is a profinite additive group defined as $\operatorname{of}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{limitConePtAux} (F)}{x_{1}})}$.

ProfiniteAddGrp.limitConedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the explicit limit cone in F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite additive groups. Then the explicit limit cone in $F$ is a cone of $F$.

ProfiniteAddGrp.limitConeIsLimitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the limit cone of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite additive groups. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the explicit limit cone in $F$.

ProfiniteAddGrp.ofdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{of}$ applied to $G$ is a profinite additive group defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $G$.

ProfiniteAddGrp.ofClosedAddSubgroupdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of H (from the name)

English

Let $H$ be a closed additive subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $G$. Then the profinite additive group of $H$ is a profinite additive group defined as $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{toAddSubgroup} (H)}{x})}$.

ProfiniteAddGrp.ofContinuousAddEquivdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of e (from the name)

English

Let $e$ be a continuous additive equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $G$ and $H$. Then the profinite additive group of $e$ is a profinite additive group defined as $\operatorname{of}$ applied to $H$.

ProfiniteAddGrp.ofFiniteAddGrpdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of G (from the name)

English

Let $G$ be a finite additive group. Then the profinite additive group of $G$ is a profinite additive group defined as $\operatorname{of}$ applied to the set of carriers of the additive group of $G$.

ProfiniteAddGrp.ofFiniteAddGrpHomdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of f (from the name)

English

Let $f$ be a homomorphism of $G$ and $H$. Then the profinite additive group of $f$ is a homomorphism of the profinite additive group of $G$ and the profinite additive group of $H$.

ProfiniteAddGrp.ofHomdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of f (from the name)

English

Let $f$ be a continuous additive monoid homomorphism of $X$ and $Y$. Then the profinite additive group of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.

ProfiniteAddGrp.ofProfinitedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite additive group of G (from the name)

English

Let $G$ be an element of $\mathrm{Profinite}$. Then the profinite additive group of $G$ is a profinite additive group defined as $\operatorname{of}$ applied to the set of carriers of the underlying topological space of $G$.

ProfiniteAddGrp.pidefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the product of x1 (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to profinite additive groups. Then the product of $x_{1}$ is a profinite additive group defined as the profinite additive group of the product of the function that maps $a$ to the underlying profinite topological space of $x_{1}$ applied to $a$.

ProfiniteAddGrp.toProfinitedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the underlying profinite topological space of self (from the docstring)

English

Let $\mathrm{self}$ be a profinite additive group. Then the underlying profinite topological space of $\mathrm{self}$ is an element of $\mathrm{Profinite}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ProfiniteGrpstructureMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, type

Wording

profinite group (from the name)

English

The profinite groups are a basic type.

ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIsodefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group isomorphism of e (from the name)

English

Let $e$ be a continuous multiplicative equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $X$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $Y$. Then the profinite group isomorphism of $e$ is an isomorphism of $X$ and $Y$.

ProfiniteGrp.HomstructureMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, type

Wording

homomorphism of A and B (from the name)

English

Let $A$ and $B$ be profinite groups. Then the homomorphisms of $A$ and $B$ are a basic type.

ProfiniteGrp.Hom.homdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $M$ and $N$. Then the homomorphism of $f$ is a continuous monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $M$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $N$ defined as the homomorphism of $f$.

ProfiniteGrp.Hom.hom'defMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $A$ and $B$. Then the homomorphism of $\mathrm{self}$ is a continuous monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $A$ and the set of carriers of the underlying topological space of the underlying profinite topological space of $B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ProfiniteGrp.limitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the abbreviation for the limit of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite groups. Then the abbreviation for the limit of $F$ is a profinite group defined as $\operatorname{of}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{limitConePtAux} (F)}{x_{1}})}$.

ProfiniteGrp.limitConedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the explicit limit cone in F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite groups. Then the explicit limit cone in $F$ is a cone of $F$.

ProfiniteGrp.limitConeIsLimitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the limit cone of F (from the docstring)

English

Let $F$ be a functor of $J$ and the set of profinite groups. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the explicit limit cone in $F$.

ProfiniteGrp.ofdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{of}$ applied to $G$ is a profinite group defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $G$.

ProfiniteGrp.ofClosedSubgroupdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of H (from the name)

English

Let $H$ be a closed subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $G$. Then the profinite group of $H$ is a profinite group defined as $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{toSubgroup} (H)}{x})}$.

ProfiniteGrp.ofContinuousMulEquivdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of e (from the name)

English

Let $e$ be a continuous multiplicative equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $G$ and $H$. Then the profinite group of $e$ is a profinite group defined as $\operatorname{of}$ applied to $H$.

ProfiniteGrp.ofFiniteGrpdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of G (from the name)

English

Let $G$ be a finite group. Then the profinite group of $G$ is a profinite group defined as $\operatorname{of}$ applied to the set of carriers of the group of $G$.

ProfiniteGrp.ofFiniteGrpHomdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of f (from the name)

English

Let $f$ be a homomorphism of $G$ and $H$. Then the profinite group of $f$ is a homomorphism of the profinite group of $G$ and the profinite group of $H$.

ProfiniteGrp.ofHomdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of f (from the name)

English

Let $f$ be a continuous monoid homomorphism of $X$ and $Y$. Then the profinite group of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.

ProfiniteGrp.ofProfinitedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the profinite group of G (from the name)

English

Let $G$ be an element of $\mathrm{Profinite}$. Then the profinite group of $G$ is a profinite group defined as $\operatorname{of}$ applied to the set of carriers of the underlying topological space of $G$.

ProfiniteGrp.pidefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the product of x1 (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to profinite groups. Then the product of $x_{1}$ is a profinite group defined as the profinite group of the product of the function that maps $a$ to the underlying profinite topological space of $x_{1}$ applied to $a$.

ProfiniteGrp.toProfinitedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Basic, function or constant

Wording

the underlying profinite topological space of self (from the docstring)

English

Let $\mathrm{self}$ be a profinite group. Then the underlying profinite topological space of $\mathrm{self}$ is an element of $\mathrm{Profinite}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroupdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the finite index normal additive subgroup of H (from the name)

English

Let $H$ be an open normal additive subgroup of $G$. Then the finite index normal additive subgroup of $H$ is a finite index normal additive subgroup of $G$ defined as the finite index normal additive subgroup of $\operatorname{toAddSubgroup}$ applied to $\operatorname{toOpenAddSubgroup}$ applied to $H$.

OpenNormalSubgroup.toFiniteIndexNormalSubgroupdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the finite index normal subgroup of H (from the name)

English

Let $H$ be an open normal subgroup of $G$. Then the finite index normal subgroup of $H$ is a finite index normal subgroup of $G$ defined as the finite index normal subgroup of $\operatorname{toSubgroup}$ applied to $\operatorname{toOpenSubgroup}$ applied to $H$.

ProfiniteAddGrp.ProfiniteCompletion.adjunctiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the adjunction (from the name)

English

The adjunction is an adjunction of the profinite completion functor and the forgetful functor of the set of profinite additive groups and the set of additive group categories.

ProfiniteAddGrp.ProfiniteCompletion.completiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the profinite completion of G (from the docstring)

English

Let $G$ be an additive group category. Then the profinite completion of $G$ is a profinite additive group defined as the abbreviation for the limit of the diagram of $G$.

ProfiniteAddGrp.ProfiniteCompletion.diagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the diagram of G (from the name)

English

Let $G$ be an additive group category. Then the diagram of $G$ is a functor of the set of finite index normal additive subgroups of the set of carriers of $G$ and the set of profinite additive groups defined as the composition of the finite additive group diagram of $G$ and the forgetful functor of the set of finite additive groups and the set of profinite additive groups.

ProfiniteAddGrp.ProfiniteCompletion.etadefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

no wording

English

Let $G$ be an additive group category. Then $\operatorname{eta}$ applied to $G$ is a homomorphism of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of the profinite completion of $G$.

ProfiniteAddGrp.ProfiniteCompletion.etaFndefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

no wording

English

Let $G$ be an additive group category. Let $x$ be a carrier of $G$. Then $\operatorname{etaFn}$ applied to $G$ and $x$ is a carrier of the underlying topological space of the underlying profinite topological space of the profinite completion of $G$ defined as the function that maps $x_{1}$ to $\operatorname{mk}$ applied to $x$.

ProfiniteAddGrp.ProfiniteCompletion.finiteAddGrpDiagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the finite additive group diagram of G (from the name)

English

Let $G$ be an additive group category. Then the finite additive group diagram of $G$ is a functor of the set of finite index normal additive subgroups of the set of carriers of $G$ and the set of finite additive groups.

ProfiniteAddGrp.ProfiniteCompletion.homEquivdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the homomorphism equivalence of G and P (from the name)

English

Let $G$ be an additive group category. Let $P$ be a profinite additive group. Then the homomorphism equivalence of $G$ and $P$ is an equivalence from the set of homomorphisms of the profinite completion of $G$ and $P$ to the set of homomorphisms of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of $P$.

ProfiniteAddGrp.ProfiniteCompletion.liftdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the lift of f (from the name)

English

ProfiniteAddGrp.ProfiniteCompletion.preimagedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the preimage of f and H (from the docstring)

English

ProfiniteAddGrp.ProfiniteCompletion.quotientMapdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the quotient map of f and H (from the name)

English

Let $f$ be a homomorphism of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Let $H$ be an open normal additive subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Then the quotient map of $f$ and $H$ is a homomorphism of $\operatorname{of}$ applied to the set of quotients of the set of carriers of $G$ and $\operatorname{toAddSubgroup}$ applied to the preimage of $f$ and $H$ and $\operatorname{of}$ applied to the set of quotients of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and $\operatorname{toAddSubgroup}$ applied to $\operatorname{toOpenAddSubgroup}$ applied to $H$ defined as the finite additive group of the map of $\operatorname{toAddSubgroup}$ applied to $\operatorname{toOpenAddSubgroup}$ applied to $H$ and the homomorphism of $f$.

ProfiniteAddGrp.profiniteCompletiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the profinite completion functor (from the docstring)

English

The profinite completion functor is a functor of the set of additive group categories and the set of profinite additive groups.

ProfiniteGrp.ProfiniteCompletion.adjunctiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the adjunction (from the name)

English

The adjunction is an adjunction of the profinite completion functor and the forgetful functor of the set of profinite groups and the set of group categories.

ProfiniteGrp.ProfiniteCompletion.completiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the profinite completion of G (from the docstring)

English

Let $G$ be a group category. Then the profinite completion of $G$ is a profinite group defined as the abbreviation for the limit of the diagram of $G$.

ProfiniteGrp.ProfiniteCompletion.diagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the diagram of G (from the name)

English

Let $G$ be a group category. Then the diagram of $G$ is a functor of the set of finite index normal subgroups of the set of carriers of $G$ and the set of profinite groups defined as the composition of the finite group diagram of $G$ and the forgetful functor of the set of finite groups and the set of profinite groups.

ProfiniteGrp.ProfiniteCompletion.etadefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

no wording

English

Let $G$ be a group category. Then $\operatorname{eta}$ applied to $G$ is a homomorphism of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of the profinite completion of $G$.

ProfiniteGrp.ProfiniteCompletion.etaFndefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

no wording

English

Let $G$ be a group category. Let $x$ be a carrier of $G$. Then $\operatorname{etaFn}$ applied to $G$ and $x$ is a carrier of the underlying topological space of the underlying profinite topological space of the profinite completion of $G$ defined as the function that maps $x_{1}$ to $\operatorname{mk}$ applied to $x$.

ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the finite group diagram of G (from the name)

English

Let $G$ be a group category. Then the finite group diagram of $G$ is a functor of the set of finite index normal subgroups of the set of carriers of $G$ and the set of finite groups.

ProfiniteGrp.ProfiniteCompletion.homEquivdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the homomorphism equivalence of G and P (from the name)

English

Let $G$ be a group category. Let $P$ be a profinite group. Then the homomorphism equivalence of $G$ and $P$ is an equivalence from the set of homomorphisms of the profinite completion of $G$ and $P$ to the set of homomorphisms of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of $P$.

ProfiniteGrp.ProfiniteCompletion.liftdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the lift of f (from the name)

English

ProfiniteGrp.ProfiniteCompletion.preimagedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the preimage of f and H (from the docstring)

English

ProfiniteGrp.ProfiniteCompletion.quotientMapdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the quotient map of f and H (from the name)

English

Let $f$ be a homomorphism of $G$ and $\operatorname{of}$ applied to the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Let $H$ be an open normal subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Then the quotient map of $f$ and $H$ is a homomorphism of $\operatorname{of}$ applied to the set of quotients of the set of carriers of $G$ and $\operatorname{toSubgroup}$ applied to the preimage of $f$ and $H$ and $\operatorname{of}$ applied to the set of quotients of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and $\operatorname{toSubgroup}$ applied to $\operatorname{toOpenSubgroup}$ applied to $H$ defined as the finite group of the map of $\operatorname{toSubgroup}$ applied to $\operatorname{toOpenSubgroup}$ applied to $H$ and the homomorphism of $f$.

ProfiniteGrp.profiniteCompletiondefMathlib.Topology.Algebra.Category.ProfiniteGrp.Completion, function or constant

Wording

the profinite completion functor (from the docstring)

English

The profinite completion functor is a functor of the set of group categories and the set of profinite groups.

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

ProfiniteAddGrp.conedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the cone of P (from the name)

English

Let $P$ be a profinite additive group. Then the cone of $P$ is a cone of the diagram of $P$.

ProfiniteAddGrp.continuousAddEquivLimittoFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite additive group. Then $\operatorname{continuousAddEquivLimittoFiniteQuotientFunctor}$ applied to $P$ is a continuous additive equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of the diagram of $P$.

ProfiniteAddGrp.diagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the diagram of P (from the name)

English

Let $P$ be a profinite additive group. Then the diagram of $P$ is a functor of the set of open normal additive subgroups of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of profinite additive groups defined as the composition of the finite quotient functor of $P$ and the forgetful functor of the set of finite additive groups and the set of profinite additive groups.

ProfiniteAddGrp.isLimitConedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite additive group. Then $\operatorname{isLimitCone}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to the cone of $P$.

ProfiniteAddGrp.isoLimittoFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite additive group. Then $\operatorname{isoLimittoFiniteQuotientFunctor}$ applied to $P$ is an isomorphism of $P$ and the abbreviation for the limit of the diagram of $P$ defined as the profinite additive group isomorphism of $\operatorname{continuousAddEquivLimittoFiniteQuotientFunctor}$ applied to $P$.

ProfiniteAddGrp.projdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the projection of U (from the name)

English

Let $U$ be an open normal additive subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Then the projection of $U$ is a homomorphism of $P$ and the action of the diagram of $P$ and $U$.

ProfiniteAddGrp.toFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the finite quotient functor of P (from the name)

English

Let $P$ be a profinite additive group. Then the finite quotient functor of $P$ is a functor of the set of open normal additive subgroups of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of finite additive groups.

ProfiniteAddGrp.toLimitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the limit of P (from the name)

English

Let $P$ be a profinite additive group. Then the limit of $P$ is a homomorphism of $P$ and the abbreviation for the limit of the diagram of $P$ defined as the profinite additive group of $\operatorname{mk}$ applied to the limit function of $P$ and $\mathrm{ProfiniteAddGrp\_\_toLimitFun\_continuous}$ applied to $P$.

ProfiniteAddGrp.toLimitFundefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the limit function of P (from the name)

English

Let $P$ be a profinite additive group. Then the limit function of $P$ is an additive monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of the diagram of $P$.

ProfiniteGrp.conedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the cone of P (from the name)

English

Let $P$ be a profinite group. Then the cone of $P$ is a cone of the diagram of $P$.

ProfiniteGrp.continuousMulEquivLimittoFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite group. Then $\operatorname{continuousMulEquivLimittoFiniteQuotientFunctor}$ applied to $P$ is a continuous multiplicative equivalence of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of the diagram of $P$.

ProfiniteGrp.diagramdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the diagram of P (from the name)

English

Let $P$ be a profinite group. Then the diagram of $P$ is a functor of the set of open normal subgroups of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of profinite groups defined as the composition of the finite quotient functor of $P$ and the forgetful functor of the set of finite groups and the set of profinite groups.

ProfiniteGrp.isLimitConedefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite group. Then $\operatorname{isLimitCone}$ applied to $P$ is an element of $\operatorname{IsLimit}$ applied to the cone of $P$.

ProfiniteGrp.isoLimittoFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

no wording

English

Let $P$ be a profinite group. Then $\operatorname{isoLimittoFiniteQuotientFunctor}$ applied to $P$ is an isomorphism of $P$ and the abbreviation for the limit of the diagram of $P$ defined as the profinite group isomorphism of $\operatorname{continuousMulEquivLimittoFiniteQuotientFunctor}$ applied to $P$.

ProfiniteGrp.projdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the projection of U (from the name)

English

Let $U$ be an open normal subgroup of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$. Then the projection of $U$ is a homomorphism of $P$ and the action of the diagram of $P$ and $U$.

ProfiniteGrp.toFiniteQuotientFunctordefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the finite quotient functor of P (from the name)

English

Let $P$ be a profinite group. Then the finite quotient functor of $P$ is a functor of the set of open normal subgroups of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of finite groups.

ProfiniteGrp.toLimitdefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the limit of P (from the name)

English

Let $P$ be a profinite group. Then the limit of $P$ is a homomorphism of $P$ and the abbreviation for the limit of the diagram of $P$ defined as the profinite group of $\operatorname{mk}$ applied to the limit function of $P$ and $\mathrm{ProfiniteGrp\_\_toLimitFun\_continuous}$ applied to $P$.

ProfiniteGrp.toLimitFundefMathlib.Topology.Algebra.Category.ProfiniteGrp.Limits, function or constant

Wording

the limit function of P (from the name)

English

Let $P$ be a profinite group. Then the limit function of $P$ is a monoid homomorphism of the set of carriers of the underlying topological space of the underlying profinite topological space of $P$ and the set of carriers of the underlying topological space of the underlying profinite topological space of the abbreviation for the limit of the diagram of $P$.

Mathlib.Topology.Algebra.ConstMulAction

ContinuousConstSMulclassMathlib.Topology.Algebra.ConstMulAction, predicate

Wording

no wording

English

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

ContinuousConstVAddclassMathlib.Topology.Algebra.ConstMulAction, predicate

Wording

no wording

English

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

Homeomorph.smuldefMathlib.Topology.Algebra.ConstMulAction, function or constant

Wording

the scalar multiple of x4 (from the name)

English

Let $x_{4}$ be an element of $G$. Then the scalar multiple of $x_{4}$ is a homeomorphism of $x$ and $x$.

Homeomorph.smulOfNeZerodefMathlib.Topology.Algebra.ConstMulAction, function or constant

Wording

the scalar multiple of c and hc (from the name)

English

Let $c$ be an element of $x_{1}$ such that $c \neq 0$. Then the scalar multiple of $c$ and $\mathrm{hc}$ is a homeomorphism of $x$ and $x$ defined as the scalar multiple of $\operatorname{mk0}$ applied to $c$ and $\mathrm{hc}$.

Homeomorph.vadddefMathlib.Topology.Algebra.ConstMulAction, function or constant

Wording

the vector sum of x4 (from the name)

English

Let $x_{4}$ be an element of $G$. Then the vector sum of $x_{4}$ is a homeomorphism of $x$ and $x$.

ProperlyDiscontinuousSMulclassMathlib.Topology.Algebra.ConstMulAction, predicate

Wording

no wording

English

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

ProperlyDiscontinuousVAddclassMathlib.Topology.Algebra.ConstMulAction, predicate

Wording

no wording

English

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

Mathlib.Topology.Algebra.Constructions

AddOpposite.opHomeomorphdefMathlib.Topology.Algebra.Constructions, function or constant

Wording

the opposite homeomorphism (from the name)

English

The opposite homeomorphism is a homeomorphism of $M$ and the set of additive opposites of $M$.

MulOpposite.opHomeomorphdefMathlib.Topology.Algebra.Constructions, function or constant

Wording

the opposite homeomorphism (from the name)

English

The opposite homeomorphism is a homeomorphism of $M$ and the set of multiplicative opposites of $M$.

Mathlib.Topology.Algebra.Constructions.DomMulAct

DomAddAct.mkHomeomorphdefMathlib.Topology.Algebra.Constructions.DomMulAct, function or constant

Wording

the homeomorphism (from the name)

English

The homeomorphism is a homeomorphism of $M$ and $\mathrm{DomAddAct}$ applied to $M$.

DomMulAct.mkHomeomorphdefMathlib.Topology.Algebra.Constructions.DomMulAct, function or constant

Wording

the homeomorphism (from the name)

English

The homeomorphism is a homeomorphism of $M$ and $\mathrm{DomMulAct}$ applied to $M$.

Mathlib.Topology.Algebra.ContinuousAffineEquiv

ContinuousAffineEquivstructureMathlib.Topology.Algebra.ContinuousAffineEquiv, type

Wording

continuous affine equivalence of x and x1 (from the name)

English

Let $k$, $x$ and $x_{1}$ be sets. Then the continuous affine equivalences of $x$ and $x_{1}$ are a basic type.

ContinuousAffineEquiv.constVAdddefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the constant sum of v (from the name)

English

Let $k$ and $x$ be sets. Let $v$ be an element of $x_{1}$. Then the constant sum of $v$ is a continuous affine equivalence of $x$ and $x$.

ContinuousAffineEquiv.constVSubdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the constant difference of k and p (from the name)

English

Let $k$ be a set. Let $p$ be an element of $x$. Then the constant difference of $k$ and $p$ is a continuous affine equivalence of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the constant difference of $k$ and $p$, $\mathrm{Homeomorph\_\_continuous\_toFun}$ applied to the constant difference of $p$ and $\mathrm{Homeomorph\_\_continuous\_invFun}$ applied to the constant difference of $p$.

ContinuousAffineEquiv.pointReflectiondefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the point reflection of k and x8 (from the name)

English

Let $k$ be a set. Let $x_{8}$ be an element of $x$. Then the point reflection of $k$ and $x_{8}$ is a continuous affine equivalence of $x$ and $x$ defined as the composition of the constant difference of $k$ and $x_{8}$ and the vector sum constant of $k$ and $x_{8}$.

ContinuousAffineEquiv.prodAssocdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the product associator of x1 and x2 (from the name)

English

Let $k$, $x$, $x_{1}$ and $x_{2}$ be sets. Then the product associator of $x_{1}$ and $x_{2}$ is a continuous affine equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

ContinuousAffineEquiv.prodCommdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

no wording

English

Let $k$, $x$ and $x_{1}$ be sets. Then $\operatorname{prodComm}$ applied to $k$, $x$ and $x_{1}$ is a continuous affine equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{prodComm}$ applied to $k$, $x$ and $x_{1}$, $\mathrm{continuous\_swap}$ and $\mathrm{continuous\_swap}$.

ContinuousAffineEquiv.prodCongrdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the product congruence of x25 and x26 (from the name)

English

Let $x_{25}$ be a continuous affine equivalence of $x$ and $x_{1}$. Let $x_{26}$ be a continuous affine equivalence of $x_{2}$ and $x_{3}$. Then the product congruence of $x_{25}$ and $x_{26}$ is a continuous affine equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.

ContinuousAffineEquiv.refldefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the identity of k and x (from the name)

English

Let $k$ and $x$ be sets. Then the identity of $k$ and $x$ is a continuous affine equivalence of $x$ and $x$.

ContinuousAffineEquiv.symmdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be a continuous affine equivalence of $x$ and $x_{1}$. Then the inverse of $e$ is a continuous affine equivalence of $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toAffineEquiv}$ applied to $e$, $\mathrm{ContinuousAffineEquiv\_\_continuous\_invFun}$ applied to $e$ and $\mathrm{ContinuousAffineEquiv\_\_continuous\_toFun}$ applied to $e$.

ContinuousAffineEquiv.toContinuousAffineMapdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the continuous affine map of e (from the name)

English

Let $e$ be a continuous affine equivalence of $x$ and $x_{1}$. Then the continuous affine map of $e$ is a continuous affine map of $x$ and $x_{1}$.

ContinuousAffineEquiv.toHomeomorphdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be a continuous affine equivalence of $x$ and $x_{1}$. Then the homeomorphism of $e$ is a homeomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toAffineEquiv}$ applied to $e$, $\mathrm{ContinuousAffineEquiv\_\_continuous\_toFun}$ applied to $e$ and $\mathrm{ContinuousAffineEquiv\_\_continuous\_invFun}$ applied to $e$.

ContinuousAffineEquiv.transdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the composition of e and #2 (from the name)

English

Let $e$ be a continuous affine equivalence of $x$ and $x_{1}$. Let $\mathrm{e'}$ be a continuous affine equivalence of $x_{1}$ and $x_{2}$. Then the composition of $e$ and $\mathrm{e'}$ is a continuous affine equivalence of $x$ and $x_{2}$.

ContinuousAffineEquiv.vaddConstdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the vector sum constant of k and p (from the name)

English

Let $k$ be a set. Let $p$ be an element of $x$. Then the vector sum constant of $k$ and $p$ is a continuous affine equivalence of $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to the vector sum constant of $k$ and $p$, $\mathrm{Homeomorph\_\_continuous\_toFun}$ applied to the vector sum constant of $p$ and $\mathrm{Homeomorph\_\_continuous\_invFun}$ applied to the vector sum constant of $p$.

ContinuousLinearEquiv.toContinuousAffineEquivdefMathlib.Topology.Algebra.ContinuousAffineEquiv, function or constant

Wording

the continuous affine equivalence of L (from the name)

English

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

Mathlib.Topology.Algebra.ContinuousAffineMap

ContinuousAffineMapstructureMathlib.Topology.Algebra.ContinuousAffineMap, type

Wording

continuous affine map of P and Q (from the name)

English

Let $R$, $P$ and $Q$ be sets. Then the continuous affine maps of $P$ and $Q$ are a basic type.

ContinuousAffineMap.compdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a continuous affine map of $Q$ and $x_{10}$. Let $g$ be a continuous affine map of $P$ and $Q$. Then the composition of $f$ and $g$ is a continuous affine map of $P$ and $x_{10}$.

ContinuousAffineMap.constdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the constant of q (from the name)

English

Let $R$ and $P$ be sets. Let $q$ be an element of $Q$. Then the constant of $q$ is a continuous affine map of $P$ and $Q$ defined as $\operatorname{mk}$ applied to the constant of $q$ and $\mathrm{continuous\_const}$.

ContinuousAffineMap.contLineardefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

no wording

English

Let $f$ be a continuous affine map of $P$ and $Q$. Then $\operatorname{contLinear}$ applied to $f$ is a continuous linear map of $V$ and $W$.

ContinuousAffineMap.decompAffineEquivdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the decomposition affine equivalence of V and Q (from the name)

English

Let $R$, $S$, $V$ and $Q$ be sets. Then the decomposition affine equivalence of $V$ and $Q$ is an affine equivalence of the set of continuous affine maps of $V$ and $Q$ and $\mathrm{Prod}$ applied to $Q$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.decompEquivdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the decomposition equivalence of V and Q (from the name)

English

Let $R$, $V$ and $Q$ be sets. Then the decomposition equivalence of $V$ and $Q$ is an equivalence from the set of continuous affine maps of $V$ and $Q$ to $\mathrm{Prod}$ applied to $Q$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.decompLinearEquivdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the decomposition linear equivalence of V and W (from the name)

English

Let $R$, $S$, $V$ and $W$ be sets. Then the decomposition linear equivalence of $V$ and $W$ is a linear equivalence of the set of continuous affine maps of $V$ and $W$ and $\mathrm{Prod}$ applied to $W$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.iddefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the identity map of R and P (from the docstring)

English

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

ContinuousAffineMap.lineMapdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the line map of x5 and x6 (from the name)

English

Let $x_{5}$ and $x_{6}$ be elements of $P$. Then the line map of $x_{5}$ and $x_{6}$ is a continuous affine map of $R$ and $P$.

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

Wording

the product of f and g (from the name)

English

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

ContinuousAffineMap.prodMapdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the product map of f and g (from the name)

English

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

ContinuousAffineMap.toContinuousMapdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the continuous map of f (from the name)

English

Let $f$ be a continuous affine map of $P$ and $Q$. Then the continuous map of $f$ is a continuous map of $P$ and $Q$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{cont}$ applied to $f$.

ContinuousLinearMap.toContinuousAffineMapdefMathlib.Topology.Algebra.ContinuousAffineMap, function or constant

Wording

the continuous affine map of f (from the name)

English

Let $f$ be a continuous linear map of $V$ and $W$. Then the continuous affine map of $f$ is a continuous affine map of $V$ and $W$.

Mathlib.Topology.Algebra.ContinuousAffineMap.Topology

ContinuousAffineMap.decompContinuousAffineEquivdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the decomposition continuous affine equivalence of V and Q (from the name)

English

Let $R$, $V$ and $Q$ be sets. Then the decomposition continuous affine equivalence of $V$ and $Q$ is a continuous affine equivalence of the set of continuous affine maps of $V$ and $Q$ and $\mathrm{Prod}$ applied to $Q$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.decompContinuousLinearEquivdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the decomposition continuous linear equivalence of V and W (from the name)

English

Let $R$, $V$ and $W$ be sets. Then the decomposition continuous linear equivalence of $V$ and $W$ is a continuous linear equivalence of the set of continuous affine maps of $V$ and $W$ and $\mathrm{Prod}$ applied to $W$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.decompHomeomorphdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the decomposition homeomorphism of V and Q (from the name)

English

Let $R$, $V$ and $Q$ be sets. Then the decomposition homeomorphism of $V$ and $Q$ is a homeomorphism of the set of continuous affine maps of $V$ and $Q$ and $\mathrm{Prod}$ applied to $Q$ and the set of continuous linear maps of $V$ and $W$.

ContinuousAffineMap.postcompAdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the postcomposition of P and f (from the name)

English

Let $P$ be a set. Let $f$ be a continuous affine map of $Q$ and $x_{1}$. Then the postcomposition of $P$ and $f$ is a continuous affine map of the set of continuous affine maps of $P$ and $Q$ and the set of continuous affine maps of $P$ and $x_{1}$.

ContinuousAffineMap.precompAdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the precomposition of x1 and g (from the name)

English

Let $x_{1}$ be a set. Let $g$ be a continuous affine map of $P$ and $Q$. Then the precomposition of $x_{1}$ and $g$ is a continuous affine map of the set of continuous affine maps of $Q$ and $x_{1}$ and the set of continuous affine maps of $P$ and $x_{1}$.

ContinuousAffineMap.precompLdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the precomposition of x and g (from the name)

English

Let $x$ be a set. Let $g$ be a continuous affine map of $P$ and $Q$. Then the precomposition of $x$ and $g$ is a continuous linear map of the set of continuous affine maps of $Q$ and $x$ and the set of continuous affine maps of $P$ and $x$.

ContinuousLinearMap.postcompContinuousAffineMapdefMathlib.Topology.Algebra.ContinuousAffineMap.Topology, function or constant

Wording

the postcomposition continuous affine map of P and f (from the name)

English

Let $P$ be a set. Let $f$ be a continuous linear map of $W$ and $x$. Then the postcomposition continuous affine map of $P$ and $f$ is a continuous linear map of the set of continuous affine maps of $P$ and $W$ and the set of continuous affine maps of $P$ and $x$.

Mathlib.Topology.Algebra.ContinuousMonoidHom

AddEquiv.toContinuousAddEquivdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous additive equivalence of e and he (from the name)

English

Let $e$ be an additive equivalence of $G$ and $H$ such that for all elements $s$ of $\wp H$, the preimage of $\operatorname{coe}$ applied to $e$ and $s$ is open, if and only if $s$ is open. Then the continuous additive equivalence of $e$ and $\mathrm{he}$ is a continuous additive equivalence of $G$ and $H$.

ContinuousAddEquivstructureMathlib.Topology.Algebra.ContinuousMonoidHom, type

Wording

continuous additive equivalence of G and H (from the name)

English

Let $G$ and $H$ be sets. Then the continuous additive equivalences of $G$ and $H$ are a basic type.

ContinuousAddEquiv.mk'defMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

no wording

English

Let $f$ be a homeomorphism of $M$ and $N$ such that for all elements $x_{4}$ and $y$ of $M$, $\EqtMACRoH {f (x_{4} + y)}{f (x_{4})+ f (y)}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is a continuous additive equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $f$ and $h$, $\mathrm{Homeomorph\_\_continuous\_toFun}$ applied to $f$ and $\mathrm{Homeomorph\_\_continuous\_invFun}$ applied to $f$.

ContinuousAddEquiv.ofUniquedefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous additive equivalence (from the name)

English

The continuous additive equivalence is a continuous additive equivalence of $M$ and $N$.

ContinuousAddEquiv.refldefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the identity map of M (from the docstring)

English

Let $M$ be a set. Then the identity map of $M$ is a continuous additive equivalence of $M$ and $M$.

ContinuousAddEquiv.symmdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the inverse of cme (from the docstring)

English

Let $\mathrm{cme}$ be a continuous additive equivalence of $M$ and $N$. Then the inverse of $\mathrm{cme}$ is a continuous additive equivalence of $N$ and $M$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toAddEquiv}$ applied to $\mathrm{cme}$, $\mathrm{ContinuousAddEquiv\_\_continuous\_invFun}$ applied to $\mathrm{cme}$ and $\mathrm{ContinuousAddEquiv\_\_continuous\_toFun}$ applied to $\mathrm{cme}$.

ContinuousAddEquiv.toHomeomorphdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the homeomorphism of self (from the name)

English

Let $\mathrm{self}$ be a continuous additive equivalence of $G$ and $H$. Then the homeomorphism of $\mathrm{self}$ is a homeomorphism of $G$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toAddEquiv}$ applied to $\mathrm{self}$, $\mathrm{ContinuousAddEquiv\_\_continuous\_toFun}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousAddEquiv\_\_continuous\_invFun}$ applied to $\mathrm{self}$.

ContinuousAddEquiv.transdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the composition of cme1 and cme2 (from the name)

English

Let $\mathrm{cme1}$ be a continuous additive equivalence of $M$ and $N$. Let $\mathrm{cme2}$ be a continuous additive equivalence of $N$ and $L$. Then the composition of $\mathrm{cme1}$ and $\mathrm{cme2}$ is a continuous additive equivalence of $M$ and $L$.

ContinuousAddMonoidHomstructureMathlib.Topology.Algebra.ContinuousMonoidHom, type

Wording

continuous additive monoid homomorphism of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the continuous additive monoid homomorphisms of $A$ and $B$ are a basic type.

ContinuousAddMonoidHom.adddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the sum of E (from the name)

English

Let $E$ be a set. Then the sum of $E$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $E$ and $E$ and $E$.

ContinuousAddMonoidHom.compdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a continuous additive monoid homomorphism of $B$ and $C$. Let $f$ be a continuous additive monoid homomorphism of $A$ and $B$. Then the composition of $g$ and $f$ is a continuous additive monoid homomorphism of $A$ and $C$.

ContinuousAddMonoidHom.coproddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be a continuous additive monoid homomorphism of $A$ and $E$. Let $g$ be a continuous additive monoid homomorphism of $B$ and $E$. Then the coproduct of $f$ and $g$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $E$ defined as the composition of the sum of $E$ and the product map of $f$ and $g$.

ContinuousAddMonoidHom.diagdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the diagonal of A (from the name)

English

Let $A$ be a set. Then the diagonal of $A$ is a continuous additive monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $A$ defined as the product of the identity continuous homomorphism of $A$ and the identity continuous homomorphism of $A$.

ContinuousAddMonoidHom.fstdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the first component of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the first component of $A$ and $B$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$ defined as $\operatorname{mk}$ applied to the first component of $A$ and $B$ and $\mathrm{continuous\_fst}$.

ContinuousAddMonoidHom.iddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the identity continuous homomorphism of A (from the docstring)

English

Let $A$ be a set. Then the identity continuous homomorphism of $A$ is a continuous additive monoid homomorphism of $A$ and $A$ defined as $\operatorname{mk}$ applied to the identity map of $A$ and $\mathrm{continuous\_id}$.

ContinuousAddMonoidHom.inldefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the left injection of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the left injection of $A$ and $B$ is a continuous additive monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of the identity continuous homomorphism of $A$ and $0$.

ContinuousAddMonoidHom.inrdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the right injection of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the right injection of $A$ and $B$ is a continuous additive monoid homomorphism of $B$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $0$ and the identity continuous homomorphism of $B$.

ContinuousAddMonoidHom.negdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the negation of E (from the name)

English

Let $E$ be a set. Then the negation of $E$ is a continuous additive monoid homomorphism of $E$ and $E$.

ContinuousAddMonoidHom.ofClassdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous additive monoid homomorphism of f (from the name)

English

Let $A$, $B$ and $F$ be sets. Let $f$ be an element of $F$. Then the continuous additive monoid homomorphism of $f$ is a continuous additive monoid homomorphism of $A$ and $B$ defined as the continuous additive monoid homomorphism of $f$.

ContinuousAddMonoidHom.proddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a continuous additive monoid homomorphism of $A$ and $B$. Let $g$ be a continuous additive monoid homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is a continuous additive monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

ContinuousAddMonoidHom.prodMapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the product map of f and g (from the name)

English

Let $f$ be a continuous additive monoid homomorphism of $A$ and $C$. Let $g$ be a continuous additive monoid homomorphism of $B$ and $D$. Then the product map of $f$ and $g$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $\mathrm{Prod}$ applied to $C$ and $D$.

ContinuousAddMonoidHom.snddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the second component of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the second component of $A$ and $B$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$ defined as $\operatorname{mk}$ applied to the second component of $A$ and $B$ and $\mathrm{continuous\_snd}$.

ContinuousAddMonoidHom.swapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the swap of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the swap of $A$ and $B$ is a continuous additive monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $\mathrm{Prod}$ applied to $B$ and $A$ defined as the product of the second component of $A$ and $B$ and the first component of $A$ and $B$.

ContinuousAddMonoidHom.toContinuousAddMonoidHomdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous additive monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the continuous additive monoid homomorphism of $f$ is a continuous additive monoid homomorphism of $A$ and $B$.

ContinuousAddMonoidHom.toContinuousMapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous map of self (from the name)

English

Let $\mathrm{self}$ be a continuous additive monoid homomorphism of $A$ and $B$. Then the continuous map of $\mathrm{self}$ is a continuous map of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toZeroHom}$ applied to $\operatorname{toAddMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousAddMonoidHom\_\_continuous\_toFun}$ applied to $\mathrm{self}$.

ContinuousMonoidHomstructureMathlib.Topology.Algebra.ContinuousMonoidHom, type

Wording

continuous monoid homomorphism of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the continuous monoid homomorphisms of $A$ and $B$ are a basic type.

ContinuousMonoidHom.compdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a continuous monoid homomorphism of $B$ and $C$. Let $f$ be a continuous monoid homomorphism of $A$ and $B$. Then the composition of $g$ and $f$ is a continuous monoid homomorphism of $A$ and $C$.

ContinuousMonoidHom.coproddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be a continuous monoid homomorphism of $A$ and $E$. Let $g$ be a continuous monoid homomorphism of $B$ and $E$. Then the coproduct of $f$ and $g$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $E$ defined as the composition of the product of $E$ and the product map of $f$ and $g$.

ContinuousMonoidHom.diagdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the diagonal of A (from the name)

English

Let $A$ be a set. Then the diagonal of $A$ is a continuous monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $A$ defined as the product of the identity continuous homomorphism of $A$ and the identity continuous homomorphism of $A$.

ContinuousMonoidHom.fstdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the first component of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the first component of $A$ and $B$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $A$ defined as $\operatorname{mk}$ applied to the first component of $A$ and $B$ and $\mathrm{continuous\_fst}$.

ContinuousMonoidHom.iddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the identity continuous homomorphism of A (from the docstring)

English

Let $A$ be a set. Then the identity continuous homomorphism of $A$ is a continuous monoid homomorphism of $A$ and $A$ defined as $\operatorname{mk}$ applied to the identity map of $A$ and $\mathrm{continuous\_id}$.

ContinuousMonoidHom.inldefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the left injection of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the left injection of $A$ and $B$ is a continuous monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of the identity continuous homomorphism of $A$ and $1$.

ContinuousMonoidHom.inrdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the right injection of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the right injection of $A$ and $B$ is a continuous monoid homomorphism of $B$ and $\mathrm{Prod}$ applied to $A$ and $B$ defined as the product of $1$ and the identity continuous homomorphism of $B$.

ContinuousMonoidHom.invdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the inverse of E (from the name)

English

Let $E$ be a set. Then the inverse of $E$ is a continuous monoid homomorphism of $E$ and $E$.

ContinuousMonoidHom.muldefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the product of E (from the name)

English

Let $E$ be a set. Then the product of $E$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $E$ and $E$ and $E$.

ContinuousMonoidHom.ofClassdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous monoid homomorphism of f (from the name)

English

Let $A$, $B$ and $F$ be sets. Let $f$ be an element of $F$. Then the continuous monoid homomorphism of $f$ is a continuous monoid homomorphism of $A$ and $B$ defined as the continuous monoid homomorphism of $f$.

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

Wording

the product of f and g (from the name)

English

Let $f$ be a continuous monoid homomorphism of $A$ and $B$. Let $g$ be a continuous monoid homomorphism of $A$ and $C$. Then the product of $f$ and $g$ is a continuous monoid homomorphism of $A$ and $\mathrm{Prod}$ applied to $B$ and $C$.

ContinuousMonoidHom.prodMapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the product map of f and g (from the name)

English

Let $f$ be a continuous monoid homomorphism of $A$ and $C$. Let $g$ be a continuous monoid homomorphism of $B$ and $D$. Then the product map of $f$ and $g$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $\mathrm{Prod}$ applied to $C$ and $D$.

ContinuousMonoidHom.snddefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the second component of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the second component of $A$ and $B$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $B$ defined as $\operatorname{mk}$ applied to the second component of $A$ and $B$ and $\mathrm{continuous\_snd}$.

ContinuousMonoidHom.swapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the swap of A and B (from the name)

English

Let $A$ and $B$ be sets. Then the swap of $A$ and $B$ is a continuous monoid homomorphism of $\mathrm{Prod}$ applied to $A$ and $B$ and $\mathrm{Prod}$ applied to $B$ and $A$ defined as the product of the second component of $A$ and $B$ and the first component of $A$ and $B$.

ContinuousMonoidHom.toContinuousMapdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous map of self (from the name)

English

Let $\mathrm{self}$ be a continuous monoid homomorphism of $A$ and $B$. Then the continuous map of $\mathrm{self}$ is a continuous map of $A$ and $B$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOneHom}$ applied to $\operatorname{toMonoidHom}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousMonoidHom\_\_continuous\_toFun}$ applied to $\mathrm{self}$.

ContinuousMonoidHom.toContinuousMonoidHomdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous monoid homomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the continuous monoid homomorphism of $f$ is a continuous monoid homomorphism of $A$ and $B$.

ContinuousMulEquivstructureMathlib.Topology.Algebra.ContinuousMonoidHom, type

Wording

continuous multiplicative equivalence of G and H (from the name)

English

Let $G$ and $H$ be sets. Then the continuous multiplicative equivalences of $G$ and $H$ are a basic type.

ContinuousMulEquiv.mk'defMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

no wording

English

Let $f$ be a homeomorphism of $M$ and $N$ such that for all elements $x_{4}$ and $y$ of $M$, $\EqtMACRoH {f (x_{4} \times y)}{f (x_{4})\times f (y)}$. Then $\operatorname{mk'}$ applied to $f$ and $h$ is a continuous multiplicative equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $f$ and $h$, $\mathrm{Homeomorph\_\_continuous\_toFun}$ applied to $f$ and $\mathrm{Homeomorph\_\_continuous\_invFun}$ applied to $f$.

ContinuousMulEquiv.ofUniquedefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous multiplicative equivalence (from the name)

English

The continuous multiplicative equivalence is a continuous multiplicative equivalence of $M$ and $N$.

ContinuousMulEquiv.refldefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the identity map of M (from the docstring)

English

Let $M$ be a set. Then the identity map of $M$ is a continuous multiplicative equivalence of $M$ and $M$.

ContinuousMulEquiv.symmdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the inverse of cme (from the docstring)

English

Let $\mathrm{cme}$ be a continuous multiplicative equivalence of $M$ and $N$. Then the inverse of $\mathrm{cme}$ is a continuous multiplicative equivalence of $N$ and $M$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toMulEquiv}$ applied to $\mathrm{cme}$, $\mathrm{ContinuousMulEquiv\_\_continuous\_invFun}$ applied to $\mathrm{cme}$ and $\mathrm{ContinuousMulEquiv\_\_continuous\_toFun}$ applied to $\mathrm{cme}$.

ContinuousMulEquiv.toHomeomorphdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the homeomorphism of self (from the name)

English

Let $\mathrm{self}$ be a continuous multiplicative equivalence of $G$ and $H$. Then the homeomorphism of $\mathrm{self}$ is a homeomorphism of $G$ and $H$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $\operatorname{toMulEquiv}$ applied to $\mathrm{self}$, $\mathrm{ContinuousMulEquiv\_\_continuous\_toFun}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousMulEquiv\_\_continuous\_invFun}$ applied to $\mathrm{self}$.

ContinuousMulEquiv.transdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the composition of cme1 and cme2 (from the name)

English

Let $\mathrm{cme1}$ be a continuous multiplicative equivalence of $M$ and $N$. Let $\mathrm{cme2}$ be a continuous multiplicative equivalence of $N$ and $L$. Then the composition of $\mathrm{cme1}$ and $\mathrm{cme2}$ is a continuous multiplicative equivalence of $M$ and $L$.

MulEquiv.toContinuousMulEquivdefMathlib.Topology.Algebra.ContinuousMonoidHom, function or constant

Wording

the continuous multiplicative equivalence of e and he (from the name)

English

Let $e$ be a multiplicative equivalence of $G$ and $H$ such that for all elements $s$ of $\wp H$, the preimage of $\operatorname{coe}$ applied to $e$ and $s$ is open, if and only if $s$ is open. Then the continuous multiplicative equivalence of $e$ and $\mathrm{he}$ is a continuous multiplicative equivalence of $G$ and $H$.

Mathlib.Topology.Algebra.Field

IsTopologicalDivisionRingclassMathlib.Topology.Algebra.Field, predicate

Wording

K is a topological division ring (from the name)

English

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

Nonneg.unitsHomeomorphPosdefMathlib.Topology.Algebra.Field, function or constant

Wording

the unit homeomorphism positive part of R (from the name)

English

Let $R$ be a set. Then the unit homeomorphism positive part of $R$ is a homeomorphism of $\UnitsMACRoAO {\mathrm{Nonneg} (R)}$ and $\SubtypeSet {r}{\mathrm{Lt} (0 , r)}$.

Subfield.topologicalClosuredefMathlib.Topology.Algebra.Field, function or constant

Wording

the topological closure of K (from the name)

English

Let $K$ be a subfield of $x$. Then the topological closure of $K$ is a subfield of $x$.

affineHomeomorphdefMathlib.Topology.Algebra.Field, function or constant

Wording

the affine homeomorphism of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$ such that $a \neq 0$. Then the affine homeomorphism of $a$ and $b$ is a homeomorphism of $x$ and $x$.

Mathlib.Topology.Algebra.FilterBasis

AddGroupFilterBasisclassMathlib.Topology.Algebra.FilterBasis, predicate

Wording

A is a additive group filter basis (from the name)

English

Let $A$ be a set. Then we can say that $A$ is an additive group filter basis.

AddGroupFilterBasis.NdefMathlib.Topology.Algebra.FilterBasis, function or constant

Wording

no wording

English

Assume that $G$ is an additive group filter basis. Let $x_{1}$ be an element of $G$. Then $\operatorname{N}$ applied to $B$ and $x_{1}$ is a filter of $G$ defined as the forward map of the function that maps $y$ to $x_{1} + y$ and the filter of $\operatorname{toFilterBasis}$.

GroupFilterBasisclassMathlib.Topology.Algebra.FilterBasis, predicate

Wording

G is a group filter basis (from the name)

English

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

GroupFilterBasis.NdefMathlib.Topology.Algebra.FilterBasis, function or constant

Wording

no wording

English

Assume that $G$ is a group filter basis. Let $x_{1}$ be an element of $G$. Then $\operatorname{N}$ applied to $B$ and $x_{1}$ is a filter of $G$ defined as the forward map of the function that maps $y$ to $x_{1} \times y$ and the filter of $\operatorname{toFilterBasis}$.

ModuleFilterBasisstructureMathlib.Topology.Algebra.FilterBasis, type

Wording

module filter basis of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the module filter bases of $R$ and $M$ are a basic type.

ModuleFilterBasis.ofBasesdefMathlib.Topology.Algebra.FilterBasis, function or constant

Wording

the module filter basis of smul_left and smul_right (from the name)

English

Assume that $R$ is a ring filter basis. Assume that $M$ is an additive group filter basis. Assume that for all elements $U_{2}$ of $\wp M$, if $\MembershipmemMACRoT {\mathrm{BM}}{U_{2}}$, then there exists an element $V_{2}$ of $\wp R$, such that $V_{2}$ is an element of $\mathrm{BR}$ and there exists an element $W$ of $\wp M$ such that $W$ is an element of $\mathrm{BM}$ and $\HSMulhSMulMACRoAL {V_{2}}{W}\leq U_{2}$. Assume that for all elements $x_{5}$ of $R$, for all elements $U_{1}$ of $\wp M$, if $U_{1}$ is an element of $\mathrm{BM}$, then there exists an element $V_{1}$ of $\wp M$, such that $V_{1}$ is an element of $\mathrm{BM}$ and $V_{1}$ is less than or equal to the preimage of the function that maps $x_{6}$ to $\HSMulhSMulMACRoAL {x_{5}}{x_{6}}$ and $U_{1}$. Assume that for all elements $x_{3}$ of $M$, for all elements $U$ of $\wp M$, if $\MembershipmemMACRoT {\mathrm{BM}}{U}$, then there exists an element $V$ of $\wp R$, such that $V$ is an element of $\mathrm{BR}$ and $V$ is less than or equal to the preimage of the function that maps $x_{4}$ to $\HSMulhSMulMACRoAL {x_{4}}{x_{3}}$ and $U$. Then the module filter basis of $\mathrm{smul\_left}$ and $\mathrm{smul\_right}$ is a module filter basis of $R$ and $M$.

RingFilterBasisclassMathlib.Topology.Algebra.FilterBasis, predicate

Wording

R is a ring filter basis (from the name)

English

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

Mathlib.Topology.Algebra.Group.Basic

Homeomorph.addLeftdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $G$. Then $\operatorname{addLeft}$ applied to $a$ is a homeomorphism of $G$ and $G$.

Homeomorph.addRightdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $G$. Then $\operatorname{addRight}$ applied to $a$ is a homeomorphism of $G$ and $G$.

Homeomorph.mulLeftdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

the left multiplicative of a (from the name)

English

Let $a$ be an element of $G$. Then the left multiplicative of $a$ is a homeomorphism of $G$ and $G$.

Homeomorph.mulRightdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

the right multiplicative of a (from the name)

English

Let $a$ be an element of $G$. Then the right multiplicative of $a$ is a homeomorphism of $G$ and $G$.

Homeomorph.shearAddRightdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{shearAddRight}$ applied to $G$ is a homeomorphism of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.

Homeomorph.shearMulRightdefMathlib.Topology.Algebra.Group.Basic, function or constant

Wording

the right shear multiplicative of G (from the name)

English

Let $G$ be a set. Then the right shear multiplicative of $G$ is a homeomorphism of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.

Mathlib.Topology.Algebra.Group.ClosedSubgroup

ClosedAddSubgroupstructureMathlib.Topology.Algebra.Group.ClosedSubgroup, type

Wording

closed additive subgroup of G (from the name)

English

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

ClosedSubgroupstructureMathlib.Topology.Algebra.Group.ClosedSubgroup, type

Wording

closed subgroup of G (from the name)

English

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

Mathlib.Topology.Algebra.Group.CompactOpen

ContinuousAddMonoidHom.compLeftdefMathlib.Topology.Algebra.Group.CompactOpen, function or constant

Wording

the left composition of E and f (from the name)

English

Let $E$ be a set. Let $f$ be a continuous additive monoid homomorphism of $A$ and $B$. Then the left composition of $E$ and $f$ is a continuous additive monoid homomorphism of the set of continuous additive monoid homomorphisms of $B$ and $E$ and the set of continuous additive monoid homomorphisms of $A$ and $E$.

ContinuousAddMonoidHom.compRightdefMathlib.Topology.Algebra.Group.CompactOpen, function or constant

Wording

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

English

Let $A$ be a set. Let $f$ be a continuous additive monoid homomorphism of $B$ and $E$. Then the right composition of $A$ and $f$ is a continuous additive monoid homomorphism of the set of continuous additive monoid homomorphisms of $A$ and $B$ and the set of continuous additive monoid homomorphisms of $A$ and $E$.

ContinuousMonoidHom.compLeftdefMathlib.Topology.Algebra.Group.CompactOpen, function or constant

Wording

the left composition of E and f (from the name)

English

Let $E$ be a set. Let $f$ be a continuous monoid homomorphism of $A$ and $B$. Then the left composition of $E$ and $f$ is a continuous monoid homomorphism of the set of continuous monoid homomorphisms of $B$ and $E$ and the set of continuous monoid homomorphisms of $A$ and $E$.

ContinuousMonoidHom.compRightdefMathlib.Topology.Algebra.Group.CompactOpen, function or constant

Wording

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

English

Let $A$ be a set. Let $f$ be a continuous monoid homomorphism of $B$ and $E$. Then the right composition of $A$ and $f$ is a continuous monoid homomorphism of the set of continuous monoid homomorphisms of $A$ and $B$ and the set of continuous monoid homomorphisms of $A$ and $E$.

Mathlib.Topology.Algebra.Group.ContinuousDiv

Homeomorph.divLeftdefMathlib.Topology.Algebra.Group.ContinuousDiv, function or constant

Wording

the left quotient of x2 (from the name)

English

Let $x_{2}$ be an element of $G$. Then the left quotient of $x_{2}$ is a homeomorphism of $G$ and $G$.

Homeomorph.divRightdefMathlib.Topology.Algebra.Group.ContinuousDiv, function or constant

Wording

the right quotient of x2 (from the name)

English

Let $x_{2}$ be an element of $G$. Then the right quotient of $x_{2}$ is a homeomorphism of $G$ and $G$.

Homeomorph.subLeftdefMathlib.Topology.Algebra.Group.ContinuousDiv, function or constant

Wording

the left difference of x2 (from the name)

English

Let $x_{2}$ be an element of $G$. Then the left difference of $x_{2}$ is a homeomorphism of $G$ and $G$.

Homeomorph.subRightdefMathlib.Topology.Algebra.Group.ContinuousDiv, function or constant

Wording

the right difference of x2 (from the name)

English

Let $x_{2}$ be an element of $G$. Then the right difference of $x_{2}$ is a homeomorphism of $G$ and $G$.

Mathlib.Topology.Algebra.Group.ContinuousInv

Homeomorph.invdefMathlib.Topology.Algebra.Group.ContinuousInv, function or constant

Wording

the inverse of G (from the name)

English

Let $G$ be a set. Then the inverse of $G$ is a homeomorphism of $G$ and $G$.

Homeomorph.negdefMathlib.Topology.Algebra.Group.ContinuousInv, function or constant

Wording

the negation of G (from the name)

English

Let $G$ be a set. Then the negation of $G$ is a homeomorphism of $G$ and $G$.

Mathlib.Topology.Algebra.Group.Defs

ContinuousDivclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a continuous quotient (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a continuous quotient.

ContinuousInvclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a continuous inverse (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a continuous inverse.

ContinuousNegclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a continuous negation (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a continuous negation.

ContinuousSubclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a continuous difference (from the name)

English

Let $G$ be a set. Then we can say that $G$ is a continuous difference.

IsTopologicalAddGroupclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a topological additive group (from the name)

English

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

IsTopologicalGroupclassMathlib.Topology.Algebra.Group.Defs, predicate

Wording

G is a topological group (from the name)

English

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

Mathlib.Topology.Algebra.Group.Extension

TopologicalAddGroup.IsSESstructureMathlib.Topology.Algebra.Group.Extension, predicate

Wording

no wording

English

Let $x_{6}$ be an additive monoid homomorphism of $A$ and $B$. Let $x_{7}$ be an additive monoid homomorphism of $B$ and $C$. Then we can say that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$.

TopologicalGroup.IsSESstructureMathlib.Topology.Algebra.Group.Extension, predicate

Wording

no wording

English

Let $x_{6}$ be a monoid homomorphism of $A$ and $B$. Let $x_{7}$ be a monoid homomorphism of $B$ and $C$. Then we can say that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$.

Mathlib.Topology.Algebra.Group.GroupTopology

AddGroupTopologystructureMathlib.Topology.Algebra.Group.GroupTopology, type

Wording

additive group topology of x (from the name)

English

Let $x$ be a set. Then the additive group topologies of $x$ are a basic type.

AddGroupTopology.coinduceddefMathlib.Topology.Algebra.Group.GroupTopology, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{coinduced}$ applied to $f$ is an additive group topology of $x_{1}$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $b$ to $\mathrm{Leq} (\operatorname{coinduced} (f , t), \operatorname{toTopologicalSpace} (b))$.

GroupTopologystructureMathlib.Topology.Algebra.Group.GroupTopology, type

Wording

group topology of x (from the name)

English

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

GroupTopology.coinduceddefMathlib.Topology.Algebra.Group.GroupTopology, function or constant

Wording

no wording

English

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

Mathlib.Topology.Algebra.Group.Neighborhood

nhdsAddHomdefMathlib.Topology.Algebra.Group.Neighborhood, function or constant

Wording

the neighbourhood filter additive homomorphism (from the name)

English

The neighbourhood filter additive homomorphism is an additive homomorphism of $G$ and the set of filters of $G$ defined as $\operatorname{mk}$ applied to $\mathrm{nhds}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{nhds\_add}$ applied to $x_{2}$ and $x_{3}$.

nhdsMulHomdefMathlib.Topology.Algebra.Group.Neighborhood, function or constant

Wording

the neighbourhood filter multiplicative homomorphism (from the name)

English

The neighbourhood filter multiplicative homomorphism is a multiplicative homomorphism of $G$ and the set of filters of $G$ defined as $\operatorname{mk}$ applied to $\mathrm{nhds}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{nhds\_mul}$ applied to $x_{2}$ and $x_{3}$.

Mathlib.Topology.Algebra.Group.Subgroup

AddSubgroup.connectedComponentOfZerodefMathlib.Topology.Algebra.Group.Subgroup, function or constant

Wording

the connected component of G (from the name)

English

Let $G$ be a set. Then the connected component of $G$ is an additive subgroup of $G$.

AddSubgroup.topologicalClosuredefMathlib.Topology.Algebra.Group.Subgroup, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be an additive subgroup of $G$. Then the topological closure of $s$ is an additive subgroup of $G$.

Subgroup.connectedComponentOfOnedefMathlib.Topology.Algebra.Group.Subgroup, function or constant

Wording

the connected component of G (from the name)

English

Let $G$ be a set. Then the connected component of $G$ is a subgroup of $G$.

Subgroup.topologicalClosuredefMathlib.Topology.Algebra.Group.Subgroup, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a subgroup of $G$. Then the topological closure of $s$ is a subgroup of $G$.

Mathlib.Topology.Algebra.Group.TopologicalAbelianization

TopologicalAbelianizationdefMathlib.Topology.Algebra.Group.TopologicalAbelianization, type

Wording

topological abelianization of G (from the name)

English

Let $G$ be a set. Then a topological abelianization of $G$ is an element of the function that maps $G$ to the set of quotients of $G$ and the topological closure of the commutator subgroup of $G$.

Mathlib.Topology.Algebra.Group.Torsor

Homeomorph.constSDivdefMathlib.Topology.Algebra.Group.Torsor, function or constant

Wording

the constant quotient of p (from the name)

English

Let $p$ be an element of $P$. Then the constant quotient of $p$ is a homeomorphism of $P$ and $V$.

Homeomorph.constVSubdefMathlib.Topology.Algebra.Group.Torsor, function or constant

Wording

the constant difference of p (from the name)

English

Let $p$ be an element of $P$. Then the constant difference of $p$ is a homeomorphism of $P$ and $V$.

Homeomorph.pointReflectiondefMathlib.Topology.Algebra.Group.Torsor, function or constant

Wording

the point reflection of p (from the name)

English

Let $p$ be an element of $P$. Then the point reflection of $p$ is a homeomorphism of $P$ and $P$ defined as the composition of the constant difference of $p$ and the vector sum constant of $p$.

Homeomorph.smulConstdefMathlib.Topology.Algebra.Group.Torsor, function or constant

Wording

the scalar multiple constant of p (from the name)

English

Let $p$ be an element of $P$. Then the scalar multiple constant of $p$ is a homeomorphism of $V$ and $P$.

Homeomorph.vaddConstdefMathlib.Topology.Algebra.Group.Torsor, function or constant

Wording

the vector sum constant of p (from the name)

English

Let $p$ be an element of $P$. Then the vector sum constant of $p$ is a homeomorphism of $V$ and $P$.

IsTopologicalAddTorsorclassMathlib.Topology.Algebra.Group.Torsor, predicate

Wording

P is a topological additive torsor (from the name)

English

Let $P$ be a set. Then we can say that $P$ is a topological additive torsor.

IsTopologicalTorsorclassMathlib.Topology.Algebra.Group.Torsor, predicate

Wording

P is a topological torsor (from the name)

English

Let $P$ be a set. Then we can say that $P$ is a topological torsor.

Mathlib.Topology.Algebra.Group.Units

ContinuousAddEquiv.piAddUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the product additive unit (from the name)

English

The product additive unit is a continuous additive equivalence of the set of additive units of the set of functions from elements $i$ of $x$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to additive units of $M$ applied to $i_{1}$.

ContinuousAddEquiv.sumAddUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the sum additive unit of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the sum additive unit of $M$ and $N$ is a continuous additive equivalence of the set of additive units of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to the set of additive units of $M$ and the set of additive units of $N$.

ContinuousMulEquiv.piUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the product unit (from the name)

English

The product unit is a continuous multiplicative equivalence of $\UnitsMACRoAO {(\mathrm{Elem} (x)\rightarrow M (i))}$ and the set of functions from elements $i_{1}$ of $x$ to units of $M$ applied to $i_{1}$.

ContinuousMulEquiv.prodUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the product unit of M and N (from the name)

English

Let $M$ and $N$ be sets. Then the product unit of $M$ and $N$ is a continuous multiplicative equivalence of $\UnitsMACRoAO {\mathrm{Prod} (M , N)}$ and $\mathrm{Prod}$ applied to $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {N}$.

Homeomorph.prodAddUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the topological group isomorphism between the additive units (from the docstring)

English

The topological group isomorphism between the additive units is a homeomorphism of the set of additive units of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to the set of additive units of $x$ and the set of additive units of $x_{1}$.

Homeomorph.prodUnitsdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the topological group isomorphism between the units (from the docstring)

English

The topological group isomorphism between the units is a homeomorphism of $\UnitsMACRoAO {\mathrm{Prod} (x , x_{1})}$ and $\mathrm{Prod}$ applied to $\UnitsMACRoAO {x}$ and $\UnitsMACRoAO {x_{1}}$.

Units.mapContinuousMulEquivdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the map continuous multiplicative equivalence of f (from the name)

English

Let $f$ be a continuous multiplicative equivalence of $M$ and $N$. Then the map continuous multiplicative equivalence of $f$ is a continuous multiplicative equivalence of $\UnitsMACRoAO {M}$ and $\UnitsMACRoAO {N}$.

toAddUnits_homeomorphdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the additive unit homeomorphism (from the name)

English

The additive unit homeomorphism is a homeomorphism of $G$ and the set of additive units of $G$.

toUnits_homeomorphdefMathlib.Topology.Algebra.Group.Units, function or constant

Wording

the unit homeomorphism (from the name)

English

The unit homeomorphism is a homeomorphism of $G$ and $\UnitsMACRoAO {G}$.

Mathlib.Topology.Algebra.GroupCompletion

AddMonoidHom.completiondefMathlib.Topology.Algebra.GroupCompletion, function or constant

Wording

the completion of f and hf (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the completion of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of completions of $x$ and the set of completions of $x_{1}$.

AddMonoidHom.extensiondefMathlib.Topology.Algebra.GroupCompletion, function or constant

Wording

the extension of f and hf (from the name)

English

Let $f$ be an additive monoid homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the extension of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of completions of $x$ and $x_{1}$.

UniformSpace.Completion.toCompldefMathlib.Topology.Algebra.GroupCompletion, function or constant

Wording

the map (from the docstring)

English

The map is an additive monoid homomorphism of $x$ and the set of completions of $x$.

Mathlib.Topology.Algebra.GroupWithZero

ContinuousInv₀classMathlib.Topology.Algebra.GroupWithZero, predicate

Wording

x is a continuous inverse (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a continuous inverse.

Homeomorph.inv₀defMathlib.Topology.Algebra.GroupWithZero, function or constant

Wording

the inverse of x (from the name)

English

Let $x$ be a set. Then the inverse of $x$ is a homeomorphism of $\SubtypeSet {g}{\mathrm{Neq} (g , 0)}$ and $\SubtypeSet {g_{1}}{\mathrm{Neq} (g_{1} , 0)}$.

Homeomorph.mulLeft₀defMathlib.Topology.Algebra.GroupWithZero, function or constant

Wording

the left multiplicative of c and hc (from the name)

English

Let $c$ be an element of $x$ such that $c \neq 0$. Then the left multiplicative of $c$ and $\mathrm{hc}$ is a homeomorphism of $x$ and $x$.

Homeomorph.mulRight₀defMathlib.Topology.Algebra.GroupWithZero, function or constant

Wording

the right multiplicative of c and hc (from the name)

English

Let $c$ be an element of $x$ such that $c \neq 0$. Then the right multiplicative of $c$ and $\mathrm{hc}$ is a homeomorphism of $x$ and $x$.

unitsHomeomorphNeZerodefMathlib.Topology.Algebra.GroupWithZero, function or constant

Wording

no wording

English

$\mathrm{unitsHomeomorphNeZero}$ is a homeomorphism of $\UnitsMACRoAO {x}$ and $\SubtypeSet {g}{\mathrm{Neq} (g , 0)}$.

Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

SummationFilter.symmetricIccdefMathlib.Topology.Algebra.InfiniteSum.ConditionalInt, function or constant

Wording

the symmetric closed interval of G (from the name)

English

Let $G$ be a set. Then the symmetric closed interval of $G$ is a summation filter of $G$ defined as $\operatorname{mk}$ applied to the forward map of the function that maps $g$ to $\FinsetIccMACRoAH {\operatorname{neg} (g)}{g}$ and $\operatorname{atTop}$.

SummationFilter.symmetricIcodefMathlib.Topology.Algebra.InfiniteSum.ConditionalInt, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{symmetricIco}$ applied to $G$ is a summation filter of $G$ defined as $\operatorname{mk}$ applied to the forward map of the function that maps $N$ to $\FinsetIcoMACRoO {\operatorname{neg} (N)}{N}$ and $\operatorname{atTop}$.

SummationFilter.symmetricIocdefMathlib.Topology.Algebra.InfiniteSum.ConditionalInt, function or constant

Wording

no wording

English

Let $G$ be a set. Then $\operatorname{symmetricIoc}$ applied to $G$ is a summation filter of $G$ defined as $\operatorname{mk}$ applied to the forward map of the function that maps $N$ to $\FinsetIocMACRoAI {\operatorname{neg} (N)}{N}$ and $\operatorname{atTop}$.

SummationFilter.symmetricIoodefMathlib.Topology.Algebra.InfiniteSum.ConditionalInt, function or constant

Wording

the symmetric open interval of G (from the name)

English

Let $G$ be a set. Then the symmetric open interval of $G$ is a summation filter of $G$ defined as $\operatorname{mk}$ applied to the forward map of the function that maps $g$ to the open interval of $\operatorname{neg}$ applied to $g$ and $g$ and $\operatorname{atTop}$.

Mathlib.Topology.Algebra.InfiniteSum.Defs

HasProddefMathlib.Topology.Algebra.InfiniteSum.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $a$ be an element of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then $\mathrm{HasProd}$ holds for $f$, $a$ and $L$, if $\operatorname{Tendsto}$ holds for the function that maps $s$ to $\FinsetProd {s}{b}{f (b)}$, the filter of $L$ and the neighbourhood filter of $a$.

HasSumdefMathlib.Topology.Algebra.InfiniteSum.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $a$ be an element of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then $\mathrm{HasSum}$ holds for $f$, $a$ and $L$, if $\operatorname{Tendsto}$ holds for the function that maps $s$ to $\FinsetSum {s}{b}{f (b)}$, the filter of $L$ and the neighbourhood filter of $a$.

MultipliabledefMathlib.Topology.Algebra.InfiniteSum.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then $\mathrm{Multipliable}$ holds for $f$ and $L$, if there exists an element $a$ of $x$, such that $\mathrm{HasProd}$ holds for $f$, $a$ and $L$.

SummabledefMathlib.Topology.Algebra.InfiniteSum.Defs, predicate

Wording

f is summable with respect to L (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then $f$ is summable with respect to $L$, if there exists an element $a$ of $x$, such that $\mathrm{HasSum}$ holds for $f$, $a$ and $L$.

tproddefMathlib.Topology.Algebra.InfiniteSum.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then $\mathrm{tprod}$ applied to $f$ and $L$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Topology\_\_Algebra\_\_InfiniteSum\_\_Defs\_\_1210274395\_\_\_hygCtx\_\_\_hyg\_\_8}$, $f$ and $L$.

tsumdefMathlib.Topology.Algebra.InfiniteSum.Defs, function or constant

Wording

the sum of f and L (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $L$ be an element of $\mathrm{optParam}$ applied to the set of summation filters of $x_{1}$ and $\operatorname{unconditional}$ applied to $x_{1}$. Then the sum of $f$ and $L$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Topology\_\_Algebra\_\_InfiniteSum\_\_Defs\_\_1210274395\_\_\_hygCtx\_\_\_hyg\_\_25}$, $f$ and $L$.

Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

DiscreteConvolution.AddConvolutionExistsdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, predicate

Wording

no wording

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Then $\operatorname{AddConvolutionExists}$ holds for $L$, $f$ and $g$, if for all elements $x_{9}$ of $M$, $\operatorname{AddConvolutionExistsAt}$ holds for $L$, $f$, $g$ and $x_{9}$.

DiscreteConvolution.AddConvolutionExistsAtdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, predicate

Wording

no wording

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Let $x_{9}$ be an element of $M$. Then $\operatorname{AddConvolutionExistsAt}$ holds for $L$, $f$, $g$ and $x_{9}$, if the function that maps $\mathrm{ab}$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $\ProdfstMACRoZ {\mathrm{ab}}$ and $g$ applied to $\ProdsndMACRoAA {\mathrm{ab}}$ is summable with respect to $\operatorname{unconditional}$ applied to the set of elements of the additive fiber of $x_{9}$.

DiscreteConvolution.ConvolutionExistsdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, predicate

Wording

no wording

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Then $\operatorname{ConvolutionExists}$ holds for $L$, $f$ and $g$, if for all elements $x_{9}$ of $M$, $\operatorname{ConvolutionExistsAt}$ holds for $L$, $f$, $g$ and $x_{9}$.

DiscreteConvolution.ConvolutionExistsAtdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, predicate

Wording

no wording

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Let $x_{9}$ be an element of $M$. Then $\operatorname{ConvolutionExistsAt}$ holds for $L$, $f$, $g$ and $x_{9}$, if the function that maps $\mathrm{ab}$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $\ProdfstMACRoZ {\mathrm{ab}}$ and $g$ applied to $\ProdsndMACRoAA {\mathrm{ab}}$ is summable with respect to $\operatorname{unconditional}$ applied to the set of elements of the multiplicative fiber of $x_{9}$.

DiscreteConvolution.addConvolutiondefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the additive convolution of g and x9 (from the name)

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Let $x_{9}$ be an element of $M$. Then the additive convolution of $g$ and $x_{9}$ is an element of $F$ defined as the sum of the function that maps $\mathrm{ab}$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $\ProdfstMACRoZ {\mathrm{ab}}$ and $g$ applied to $\ProdsndMACRoAA {\mathrm{ab}}$ and $\operatorname{unconditional}$ applied to the set of elements of the additive fiber of $x_{9}$.

DiscreteConvolution.addFiberdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the additive fiber of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the additive fiber of $x_{1}$ is an element of $\wp \mathrm{Prod} (M , M)$ defined as $\operatorname{antidiagonal}$ applied to the universal set, the universal set and $x_{1}$.

DiscreteConvolution.addRingConvolutiondefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the additive ring convolution of g and x3 (from the name)

English

Let $f$ and $g$ be functions from elements of $M$ to elements of $R$. Let $x_{3}$ be an element of $M$. Then the additive ring convolution of $g$ and $x_{3}$ is an element of $R$ defined as the additive convolution of $g$ and $x_{3}$.

DiscreteConvolution.convolutiondefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the convolution of g and x9 (from the name)

English

Let $L$ be a linear map of $E$ and the set of linear maps of $\mathrm{E'}$ and $F$. Let $f$ be a function from elements of $M$ to elements of $E$. Let $g$ be a function from elements of $M$ to elements of $\mathrm{E'}$. Let $x_{9}$ be an element of $M$. Then the convolution of $g$ and $x_{9}$ is an element of $F$ defined as the sum of the function that maps $\mathrm{ab}$ to $\operatorname{coe}$ applied to $L$, $f$ applied to $\ProdfstMACRoZ {\mathrm{ab}}$ and $g$ applied to $\ProdsndMACRoAA {\mathrm{ab}}$ and $\operatorname{unconditional}$ applied to the set of elements of the multiplicative fiber of $x_{9}$.

DiscreteConvolution.mulFiberdefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the multiplicative fiber of x1 (from the name)

English

Let $x_{1}$ be an element of $M$. Then the multiplicative fiber of $x_{1}$ is an element of $\wp \mathrm{Prod} (M , M)$ defined as $\operatorname{mulAntidiagonal}$ applied to the universal set, the universal set and $x_{1}$.

DiscreteConvolution.ringConvolutiondefMathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution, function or constant

Wording

the ring convolution of g and x3 (from the name)

English

Let $f$ and $g$ be functions from elements of $M$ to elements of $R$. Let $x_{3}$ be an element of $M$. Then the ring convolution of $g$ and $x_{3}$ is an element of $R$ defined as the convolution of $g$ and $x_{3}$.

Mathlib.Topology.Algebra.InfiniteSum.Module

AddAction.automorphizedefMathlib.Topology.Algebra.InfiniteSum.Module, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $M$. Let $x_{6}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $x$ and $x_{1}$. Then $\operatorname{automorphize}$ applied to $f$ and $x_{6}$ is an element of $M$.

MulAction.automorphizedefMathlib.Topology.Algebra.InfiniteSum.Module, function or constant

Wording

no wording

English

QuotientAddGroup.automorphizedefMathlib.Topology.Algebra.InfiniteSum.Module, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $G$ to elements of $M$. Let $x_{4}$ be a quotient of $G$ and $x_{3}$. Then $\operatorname{automorphize}$ applied to $f$ and $x_{4}$ is an element of $M$ defined as $\operatorname{automorphize}$ applied to $f$ and $x_{4}$.

QuotientGroup.automorphizedefMathlib.Topology.Algebra.InfiniteSum.Module, function or constant

Wording

no wording

English

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

SummationFilterstructureMathlib.Topology.Algebra.InfiniteSum.SummationFilter, type

Wording

summation filter of x (from the name)

English

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

SummationFilter.HasSupportclassMathlib.Topology.Algebra.InfiniteSum.SummationFilter, predicate

Wording

L has supports (from the name)

English

Let $L$ be a summation filter of $x$. Then we can say that $L$ has supports.

SummationFilter.LeAtTopclassMathlib.Topology.Algebra.InfiniteSum.SummationFilter, predicate

Wording

no wording

English

Let $L$ be a summation filter of $x$. Then we can say that $\operatorname{LeAtTop}$ holds for $L$.

SummationFilter.NeBotclassMathlib.Topology.Algebra.InfiniteSum.SummationFilter, predicate

Wording

no wording

English

Let $L$ be a summation filter of $x$. Then we can say that $\operatorname{NeBot}$ holds for $L$.

SummationFilter.comapdefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

the preimage of L and f (from the name)

English

Let $L$ be a summation filter of $x$. Let $f$ be an embedding of $x_{1}$ and $x$. Then the preimage of $L$ and $f$ is a summation filter of $x_{1}$.

SummationFilter.conditionaldefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{conditional}$ applied to $x$ is a summation filter of $x$ defined as $\operatorname{mk}$ applied to the forward map of the function that maps $p$ to $\FinsetIccMACRoAH {\ProdfstMACRoZ {p}}{\ProdsndMACRoAA {p}}$ and $\operatorname{sprod}$ applied to $\operatorname{atBot}$ and $\operatorname{atTop}$.

SummationFilter.filterdefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

the filter of self (from the docstring)

English

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

SummationFilter.mapdefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

the map of L and f (from the name)

English

Let $L$ be a summation filter of $x$. Let $f$ be an embedding of $x$ and $x_{1}$. Then the map of $L$ and $f$ is a summation filter of $x_{1}$ defined as $\operatorname{mk}$ applied to the forward map of $\operatorname{map}$ applied to $f$ and the filter of $L$.

SummationFilter.supportdefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

the support of L (from the docstring)

English

Let $L$ be a summation filter of $x$. Then the support of $L$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to $\operatorname{Eventually}$ applied to the function that maps $s$ to $\MembershipmemMACRoT {s}{b}$ and the filter of $L$.

SummationFilter.unconditionaldefMathlib.Topology.Algebra.InfiniteSum.SummationFilter, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{unconditional}$ applied to $x$ is a summation filter of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{atTop}$.

Mathlib.Topology.Algebra.InfiniteSum.UniformOn

HasProdLocallyUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{HasProdLocallyUniformly}$ holds for $f$ and $g$, if $\mathrm{TendstoLocallyUniformly}$ holds for the function that maps $x_{6}$ and $x_{7}$ to $\FinsetProd {x_{6}}{i}{f (i , x_{7})}$, $g$ and $\operatorname{atTop}$.

HasProdLocallyUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{HasProdLocallyUniformlyOn}$ holds for $f$, $g$ and $s$, if $\mathrm{TendstoLocallyUniformlyOn}$ holds for the function that maps $x_{6}$ and $x_{7}$ to $\FinsetProd {x_{6}}{i}{f (i , x_{7})}$, $g$, $\operatorname{atTop}$ and $s$.

HasProdUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{HasProdUniformly}$ holds for $f$ and $g$, if $\mathrm{HasProd}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the uniform function and $f$, $\operatorname{ofFun}$ applied to $g$ and $\operatorname{unconditional}$ applied to $x_{2}$.

HasProdUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{HasProdUniformlyOn}$ holds for $f$, $g$ and $s$, if $\mathrm{HasProd}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $f$, $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $g$ and $\operatorname{unconditional}$ applied to $x_{2}$.

HasSumLocallyUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{HasSumLocallyUniformly}$ holds for $f$ and $g$, if $\mathrm{TendstoLocallyUniformly}$ holds for the function that maps $x_{6}$ and $x_{7}$ to $\FinsetSum {x_{6}}{i}{f (i , x_{7})}$, $g$ and $\operatorname{atTop}$.

HasSumLocallyUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{HasSumLocallyUniformlyOn}$ holds for $f$, $g$ and $s$, if $\mathrm{TendstoLocallyUniformlyOn}$ holds for the function that maps $x_{6}$ and $x_{7}$ to $\FinsetSum {x_{6}}{i}{f (i , x_{7})}$, $g$, $\operatorname{atTop}$ and $s$.

HasSumUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{HasSumUniformly}$ holds for $f$ and $g$, if $\mathrm{HasSum}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the uniform function and $f$, $\operatorname{ofFun}$ applied to $g$ and $\operatorname{unconditional}$ applied to $x_{2}$.

HasSumUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{HasSumUniformlyOn}$ holds for $f$, $g$ and $s$, if $\mathrm{HasSum}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $f$, $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $g$ and $\operatorname{unconditional}$ applied to $x_{2}$.

MultipliableLocallyUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Then $\mathrm{MultipliableLocallyUniformly}$ holds for $f$, if there exists a function $g$ from elements of $x_{1}$ to elements of $x$, such that $\mathrm{HasProdLocallyUniformly}$ holds for $f$ and $g$.

MultipliableLocallyUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{MultipliableLocallyUniformlyOn}$ holds for $f$ and $s$, if there exists a function $g$ from elements of $x_{1}$ to elements of $x$, such that $\mathrm{HasProdLocallyUniformlyOn}$ holds for $f$, $g$ and $s$.

MultipliableUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Then $\mathrm{MultipliableUniformly}$ holds for $f$, if $\mathrm{Multipliable}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the uniform function and $f$ and $\operatorname{unconditional}$ applied to $x_{2}$.

MultipliableUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{MultipliableUniformlyOn}$ holds for $f$ and $s$, if $\mathrm{Multipliable}$ holds for $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $f$ and $\operatorname{unconditional}$ applied to $x_{2}$.

SummableLocallyUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Then $\mathrm{SummableLocallyUniformly}$ holds for $f$, if there exists a function $g$ from elements of $x_{1}$ to elements of $x$, such that $\mathrm{HasSumLocallyUniformly}$ holds for $f$ and $g$.

SummableLocallyUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{SummableLocallyUniformlyOn}$ holds for $f$ and $s$, if there exists a function $g$ from elements of $x_{1}$ to elements of $x$, such that $\mathrm{HasSumLocallyUniformlyOn}$ holds for $f$, $g$ and $s$.

SummableUniformlydefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Then $\mathrm{SummableUniformly}$ holds for $f$, if $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the uniform function and $f$ is summable with respect to $\operatorname{unconditional}$ applied to $x_{2}$.

SummableUniformlyOndefMathlib.Topology.Algebra.InfiniteSum.UniformOn, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x_{2}$ and elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x_{1}$. Then $\mathrm{SummableUniformlyOn}$ holds for $f$ and $s$, if $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{ofFun}$ applied to $\operatorname{singleton}$ applied to $s$ and $f$ is summable with respect to $\operatorname{unconditional}$ applied to $x_{2}$.

Mathlib.Topology.Algebra.IsOpenUnits

IsOpenUnitsclassMathlib.Topology.Algebra.IsOpenUnits, predicate

Wording

no wording

English

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

Mathlib.Topology.Algebra.IsUniformGroup.Basic

AddOpposite.opUniformEquivLeftdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the left opposite uniform equivalence of G (from the name)

English

Let $G$ be a set. Then the left opposite uniform equivalence of $G$ is a uniform equivalence of $G$ and the set of additive opposites of $G$.

AddOpposite.opUniformEquivRightdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the right opposite uniform equivalence of G (from the name)

English

Let $G$ be a set. Then the right opposite uniform equivalence of $G$ is a uniform equivalence of $G$ and the set of additive opposites of $G$.

MulOpposite.opUniformEquivLeftdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the left opposite uniform equivalence of G (from the name)

English

Let $G$ be a set. Then the left opposite uniform equivalence of $G$ is a uniform equivalence of $G$ and the set of multiplicative opposites of $G$.

MulOpposite.opUniformEquivRightdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the right opposite uniform equivalence of G (from the name)

English

Let $G$ be a set. Then the right opposite uniform equivalence of $G$ is a uniform equivalence of $G$ and the set of multiplicative opposites of $G$.

UniformEquiv.invdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the inverse of G (from the name)

English

Let $G$ be a set. Then the inverse of $G$ is a uniform equivalence of $G$ and $G$.

UniformEquiv.negdefMathlib.Topology.Algebra.IsUniformGroup.Basic, function or constant

Wording

the negation of G (from the name)

English

Let $G$ be a set. Then the negation of $G$ is a uniform equivalence of $G$ and $G$.

Mathlib.Topology.Algebra.IsUniformGroup.Defs

IsLeftUniformAddGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

G is a left uniform additive group (from the name)

English

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

IsLeftUniformGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

G is a left uniform group (from the name)

English

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

IsRightUniformAddGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

G is a right uniform additive group (from the name)

English

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

IsRightUniformGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

G is a right uniform group (from the name)

English

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

IsUniformAddGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

x is a uniform additive group (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a uniform additive group.

IsUniformGroupclassMathlib.Topology.Algebra.IsUniformGroup.Defs, predicate

Wording

x is a uniform group (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a uniform group.

Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

AddSubgroup.addSubgroupOfContinuousAddEquivOfLedefMathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup, function or constant

Wording

the additive subgroup of hHK (from the name)

English

Assume that $H \leq K$. Then the additive subgroup of $\mathrm{hHK}$ is a continuous additive equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{addSubgroupOf} (H , K)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$.

Subgroup.subgroupOfContinuousMulEquivOfLedefMathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup, function or constant

Wording

the subgroup of hHK (from the name)

English

Assume that $H \leq K$. Then the subgroup of $\mathrm{hHK}$ is a continuous multiplicative equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{subgroupOf} (H , K)}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$.

Mathlib.Topology.Algebra.LinearMapCompletion

ContinuousLinearMap.completiondefMathlib.Topology.Algebra.LinearMapCompletion, function or constant

Wording

the completion of f (from the name)

English

Let $f$ be a continuous linear map of $x$ and $x_{1}$. Then the completion of $f$ is a continuous linear map of the set of completions of $x$ and the set of completions of $x_{1}$.

ContinuousLinearMap.fromCompletiondefMathlib.Topology.Algebra.LinearMapCompletion, function or constant

Wording

no wording

English

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

UniformSpace.Completion.toComplLdefMathlib.Topology.Algebra.LinearMapCompletion, function or constant

Wording

the complement (from the name)

English

The complement is a continuous linear map of $x$ and the set of completions of $x$.

Mathlib.Topology.Algebra.LinearTopology

IsLinearTopologyclassMathlib.Topology.Algebra.LinearTopology, predicate

Wording

M is a linear topology with respect to R (from the name)

English

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

Mathlib.Topology.Algebra.Localization

Localization.ringTopologydefMathlib.Topology.Algebra.Localization, function or constant

Wording

the ring topology (from the name)

English

The ring topology is a ring topology of the set of localizations of $M$ defined as $\operatorname{coinduced}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toMulHom}$ applied to the monoid of $M$.

Mathlib.Topology.Algebra.Module.Alternating.Basic

ContinuousAlternatingMapstructureMathlib.Topology.Algebra.Module.Alternating.Basic, type

Wording

continuous alternating map of N and x (from the name)

English

Let $R$, $M$, $N$ and $x$ be sets. Then the continuous alternating maps of $N$ and $x$ are a basic type.

ContinuousAlternatingMap.applyAddHomdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

Let $v$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{applyAddHom}$ applied to $v$ is an additive monoid homomorphism of the set of continuous alternating maps of $N$ and $x$ and $N$.

ContinuousAlternatingMap.codRestrictdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

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

ContinuousAlternatingMap.compContinuousLinearMapdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

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

English

Let $g$ be a continuous alternating map of $N$ and $x$. Let $f$ be a continuous linear map of $\mathrm{M'}$ and $M$. Then the composition continuous linear map of $g$ and $f$ is a continuous alternating map of $N$ and $x$ defined as $\operatorname{mk}$ applied to the composition continuous linear map of $\operatorname{toContinuousMultilinearMap}$ applied to $g$ and the function that maps $x_{11}$ to $f$ and $\mathrm{AlternatingMap\_\_map\_eq\_zero\_of\_eq'}$ applied to the composition linear map of the alternating map of $g$ and $\operatorname{toLinearMap}$ applied to $f$.

ContinuousAlternatingMap.compContinuousLinearMapₗdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

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

English

Let $f$ be a continuous linear map of $M$ and $\mathrm{M'}$. Then the composition continuous linear map of $f$ is a linear map of the set of continuous alternating maps of $N$ and $x$ and the set of continuous alternating maps of $N$ and $x$.

ContinuousAlternatingMap.constOfIsEmptydefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the constant of m (from the name)

English

Let $R$, $M$ and $x$ be sets. Let $m$ be an element of $N$. Then the constant of $m$ is a continuous alternating map of $N$ and $x$ defined as $\operatorname{mk}$ applied to the constant of the function that maps $x_{8}$ to $M$ and $m$ and $\mathrm{AlternatingMap\_\_map\_eq\_zero\_of\_eq'}$ applied to the constant of $m$.

ContinuousAlternatingMap.ofSubsingletondefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the continuous alternating map of i (from the name)

English

Let $R$, $M$ and $N$ be sets. Let $i$ be an element of $x$. Then the continuous alternating map of $i$ is an equivalence from the set of continuous linear maps of $M$ and $N$ to the set of continuous alternating maps of $N$ and $x$.

ContinuousAlternatingMap.pidefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the product of f (from the name)

English

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

ContinuousAlternatingMap.piEquivdefMathlib.Topology.Algebra.Module.Alternating.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_{5}$ to continuous alternating maps of $N$ applied to $i$ and $x$ to the set of continuous alternating maps of the set of functions from elements $i_{1}$ of $x_{5}$ to elements of $N$ applied to $i_{1}$ and $x$.

ContinuousAlternatingMap.piLinearEquivdefMathlib.Topology.Algebra.Module.Alternating.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_{6}$ to continuous alternating maps of $\mathrm{M'}$ applied to $i$ and $x$ and the set of continuous alternating maps of the set of functions from elements $i_{1}$ of $x_{6}$ to elements of $\mathrm{M'}$ applied to $i_{1}$ and $x$.

ContinuousAlternatingMap.proddefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a continuous alternating map of $N$ and $x$. Let $g$ be a continuous alternating map of $\mathrm{N'}$ and $x$. Then the product of $f$ and $g$ is a continuous alternating map of $\mathrm{Prod}$ applied to $N$ and $\mathrm{N'}$ and $x$.

ContinuousAlternatingMap.restrictScalarsdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a continuous alternating map of $N$ and $x$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a continuous alternating map of $N$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toContinuousMultilinearMap}$ applied to $f$ and $\mathrm{ContinuousAlternatingMap\_\_map\_eq\_zero\_of\_eq'}$ applied to $f$.

ContinuousAlternatingMap.smulRightdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

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

English

Let $f$ be a continuous alternating map of $R$ and $x$. Let $z$ be an element of $N$. Then the right scalar multiple of $f$ and $z$ is a continuous alternating map of $N$ and $x$.

ContinuousAlternatingMap.toAlternatingMapdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the alternating map of self (from the name)

English

Let $\mathrm{self}$ be a continuous alternating map of $N$ and $x$. Then the alternating map of $\mathrm{self}$ is an alternating map of $N$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{toMultilinearMap}$ applied to $\operatorname{toContinuousMultilinearMap}$ applied to $\mathrm{self}$ and $\mathrm{ContinuousAlternatingMap\_\_map\_eq\_zero\_of\_eq'}$ applied to $\mathrm{self}$.

ContinuousAlternatingMap.toAlternatingMapLineardefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

$\operatorname{toAlternatingMapLinear}$ is a linear map of the set of continuous alternating maps of $N$ and $x$ and the set of alternating maps of $N$ and $x$.

ContinuousAlternatingMap.toContinuousLinearMapdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

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

English

Let $f$ be a continuous alternating map of $N$ and $x$. Let $m$ be a function from elements of $x$ to elements of $M$. Let $i$ be an element of $x$. Then the continuous linear map of $m$ and $i$ is a continuous linear map of $M$ and $N$ defined as the continuous linear map of $m$ and $i$.

ContinuousAlternatingMap.toContinuousMultilinearMapLineardefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

$\operatorname{toContinuousMultilinearMapLinear}$ is a linear map of the set of continuous alternating maps of $N$ and $x$ and the set of continuous multilinear maps of the function that maps $x_{10}$ to $M$ and $N$.

ContinuousAlternatingMap.toMultilinearAddHomdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the multilinear additive homomorphism (from the name)

English

The multilinear additive homomorphism is an additive monoid homomorphism of the set of continuous alternating maps of $N$ and $x$ and the set of continuous multilinear maps of the function that maps $x_{8}$ to $M$ and $N$.

ContinuousLinearEquiv.continuousAlternatingMapCongrEquivdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the continuous alternating map congruence equivalence of e and #2 (from the name)

English

Let $e$ be a continuous linear equivalence of $M$ and $\mathrm{M'}$. Let $\mathrm{e'}$ be a continuous linear equivalence of $N$ and $\mathrm{N'}$. Then the continuous alternating map congruence equivalence of $e$ and $\mathrm{e'}$ is an equivalence from the set of continuous alternating maps of $N$ and $x$ to the set of continuous alternating maps of $\mathrm{N'}$ and $x$ defined as the composition of the continuous alternating map congruence left equivalence of $e$ and the continuous alternating map congruence right equivalence of $\mathrm{e'}$.

ContinuousLinearEquiv.continuousAlternatingMapCongrLeftEquivdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the continuous alternating map congruence left equivalence of e (from the name)

English

Let $e$ be a continuous linear equivalence of $M$ and $\mathrm{M'}$. Then the continuous alternating map congruence left equivalence of $e$ is an equivalence from the set of continuous alternating maps of $N$ and $x$ to the set of continuous alternating maps of $N$ and $x$.

ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquivdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

the continuous alternating map congruence right equivalence of e (from the name)

English

Let $e$ be a continuous linear equivalence of $N$ and $\mathrm{N'}$. Then the continuous alternating map congruence right equivalence of $e$ is an equivalence from the set of continuous alternating maps of $N$ and $x$ to the set of continuous alternating maps of $\mathrm{N'}$ and $x$.

ContinuousLinearMap.compContinuousAlternatingMapdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

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

English

Let $g$ be a continuous linear map of $N$ and $\mathrm{N'}$. Let $f$ be a continuous alternating map of $N$ and $x$. Then the composition continuous alternating map of $g$ and $f$ is a continuous alternating map of $\mathrm{N'}$ and $x$ defined as $\operatorname{mk}$ applied to the composition continuous multilinear map of $g$ and $\operatorname{toContinuousMultilinearMap}$ applied to $f$ and $\mathrm{AlternatingMap\_\_map\_eq\_zero\_of\_eq'}$ applied to the composition alternating map of $\operatorname{toLinearMap}$ applied to $g$ and the alternating map of $f$.

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

Wording

the composition continuous alternating map of N and #4 (from the name)

English

Let $R$, $M$, $N$ and $\mathrm{N'}$ be sets. Then the composition continuous alternating map of $N$ and $\mathrm{N'}$ is a linear map of the set of continuous linear maps of $N$ and $\mathrm{N'}$ and the set of linear maps of the set of continuous alternating maps of $N$ and $x$ and the set of continuous alternating maps of $\mathrm{N'}$ and $x$.

ContinuousMultilinearMap.alternatizationdefMathlib.Topology.Algebra.Module.Alternating.Basic, function or constant

Wording

no wording

English

$\operatorname{alternatization}$ is an additive monoid homomorphism of the set of continuous multilinear maps of the function that maps $x_{10}$ to $M$ and $N$ and the set of continuous alternating maps of $N$ and $x$.

Mathlib.Topology.Algebra.Module.Alternating.Topology

ContinuousAlternatingMap.applydefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the continuous alternating map of m (from the name)

English

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

ContinuousAlternatingMap.compContinuousLinearMapCLMdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

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

English

Let $f$ be a continuous linear map of $E$ and $\mathrm{E'}$. Then the composition continuous linear map continuous linear map of $f$ is a continuous linear map of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $F$ and $x_{1}$.

ContinuousAlternatingMap.liftCLMdefMathlib.Topology.Algebra.Module.Alternating.Topology, 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 $G$ and the set of continuous multilinear maps of the function that maps $x_{14}$ to $E$ and $F$ such that for all elements $x_{12}$ of $G$, for all functions $v$ from elements of $x_{1}$ to elements of $E$, for all elements $i$ and $j$ of $x_{1}$, if $\EqtMACRoH {v (i)}{v (j)}$, then if $i \neq j$, then $\EqtMACRoH {\operatorname{coe} (f , x_{12} , v)}{0}$. Then the lift continuous linear map of $f$ and $\mathrm{hf}$ is a continuous linear map of $G$ and the set of continuous alternating maps of $F$ and $x_{1}$.

ContinuousAlternatingMap.restrictScalarsCLMdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

no wording

English

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

ContinuousAlternatingMap.toContinuousMultilinearMapCLMdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the continuous multilinear map continuous linear map of R (from the name)

English

Let $R$ be a set. Then the continuous multilinear map continuous linear map of $R$ is a continuous linear map of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous multilinear maps of the function that maps $x_{11}$ to $E$ and $F$.

ContinuousLinearEquiv.continuousAlternatingMapCongrdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the continuous alternating map congruence of e and #2 (from the name)

English

Let $e$ be a continuous linear equivalence of $E$ and $\mathrm{E'}$. Let $\mathrm{e'}$ be a continuous linear equivalence of $F$ and $G$. Then the continuous alternating map congruence of $e$ and $\mathrm{e'}$ is a continuous linear equivalence of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $G$ and $x_{1}$ defined as the composition of the left continuous alternating map congruence of $e$ and the right continuous alternating map congruence of $\mathrm{e'}$.

ContinuousLinearEquiv.continuousAlternatingMapCongrLeftdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the left continuous alternating map congruence of f (from the name)

English

Let $f$ be a continuous linear equivalence of $E$ and $\mathrm{E'}$. Then the left continuous alternating map congruence of $f$ is a continuous linear equivalence of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $F$ and $x_{1}$.

ContinuousLinearEquiv.continuousAlternatingMapCongrRightdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the right continuous alternating map congruence of g (from the name)

English

Let $g$ be a continuous linear equivalence of $F$ and $G$. Then the right continuous alternating map congruence of $g$ is a continuous linear equivalence of the set of continuous alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $G$ and $x_{1}$.

ContinuousLinearMap.compContinuousAlternatingMapCLMdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

the composition continuous alternating map continuous linear map of G and x1 (from the name)

English

Let $x$, $E$, $F$, $G$ and $x_{1}$ be sets. Then the composition continuous alternating map continuous linear map of $G$ and $x_{1}$ 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 alternating maps of $F$ and $x_{1}$ and the set of continuous alternating maps of $G$ and $x_{1}$.

ContinuousMultilinearMap.alternatizationLdefMathlib.Topology.Algebra.Module.Alternating.Topology, function or constant

Wording

no wording

English

$\operatorname{alternatizationL}$ is a continuous linear map of the set of continuous multilinear maps of the function that maps $x_{11}$ to $E$ and $F$ and the set of continuous alternating maps of $F$ and $x_{1}$.

Mathlib.Topology.Algebra.Module.Basic

Submodule.topologicalClosuredefMathlib.Topology.Algebra.Module.Basic, function or constant

Wording

the topological closure of s (from the name)

English

Let $s$ be a submodule of $R$ and $M$. Then the topological closure of $s$ is a submodule of $R$ and $M$ defined as $\operatorname{mk}$ applied to the topological closure of $\operatorname{toAddSubmonoid}$ applied to $s$ and $\mathrm{Submodule\_\_mapsTo\_smul\_closure}$ applied to $s$.

linearMapOfMemClosureRangeCoedefMathlib.Topology.Algebra.Module.Basic, function or constant

Wording

the linear map 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 $\operatorname{coe}$. Then the linear map of $f$ and $\mathrm{hf}$ is a linear map of $x$ and $x_{1}$.

linearMapOfTendstodefMathlib.Topology.Algebra.Module.Basic, function or constant

Wording

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

English

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

Mathlib.Topology.Algebra.Module.ClosedSubmodule

ClosedSubmodulestructureMathlib.Topology.Algebra.Module.ClosedSubmodule, type

Wording

closed submodule of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the closed submodules of $R$ and $M$ are a basic type.

ClosedSubmodule.comapdefMathlib.Topology.Algebra.Module.ClosedSubmodule, function or constant

Wording

the preimage of f and s (from the docstring)

English

Let $f$ be a continuous linear map of $M$ and $N$. Let $s$ be a closed submodule of $R$ and $N$. Then the preimage of $f$ and $s$ is a closed submodule of $R$ and $M$.

ClosedSubmodule.mapdefMathlib.Topology.Algebra.Module.ClosedSubmodule, function or constant

Wording

the map of f and s (from the name)

English

Let $f$ be a continuous linear map of $M$ and $N$. Let $s$ be a closed submodule of $R$ and $M$. Then the map of $f$ and $s$ is a closed submodule of $R$ and $N$ defined as the closure of the map of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{toSubmodule}$ applied to $s$.

ClosedSubmodule.mapEquivdefMathlib.Topology.Algebra.Module.ClosedSubmodule, function or constant

Wording

the map equivalence of f (from the name)

English

Let $f$ be a continuous linear equivalence of $M$ and $N$. Then the map equivalence of $f$ is an equivalence from the set of closed submodules of $R$ and $M$ to the set of closed submodules of $R$ and $N$.

ClosedSubmodule.toClosedsdefMathlib.Topology.Algebra.Module.ClosedSubmodule, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a closed submodule of $R$ and $M$. Then $\operatorname{toCloseds}$ applied to $\mathrm{self}$ is an element of $\operatorname{Closeds}$ applied to $M$ defined as $\operatorname{mk}$ applied to the carrier of $\operatorname{toAddSubsemigroup}$ applied to $\operatorname{toAddSubmonoid}$ applied to $\operatorname{toSubmodule}$ applied to $\mathrm{self}$ and $\operatorname{isClosed'}$ applied to $\mathrm{self}$.

Submodule.closuredefMathlib.Topology.Algebra.Module.ClosedSubmodule, function or constant

Wording

the closure of s (from the docstring)

English

Let $s$ be a submodule of $R$ and $M$. Then the closure of $s$ is a closed submodule of $R$ and $M$.

Mathlib.Topology.Algebra.Module.Complement

ContinuousLinearMap.ofIsTopCompldefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

the continuous linear map of x7 and x8 (from the name)

English

Assume that $p$ is a top complement with respect to $q$. Let $x_{7}$ be a continuous linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {p}{x_{10}})}$ and $F$. Let $x_{8}$ be a continuous linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {q}{x_{9}})}$ and $F$. Then the continuous linear map of $x_{7}$ and $x_{8}$ is a continuous linear map of $E$ and $F$ defined as the composition of the coproduct of $x_{7}$ and $x_{8}$ and the continuous linear map of the inverse of the product equivalence of $p$ and $q$.

Submodule.ClosedComplementeddefMathlib.Topology.Algebra.Module.Complement, predicate

Wording

no wording

English

Let $p$ be a submodule of $R$ and $M$. Then $\operatorname{ClosedComplemented}$ holds for $p$, if there exists a continuous linear map $f$ of $M$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {p}{x_{7}})}$, such that for all elements $x_{4}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$, $\EqtMACRoH {f (x_{4})}{x_{4}}$.

Submodule.ClosedComplemented.complementdefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

the complement of h (from the name)

English

Assume that $\operatorname{ClosedComplemented}$ holds for $p$. Then the complement of $h$ is a submodule of $R$ and $M$ defined as $\operatorname{choose}$ applied to $\mathrm{Submodule\_\_ClosedComplemented\_\_exists\_isTopCompl}$ applied to $h$.

Submodule.IsTopComplstructureMathlib.Topology.Algebra.Module.Complement, predicate

Wording

p is a top complement with respect to q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$. Then we can say that $p$ is a top complement with respect to $q$.

Submodule.prodEquivOfIsTopCompldefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

the product equivalence of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $p$ is a top complement with respect to $q$. Then the product equivalence of $p$ and $q$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {q}{x_{5}})}$ and $M$.

Submodule.projectionLdefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

the projection of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $p$ is a top complement with respect to $q$. Then the projection of $p$ and $q$ is a continuous linear map of $M$ and $M$ defined as the composition of the subtype of $p$ and $\operatorname{projectionOntoL}$ applied to $p$, $q$ and $h$.

Submodule.projectionOntoLdefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

no wording

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $p$ is a top complement with respect to $q$. Then $\operatorname{projectionOntoL}$ applied to $p$, $q$ and $h$ is a continuous linear map of $M$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{projectionOnto}$ applied to $p$, $q$ and $\operatorname{isCompl}$ applied to $h$ and $\mathrm{Submodule\_\_IsTopCompl\_\_continuous\_projectionOnto}$ applied to $h$.

Submodule.quotientEquivOfIsTopCompldefMathlib.Topology.Algebra.Module.Complement, function or constant

Wording

the quotient equivalence of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $p$ is a top complement with respect to $q$. Then the quotient equivalence of $p$ and $q$ is a continuous linear equivalence of the set of quotients of $M$ and $p$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {q}{x_{4}})}$.

Mathlib.Topology.AlexandrovDiscrete

Mathlib.Topology.Algebra.AffineSubspace

Mathlib.Topology.Algebra.Algebra

Mathlib.Topology.Algebra.Algebra.Equiv

Mathlib.Topology.Algebra.AsymptoticCone

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Mathlib.Topology.Algebra.ConstMulAction

Mathlib.Topology.Algebra.Constructions

Mathlib.Topology.Algebra.Constructions.DomMulAct

Mathlib.Topology.Algebra.ContinuousAffineEquiv

Mathlib.Topology.Algebra.ContinuousAffineMap

Mathlib.Topology.Algebra.ContinuousAffineMap.Topology

Mathlib.Topology.Algebra.ContinuousMonoidHom

Mathlib.Topology.Algebra.Field

Mathlib.Topology.Algebra.FilterBasis

Mathlib.Topology.Algebra.Group.Basic

Mathlib.Topology.Algebra.Group.ClosedSubgroup

Mathlib.Topology.Algebra.Group.CompactOpen

Mathlib.Topology.Algebra.Group.ContinuousDiv

Mathlib.Topology.Algebra.Group.ContinuousInv

Mathlib.Topology.Algebra.Group.Defs

Mathlib.Topology.Algebra.Group.Extension

Mathlib.Topology.Algebra.Group.GroupTopology

Mathlib.Topology.Algebra.Group.Neighborhood

Mathlib.Topology.Algebra.Group.Subgroup

Mathlib.Topology.Algebra.Group.TopologicalAbelianization

Mathlib.Topology.Algebra.Group.Torsor

Mathlib.Topology.Algebra.Group.Units

Mathlib.Topology.Algebra.GroupCompletion

Mathlib.Topology.Algebra.GroupWithZero

Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Mathlib.Topology.Algebra.InfiniteSum.Defs

Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Mathlib.Topology.Algebra.InfiniteSum.Module

Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Mathlib.Topology.Algebra.IsOpenUnits

Mathlib.Topology.Algebra.IsUniformGroup.Basic

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Mathlib.Topology.Algebra.LinearMapCompletion

Mathlib.Topology.Algebra.LinearTopology

Mathlib.Topology.Algebra.Localization

Mathlib.Topology.Algebra.Module.Alternating.Basic

Mathlib.Topology.Algebra.Module.Alternating.Topology

Mathlib.Topology.Algebra.Module.Basic

Mathlib.Topology.Algebra.Module.ClosedSubmodule

Mathlib.Topology.Algebra.Module.Complement