Definitions: Mathlib.Topology, part 4 of 8

TopPair.Hom.fstdefMathlib.Topology.Category.TopPair, function or constant

Wording

the map between the first spaces of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the map between the first spaces of $f$ is a homomorphism of the first space of the pair and the first space of the pair defined as the right of the homomorphism of $f$.

TopPair.Hom.snddefMathlib.Topology.Category.TopPair, function or constant

Wording

the map between the second spaces of f (from the docstring)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the map between the second spaces of $f$ is a homomorphism of the second space of the pair and the second space of the pair defined as the left of the homomorphism of $f$.

TopPair.HomotopicdefMathlib.Topology.Category.TopPair, predicate

Wording

f is homotopic to g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $f$ is homotopic to $g$, if $\mathrm{Nonempty}$ holds for the set of homotopies of $f$ and $g$.

TopPair.HomotopystructureMathlib.Topology.Category.TopPair, type

Wording

homotopy of f and g (from the name)

English

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the homotopies of $f$ and $g$ are a basic type.

TopPair.Homotopy.compdefMathlib.Topology.Category.TopPair, function or constant

Wording

the composition of G and F (from the name)

English

Let $G$ be a homotopy of $x_{2}$ and $x_{3}$. Let $F$ be a homotopy of $x$ and $x_{1}$. Then the composition of $G$ and $F$ is a homotopy of the composition of $x$ and $x_{2}$ and the composition of $x_{1}$ and $x_{3}$.

TopPair.Homotopy.fstdefMathlib.Topology.Category.TopPair, function or constant

Wording

the homotopy on the first space of self (from the docstring)

English

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Then the homotopy on the first space of $\mathrm{self}$ is a homotopy of the map between the first spaces of $f$ and the map between the first spaces of $g$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

TopPair.Homotopy.refldefMathlib.Topology.Category.TopPair, function or constant

Wording

the identity of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the identity of $f$ is a homotopy of $f$ and $f$.

TopPair.Homotopy.snddefMathlib.Topology.Category.TopPair, function or constant

Wording

the homotopy on the second space of self (from the docstring)

English

Let $\mathrm{self}$ be a homotopy of $f$ and $g$. Then the homotopy on the second space of $\mathrm{self}$ is a homotopy of the map between the second spaces of $f$ and the map between the second spaces of $g$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

TopPair.Homotopy.symmdefMathlib.Topology.Category.TopPair, function or constant

Wording

the inverse of F (from the name)

English

Let $F$ be a homotopy of $x$ and $x_{1}$. Then the inverse of $F$ is a homotopy of $x_{1}$ and $x$.

TopPair.Homotopy.transdefMathlib.Topology.Category.TopPair, function or constant

Wording

the composition of F and G (from the name)

English

Let $F$ be a homotopy of $x$ and $x_{1}$. Let $G$ be a homotopy of $x_{1}$ and $x_{2}$. Then the composition of $F$ and $G$ is a homotopy of $x$ and $x_{2}$.

TopPair.diagdefMathlib.Topology.Category.TopPair, function or constant

Wording

the diagonal (from the name)

English

The diagonal is a functor of the set of topological categories and the set of top pairs.

TopPair.fstdefMathlib.Topology.Category.TopPair, function or constant

Wording

the first space of the pair (from the docstring)

English

The first space of the pair is a topological category defined as the right subobject of $\operatorname{toComma}$ applied to $X$.

TopPair.incldefMathlib.Topology.Category.TopPair, function or constant

Wording

the inclusion (from the name)

English

The inclusion is a functor of the set of topological categories and the set of top pairs.

TopPair.inclAdjProj₁defMathlib.Topology.Category.TopPair, function or constant

Wording

the inclusion functor (from the docstring)

English

The inclusion functor is an adjunction of the inclusion and the projection.

TopPair.jdefMathlib.Topology.Category.TopPair, function or constant

Wording

no wording

English

Let $X$ be a top pair. Then $\operatorname{j}$ applied to $X$ is a homomorphism of the action of the inclusion and the first space of the pair and $X$.

TopPair.mapdefMathlib.Topology.Category.TopPair, function or constant

Wording

the map (from the name)

English

The map is a homomorphism of the second space of the pair and the first space of the pair defined as the homomorphism of $\operatorname{toComma}$ applied to $X$.

TopPair.ofdefMathlib.Topology.Category.TopPair, function or constant

Wording

no wording

English

Let $f$ be a homomorphism of $A$ and $X$ such that $\operatorname{coe}$ applied to the homomorphism of $f$ is an embedding. Then $\operatorname{of}$ applied to $f$ and $h$ is a top pair defined as $\operatorname{mk}$ applied to $f$ and $h$.

TopPair.ofHomdefMathlib.Topology.Category.TopPair, function or constant

Wording

the top pair of f and g (from the name)

English

Let $f$ be a homomorphism of the first space of the pair and the first space of the pair. Let $g$ be a homomorphism of the second space of the pair and the second space of the pair such that $\mathrm{autoParam}$ holds for the proposition that the composition of $g$ and the map is equal to the composition of the map and $f$ and $\mathrm{TopPair\_\_ofHom\_\_\_auto\_1}$. Then the top pair of $f$ and $g$ is a homomorphism of $X$ and $Y$.

TopPair.ofSubsetdefMathlib.Topology.Category.TopPair, function or constant

Wording

the top pair of A (from the name)

English

Let $A$ be an element of the power set of the set of carriers of $X$. Then the top pair of $A$ is a top pair.

TopPair.ofTopCatdefMathlib.Topology.Category.TopPair, function or constant

Wording

the top pair of X (from the name)

English

Let $X$ be a topological category. Then the top pair of $X$ is a top pair.

TopPair.proj₁defMathlib.Topology.Category.TopPair, function or constant

Wording

the projection (from the name)

English

The projection is a functor of the set of top pairs and the set of topological categories defined as the composition of the forgetful functor from the full subcategory of $\operatorname{isEmbedding}$ and the right function.

TopPair.proj₁AdjDiagdefMathlib.Topology.Category.TopPair, function or constant

Wording

the projection functor to the first component (from the docstring)

English

The projection functor to the first component is an adjunction of the projection and the diagonal.

TopPair.proj₂defMathlib.Topology.Category.TopPair, function or constant

Wording

the projection (from the name)

English

TopPair.snddefMathlib.Topology.Category.TopPair, function or constant

Wording

the second space of the pair (from the docstring)

English

The second space of the pair is a topological category defined as the left subobject of $\operatorname{toComma}$ applied to $X$.

Mathlib.Topology.Category.UniformSpace

CpltSepUniformSpacestructureMathlib.Topology.Category.UniformSpace, type

Wording

no wording

English

The elements of $\mathrm{CpltSepUniformSpace}$ are a basic type.

CpltSepUniformSpace.ofdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{CpltSepUniformSpace}$ defined as $\operatorname{mk}$ applied to $X$.

CpltSepUniformSpace.toUniformSpacedefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the uniform space of X (from the name)

English

Let $X$ be an element of $\mathrm{CpltSepUniformSpace}$. Then the uniform space of $X$ is a uniform space category defined as $\operatorname{of}$ applied to $\mathrm{CpltSepUniformSpace\_\_\_u3b1\_}$ applied to $X$.

CpltSepUniformSpace.αdefMathlib.Topology.Category.UniformSpace, type

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{CpltSepUniformSpace}$. Then an element of $\mathrm{CpltSepUniformSpace\_\_\_u3b1\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

UniformSpaceCatstructureMathlib.Topology.Category.UniformSpace, type

Wording

uniform space category (from the name)

English

The uniform space categories are a basic type.

UniformSpaceCat.HomstructureMathlib.Topology.Category.UniformSpace, type

Wording

homomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be uniform space categories. Then the homomorphisms of $X$ and $Y$ are a basic type.

UniformSpaceCat.Hom.homdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an element of $\SubtypeSet {f_{1}}{\mathrm{UniformContinuous} (f_{1})}$ defined as the homomorphism of $f$.

UniformSpaceCat.Hom.hom'defMathlib.Topology.Category.UniformSpace, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an element of $\SubtypeSet {f}{\mathrm{UniformContinuous} (f)}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

UniformSpaceCat.adjdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the adjoint (from the name)

English

The adjoint is an adjunction of the completion functor and the forgetful functor of $\mathrm{CpltSepUniformSpace}$ and the set of uniform space categories.

UniformSpaceCat.carrierdefMathlib.Topology.Category.UniformSpace, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be a uniform space category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

UniformSpaceCat.completionFunctordefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the completion functor (from the name)

English

The completion functor is a functor of the set of uniform space categories and $\mathrm{CpltSepUniformSpace}$.

UniformSpaceCat.completionHomdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the inclusion of X (from the docstring)

English

Let $X$ be a uniform space category. Then the inclusion of $X$ is a homomorphism of $X$ and the action of the forgetful functor of $\mathrm{CpltSepUniformSpace}$ and the set of uniform space categories and the action of the completion functor and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{coe'}$.

UniformSpaceCat.extensionHomdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the extension homomorphism of f (from the name)

English

Let $f$ be a homomorphism of $X$ and the action of the forgetful functor of $\mathrm{CpltSepUniformSpace}$ and the set of uniform space categories and $Y$. Then the extension homomorphism of $f$ is a homomorphism of the action of the completion functor and $X$ and $Y$ defined as the concrete category of $\operatorname{extension}$ applied to $\operatorname{coe}$ applied to the homomorphism of $f$.

UniformSpaceCat.ofHomdefMathlib.Topology.Category.UniformSpace, function or constant

Wording

the uniform space category of f (from the name)

English

Let $f$ be an element of $\SubtypeSet {f_{1}}{\mathrm{UniformContinuous} (f_{1})}$. Then the uniform space category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.

Mathlib.Topology.Closure

Topology.closureOperatordefMathlib.Topology.Closure, function or constant

Wording

the closure operator of X (from the name)

English

Let $X$ be a set. Then the closure operator of $X$ is a closure operator of $\wp X$ defined as the closure operator of $\mathrm{closure}$ and the proposition that $\mathrm{IsClosed}$.

Mathlib.Topology.CompactOpen

ContinuousMap.coevdefMathlib.Topology.CompactOpen, function or constant

Wording

no wording

English

Let $X$ and $Y$ be sets. Let $b$ be an element of $Y$. Then $\operatorname{coev}$ applied to $X$, $Y$ and $b$ is a continuous map of $X$ and $\mathrm{Prod}$ applied to $Y$ and $X$.

ContinuousMap.compRightContinuousMapdefMathlib.Topology.CompactOpen, function or constant

Wording

the composition right continuous map of Z and f (from the name)

English

Let $Z$ be a set. Let $f$ be a continuous map of $X$ and $Y$. Then the composition right continuous map of $Z$ and $f$ is a continuous map of the set of continuous maps of $Y$ and $Z$ and the set of continuous maps of $X$ and $Z$.

ContinuousMap.const'defMathlib.Topology.CompactOpen, function or constant

Wording

the constant (from the name)

English

The constant is a continuous map of $Y$ and the set of continuous maps of $X$ and $Y$ defined as the curried form of the first component.

ContinuousMap.currydefMathlib.Topology.CompactOpen, function or constant

Wording

the curried form of f (from the docstring)

English

Let $f$ be a continuous map of $\mathrm{Prod}$ applied to $X$ and $Y$ and $Z$. Then the curried form of $f$ is a continuous map of $X$ and the set of continuous maps of $Y$ and $Z$.

ContinuousMap.homeoFnOfDiscretedefMathlib.Topology.CompactOpen, function or constant

Wording

the homeomorphism function (from the name)

English

The homeomorphism function is a homeomorphism of the set of continuous maps of $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.

ContinuousMap.uncurrydefMathlib.Topology.CompactOpen, function or constant

Wording

the uncurried form of f (from the docstring)

English

Let $f$ be a continuous map of $X$ and the set of continuous maps of $Y$ and $Z$. Then the uncurried form of $f$ is a continuous map of $\mathrm{Prod}$ applied to $X$ and $Y$ and $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{uncurry}$ applied to the function that maps $x_{3}$ and $y$ to $\operatorname{coe}$ applied to $f$, $x_{3}$ and $y$ and $\mathrm{ContinuousMap\_\_continuous\_uncurry\_of\_continuous}$ applied to $f$.

Homeomorph.arrowCongrdefMathlib.Topology.CompactOpen, function or constant

Wording

the arrow congruence of x4 and x5 (from the name)

English

Let $x_{4}$ be a homeomorphism of $X$ and $Z$. Let $x_{5}$ be a homeomorphism of $Y$ and $T$. Then the arrow congruence of $x_{4}$ and $x_{5}$ is a homeomorphism of the set of continuous maps of $X$ and $Y$ and the set of continuous maps of $Z$ and $T$.

Homeomorph.continuousMapOfUniquedefMathlib.Topology.CompactOpen, function or constant

Wording

the continuous map (from the name)

English

The continuous map is a homeomorphism of $Y$ and the set of continuous maps of $X$ and $Y$.

Homeomorph.currydefMathlib.Topology.CompactOpen, function or constant

Wording

the curry (from the name)

English

The curry is a homeomorphism of the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $Z$ and the set of continuous maps of $X$ and the set of continuous maps of $Y$ and $Z$.

Mathlib.Topology.Compactification.OnePoint.Basic

Homeomorph.onePointCongrdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the one point congruence of h (from the name)

English

Let $h$ be a homeomorphism of $X$ and $Y$. Then the one point congruence of $h$ is a homeomorphism of the set of one points of $X$ and the set of one points of $Y$.

OnePointdefMathlib.Topology.Compactification.OnePoint.Basic, type

Wording

one point of X (from the name)

English

Let $X$ be a set. Then an one point of $X$ is an element of the function that maps $X$ to $\mathrm{Option}$ applied to $X$.

OnePoint.continuousMapDiscreteEquivdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the continuous map discrete equivalence of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the continuous map discrete equivalence of $X$ and $Y$ is an element of $\EquivMACRoAE {\mathrm{ContinuousMap} (\mathrm{OnePoint} (X), Y)}{(\SubtypeSet {f}{\mathrm{exists} (Y , \lambda L . \operatorname{Tendsto} (\lambda x_{2} . f (x_{2}), \operatorname{cofinite} , \mathrm{nhds} (L)))})}$.

OnePoint.continuousMapMkdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the continuous map of f and y (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$. Let $y$ be an element of $Y$ such that $\operatorname{Tendsto}$ holds for $\operatorname{coe}$ applied to $f$, $\operatorname{coclosedCompact}$ applied to $X$ and the neighbourhood filter of $y$. Then the continuous map of $f$ and $y$ is a continuous map of the set of one points of $X$ and $Y$.

OnePoint.continuousMapMkDiscretedefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $y$ be an element of $Y$ such that $\operatorname{Tendsto}$ holds for $f$, the cofinite filter and the neighbourhood filter of $y$. Then $\operatorname{continuousMapMkDiscrete}$ applied to $f$, $y$ and $h_{1}$ is a continuous map of the set of one points of $X$ and $Y$.

OnePoint.continuousMapMkNatdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the continuous map natural number of f and y (from the name)

English

Let $f$ be a function from natural numbers to elements of $Y$. Let $y$ be an element of $Y$ such that $\operatorname{Tendsto}$ holds for $f$, $\operatorname{atTop}$ and the neighbourhood filter of $y$. Then the continuous map natural number of $f$ and $y$ is a continuous map of the set of one points of $\Natural$ and $Y$.

OnePoint.continuousMapNatEquivdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the continuous map natural equivalence of Y (from the name)

English

Let $Y$ be a set. Then the continuous map natural equivalence of $Y$ is an element of $\EquivMACRoAE {\mathrm{ContinuousMap} (\mathrm{OnePoint} (\Natural), Y)}{(\SubtypeSet {f}{\mathrm{exists} (Y , \lambda L . \operatorname{Tendsto} (\lambda x_{1} . f (x_{1}), \operatorname{atTop} , \mathrm{nhds} (L)))})}$.

OnePoint.elimdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the eliminator of x1 and x2 (from the name)

English

Let $x$ be an one point of $X$. Let $x_{1}$ be an element of $Y$. Let $x_{2}$ be a function from elements of $X$ to elements of $Y$. Then the eliminator of $x_{1}$ and $x_{2}$ is an element of $Y$ defined as $\operatorname{elim}$ applied to $x$, $x_{1}$ and $x_{2}$.

OnePoint.equivOfIsEmbeddingOfRangeEqdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the equivalence of y and f (from the name)

English

Let $y$ be an element of $Y$. Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is an embedding and the range of $f$ is equal to the complement of $\operatorname{singleton}$ applied to $y$. Then the equivalence of $y$ and $f$ is a homeomorphism of the set of one points of $X$ and $Y$.

OnePoint.inftydefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the infty (from the name)

English

The infty is an one point of $X$ defined as $\operatorname{none}$.

OnePoint.mapdefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the map of f and x (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $x$ be an one point of $X$. Then the map of $f$ and $x$ is an one point of $Y$ defined as $\operatorname{map}$ applied to $f$ and $x$.

OnePoint.opensOfCompldefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

the open of s (from the name)

English

Let $s$ be an element of $\wp X$ such that $s$ is closed and compact. Then the open of $s$ is an open of the set of one points of $X$.

OnePoint.somedefMathlib.Topology.Compactification.OnePoint.Basic, function or constant

Wording

no wording

English

Let $x$ be an element of $X$. Then $\operatorname{some}$ applied to $x$ is an one point of $X$ defined as $\operatorname{some}$ applied to $x$.

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Matrix.GeneralLinearGroup.parabolicFixedPointdefMathlib.Topology.Compactification.OnePoint.ProjectiveLine, function or constant

Wording

the parabolic fixed point of g (from the name)

English

Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $K$. Then the parabolic fixed point of $g$ is an one point of $K$ defined as $\iteMACRoG {(\EqtMACRoH {\operatorname{val} (g)}{0})}{\operatorname{infty}}{\operatorname{some} (\frac{ \operatorname{val} (g)- \operatorname{val} (g)}{2 \times \operatorname{val} (g)})}$.

OnePoint.equivProjectivizationdefMathlib.Topology.Compactification.OnePoint.ProjectiveLine, function or constant

Wording

the equivalence projectivization of K (from the name)

English

Let $K$ be a set. Then the equivalence projectivization of $K$ is an equivalence from the set of one points of $K$ to the set of projectivizations of $K$ and the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $K$.

Mathlib.Topology.Compactification.OnePoint.Sphere

onePointEquivSphereOfFinrankEqdefMathlib.Topology.Compactification.OnePoint.Sphere, function or constant

Wording

the one point equivalence sphere of h4 (from the name)

English

Assume that the sum of the rank of $\Real$ and $V$ and $1$ is equal to the cardinality of $x$. Then the one point equivalence sphere of $h_{4}$ is a homeomorphism of the set of one points of $V$ and the set of elements of the sphere of $0$ and $1$.

onePointHyperplaneHomeoUnitSpheredefMathlib.Topology.Compactification.OnePoint.Sphere, function or constant

Wording

the one point hyperplane homeomorphism unit sphere of hv (from the name)

English

Assume that $\operatorname{norm} (v)= 1$. Then the one point hyperplane homeomorphism unit sphere of $\mathrm{hv}$ is a homeomorphism of the set of one points of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (\Real , \operatorname{singleton} (v)))}{x_{2}})}$ and the set of elements of the sphere of $0$ and $1$.

Mathlib.Topology.Compactification.StoneCech

StoneCechdefMathlib.Topology.Compactification.StoneCech, type

Wording

Stone Cech of x (from the name)

English

Let $x$ be a set. Then a Stone Cech of $x$ is an element of the function that maps $x$ to the set of quotients of $\mathrm{PreStoneCech}$ applied to $x$.

Ultrafilter.extenddefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the extension of f and x3 (from the docstring)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be a ultrafilter of $x$. Then the extension of $f$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{extend}$ applied to $\mathrm{isDenseInducing\_pure}$, $f$ and $x_{3}$.

preStoneCechExtenddefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the extension of hg and x4 (from the docstring)

English

Assume that $g$ is continuous. Let $x_{4}$ be an element of $\mathrm{PreStoneCech}$ applied to $x$. Then the extension of $\mathrm{hg}$ and $x_{4}$ is an element of $x_{2}$.

preStoneCechUnitdefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the Stone Cech unit of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the Stone Cech unit of $x_{2}$ is an element of $\mathrm{PreStoneCech}$ applied to $x$ defined as $\operatorname{mk}$ applied to the function that maps $F$ and $G$ to the proposition that there exists an element $x_{3}$ of $x$, such that $\operatorname{toFilter}$ applied to $F$ is less than or equal to the neighbourhood filter of $x_{3}$ and $\operatorname{toFilter}$ applied to $G$ is less than or equal to the neighbourhood filter of $x_{3}$ and $\operatorname{pure}$ applied to $x_{2}$.

stoneCechExtenddefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the extension of hg and x4 (from the docstring)

English

Assume that $g$ is continuous. Let $x_{4}$ be a Stone Cech of $x$. Then the extension of $\mathrm{hg}$ and $x_{4}$ is an element of $x_{2}$ defined as the lift of $\mathrm{continuous\_preStoneCechExtend}$ applied to $\mathrm{hg}$ and $x_{4}$.

stoneCechUnitdefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the Stone Cech unit of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the Stone Cech unit of $x_{2}$ is a Stone Cech of $x$ defined as $\operatorname{mk}$ applied to the Stone Cech unit of $x_{2}$.

ultrafilterBasisdefMathlib.Topology.Compactification.StoneCech, function or constant

Wording

the ultrafilter basis of x (from the name)

English

Let $x$ be a set. Then the ultrafilter basis of $x$ is an element of the power set of the power set of the set of ultrafilters of $x$ defined as the range of the function that maps $s$ to $\operatorname{ofPred}$ applied to the function that maps $u$ to $\MembershipmemMACRoT {u}{s}$.

Mathlib.Topology.Compactness.CompactSystem

IsCompactSystemdefMathlib.Topology.Compactness.CompactSystem, predicate

Wording

S is a compact system (from the docstring)

English

Let $S$ be an element of $\wp (\wp x)$. Then $S$ is a compact system, if for all functions $C$ from natural numbers to elements of $\wp x$, if for all natural numbers $i_{1}$, $\MembershipmemMACRoT {S}{C (i_{1})}$, then if the intersection of the function that maps $i$ to $C$ applied to $i$ is equal to $\operatorname{emptyCollection}$, then there exists a natural number $n$, such that $\EqtMACRoH {\operatorname{dissipate} (C , n)}{\operatorname{emptyCollection}}$.

compactClosedSquareCylindersdefMathlib.Topology.Compactness.CompactSystem, function or constant

Wording

the compact closed square cylinder of x1 (from the name)

English

Let $x_{1}$ be a function from elements of $x$ to sets. Then the compact closed square cylinder of $x_{1}$ is an element of $\wp (\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i)))$ defined as the square cylinder of the function that maps $i$ to $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is compact and closed.

Mathlib.Topology.Compactness.CompactlyCoherentSpace

CompactCoherentificationdefMathlib.Topology.Compactness.CompactlyCoherentSpace, type

Wording

compact coherentification of X (from the name)

English

Let $X$ be a set. Then a compact coherentification of $X$ is an element of the function that maps $X$ to $X$.

CompactCoherentification.homeodefMathlib.Topology.Compactness.CompactlyCoherentSpace, function or constant

Wording

the homeomorphism (from the name)

English

The homeomorphism is a homeomorphism of $X$ and the set of compact coherentifications of $X$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $X$, $\mathrm{CompactCoherentification\_\_continuous\_mk}$ and $\mathrm{CompactCoherentification\_\_continuous\_mk\_symm}$.

CompactCoherentification.mapdefMathlib.Topology.Compactness.CompactlyCoherentSpace, function or constant

Wording

the map of f and x (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $x$ be a compact coherentification of $X$. Then the map of $f$ and $x$ is a compact coherentification of $Y$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\operatorname{mk}$ applied to $Y$, $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to the inverse of $\operatorname{mk}$ applied to $X$ and $x$.

CompactCoherentification.mkdefMathlib.Topology.Compactness.CompactlyCoherentSpace, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{mk}$ applied to $X$ is an equivalence from $X$ to the set of compact coherentifications of $X$ defined as the identity of $X$.

CompactlyCoherentSpaceclassMathlib.Topology.Compactness.CompactlyCoherentSpace, predicate

Wording

X is a compactly coherent space (from the docstring)

English

generation took over the time limit

Mathlib.Topology.Compactness.CompactlyGeneratedSpace

CompactlyGeneratedSpacedefMathlib.Topology.Compactness.CompactlyGeneratedSpace, predicate

Wording

no wording

English

Let $X$ be a set. Then $\mathrm{CompactlyGeneratedSpace}$ holds for $X$, if $\mathrm{UCompactlyGeneratedSpace}$ holds for $X$.

UCompactlyGeneratedSpaceclassMathlib.Topology.Compactness.CompactlyGeneratedSpace, predicate

Wording

no wording

English

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

Mathlib.Topology.Compactness.CountablyCompact

CountablyCompactSpaceclassMathlib.Topology.Compactness.CountablyCompact, predicate

Wording

E is countably compact (from the docstring)

English

generation took over the time limit

IsCountablyCompactdefMathlib.Topology.Compactness.CountablyCompact, predicate

Wording

A is countably compact (from the name)

English

generation took over the time limit

Mathlib.Topology.Compactness.DeltaGeneratedSpace

DeltaGeneratedSpacedefMathlib.Topology.Compactness.DeltaGeneratedSpace, predicate

Wording

no wording

English

Let $Y$ be a set. Then $\mathrm{DeltaGeneratedSpace}$ holds for $Y$, if $\operatorname{IsGeneratedBy}$ holds for the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers and $Y$.

DeltaGeneratedSpace.ofdefMathlib.Topology.Compactness.DeltaGeneratedSpace, type

Wording

no wording

English

An element of $\operatorname{of}$ is an element of $\operatorname{WithGeneratedByTopology}$ applied to the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers and $Y$.

Mathlib.Topology.Compactness.Lindelof

Filter.coLindelofdefMathlib.Topology.Compactness.Lindelof, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{coLindelof}$ applied to $X$ is a filter of $X$ defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to the principal filter of the complement of $s$.

Filter.coclosedLindelofdefMathlib.Topology.Compactness.Lindelof, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{coclosedLindelof}$ applied to $X$ is a filter of $X$ defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to the infimum of the function that maps $h_{1}$ to the principal filter of the complement of $s$.

HereditarilyLindelofSpaceclassMathlib.Topology.Compactness.Lindelof, predicate

Wording

no wording

English

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

IsHereditarilyLindelofdefMathlib.Topology.Compactness.Lindelof, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{IsHereditarilyLindelof}$ holds for $s$, if for all elements $t$ of $\wp X$, if $t \leq s$, then $t$ is a Lindelof.

IsLindelofdefMathlib.Topology.Compactness.Lindelof, predicate

Wording

s is a Lindelof (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is a Lindelof, if for all filters $f$ of $X$, if $\operatorname{NeBot}$ holds for $f$, then if $f$ is a countable intersection filter, then if $f$ is less than or equal to the principal filter of $s$, then there exists an element $x_{1}$ of $X$, such that $x_{1}$ is an element of $s$ and $\mathrm{ClusterPt}$ holds for $x_{1}$ and $f$.

LindelofSpaceclassMathlib.Topology.Compactness.Lindelof, predicate

Wording

X is a Lindelof space (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a Lindelof space.

NonLindelofSpaceclassMathlib.Topology.Compactness.Lindelof, predicate

Wording

no wording

English

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

Mathlib.Topology.Compactness.Paracompact

ParacompactSpaceclassMathlib.Topology.Compactness.Paracompact, predicate

Wording

X is a paracompact space (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a paracompact space.

Mathlib.Topology.Compactness.SigmaCompact

CompactExhaustionstructureMathlib.Topology.Compactness.SigmaCompact, type

Wording

compact exhaustion of X (from the name)

English

Let $X$ be a set. Then the compact exhaustions of $X$ are a basic type.

CompactExhaustion.choicedefMathlib.Topology.Compactness.SigmaCompact, function or constant

Wording

the choice of X (from the name)

English

Let $X$ be a set. Then the choice of $X$ is a compact exhaustion of $X$.

CompactExhaustion.finddefMathlib.Topology.Compactness.SigmaCompact, function or constant

Wording

no wording

English

Let $K$ be a compact exhaustion of $X$. Let $x_{1}$ be an element of $X$. Then $\operatorname{find}$ applied to $K$ and $x_{1}$ is a natural number defined as $\operatorname{find}$ applied to $\mathrm{CompactExhaustion\_\_exists\_mem}$ applied to $K$ and $x_{1}$.

CompactExhaustion.shiftrdefMathlib.Topology.Compactness.SigmaCompact, function or constant

Wording

no wording

English

Let $K$ be a compact exhaustion of $X$. Then $\operatorname{shiftr}$ applied to $K$ is a compact exhaustion of $X$.

CompactExhaustion.toFundefMathlib.Topology.Compactness.SigmaCompact, function or constant

Wording

the compact exhaustion of self and x1 (from the name)

English

Let $\mathrm{self}$ be a compact exhaustion of $X$. Let $x_{1}$ be a natural number. Then the compact exhaustion of $\mathrm{self}$ and $x_{1}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

IsSigmaCompactdefMathlib.Topology.Compactness.SigmaCompact, predicate

Wording

s is a sigma compact (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is a sigma compact, if there exists a function $K$ from natural numbers to elements of $\wp X$, such that for all natural numbers $n$, $K$ applied to $n$ is compact and the union of the function that maps $n_{1}$ to $K$ applied to $n_{1}$ is equal to $s$.

SigmaCompactSpaceclassMathlib.Topology.Compactness.SigmaCompact, predicate

Wording

X is a sigma compact space (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a sigma compact space.

compactCoveringdefMathlib.Topology.Compactness.SigmaCompact, function or constant

Wording

the compact covering of X and x1 (from the name)

English

Let $X$ be a set. Let $x_{1}$ be a natural number. Then the compact covering of $X$ and $x_{1}$ is an element of $\wp X$ defined as $\operatorname{accumulate}$ applied to $\operatorname{choose}$ applied to $\mathrm{SigmaCompactSpace\_\_exists\_compact\_covering}$ and $x_{1}$.

Mathlib.Topology.Connected.Basic

ConnectedSpaceclassMathlib.Topology.Connected.Basic, predicate

Wording

x is a connected space (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a connected space.

IsConnecteddefMathlib.Topology.Connected.Basic, predicate

Wording

s is connected (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is connected, if $s$ is nonempty and preconnected.

IsPreconnecteddefMathlib.Topology.Connected.Basic, predicate

Wording

s is preconnected (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is preconnected, if for all elements $u$ and $v$ of $\wp x$, if $u$ is open, then if $v$ is open, then if $s \leq \UnionunionMACRoAB {u}{v}$, then if $\operatorname{inter}$ applied to $s$ and $u$ is nonempty, then if $\operatorname{inter}$ applied to $s$ and $v$ is nonempty, then $\operatorname{inter}$ applied to $s$ and $\operatorname{inter}$ applied to $u$ and $v$ is nonempty.

PreconnectedSpaceclassMathlib.Topology.Connected.Basic, predicate

Wording

x is a preconnected space (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a preconnected space.

connectedComponentdefMathlib.Topology.Connected.Basic, function or constant

Wording

the connected component of x2 (from the docstring)

English

Let $x_{2}$ be an element of $x$. Then the connected component of $x_{2}$ is an element of $\wp x$ defined as the union of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is preconnected and $x_{2}$ is an element of $s$.

connectedComponentIndefMathlib.Topology.Connected.Basic, function or constant

Wording

no wording

English

Let $F$ be an element of $\wp x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{connectedComponentIn}$ applied to $F$ and $x_{2}$ is an element of $\wp x$ defined as $\mathrm{dite}$ applied to $\MembershipmemMACRoT {F}{x_{2}}$, the function that maps $h$ to the image of the function that maps $x_{3}$ to $\MembershipmemMACRoT {F}{x_{3}}$ and the connected component of $x_{2}$ and the function that maps $h_{1}$ to $\operatorname{emptyCollection}$.

Mathlib.Topology.Connected.Clopen

ConnectedComponentsdefMathlib.Topology.Connected.Clopen, type

Wording

connected component of x (from the name)

English

Let $x$ be a set. Then a connected component of $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\mathrm{connectedComponentSetoid}$ applied to $x$.

ConnectedComponents.equivOfIsClopendefMathlib.Topology.Connected.Clopen, function or constant

Wording

the equivalence of hdisj and hunion (from the name)

English

Assume that for all elements $i_{2}$ of $x_{2}$, $U$ applied to $i_{2}$ is a clopen. Assume that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $U$ is pairwise. Assume that the union of the function that maps $i_{1}$ to $U$ applied to $i_{1}$ is equal to the universal set. Then the equivalence of $\mathrm{hdisj}$ and $\mathrm{hunion}$ is an equivalence from the set of connected components of $x$ to $\Sigma$ applied to the function that maps $i$ to the set of connected components of the set of elements of $U$ applied to $i$.

ConnectedComponents.equivOfIsClopenOfIsConnecteddefMathlib.Topology.Connected.Clopen, function or constant

Wording

the equivalence of hunion and hconn (from the name)

English

Assume that for all elements $i_{2}$ of $x_{2}$, $U$ applied to $i_{2}$ is a clopen. Assume that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $U$ is pairwise. Assume that the union of the function that maps $i_{1}$ to $U$ applied to $i_{1}$ is equal to the universal set. Assume that for all elements $i$ of $x_{2}$, $U$ applied to $i$ is connected. Then the equivalence of $\mathrm{hunion}$ and $\mathrm{hconn}$ is an equivalence from the set of connected components of $x$ to $x_{2}$ defined as the composition of the equivalence of $\mathrm{hdisj}$ and $\mathrm{hunion}$ and $\operatorname{sigmaUnique}$ applied to $x_{2}$ and the function that maps $i$ to the set of connected components of the set of elements of $U$ applied to $i$.

ConnectedComponents.mkdefMathlib.Topology.Connected.Clopen, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{mk}$ applied to $x_{2}$ is a connected component of $x$ defined as $\operatorname{mk''}$ applied to $x_{2}$.

Mathlib.Topology.Connected.LocallyConnected

LocallyConnectedSpaceclassMathlib.Topology.Connected.LocallyConnected, predicate

Wording

x is a locally connected space (from the name)

English

generation took over the time limit

Mathlib.Topology.Connected.LocallyPathConnected

LocallyPathConnectedSpaceclassMathlib.Topology.Connected.LocallyPathConnected, predicate

Wording

no wording

English

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

connectedComponentsEquivZerothHomotopydefMathlib.Topology.Connected.LocallyPathConnected, function or constant

Wording

the connected component equivalence zeroth homotopy (from the name)

English

The connected component equivalence zeroth homotopy is an equivalence from the set of connected components of $X$ to the set of zeroth homotopies of $X$.

Mathlib.Topology.Connected.PathComponentOne

OpenNormalAddSubgroup.pathComponentZerodefMathlib.Topology.Connected.PathComponentOne, function or constant

Wording

the path component zero of G (from the name)

English

Let $G$ be a set. Then the path component zero of $G$ is an open normal additive subgroup of $G$.

OpenNormalSubgroup.pathComponentOnedefMathlib.Topology.Connected.PathComponentOne, function or constant

Wording

the path component one of G (from the name)

English

Let $G$ be a set. Then the path component one of $G$ is an open normal subgroup of $G$.

Mathlib.Topology.Connected.PathConnected

AddSubgroup.pathComponentZerodefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the path component zero of G (from the name)

English

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

AddSubmonoid.pathComponentZerodefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the path component zero of M (from the name)

English

Let $M$ be a set. Then the path component zero of $M$ is an additive submonoid of $M$.

IsPathConnecteddefMathlib.Topology.Connected.PathConnected, predicate

Wording

no wording

English

Let $F$ be an element of $\wp X$. Then $\mathrm{IsPathConnected}$ holds for $F$, if there exists an element $x_{1}$ of $X$, such that $x_{1}$ is an element of $F$ and for all elements $y$ of $X$, if $y$ is an element of $F$, then $\mathrm{JoinedIn}$ holds for $F$, $x_{1}$ and $y$.

JoineddefMathlib.Topology.Connected.PathConnected, predicate

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $X$. Then $\mathrm{Joined}$ holds for $x_{1}$ and $y$, if $\mathrm{Nonempty}$ holds for the set of paths of $x_{1}$ and $y$.

Joined.somePathdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

no wording

English

Assume that $\mathrm{Joined}$ holds for $x_{1}$ and $y$. Then $\operatorname{somePath}$ applied to $h$ is a path of $x_{1}$ and $y$ defined as $\operatorname{some}$ applied to $h$.

JoinedIndefMathlib.Topology.Connected.PathConnected, predicate

Wording

no wording

English

Let $F$ be an element of $\wp X$. Let $x_{1}$ and $y$ be elements of $X$. Then $\mathrm{JoinedIn}$ holds for $F$, $x_{1}$ and $y$, if there exists a path $x_{2}$ of $x_{1}$ and $y$, such that for all elements $t$ of the unit interval, $\MembershipmemMACRoT {F}{x_{2} (t)}$.

JoinedIn.somePathdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

no wording

English

Assume that $\mathrm{JoinedIn}$ holds for $F$, $x_{1}$ and $y$. Then $\operatorname{somePath}$ applied to $h$ is a path of $x_{1}$ and $y$ defined as $\operatorname{choose}$ applied to $h$.

PathConnectedSpaceclassMathlib.Topology.Connected.PathConnected, predicate

Wording

X is a path connected space (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a path connected space.

PathConnectedSpace.somePathdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $X$. Then $\operatorname{somePath}$ applied to $x_{1}$ and $y$ is a path of $x_{1}$ and $y$ defined as $\operatorname{some}$ applied to $\operatorname{joined}$ applied to $x_{1}$ and $y$.

Subgroup.pathComponentOnedefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the path component one of G (from the name)

English

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

Submonoid.pathComponentOnedefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the path component one of M (from the name)

English

Let $M$ be a set. Then the path component one of $M$ is a submonoid of $M$.

ZerothHomotopydefMathlib.Topology.Connected.PathConnected, type

Wording

zeroth homotopy of X (from the name)

English

Let $X$ be a set. Then a zeroth homotopy of $X$ is an element of the function that maps $X$ to $\mathrm{Quotient}$ applied to $\mathrm{pathSetoid}$ applied to $X$.

ZerothHomotopy.liftdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the lift of f and x1 (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $T$ such that for all elements $x_{2}$ and $y$ of $X$, for all paths $x_{3}$ of $x_{2}$ and $y$, $\EqtMACRoH {f (x_{2})}{f (y)}$. Let $x_{1}$ be a zeroth homotopy of $X$. Then the lift of $f$ and $x_{1}$ is an element of $T$.

ZerothHomotopy.mkdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $X$. Then $\operatorname{mk}$ applied to $x_{1}$ is a zeroth homotopy of $X$ defined as $\operatorname{mk}$ applied to $\mathrm{pathSetoid}$ applied to $X$ and $x_{1}$.

ZerothHomotopy.toConnectedComponentsdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the connected component of x1 (from the name)

English

Let $x_{1}$ be a zeroth homotopy of $X$. Then the connected component of $x_{1}$ is a connected component of $X$.

pathComponentdefMathlib.Topology.Connected.PathConnected, function or constant

Wording

the path component of x1 (from the docstring)

English

Let $x_{1}$ be an element of $X$. Then the path component of $x_{1}$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Joined}$ applied to $x_{1}$ and $y$.

pathComponentIndefMathlib.Topology.Connected.PathConnected, function or constant

Wording

no wording

English

Let $F$ be an element of $\wp X$. Let $x_{1}$ be an element of $X$. Then $\mathrm{pathComponentIn}$ applied to $F$ and $x_{1}$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{JoinedIn}$ applied to $F$, $x_{1}$ and $y$.

Mathlib.Topology.Connected.TotallyDisconnected

Continuous.connectedComponentsLiftdefMathlib.Topology.Connected.TotallyDisconnected, function or constant

Wording

the connected component lift of h1 and x4 (from the name)

English

Assume that $f$ is continuous. Let $x_{4}$ be a connected component of $x$. Then the connected component lift of $h_{1}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{liftOn'}$ applied to $x_{4}$, $f$ and $\mathrm{Continuous\_\_image\_eq\_of\_connectedComponent\_eq}$ applied to $h_{1}$.

Continuous.connectedComponentsMapdefMathlib.Topology.Connected.TotallyDisconnected, function or constant

Wording

the connected component map of h and x4 (from the name)

English

Assume that $f$ is continuous. Let $x_{4}$ be a connected component of $x$. Then the connected component map of $h$ and $x_{4}$ is a connected component of $x_{2}$.

IsTotallyDisconnecteddefMathlib.Topology.Connected.TotallyDisconnected, predicate

Wording

s is totally disconnected (from the name)

English

generation took over the time limit

IsTotallySeparateddefMathlib.Topology.Connected.TotallyDisconnected, predicate

Wording

s is totally separated (from the name)

English

generation took over the time limit

TotallyDisconnectedSpaceclassMathlib.Topology.Connected.TotallyDisconnected, predicate

Wording

x is totally disconnected (from the docstring)

English

generation took over the time limit

TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpacedefMathlib.Topology.Connected.TotallyDisconnected, function or constant

Wording

the continuous map equivalence of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the continuous map equivalence of $X$ and $Y$ is an equivalence from the set of continuous maps of $X$ and $Y$ to $Y$.

TotallySeparatedSpaceclassMathlib.Topology.Connected.TotallyDisconnected, predicate

Wording

x is totally separated (from the docstring)

English

generation took over the time limit

Mathlib.Topology.Constructible

IsRetrocompactdefMathlib.Topology.Constructible, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{IsRetrocompact}$ holds for $s$, if for all elements $U$ of $\wp X$, if $U$ is compact, then if $U$ is open, then $\operatorname{inter}$ applied to $s$ and $U$ is compact.

Topology.IsConstructibledefMathlib.Topology.Constructible, predicate

Wording

s is constructible (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is constructible, if $s$ is an element of the closure of $\operatorname{ofPred}$ applied to the function that maps $U$ to the proposition that $U$ is open and $\mathrm{IsRetrocompact}$ holds for $U$.

Topology.IsLocallyConstructibledefMathlib.Topology.Constructible, predicate

Wording

s is locally constructible (from the name)

English

generation took over the time limit

Mathlib.Topology.Constructions

CofiniteTopologydefMathlib.Topology.Constructions, type

Wording

cofinite topology of X (from the name)

English

Let $X$ be a set. Then a cofinite topology of $X$ is an element of the function that maps $X$ to $\mathrm{WithTopology}$ applied to $X$ and $\operatorname{cofinite}$.

CofiniteTopology.ofdefMathlib.Topology.Constructions, function or constant

Wording

no wording

English

$\operatorname{of}$ is an equivalence from $X$ to the set of cofinite topologies of $X$ defined as the inverse of the equivalence of $X$ and $\operatorname{cofinite}$.

ContinuousMap.uliftEquivdefMathlib.Topology.Constructions, function or constant

Wording

the lift equivalence of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the lift equivalence of $X$ and $Y$ is an equivalence from the set of continuous maps of $\mathrm{ULift}$ applied to $X$ and $\mathrm{ULift}$ applied to $Y$ to the set of continuous maps of $X$ and $Y$.

Homeomorph.ofEqSubtypesdefMathlib.Topology.Constructions, function or constant

Wording

the homeomorphism of hpq (from the name)

English

Assume that $\EqtMACRoH {p}{q}$. Then the homeomorphism of $\mathrm{hpq}$ is a homeomorphism of $\SubtypeSet {x_{1}}{p (x_{1})}$ and $\SubtypeSet {x_{2}}{q (x_{2})}$.

Homeomorph.piCurrydefMathlib.Topology.Constructions, function or constant

Wording

the product curry (from the name)

English

The product curry is a homeomorphism of the set of functions from elements of $\mathrm{Prod}$ applied to $X$ and $Y$ to elements of $Z$ and the set of functions from elements of $X$ and elements of $Y$ to elements of $Z$.

IsDiscretestructureMathlib.Topology.Constructions, predicate

Wording

s is discrete (from the name)

English

Let $s$ be an element of $\wp X$. Then we can say that $s$ is discrete.

Mathlib.Topology.Constructions.SumProd

Homeomorph.emptySumdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the empty sum of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the empty sum of $X$ and $Y$ is a homeomorphism of $\mathrm{Sum}$ applied to $Y$ and $X$ and $X$ defined as the composition of $\operatorname{sumComm}$ applied to $Y$ and $X$ and $\operatorname{sumEmpty}$ applied to $X$ and $Y$.

Homeomorph.prodAssocdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the product associator of Y and Z (from the name)

English

Let $X$, $Y$ and $Z$ be sets. Then the product associator of $Y$ and $Z$ is a homeomorphism of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $X$ and $Y$ and $Z$ and $\mathrm{Prod}$ applied to $X$ and $\mathrm{Prod}$ applied to $Y$ and $Z$.

Homeomorph.prodCommdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$ and $Y$ be sets. Then $\operatorname{prodComm}$ applied to $X$ and $Y$ is a homeomorphism of $\mathrm{Prod}$ applied to $X$ and $Y$ and $\mathrm{Prod}$ applied to $Y$ and $X$.

Homeomorph.prodCongrdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the product congruence of x4 and x5 (from the name)

English

Let $x_{4}$ be a homeomorphism of $X$ and $\mathrm{X'}$. Let $x_{5}$ be a homeomorphism of $Y$ and $\mathrm{Y'}$. Then the product congruence of $x_{4}$ and $x_{5}$ is a homeomorphism of $\mathrm{Prod}$ applied to $X$ and $Y$ and $\mathrm{Prod}$ applied to $\mathrm{X'}$ and $\mathrm{Y'}$.

Homeomorph.prodPUnitdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the product unit of X (from the name)

English

Let $X$ be a set. Then the product unit of $X$ is a homeomorphism of $\mathrm{Prod}$ applied to $X$ and $\mathrm{PUnit}$ and $X$.

Homeomorph.prodProdProdCommdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$, $Y$, $W$ and $Z$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $X$, $Y$, $W$ and $Z$ is a homeomorphism of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $X$ and $Y$ and $\mathrm{Prod}$ applied to $W$ and $Z$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $X$ and $W$ and $\mathrm{Prod}$ applied to $Y$ and $Z$.

Homeomorph.prodSumDistribdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

$\operatorname{prodSumDistrib}$ is a homeomorphism of $\mathrm{Prod}$ applied to $X$ and $\mathrm{Sum}$ applied to $Y$ and $Z$ and $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $X$ and $Y$ and $\mathrm{Prod}$ applied to $X$ and $Z$ defined as the composition of $\operatorname{prodComm}$ applied to $X$ and $\mathrm{Sum}$ applied to $Y$ and $Z$ and the composition of $\operatorname{sumProdDistrib}$ and the sum congruence of $\operatorname{prodComm}$ applied to $Y$ and $X$ and $\operatorname{prodComm}$ applied to $Z$ and $X$.

Homeomorph.punitProddefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\operatorname{punitProd}$ applied to $X$ is a homeomorphism of $\mathrm{Prod}$ applied to $\mathrm{PUnit}$ and $X$ and $X$ defined as the composition of $\operatorname{prodComm}$ applied to $\mathrm{PUnit}$ and $X$ and the product unit of $X$.

Homeomorph.sumAssocdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the sum associator of Y and Z (from the name)

English

Let $X$, $Y$ and $Z$ be sets. Then the sum associator of $Y$ and $Z$ is a homeomorphism of $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $X$ and $Y$ and $Z$ and $\mathrm{Sum}$ applied to $X$ and $\mathrm{Sum}$ applied to $Y$ and $Z$.

Homeomorph.sumCommdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$ and $Y$ be sets. Then $\operatorname{sumComm}$ applied to $X$ and $Y$ is a homeomorphism of $\mathrm{Sum}$ applied to $X$ and $Y$ and $\mathrm{Sum}$ applied to $Y$ and $X$.

Homeomorph.sumCongrdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

the sum congruence of x4 and x5 (from the name)

English

Let $x_{4}$ be a homeomorphism of $X$ and $\mathrm{X'}$. Let $x_{5}$ be a homeomorphism of $Y$ and $\mathrm{Y'}$. Then the sum congruence of $x_{4}$ and $x_{5}$ is a homeomorphism of $\mathrm{Sum}$ applied to $X$ and $Y$ and $\mathrm{Sum}$ applied to $\mathrm{X'}$ and $\mathrm{Y'}$.

Homeomorph.sumEmptydefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$ and $Y$ be sets. Then $\operatorname{sumEmpty}$ applied to $X$ and $Y$ is a homeomorphism of $\mathrm{Sum}$ applied to $X$ and $Y$ and $X$.

Homeomorph.sumProdDistribdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

$\operatorname{sumProdDistrib}$ is a homeomorphism of $\mathrm{Prod}$ applied to $\mathrm{Sum}$ applied to $X$ and $Y$ and $Z$ and $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $X$ and $Z$ and $\mathrm{Prod}$ applied to $Y$ and $Z$.

Homeomorph.sumSumSumCommdefMathlib.Topology.Constructions.SumProd, function or constant

Wording

no wording

English

Let $X$, $Y$, $W$ and $Z$ be sets. Then $\operatorname{sumSumSumComm}$ applied to $X$, $Y$, $W$ and $Z$ is a homeomorphism of $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $X$ and $Y$ and $\mathrm{Sum}$ applied to $W$ and $Z$ and $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $X$ and $W$ and $\mathrm{Sum}$ applied to $Y$ and $Z$.

Mathlib.Topology.Continuous

DenseRange.somedefMathlib.Topology.Continuous, function or constant

Wording

no wording

English

Assume that $f$ is a dense range. Let $x_{2}$ be an element of $X$. Then $\operatorname{some}$ applied to $\mathrm{hf}$ and $x_{2}$ is an element of $x_{1}$.

LibraryNote.comp_of_eq_lemmasdefMathlib.Topology.Continuous, function or constant

Wording

the composition (from the name)

English

The composition is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

LibraryNote.continuity_lemma_statementdefMathlib.Topology.Continuous, function or constant

Wording

the continuity lemma statement (from the name)

English

The continuity lemma statement is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.

Mathlib.Topology.ContinuousMap.Algebra

AddMonoidHom.compLeftContinuousdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

Let $x$ be a set. Let $g$ be an additive monoid homomorphism of $x_{1}$ and $x_{4}$ such that $\operatorname{coe}$ applied to $g$ is continuous. Then $\operatorname{compLeftContinuous}$ applied to $x$, $g$ and $\mathrm{hg}$ is an additive monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{4}$.

AlgHom.compLeftContinuousdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $g$ be an algebra homomorphism of $A$ and $x_{4}$ such that $\operatorname{coe}$ applied to $g$ is continuous. Then $\operatorname{compLeftContinuous}$ applied to $R$, $g$ and $\mathrm{hg}$ is an algebra homomorphism of the set of continuous maps of $x_{8}$ and $A$ and the set of continuous maps of $x_{8}$ and $x_{4}$.

ContinuousLinearMap.compLeftContinuousdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

Let $R$ and $x_{8}$ be sets. Let $g$ be a continuous linear map of $M$ and $x_{1}$. Then $\operatorname{compLeftContinuous}$ applied to $R$, $x_{8}$ and $g$ is a continuous linear map of the set of continuous maps of $x_{8}$ and $M$ and the set of continuous maps of $x_{8}$ and $x_{1}$.

ContinuousLinearMap.constdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the constant map of R and x4 (from the docstring)

English

Let $R$ and $x_{4}$ be sets. Then the constant map of $R$ and $x_{4}$ is a continuous linear map of $M$ and the set of continuous maps of $x_{4}$ and $M$.

ContinuousMap.CdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $R$ and the set of continuous maps of $x$ and $A$.

ContinuousMap.coeFnAddMonoidHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

ContinuousMap.coeFnAlgHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function algebra homomorphism of R (from the name)

English

Let $R$ be a set. Then the coercion function algebra homomorphism of $R$ is an algebra homomorphism of the set of continuous maps of $x$ and $A$ and the set of functions from elements of $x$ to elements of $A$.

ContinuousMap.coeFnCLMdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function continuous linear map of R (from the name)

English

Let $R$ be a set. Then the coercion function continuous linear map of $R$ is a continuous linear map of the set of continuous maps of $x$ and $M$ and the set of functions from elements of $x$ to elements of $M$.

ContinuousMap.coeFnLinearMapdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function linear map of R (from the name)

English

Let $R$ be a set. Then the coercion function linear map of $R$ is a linear map of the set of continuous maps of $x$ and $M$ and the set of functions from elements of $x$ to elements of $M$.

ContinuousMap.coeFnMonoidHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function monoid homomorphism (from the name)

English

The coercion function monoid homomorphism is a monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

ContinuousMap.coeFnRingHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the coercion function ring homomorphism (from the name)

English

The coercion function ring homomorphism is a ring homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

ContinuousMap.compAddMonoidHom'defMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the composition additive monoid homomorphism of g (from the name)

English

Let $g$ be a continuous map of $x$ and $x_{1}$. Then the composition additive monoid homomorphism of $g$ is an additive monoid homomorphism of the set of continuous maps of $x_{1}$ and $x_{4}$ and the set of continuous maps of $x$ and $x_{4}$.

ContinuousMap.compCLMdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

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

English

Let $R$ and $M$ be sets. Let $f$ be a continuous map of $x$ and $x_{1}$. Then the composition continuous linear map of $f$ is a continuous linear map of the set of continuous maps of $x_{1}$ and $M$ and the set of continuous maps of $x$ and $M$.

ContinuousMap.compMonoidHom'defMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the composition monoid homomorphism of g (from the name)

English

Let $g$ be a continuous map of $x$ and $x_{1}$. Then the composition monoid homomorphism of $g$ is a monoid homomorphism of the set of continuous maps of $x_{1}$ and $x_{4}$ and the set of continuous maps of $x$ and $x_{4}$.

ContinuousMap.compRightAlgHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the composition right algebra homomorphism of f (from the name)

English

Let $R$ and $A$ be sets. Let $f$ be a continuous map of $x_{4}$ and $x_{5}$. Then the composition right algebra homomorphism of $f$ is an algebra homomorphism of the set of continuous maps of $x_{5}$ and $A$ and the set of continuous maps of $x_{4}$ and $A$.

ContinuousMap.evalAlgHomdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the evaluation algebra homomorphism of x5 (from the name)

English

Let $S$ and $R$ be sets. Let $x_{5}$ be an element of $X$. Then the evaluation algebra homomorphism of $x_{5}$ is an algebra homomorphism of the set of continuous maps of $X$ and $R$ and $R$.

ContinuousMap.evalCLMdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the evaluation continuous linear map of R and x6 (from the name)

English

Let $R$ be a set. Let $x_{6}$ be an element of $x$. Then the evaluation continuous linear map of $R$ and $x_{6}$ is a continuous linear map of the set of continuous maps of $x$ and $M$ and $M$.

MonoidHom.compLeftContinuousdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

Let $x$ be a set. Let $g$ be a monoid homomorphism of $x_{1}$ and $x_{4}$ such that $\operatorname{coe}$ applied to $g$ is continuous. Then $\operatorname{compLeftContinuous}$ applied to $x$, $g$ and $\mathrm{hg}$ is a monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{4}$.

RingHom.compLeftContinuousdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

no wording

English

Let $x$ be a set. Let $g$ be a ring homomorphism of $x_{1}$ and $x_{2}$ such that $\operatorname{coe}$ applied to $g$ is continuous. Then $\operatorname{compLeftContinuous}$ applied to $x$, $g$ and $\mathrm{hg}$ is a ring homomorphism of the set of continuous maps of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{2}$.

Set.SeparatesPointsStronglydefMathlib.Topology.ContinuousMap.Algebra, predicate

Wording

no wording

English

Let $s$ be an element of the power set of the set of continuous maps of $x$ and $x_{2}$. Then $\operatorname{SeparatesPointsStrongly}$ holds for $s$, if for all functions $v$ from elements of $x$ to elements of $x_{2}$, for all elements $x_{4}$ and $y$ of $x$, there exists a continuous map $f$ of $x$ and $x_{2}$, such that $f$ is an element of $s$, $\EqtMACRoH {f (x_{4})}{v (x_{4})}$ and $\EqtMACRoH {f (y)}{v (y)}$.

Subalgebra.SeparatesPointsdefMathlib.Topology.ContinuousMap.Algebra, predicate

Wording

no wording

English

Let $s$ be a subalgebra of $R$ and the set of continuous maps of $x$ and $A$. Then $\operatorname{SeparatesPoints}$ holds for $s$, if $\operatorname{SeparatesPoints}$ holds for the image of the function that maps $f$ to $\operatorname{coe}$ applied to $f$ and $s$.

continuousAddSubgroupdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous additive subgroup of x and x1 (from the name)

English

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

continuousAddSubmonoiddefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

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

English

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

continuousSubalgebradefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous subalgebra (from the name)

English

The continuous subalgebra is a subalgebra of $R$ and the set of functions from elements of $x$ to elements of $A$.

continuousSubgroupdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous subgroup of x and x1 (from the name)

English

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

continuousSubmoduledefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous submodule of R and M (from the name)

English

Let $x$, $R$ and $M$ be sets. Then the continuous submodule of $R$ and $M$ is a submodule of $R$ and the set of functions from elements of $x$ to elements of $M$.

continuousSubmonoiddefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

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

English

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

continuousSubringdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous subring of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the continuous subring of $x$ and $R$ is a subring of the set of functions from elements of $x$ to elements of $R$.

continuousSubsemiringdefMathlib.Topology.ContinuousMap.Algebra, function or constant

Wording

the continuous subsemiring of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the continuous subsemiring of $x$ and $R$ is a subsemiring of the set of functions from elements of $x$ to elements of $R$.

Mathlib.Topology.ContinuousMap.Basic

ContinuousMap.compdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the composition of f and g (from the name)

English

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

ContinuousMap.constdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the constant map of x and b (from the docstring)

English

Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant map of $x$ and $b$ is a continuous map of $x$ and $x_{1}$.

ContinuousMap.constPidefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the constant product of x (from the name)

English

Let $x$ be a set. Then the constant product of $x$ is a continuous map of $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

ContinuousMap.equivFnOfDiscretedefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the equivalence function (from the name)

English

The equivalence function is an equivalence from the set of continuous maps of $x$ and $x_{1}$ to the set of functions from elements of $x$ to elements of $x_{1}$.

ContinuousMap.evaldefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the evaluation of i (from the name)

English

Let $i$ be an element of $I$. Then the evaluation of $i$ is a continuous map of the set of functions from elements $j$ of $I$ to elements of $X$ applied to $j$ and $X$ applied to $i$.

ContinuousMap.fstdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the first component (from the name)

English

The first component is a continuous map of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

ContinuousMap.iddefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the identity of x (from the docstring)

English

Let $x$ be a set. Then the identity of $x$ is a continuous map of $x$ and $x$.

ContinuousMap.inclusiondefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $s \leq t$. Then the inclusion of $h$ is a continuous map of the set of elements of $s$ and the set of elements of $t$ defined as $\operatorname{mk}$ applied to $\operatorname{inclusion}$ applied to $h$ and $\mathrm{continuous\_inclusion}$ applied to $h$.

ContinuousMap.liftCoverdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the lift cover of S and x5 (from the name)

English

Let $S$ be a function from elements of $x_{4}$ to elements of $\wp x$. Let $x_{5}$ be a function from elements $i_{2}$ of $x_{4}$ to continuous maps of the set of elements of $S$ applied to $i_{2}$ and $x_{1}$ such that for all elements $i_{1}$ and $j$ of $x_{4}$, for all elements $x_{7}$ of $x$, for all elements $\mathrm{hxi}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (i_{1})}{x_{7}}$, for all elements $\mathrm{hxj}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {S (j)}{x_{7}}$, $\EqtMACRoH {x_{5} (i_{1} , x_{7})}{x_{5} (j , x_{7})}$. Assume that for all elements $x_{6}$ of $x$, there exists an element $i$ of $x_{4}$, such that $S$ applied to $i$ is an element of the neighbourhood filter of $x_{6}$. Then the lift cover of $S$ and $i_{2}$ is a continuous map of $x$ and $x_{1}$.

ContinuousMap.liftCover'defMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the lift cover of A and F (from the name)

English

Let $A$ be an element of $\wp (\wp x)$. Let $F$ be a function from elements $s_{1}$ of $\wp x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {A}{s_{1}}$ to continuous maps of the set of elements of $s_{1}$ and $x_{1}$ such that for all elements $s$ of $\wp x$, for all elements $\mathrm{hs}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {A}{s}$, for all elements $t$ of $\wp x$, for all elements $\mathrm{ht}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {A}{t}$, for all elements $x_{5}$ of $x$, for all elements $\mathrm{hxi}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{x_{5}}$, for all elements $\mathrm{hxj}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {t}{x_{5}}$, $\EqtMACRoH {F (s , \mathrm{hs} , x_{5})}{F (t , \mathrm{ht} , x_{5})}$. Assume that for all elements $x_{4}$ of $x$, there exists an element $i$ of $\wp x$, such that $\MembershipmemMACRoT {A}{i}$ and $i$ is an element of the neighbourhood filter of $x_{4}$. Then the lift cover of $A$ and $s_{1}$ is a continuous map of $x$ and $x_{1}$.

ContinuousMap.mkDdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{default}$ be a continuous map of $x$ and $x_{1}$. Then $\operatorname{mkD}$ applied to $f$ and $\mathrm{default}$ is a continuous map of $x$ and $x_{1}$ defined as $\mathrm{dite}$ applied to the proposition that $f$ is continuous, the function that maps $h$ to $\operatorname{mk}$ applied to $f$ and $h$ and the function that maps $h_{1}$ to $\mathrm{default}$.

ContinuousMap.pidefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $I$ to continuous maps of $A$ and $X$ applied to $i_{1}$. Then the product of $i_{1}$ is a continuous map of $A$ and the set of functions from elements $i$ of $I$ to elements of $X$ applied to $i$.

ContinuousMap.piEquivdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the product equivalence of A and X (from the name)

English

Let $A$ be a set. Let $X$ be a function from elements of $I$ to sets. Then the product equivalence of $A$ and $X$ is an equivalence from the set of functions from elements $i$ of $I$ to continuous maps of $A$ and $X$ applied to $i$ to the set of continuous maps of $A$ and the set of functions from elements $i_{1}$ of $I$ to elements of $X$ applied to $i_{1}$.

ContinuousMap.piMapdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the product map of f (from the name)

English

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

ContinuousMap.precompdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the precomposition of x2 (from the name)

English

Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $I$. Then the precomposition of $x_{2}$ is a continuous map of the set of functions from elements $i$ of $I$ to elements of $X$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $X$ applied to $x_{2}$ applied to $i_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $f$ and $j$ to $f$ applied to $x_{2}$ applied to $j$ and $\mathrm{Pi\_\_continuous\_precomp'}$ applied to $x_{2}$.

ContinuousMap.prodMapdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

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

English

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

ContinuousMap.prodMkdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the product of f and g (from the name)

English

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

ContinuousMap.prodSwapdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the product swap (from the name)

English

The product swap is a continuous map of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$ defined as the product of the second component and the first component.

ContinuousMap.restrictdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the restriction of s and f (from the docstring)

English

Let $s$ be an element of $\wp x$. Let $f$ be a continuous map of $x$ and $x_{1}$. Then the restriction of $s$ and $f$ is a continuous map of the set of elements of $s$ and $x_{1}$.

ContinuousMap.restrictPreimagedefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the restriction of f and s (from the docstring)

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then the restriction of $f$ and $s$ is a continuous map of the set of elements of the preimage of $\operatorname{coe}$ applied to $f$ and $s$ and the set of elements of $s$.

ContinuousMap.sigmadefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the sigma of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $I$ to continuous maps of $X$ applied to $i_{1}$ and $A$. Then the sigma of $i_{1}$ is a continuous map of $\Sigma$ applied to the function that maps $i$ to $X$ applied to $i$ and $A$.

ContinuousMap.sigmaEquivdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the sigma equivalence of A and X (from the name)

English

Let $A$ be a set. Let $X$ be a function from elements of $I$ to sets. Then the sigma equivalence of $A$ and $X$ is an equivalence from the set of functions from elements $i$ of $I$ to continuous maps of $X$ applied to $i$ and $A$ to the set of continuous maps of $\Sigma$ applied to the function that maps $i_{1}$ to $X$ applied to $i_{1}$ and $A$.

ContinuousMap.sigmaMkdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the sigma of i (from the name)

English

Let $i$ be an element of $I$. Then the sigma of $i$ is a continuous map of $X$ applied to $i$ and $\Sigma$ applied to the function that maps $i_{1}$ to $X$ applied to $i_{1}$.

ContinuousMap.snddefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the second component (from the name)

English

The second component is a continuous map of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

ContinuousMap.subtypeValdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the subtype value of s (from the name)

English

Let $s$ be an element of $\wp x$. Then the subtype value of $s$ is a continuous map of the set of elements of $s$ and $x$.

Function.RightInverse.homeomorphdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the homeomorphism of hf (from the name)

English

Assume that $\operatorname{RightInverse}$ holds for $\operatorname{coe}$ applied to $\mathrm{f'}$ and $\operatorname{coe}$ applied to $f$. Then the homeomorphism of $\mathrm{hf}$ is a homeomorphism of $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $\operatorname{coe}$ applied to $f$ and $Y$.

Homeomorph.continuousMapCongrdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

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

English

Let $e$ be a homeomorphism of $x$ and $x_{1}$. Let $\mathrm{e'}$ be a homeomorphism of $x_{2}$ and $x_{3}$. Then the continuous map congruence of $e$ and $\mathrm{e'}$ is an equivalence from the set of continuous maps of $x$ and $x_{2}$ to the set of continuous maps of $x_{1}$ and $x_{3}$.

Topology.IsQuotientMap.homeomorphdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the homeomorphism from the quotient of hf (from the docstring)

English

Assume that $\operatorname{coe}$ applied to $f$ is a quotient map. Then the homeomorphism from the quotient of $\mathrm{hf}$ is a homeomorphism of $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $\operatorname{coe}$ applied to $f$ and $Y$.

Topology.IsQuotientMap.liftdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the lift of g (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is a quotient map. Let $g$ be a continuous map of $X$ and $Z$ such that $\operatorname{FactorsThrough}$ holds for $\operatorname{coe}$ applied to $g$ and $\operatorname{coe}$ applied to $f$. Then the lift of $g$ is a continuous map of $Y$ and $Z$.

Topology.IsQuotientMap.liftEquivdefMathlib.Topology.ContinuousMap.Basic, function or constant

Wording

the lift equivalence of hf (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is a quotient map. Then the lift equivalence of $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\operatorname{FactorsThrough} (\operatorname{coe} (g), \operatorname{coe} (f))})}{\mathrm{ContinuousMap} (Y , Z)}$.

Mathlib.Topology.ContinuousMap.Bounded.Basic

AddMonoidHom.compLeftContinuousBoundeddefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a set. Let $g$ be an additive monoid homomorphism of $x$ and $x_{1}$ such that $\mathrm{LipschitzWith}$ holds for $C$ and $\operatorname{coe}$ applied to $g$. Then $\operatorname{compLeftContinuousBounded}$ applied to $x_{2}$, $g$ and $\mathrm{hg}$ is an additive monoid homomorphism of the set of bounded continuous functions of $x_{2}$ and $x$ and the set of bounded continuous functions of $x_{2}$ and $x_{1}$.

BoundedContinuousFunctionstructureMathlib.Topology.ContinuousMap.Bounded.Basic, type

Wording

bounded continuous function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the bounded continuous functions of $x$ and $x_{1}$ are a basic type.

BoundedContinuousFunction.codRestrictdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp x_{1}$. Let $f$ be a bounded continuous function of $x$ and $x_{1}$ such that for all elements $x_{4}$ of $x$, $\MembershipmemMACRoT {s}{f (x_{4})}$. Then $\operatorname{codRestrict}$ applied to $s$, $f$ and $H$ is a bounded continuous function of $x$ and the set of elements of $s$.

BoundedContinuousFunction.coeFnAddMonoidHomdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of bounded continuous functions of $x$ and $R$ and the set of functions from elements of $x$ to elements of $R$.

BoundedContinuousFunction.coeFnMonoidHomdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the coercion function monoid homomorphism (from the name)

English

The coercion function monoid homomorphism is a monoid homomorphism of the set of bounded continuous functions of $x$ and $R$ and the set of functions from elements of $x$ to elements of $R$.

BoundedContinuousFunction.compdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the composition of G and f (from the name)

English

Let $G$ be a function from elements of $x_{1}$ to elements of $x_{2}$ such that $\mathrm{LipschitzWith}$ holds for $C$ and $G$. Let $f$ be a bounded continuous function of $x$ and $x_{1}$. Then the composition of $G$ and $f$ is a bounded continuous function of $x$ and $x_{2}$.

BoundedContinuousFunction.compContinuousdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be a bounded continuous function of $x$ and $x_{1}$. Let $g$ be a continuous map of $x_{4}$ and $x$. Then $\operatorname{compContinuous}$ applied to $f$ and $g$ is a bounded continuous function of $x_{4}$ and $x_{1}$.

BoundedContinuousFunction.constdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the constant of x and b (from the name)

English

Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant of $x$ and $b$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.domRestrictdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be a bounded continuous function of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{domRestrict}$ applied to $f$ and $s$ is a bounded continuous function of the set of elements of $s$ and $x_{1}$ defined as $\operatorname{compContinuous}$ applied to $f$ and the restriction of $s$ and the identity of $x$.

BoundedContinuousFunction.evalCLMdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the evaluation continuous linear map of x2 and x9 (from the name)

English

Let $x_{2}$ be a set. Let $x_{9}$ be an element of $x$. Then the evaluation continuous linear map of $x_{2}$ and $x_{9}$ is a continuous linear map of the set of bounded continuous functions of $x$ and $x_{1}$ and $x_{1}$.

BoundedContinuousFunction.extenddefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be an embedding of $x$ and $x_{4}$. Let $g$ be a bounded continuous function of $x$ and $x_{1}$. Let $h_{1}$ be a bounded continuous function of $x_{4}$ and $x_{1}$. Then $\operatorname{extend}$ applied to $f$, $g$ and $h_{1}$ is a bounded continuous function of $x_{4}$ and $x_{1}$.

BoundedContinuousFunction.indicatordefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the indicator function of s and hs (from the docstring)

English

Let $s$ be an element of $\wp x$ such that $s$ is a clopen. Then the indicator function of $s$ and $\mathrm{hs}$ is a bounded continuous function of $x$ and $\Real$.

BoundedContinuousFunction.mkOfBounddefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Let $C$ be a real number such that for all elements $x_{4}$ and $y$ of $x$, the distance of $f$ applied to $x_{4}$ and $f$ applied to $y$ is less than or equal to $C$. Then $\operatorname{mkOfBound}$ applied to $f$, $C$ and $h$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.mkOfCompactdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Then $\operatorname{mkOfCompact}$ applied to $f$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.mkOfDiscretedefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $C$ be a real number such that for all elements $x_{4}$ and $y$ of $x$, the distance of $f$ applied to $x_{4}$ and $f$ applied to $y$ is less than or equal to $C$. Then $\operatorname{mkOfDiscrete}$ applied to $f$, $C$ and $h_{1}$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.toContinuousMapAddMonoidHomdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the continuous map additive monoid homomorphism of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the continuous map additive monoid homomorphism of $x$ and $R$ is an additive monoid homomorphism of the set of bounded continuous functions of $x$ and $R$ and the set of continuous maps of $x$ and $R$.

BoundedContinuousFunction.toContinuousMapLinearMapdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

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

English

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the continuous map linear map of $x_{1}$ and $x_{2}$ is a linear map of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{1}$.

BoundedContinuousFunction.toContinuousMapMonoidHomdefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

the continuous map monoid homomorphism of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the continuous map monoid homomorphism of $x$ and $R$ is a monoid homomorphism of the set of bounded continuous functions of $x$ and $R$ and the set of continuous maps of $x$ and $R$.

BoundedContinuousMapClassclassMathlib.Topology.ContinuousMap.Bounded.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{BoundedContinuousMapClass}$ holds for $F$, $x$ and $x_{1}$.

MonoidHom.compLeftContinuousBoundeddefMathlib.Topology.ContinuousMap.Bounded.Basic, function or constant

Wording

no wording

English

Let $x_{2}$ be a set. Let $g$ be a monoid homomorphism of $x$ and $x_{1}$ such that $\mathrm{LipschitzWith}$ holds for $C$ and $\operatorname{coe}$ applied to $g$. Then $\operatorname{compLeftContinuousBounded}$ applied to $x_{2}$, $g$ and $\mathrm{hg}$ is a monoid homomorphism of the set of bounded continuous functions of $x_{2}$ and $x$ and the set of bounded continuous functions of $x_{2}$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.Bounded.Normed

BoundedContinuousFunction.AlgHom.compLeftContinuousBoundeddefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

no wording

English

Let $x_{3}$ be a set. Let $g$ be an algebra homomorphism of $x_{1}$ and $x_{2}$ such that $\mathrm{LipschitzWith}$ holds for $C$ and $\operatorname{coe}$ applied to $g$. Then $\operatorname{compLeftContinuousBounded}$ applied to $x_{3}$, $g$ and $\mathrm{hg}$ is an algebra homomorphism of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of bounded continuous functions of $x$ and $x_{2}$.

BoundedContinuousFunction.CdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

no wording

English

$\operatorname{C}$ is a ring homomorphism of $x_{2}$ and the set of bounded continuous functions of $x$ and $x_{1}$.

BoundedContinuousFunction.compContinuousCLMdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

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

English

Let $x_{1}$ and $x_{5}$ be sets. Let $g$ be a continuous map of $x_{2}$ and $x$. Then the composition continuous continuous linear map of $g$ is a continuous linear map of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of bounded continuous functions of $x_{2}$ and $x_{1}$.

BoundedContinuousFunction.nnnormdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the norm of f (from the name)

English

Let $f$ be a bounded continuous function of $x$ and $\Real$. Then the norm of $f$ is a bounded continuous function of $x$ and $\mathrm{NNReal}$.

BoundedContinuousFunction.nnrealPartdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the nonnegative part of f (from the docstring)

English

Let $f$ be a bounded continuous function of $x$ and $\Real$. Then the nonnegative part of $f$ is a bounded continuous function of $x$ and $\mathrm{NNReal}$.

BoundedContinuousFunction.normCompdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the norm composition of f (from the name)

English

Let $f$ be a bounded continuous function of $x$ and $x_{1}$. Then the norm composition of $f$ is a bounded continuous function of $x$ and $\Real$.

BoundedContinuousFunction.ofNormedAddCommGroupdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the bounded continuous function of f and C (from the name)

English

Let $f$ be a continuous function from elements of $x$ to elements of $x_{1}$. Let $C$ be a real number such that for all elements $x_{4}$ of $x$, the norm of $f$ applied to $x_{4}$ is less than or equal to $C$. Then the bounded continuous function of $f$ and $C$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.ofNormedAddCommGroupDiscretedefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the bounded continuous function of f and C (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $C$ be a real number such that for all elements $x_{4}$ of $x$, the norm of $f$ applied to $x_{4}$ is less than or equal to $C$. Then the bounded continuous function of $f$ and $C$ is a bounded continuous function of $x$ and $x_{1}$.

BoundedContinuousFunction.toContinuousMapₐdefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

the continuous map of x2 (from the name)

English

Let $x_{2}$ be a set. Then the continuous map of $x_{2}$ is an algebra homomorphism of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{1}$.

ContinuousLinearMap.compLeftContinuousBoundeddefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

no wording

English

Let $x$ be a set. Let $g$ be a continuous linear map of $x_{1}$ and $x_{2}$. Then $\operatorname{compLeftContinuousBounded}$ applied to $x$ and $g$ is a continuous linear map of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of bounded continuous functions of $x$ and $x_{2}$.

RingHom.compLeftContinuousBoundeddefMathlib.Topology.ContinuousMap.Bounded.Normed, function or constant

Wording

no wording

English

Let $x_{2}$ be a set. Let $g$ be a ring homomorphism of $x$ and $x_{1}$ such that $\mathrm{LipschitzWith}$ holds for $C$ and $\operatorname{coe}$ applied to $g$. Then $\operatorname{compLeftContinuousBounded}$ applied to $x_{2}$, $g$ and $\mathrm{hg}$ is a ring homomorphism of the set of bounded continuous functions of $x_{2}$ and $x$ and the set of bounded continuous functions of $x_{2}$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.Bounded.Star

BoundedContinuousFunction.toContinuousMapStarₐdefMathlib.Topology.ContinuousMap.Bounded.Star, function or constant

Wording

the continuous map star of x2 (from the name)

English

Let $x_{2}$ be a set. Then the continuous map star of $x_{2}$ is a star algebra homomorphism of the set of bounded continuous functions of $x$ and $x_{1}$ and the set of continuous maps of $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

compactlySupporteddefMathlib.Topology.ContinuousMap.BoundedCompactlySupported, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\mathrm{compactlySupported}$ applied to $x$ and $x_{1}$ is an element of $\mathrm{TwoSidedIdeal}$ applied to the set of bounded continuous functions of $x$ and $x_{1}$.

ofCompactSupportdefMathlib.Topology.ContinuousMap.BoundedCompactlySupported, function or constant

Wording

the compact support of g (from the name)

English

Let $g$ be a function from elements of $x$ to elements of $x_{1}$ such that $g$ is continuous and $g$ has compact supports. Then the compact support of $g$ is a bounded continuous function of $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.CocompactMap

CocompactMapstructureMathlib.Topology.ContinuousMap.CocompactMap, type

Wording

cocompact map of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the cocompact maps of $x$ and $x_{1}$ are a basic type.

CocompactMap.compdefMathlib.Topology.ContinuousMap.CocompactMap, function or constant

Wording

the composition of f and g (from the name)

English

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

CocompactMap.copydefMathlib.Topology.ContinuousMap.CocompactMap, function or constant

Wording

the copy of f and h (from the name)

English

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

CocompactMap.iddefMathlib.Topology.ContinuousMap.CocompactMap, function or constant

Wording

the identity of x (from the docstring)

English

Let $x$ be a set. Then the identity of $x$ is a cocompact map of $x$ and $x$.

CocompactMapClassclassMathlib.Topology.ContinuousMap.CocompactMap, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{CocompactMapClass}$ holds for $F$, $x$ and $x_{1}$.

CocompactMapClass.toCocompactMapdefMathlib.Topology.ContinuousMap.CocompactMap, function or constant

Wording

the cocompact map of f (from the name)

English

Let $f$ be an element of $F$. Then the cocompact map of $f$ is a cocompact map of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the continuous map of $f$ and $\mathrm{CocompactMapClass\_\_cocompact\_tendsto}$ applied to $f$.

Homeomorph.toCocompactMapdefMathlib.Topology.ContinuousMap.CocompactMap, function or constant

Wording

the cocompact map of f (from the name)

English

Let $f$ be a homeomorphism of $x$ and $x_{1}$. Then the cocompact map of $f$ is a cocompact map of $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.Compact

ContinuousMap.addEquivBoundedOfCompactdefMathlib.Topology.ContinuousMap.Compact, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{addEquivBoundedOfCompact}$ applied to $x$ and $x_{1}$ is an additive equivalence of the set of continuous maps of $x$ and $x_{1}$ and the set of bounded continuous functions of $x$ and $x_{1}$.

ContinuousMap.equivBoundedOfCompactdefMathlib.Topology.ContinuousMap.Compact, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{equivBoundedOfCompact}$ applied to $x$ and $x_{1}$ is an equivalence from the set of continuous maps of $x$ and $x_{1}$ to the set of bounded continuous functions of $x$ and $x_{1}$.

ContinuousMap.isometryEquivBoundedOfCompactdefMathlib.Topology.ContinuousMap.Compact, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{isometryEquivBoundedOfCompact}$ applied to $x$ and $x_{1}$ is an isometry equivalence of the set of continuous maps of $x$ and $x_{1}$ and the set of bounded continuous functions of $x$ and $x_{1}$.

ContinuousMap.linearIsometryBoundedOfCompactdefMathlib.Topology.ContinuousMap.Compact, function or constant

Wording

no wording

English

Let $x$, $E$ and $x_{3}$ be sets. Then $\operatorname{linearIsometryBoundedOfCompact}$ applied to $x$, $E$ and $x_{3}$ is a linear isometry equivalence of the set of continuous maps of $x$ and $E$ and the set of bounded continuous functions of $x$ and $E$.

ContinuousMap.modulusdefMathlib.Topology.ContinuousMap.Compact, function or constant

Wording

the modulus of f and x4 (from the name)

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Let $x_{4}$ be a real number such that $0 < x_{4}$. Then the modulus of $f$ and $x_{4}$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{ContinuousMap\_\_uniform\_continuity}$ applied to $f$, $x_{4}$ and $h_{1}$.

Mathlib.Topology.ContinuousMap.CompactlySupported

CompactlySupportedContinuousMapstructureMathlib.Topology.ContinuousMap.CompactlySupported, type

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$ are a basic type.

CompactlySupportedContinuousMap.coeFnMonoidHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the coercion function monoid homomorphism (from the name)

English

The coercion function monoid homomorphism is an additive monoid homomorphism of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$.

CompactlySupportedContinuousMap.compdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$. Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.compAddMonoidHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the composition additive monoid homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition additive monoid homomorphism of $g$ is an additive monoid homomorphism of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.compLeftdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

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

English

Let $g$ be a continuous map of $x_{1}$ and $x_{5}$. Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$. Then the left composition of $g$ and $f$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{5}$.

CompactlySupportedContinuousMap.compLinearMapdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the composition linear map of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition linear map of $g$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.compMulHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the composition multiplicative homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition multiplicative homomorphism of $g$ is a multiplicative homomorphism of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.compNonUnitalAlgHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the composition non unital algebra homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition non unital algebra homomorphism of $g$ is a non unital algebra homomorphism of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.continuousMapEquivdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the continuous map equivalence (from the name)

English

The continuous map equivalence is an equivalence from the set of continuous maps of $x$ and $x_{1}$ to $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$.

CompactlySupportedContinuousMap.copydefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{1}$.

CompactlySupportedContinuousMap.nnrealPartdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the nonnegative part of f (from the docstring)

English

Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\Real$. Then the nonnegative part of $f$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\mathrm{NNReal}$.

CompactlySupportedContinuousMap.pullback_addMonoidHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the pullback additive monoid homomorphism of f and b (from the name)

English

Assume that $\operatorname{coe}$ applied to $x_{8}$ is a closed embedding. Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$. Let $b$ be an element of $x_{1}$. Then the pullback additive monoid homomorphism of $f$ and $b$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.pullback_monoidHomdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the pullback monoid homomorphism of f and b (from the name)

English

Assume that $\operatorname{coe}$ applied to $x_{8}$ is a closed embedding. Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x_{1}$ and $x_{2}$. Let $b$ be an element of $x_{1}$. Then the pullback monoid homomorphism of $f$ and $b$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$.

CompactlySupportedContinuousMap.toBoundedContinuousFunctiondefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the bounded continuous function of f (from the name)

English

Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $x_{2}$. Then the bounded continuous function of $f$ is a bounded continuous function of $x$ and $x_{2}$.

CompactlySupportedContinuousMap.toNNRealLineardefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

no wording

English

Let $x_{2}$ be a positive linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\Real$ and $\Real$. Then $\operatorname{toNNRealLinear}$ applied to $x_{2}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\mathrm{NNReal}$ and $\mathrm{NNReal}$.

CompactlySupportedContinuousMap.toRealdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\mathrm{NNReal}$. Then $\operatorname{toReal}$ applied to $f$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\Real$ defined as the left composition of $\operatorname{coeNNRealReal}$ and $f$.

CompactlySupportedContinuousMap.toRealLinearMapdefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

the map (from the docstring)

English

The map is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\mathrm{NNReal}$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\Real$.

CompactlySupportedContinuousMap.toRealPositiveLineardefMathlib.Topology.ContinuousMap.CompactlySupported, function or constant

Wording

no wording

English

Let $x_{2}$ be a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\mathrm{NNReal}$ and $\mathrm{NNReal}$. Then $\operatorname{toRealPositiveLinear}$ applied to $x_{2}$ is a positive linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $x$ and $\Real$ and $\Real$.

CompactlySupportedContinuousMapClassclassMathlib.Topology.ContinuousMap.CompactlySupported, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{CompactlySupportedContinuousMapClass}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.ContinuousMapZero

ContinuousMapZerostructureMathlib.Topology.ContinuousMap.ContinuousMapZero, type

Wording

continuous map zero of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the continuous map zeros of $X$ and $R$ are a basic type.

ContinuousMapZero.coeFnAddMonoidHomdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of continuous map zeros of $X$ and $R$ and the set of functions from elements of $X$ to elements of $R$.

ContinuousMapZero.compdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a continuous map zero of $Y$ and $R$. Let $f$ be a continuous map zero of $X$ and $Y$. Then the composition of $g$ and $f$ is a continuous map zero of $X$ and $R$.

ContinuousMapZero.evalCLMdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

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

English

Let $x_{4}$ be a set. Let $x_{7}$ be an element of $X$. Then the evaluation continuous linear map of $x_{4}$ and $x_{7}$ is a continuous linear map of the set of continuous map zeros of $X$ and $R$ and $R$ defined as the composition of the evaluation continuous linear map of $x_{4}$ and $x_{7}$ and the continuous map continuous linear map of $x_{4}$.

ContinuousMapZero.iddefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the identity function of s (from the docstring)

English

Let $s$ be an element of $\wp R$. Then the identity function of $s$ is a continuous map zero of the set of elements of $s$ and $R$.

ContinuousMapZero.mkDdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $R$. Let $\mathrm{default}$ be a continuous map zero of $X$ and $R$. Then $\operatorname{mkD}$ applied to $f$ and $\mathrm{default}$ is a continuous map zero of $X$ and $R$.

ContinuousMapZero.nonUnitalStarAlgHom_postcompdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the non unital star algebra homomorphism postcomposition of x11 (from the name)

English

Let $X$ be a set. Let $x_{11}$ be a non unital star algebra homomorphism of $R$ and $S$ such that $\operatorname{coe}$ applied to $x_{11}$ is continuous. Then the non unital star algebra homomorphism postcomposition of $x_{11}$ is a non unital star algebra homomorphism of the set of continuous map zeros of $X$ and $R$ and the set of continuous map zeros of $X$ and $S$.

ContinuousMapZero.nonUnitalStarAlgHom_precompdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the non unital star algebra homomorphism precomposition of R and f (from the name)

English

Let $R$ be a set. Let $f$ be a continuous map zero of $X$ and $Y$. Then the non unital star algebra homomorphism precomposition of $R$ and $f$ is a non unital star algebra homomorphism of the set of continuous map zeros of $Y$ and $R$ and the set of continuous map zeros of $X$ and $R$.

ContinuousMapZero.starAlgEquivPrecompdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the star algebra isomorphism precomposition of f (from the name)

English

Let $R$ be a set. Let $f$ be a homeomorphism of $X$ and $Y$ such that $\EqtMACRoH {f (0)}{0}$. Then the star algebra isomorphism precomposition of $f$ is a star algebra isomorphism of the set of continuous map zeros of $Y$ and $R$ and the set of continuous map zeros of $X$ and $R$.

ContinuousMapZero.toContinuousMapCLMdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

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

English

Let $M$ be a set. Then the continuous map continuous linear map of $M$ is a continuous linear map of the set of continuous map zeros of $X$ and $R$ and the set of continuous maps of $X$ and $R$.

ContinuousMapZero.toContinuousMapHomdefMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the continuous map homomorphism (from the name)

English

The continuous map homomorphism is a non unital star algebra homomorphism of the set of continuous map zeros of $X$ and $R$ and the set of continuous maps of $X$ and $R$.

UniformEquiv.arrowCongrLeft₀defMathlib.Topology.ContinuousMap.ContinuousMapZero, function or constant

Wording

the left arrow congruence of f and hf (from the name)

English

Let $f$ be a homeomorphism of $X$ and $Y$ such that $\EqtMACRoH {f (0)}{0}$. Then the left arrow congruence of $f$ and $\mathrm{hf}$ is a uniform equivalence of the set of continuous map zeros of $X$ and $R$ and the set of continuous map zeros of $Y$ and $R$.

Mathlib.Topology.ContinuousMap.Defs

ContinuousMapstructureMathlib.Topology.ContinuousMap.Defs, type

Wording

continuous map of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the continuous maps of $X$ and $Y$ are a basic type.

ContinuousMap.copydefMathlib.Topology.ContinuousMap.Defs, function or constant

Wording

the copy of f and h (from the name)

English

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

ContinuousMap.ofClassdefMathlib.Topology.ContinuousMap.Defs, function or constant

Wording

the continuous map of f (from the name)

English

Let $f$ be an element of $F$. Then the continuous map of $f$ is a continuous map of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{ContinuousMapClass\_\_map\_continuous}$ applied to $f$.

ContinuousMap.toFundefMathlib.Topology.ContinuousMap.Defs, function or constant

Wording

the continuous map of self and x2 (from the name)

English

Let $\mathrm{self}$ be a continuous map of $X$ and $Y$. Let $x_{2}$ be an element of $X$. Then the continuous map of $\mathrm{self}$ and $x_{2}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

ContinuousMapClassclassMathlib.Topology.ContinuousMap.Defs, predicate

Wording

no wording

English

Let $F$ be a set. Let $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ContinuousMapClass}$ holds for $F$, $X$ and $Y$.

Mathlib.Topology.ContinuousMap.Ideals

ContinuousMap.idealOfSetdefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

the ideal of R and s (from the name)

English

Let $R$ be a set. Let $s$ be an element of $\wp X$. Then the ideal of $R$ and $s$ is an ideal of the set of continuous maps of $X$ and $R$.

ContinuousMap.idealOpensGIdefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

no wording

English

Let $X$ and $x$ be sets. Then $\operatorname{idealOpensGI}$ applied to $X$ and $x$ is a Galois insertion of $\operatorname{opensOfIdeal}$ and the function that maps $s$ to the ideal of $x$ and $s$.

ContinuousMap.opensOfIdealdefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

the open set of I (from the docstring)

English

Let $I$ be an ideal of the set of continuous maps of $X$ and $R$. Then the open set of $I$ is an open of $X$ defined as $\operatorname{mk}$ applied to the set of $I$ and $\mathrm{ContinuousMap\_\_setOfIdeal\_open}$ applied to $I$.

ContinuousMap.setOfIdealdefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

the set of I (from the name)

English

Let $I$ be an ideal of the set of continuous maps of $X$ and $R$. Then the set of $I$ is an element of $\wp X$ defined as the complement of $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that for all continuous maps $f$ of $X$ and $R$, if $f$ is an element of $I$, then $\EqtMACRoH {f (x_{3})}{0}$.

WeakDual.CharacterSpace.continuousMapEvaldefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

the continuous map evaluation of X and x (from the name)

English

Let $X$ and $x$ be sets. Then the continuous map evaluation of $X$ and $x$ is a continuous map of $X$ and the set of elements of the character space of $x$ and the set of continuous maps of $X$ and $x$.

WeakDual.CharacterSpace.homeoEvaldefMathlib.Topology.ContinuousMap.Ideals, function or constant

Wording

the homeomorphism evaluation of X and x (from the name)

English

Let $X$ and $x$ be sets. Then the homeomorphism evaluation of $X$ and $x$ is a homeomorphism of $X$ and the set of elements of the character space of $x$ and the set of continuous maps of $X$ and $x$.

Mathlib.Topology.ContinuousMap.Interval

ContinuousMap.IccExtendCMdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

no wording

English

$\operatorname{IccExtendCM}$ is a continuous map of the set of continuous maps of the set of elements of $\SetIccMACRoP {a}{b}$ and $E$ and the set of continuous maps of $x$ and $E$.

ContinuousMap.IccInclusionLeftdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

the left closed interval inclusion (from the name)

English

The left closed interval inclusion is a continuous map of the set of elements of $\SetIccMACRoP {a}{b}$ and the set of elements of $\SetIccMACRoP {a}{c}$.

ContinuousMap.IccInclusionRightdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

the right closed interval inclusion (from the name)

English

The right closed interval inclusion is a continuous map of the set of elements of $\SetIccMACRoP {b}{c}$ and the set of elements of $\SetIccMACRoP {a}{c}$.

ContinuousMap.concatdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

no wording

English

Let $f$ be a continuous map of the set of elements of $\SetIccMACRoP {a}{b}$ and $E$. Let $g$ be a continuous map of the set of elements of $\SetIccMACRoP {b}{c}$ and $E$. Then $\operatorname{concat}$ applied to $f$ and $g$ is a continuous map of the set of elements of $\SetIccMACRoP {a}{c}$ and $E$.

ContinuousMap.concatCMdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

no wording

English

$\operatorname{concatCM}$ is a continuous map of $\SubtypeSet {\mathrm{fg}}{(\EqtMACRoH {\operatorname{fst} (\mathrm{fg} , \operatorname{top})}{\operatorname{snd} (\mathrm{fg} , \operatorname{bot})})}$ and the set of continuous maps of the set of elements of $\SetIccMACRoP {a}{c}$ and $E$.

ContinuousMap.projIccCMdefMathlib.Topology.ContinuousMap.Interval, function or constant

Wording

no wording

English

$\operatorname{projIccCM}$ is a continuous map of $x$ and the set of elements of $\SetIccMACRoP {a}{b}$.

Mathlib.Topology.ContinuousMap.LocallyConstant

LocallyConstant.toContinuousMapAddMonoidHomdefMathlib.Topology.ContinuousMap.LocallyConstant, function or constant

Wording

the continuous map additive monoid homomorphism (from the name)

English

The continuous map additive monoid homomorphism is an additive monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of continuous maps of $X$ and $Y$.

LocallyConstant.toContinuousMapAlgHomdefMathlib.Topology.ContinuousMap.LocallyConstant, function or constant

Wording

the continuous map algebra homomorphism of R (from the name)

English

Let $R$ be a set. Then the continuous map algebra homomorphism of $R$ is an algebra homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of continuous maps of $X$ and $Y$.

LocallyConstant.toContinuousMapLinearMapdefMathlib.Topology.ContinuousMap.LocallyConstant, function or constant

Wording

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

English

Let $R$ be a set. Then the continuous map linear map of $R$ is a linear map of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of continuous maps of $X$ and $Y$.

LocallyConstant.toContinuousMapMonoidHomdefMathlib.Topology.ContinuousMap.LocallyConstant, function or constant

Wording

the continuous map monoid homomorphism (from the name)

English

The continuous map monoid homomorphism is a monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of continuous maps of $X$ and $Y$.

Mathlib.Topology.ContinuousMap.Ordered

ContinuousMap.IccExtenddefMathlib.Topology.ContinuousMap.Ordered, function or constant

Wording

no wording

English

Assume that $a \leq b$. Let $f$ be a continuous map of the set of elements of $\SetIccMACRoP {a}{b}$ and $x_{1}$. Then $\operatorname{IccExtend}$ applied to $h_{1}$ and $f$ is a continuous map of $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.Polynomial

Polynomial.toContinuousMapdefMathlib.Topology.ContinuousMap.Polynomial, function or constant

Wording

the continuous map of p (from the name)

English

Let $p$ be a polynomial of $R$. Then the continuous map of $p$ is a continuous map of $R$ and $R$.

Polynomial.toContinuousMapAlgHomdefMathlib.Topology.ContinuousMap.Polynomial, function or constant

Wording

the continuous map algebra homomorphism (from the name)

English

The continuous map algebra homomorphism is an algebra homomorphism of the set of polynomials of $R$ and the set of continuous maps of $R$ and $R$.

Polynomial.toContinuousMapOndefMathlib.Topology.ContinuousMap.Polynomial, function or constant

Wording

no wording

English

Let $p$ be a polynomial of $R$. Let $X$ be an element of $\wp R$. Then $\operatorname{toContinuousMapOn}$ applied to $p$ and $X$ is a continuous map of the set of elements of $X$ and $R$.

Polynomial.toContinuousMapOnAlgHomdefMathlib.Topology.ContinuousMap.Polynomial, function or constant

Wording

the continuous map on algebra homomorphism of X (from the name)

English

Let $X$ be an element of $\wp R$. Then the continuous map on algebra homomorphism of $X$ is an algebra homomorphism of the set of polynomials of $R$ and the set of continuous maps of the set of elements of $X$ and $R$.

polynomialFunctionsdefMathlib.Topology.ContinuousMap.Polynomial, function or constant

Wording

the polynomial function of X (from the name)

English

Let $X$ be an element of $\wp R$. Then the polynomial function of $X$ is a subalgebra of $R$ and the set of continuous maps of the set of elements of $X$ and $R$ defined as the map of the continuous map on algebra homomorphism of $X$ and the top.

Mathlib.Topology.ContinuousMap.Sigma

ContinuousMap.sigmaCodHomeomorphdefMathlib.Topology.ContinuousMap.Sigma, function or constant

Wording

the sigma codomain homeomorphism of X and Y (from the name)

English

Let $X$ be a set. Let $Y$ be a function from elements of $x$ to sets. Then the sigma codomain homeomorphism of $X$ and $Y$ is a homeomorphism of the set of continuous maps of $X$ and $\Sigma$ applied to the function that maps $i$ to $Y$ applied to $i$ and $\Sigma$ applied to the function that maps $i_{1}$ to the set of continuous maps of $X$ and $Y$ applied to $i_{1}$.

Mathlib.Topology.ContinuousMap.Star

ContinuousMap.compStarAlgHomdefMathlib.Topology.ContinuousMap.Star, function or constant

Wording

the composition star algebra homomorphism of x11 (from the name)

English

Let $X$ be a set. Let $x_{11}$ be a star algebra homomorphism of $A$ and $B$ such that $\operatorname{coe}$ applied to $x_{11}$ is continuous. Then the composition star algebra homomorphism of $x_{11}$ is a star algebra homomorphism of the set of continuous maps of $X$ and $A$ and the set of continuous maps of $X$ and $B$.

ContinuousMap.compStarAlgHom'defMathlib.Topology.ContinuousMap.Star, function or constant

Wording

the composition star algebra homomorphism of f (from the name)

English

Let $x_{2}$ and $A$ be sets. Let $f$ be a continuous map of $X$ and $Y$. Then the composition star algebra homomorphism of $f$ is a star algebra homomorphism of the set of continuous maps of $Y$ and $A$ and the set of continuous maps of $X$ and $A$.

ContinuousMap.evalStarAlgHomdefMathlib.Topology.ContinuousMap.Star, function or constant

Wording

the evaluation star algebra homomorphism of x6 (from the name)

English

Let $S$ and $R$ be sets. Let $x_{6}$ be an element of $X$. Then the evaluation star algebra homomorphism of $x_{6}$ is a star algebra homomorphism of the set of continuous maps of $X$ and $R$ and $R$.

Homeomorph.compStarAlgEquiv'defMathlib.Topology.ContinuousMap.Star, function or constant

Wording

the composition star algebra isomorphism of f (from the name)

English

Let $x_{2}$ and $A$ be sets. Let $f$ be a homeomorphism of $X$ and $Y$. Then the composition star algebra isomorphism of $f$ is a star algebra isomorphism of the set of continuous maps of $Y$ and $A$ and the set of continuous maps of $X$ and $A$.

Mathlib.Topology.ContinuousMap.StarOrdered

ContinuousSqrtclassMathlib.Topology.ContinuousMap.StarOrdered, predicate

Wording

R is a continuous square root (from the name)

English

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

ContinuousSqrt.sqrtdefMathlib.Topology.ContinuousMap.StarOrdered, function or constant

Wording

the square root of x3 (from the name)

English

Let $x_{3}$ be an element of $\mathrm{Prod}$ applied to $R$ and $R$. Then the square root of $x_{3}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.

Mathlib.Topology.ContinuousMap.StoneWeierstrass

ContinuousMap.attachBounddefMathlib.Topology.ContinuousMap.StoneWeierstrass, function or constant

Wording

no wording

English

Let $f$ be a continuous map of $X$ and $\Real$. Then $\operatorname{attachBound}$ applied to $f$ is a continuous map of $X$ and the set of elements of $\SetIccMACRoP {\operatorname{neg} (\operatorname{norm} (f))}{\operatorname{norm} (f)}$.

Mathlib.Topology.ContinuousMap.T0Sierpinski

TopologicalSpace.productOfMemOpensdefMathlib.Topology.ContinuousMap.T0Sierpinski, function or constant

Wording

the product of X (from the name)

English

Let $X$ be a set. Then the product of $X$ is a continuous map of $X$ and the set of functions from opens of $X$ to propositions.

Mathlib.Topology.ContinuousMap.Units

ContinuousMap.addUnitsLiftdefMathlib.Topology.ContinuousMap.Units, function or constant

Wording

the additive unit lift (from the name)

English

The additive unit lift is an equivalence from the set of continuous maps of $X$ and the set of additive units of $M$ to the set of additive units of the set of continuous maps of $X$ and $M$.

ContinuousMap.unitsLiftdefMathlib.Topology.ContinuousMap.Units, function or constant

Wording

the unit lift (from the name)

English

The unit lift is an equivalence from the set of continuous maps of $X$ and $\UnitsMACRoAO {M}$ to the set of units of the set of continuous maps of $X$ and $M$.

ContinuousMap.unitsOfForallIsUnitdefMathlib.Topology.ContinuousMap.Units, function or constant

Wording

the unit of h1 (from the name)

English

Assume that for all elements $x_{2}$ of $X$, $f$ applied to $x_{2}$ is a unit. Then the unit of $h_{1}$ is a continuous map of $X$ and $\UnitsMACRoAO {R}$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to the unit of $h_{1}$ applied to $x_{2}$ and $\mathrm{ContinuousMap\_\_continuous\_isUnit\_unit}$ applied to $h_{1}$.

Mathlib.Topology.ContinuousMap.ZeroAtInfty

ZeroAtInftyContinuousMapstructureMathlib.Topology.ContinuousMap.ZeroAtInfty, type

Wording

zero at infty continuous map of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the zero at infty continuous maps of $x$ and $x_{1}$ are a basic type.

ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInftydefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the lift zero at infty (from the name)

English

The lift zero at infty is an equivalence from the set of continuous maps of $x$ and $x_{1}$ to the set of zero at infty continuous maps of $x$ and $x_{1}$.

ZeroAtInftyContinuousMap.compdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a zero at infty continuous map of $x_{1}$ and $x_{2}$. Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a zero at infty continuous map of $x$ and $x_{2}$.

ZeroAtInftyContinuousMap.compAddMonoidHomdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the composition additive monoid homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition additive monoid homomorphism of $g$ is an additive monoid homomorphism of the set of zero at infty continuous maps of $x_{1}$ and $x_{2}$ and the set of zero at infty continuous maps of $x$ and $x_{2}$.

ZeroAtInftyContinuousMap.compLinearMapdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the composition linear map of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition linear map of $g$ is a linear map of the set of zero at infty continuous maps of $x_{1}$ and $x_{2}$ and the set of zero at infty continuous maps of $x$ and $x_{2}$.

ZeroAtInftyContinuousMap.compMulHomdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the composition multiplicative homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition multiplicative homomorphism of $g$ is a multiplicative homomorphism of the set of zero at infty continuous maps of $x_{1}$ and $x_{2}$ and the set of zero at infty continuous maps of $x$ and $x_{2}$.

ZeroAtInftyContinuousMap.compNonUnitalAlgHomdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the composition non unital algebra homomorphism of g (from the name)

English

Let $g$ be a cocompact map of $x$ and $x_{1}$. Then the composition non unital algebra homomorphism of $g$ is a non unital algebra homomorphism of the set of zero at infty continuous maps of $x_{1}$ and $x_{2}$ and the set of zero at infty continuous maps of $x$ and $x_{2}$.

ZeroAtInftyContinuousMap.copydefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a zero at infty continuous map of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a zero at infty continuous map of $x$ and $x_{1}$.

ZeroAtInftyContinuousMap.toBCFdefMathlib.Topology.ContinuousMap.ZeroAtInfty, function or constant

Wording

no wording

English

Let $f$ be a zero at infty continuous map of $x$ and $x_{1}$. Then $\operatorname{toBCF}$ applied to $f$ is a bounded continuous function of $x$ and $x_{1}$.

ZeroAtInftyContinuousMapClassclassMathlib.Topology.ContinuousMap.ZeroAtInfty, predicate

Wording

no wording

English

Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ZeroAtInftyContinuousMapClass}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization

ContinuousMap.toZeroAtInftydefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the zero at infty of g (from the name)

English

Let $g$ be a continuous map of the set of one points of $X$ and $R$. Then the zero at infty of $g$ is a zero at infty continuous map of $X$ and $R$.

ContinuousMap.toZeroAtInftyAddMonoidHomdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the zero at infty additive monoid homomorphism of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the zero at infty additive monoid homomorphism of $X$ and $R$ is an additive monoid homomorphism of the set of continuous maps of the set of one points of $X$ and $R$ and the set of zero at infty continuous maps of $X$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toZeroAtInfty}$ and $\mathrm{ContinuousMap\_\_toZeroAtInfty\_zero}$ and $\mathrm{ContinuousMap\_\_toZeroAtInfty\_add}$.

ContinuousMap.toZeroAtInftyLinearMapdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the zero at infty linear map of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the zero at infty linear map of $R$ and $S$ is a linear map of the set of continuous maps of the set of one points of $X$ and $R$ and the set of zero at infty continuous maps of $X$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toZeroAtInfty}$ and $\mathrm{ContinuousMap\_\_toZeroAtInfty\_add}$ and $\mathrm{ContinuousMap\_\_toZeroAtInfty\_smul}$.

ZeroAtInftyContinuousMap.toOnePointdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point of f (from the name)

English

Let $f$ be a zero at infty continuous map of $X$ and $R$. Then the one point of $f$ is a continuous map of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.toOnePointAddMonoidHomdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point additive monoid homomorphism of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the one point additive monoid homomorphism of $X$ and $R$ is an additive monoid homomorphism of the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.toOnePointLinearMapdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point linear map of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the one point linear map of $R$ and $S$ is a linear map of the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.toOnePointNonUnitalAlgHomdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point non unital algebra homomorphism of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the one point non unital algebra homomorphism of $R$ and $S$ is a non unital algebra homomorphism of the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.toOnePointNonUnitalRingHomdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point non unital ring homomorphism of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the one point non unital ring homomorphism of $X$ and $R$ is a non unital ring homomorphism of the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.toOnePointNonUnitalStarAlgHomdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the one point non unital star algebra homomorphism of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the one point non unital star algebra homomorphism of $R$ and $S$ is a non unital star algebra homomorphism of the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.unitizationAddEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the unitization additive equivalence of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the unitization additive equivalence of $X$ and $R$ is an additive equivalence of the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$ defined as $\operatorname{mk}$ applied to the canonical equivalence of $X$ and $R$ and $\mathrm{ZeroAtInftyContinuousMap\_\_unitizationEquiv\_add}$.

ZeroAtInftyContinuousMap.unitizationAlgEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the unitization algebra isomorphism of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the unitization algebra isomorphism of $R$ and $S$ is an algebra isomorphism of the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.unitizationEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the canonical equivalence of X and R (from the docstring)

English

Let $X$ and $R$ be sets. Then the canonical equivalence of $X$ and $R$ is an equivalence from the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ to the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.unitizationLinearEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the unitization linear equivalence of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the unitization linear equivalence of $R$ and $S$ is a linear equivalence of the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.unitizationRingEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the unitization ring isomorphism of X and R (from the name)

English

Let $X$ and $R$ be sets. Then the unitization ring isomorphism of $X$ and $R$ is a ring isomorphism of the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

ZeroAtInftyContinuousMap.unitizationStarAlgEquivdefMathlib.Topology.ContinuousMap.ZeroAtInftyUnitization, function or constant

Wording

the unitization star algebra isomorphism of R and S (from the name)

English

Let $X$, $R$ and $S$ be sets. Then the unitization star algebra isomorphism of $R$ and $S$ is a star algebra isomorphism of the set of unitizations of $R$ and the set of zero at infty continuous maps of $X$ and $R$ and the set of continuous maps of the set of one points of $X$ and $R$.

Mathlib.Topology.Convenient.Category

ContinuousGeneratedByCatstructureMathlib.Topology.Convenient.Category, type

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then the elements of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ are a basic type.

ContinuousGeneratedByCat.HomstructureMathlib.Topology.Convenient.Category, type

Wording

homomorphism of Y and Z (from the name)

English

Let $Y$ and $Z$ be elements of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$. Then the homomorphisms of $Y$ and $Z$ are a basic type.

ContinuousGeneratedByCat.Hom.homdefMathlib.Topology.Convenient.Category, function or constant

Wording

the homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a homomorphism of $Y$ and $Z$. Then the homomorphism of $\mathrm{self}$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, the set of carriers of $Y$ and the set of carriers of $Z$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ContinuousGeneratedByCat.adjdefMathlib.Topology.Convenient.Category, function or constant

Wording

the adjoint (from the name)

English

The adjoint is an adjunction of the topological category of $X$ and $\operatorname{toContinuousGeneratedByCat}$ applied to $X$.

ContinuousGeneratedByCat.adjCounitdefMathlib.Topology.Convenient.Category, function or constant

Wording

the counit of the adjunction (from the docstring)

English

The counit of the adjunction is a homomorphism of the composition of $\operatorname{toContinuousGeneratedByCat}$ applied to $X$ and the topological category of $X$ and the identity of the set of topological categories.

ContinuousGeneratedByCat.adjUnitIsodefMathlib.Topology.Convenient.Category, function or constant

Wording

the adjoint unit isomorphism (from the name)

English

The adjoint unit isomorphism is an isomorphism of the identity of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ and the composition of the topological category of $X$ and $\operatorname{toContinuousGeneratedByCat}$ applied to $X$.

ContinuousGeneratedByCat.carrierdefMathlib.Topology.Convenient.Category, type

Wording

carrier of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

ContinuousGeneratedByCat.equivalencedefMathlib.Topology.Convenient.Category, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence of $\mathrm{GeneratedByTopCat}$ applied to $X$ and $\mathrm{ContinuousGeneratedByCat}$ applied to $X$.

ContinuousGeneratedByCat.equivalenceCounitIsodefMathlib.Topology.Convenient.Category, function or constant

Wording

the counit isomorphism of the equivalence (from the docstring)

English

The counit isomorphism of the equivalence is an isomorphism of the composition of $\operatorname{toGeneratedByTopCat}$ and $\operatorname{fromGeneratedByTopCat}$ and the identity of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ defined as the inverse of the adjoint unit isomorphism.

ContinuousGeneratedByCat.equivalenceFunctorIsodefMathlib.Topology.Convenient.Category, function or constant

Wording

the equivalence functor isomorphism (from the name)

English

The equivalence functor isomorphism is an isomorphism of the composition of $\operatorname{fromGeneratedByTopCat}$ and the topological category of $X$ and the topological category.

ContinuousGeneratedByCat.equivalenceUnitIsodefMathlib.Topology.Convenient.Category, function or constant

Wording

the unit isomorphism of the equivalence (from the docstring)

English

The unit isomorphism of the equivalence is an isomorphism of the identity of $\mathrm{GeneratedByTopCat}$ applied to $X$ and the composition of $\operatorname{fromGeneratedByTopCat}$ and $\operatorname{toGeneratedByTopCat}$.

ContinuousGeneratedByCat.fromGeneratedByTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

$\operatorname{fromGeneratedByTopCat}$ is a functor of $\mathrm{GeneratedByTopCat}$ applied to $X$ and $\mathrm{ContinuousGeneratedByCat}$ applied to $X$.

ContinuousGeneratedByCat.fullyFaithfulToTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then $\operatorname{fullyFaithfulToTopCat}$ applied to $X$ is an element of $\operatorname{FullyFaithful}$ applied to the topological category of $X$.

ContinuousGeneratedByCat.homMkdefMathlib.Topology.Convenient.Category, function or constant

Wording

the homomorphism of f and hf (from the name)

English

Let $f$ be a function from carriers of $Y$ to carriers of $Z$ such that $\operatorname{ContinuousGeneratedBy}$ holds for $X$ and $f$. Then the homomorphism of $f$ and $\mathrm{hf}$ is a homomorphism of $Y$ and $Z$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$.

ContinuousGeneratedByCat.toGeneratedByTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

$\operatorname{toGeneratedByTopCat}$ is a functor of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ and $\mathrm{GeneratedByTopCat}$ applied to $X$.

ContinuousGeneratedByCat.toTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

the topological category of X (from the name)

English

Let $X$ be a function from elements of $x$ to sets. Then the topological category of $X$ is a functor of $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ and the set of topological categories.

GeneratedByTopCatdefMathlib.Topology.Convenient.Category, type

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then an element of $\mathrm{GeneratedByTopCat}$ applied to $X$ is an element of the function that maps $X$ to the set of full subcategories of $\operatorname{generatedBy}$ applied to $X$.

GeneratedByTopCat.adjdefMathlib.Topology.Convenient.Category, function or constant

Wording

the adjoint (from the name)

English

The adjoint is an adjunction of the topological category and $\operatorname{toGeneratedByTopCat}$.

GeneratedByTopCat.adjCounitdefMathlib.Topology.Convenient.Category, function or constant

Wording

the counit of the adjunction (from the docstring)

English

The counit of the adjunction is a homomorphism of the composition of $\operatorname{toGeneratedByTopCat}$ and the topological category and the identity of the set of topological categories defined as the counit of the adjunction.

GeneratedByTopCat.adjUnitIsodefMathlib.Topology.Convenient.Category, function or constant

Wording

the adjoint unit isomorphism (from the name)

English

The adjoint unit isomorphism is an isomorphism of the identity of $\mathrm{GeneratedByTopCat}$ applied to $X$ and the composition of the topological category and $\operatorname{toGeneratedByTopCat}$ defined as the unit isomorphism of the equivalence.

GeneratedByTopCat.fullyFaithfulToTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

GeneratedByTopCat.ofdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

Let $Y$ be a set. Then $\operatorname{of}$ applied to $Y$ is an element of $\mathrm{GeneratedByTopCat}$ applied to $X$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $Y$ and $h$.

GeneratedByTopCat.toTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

the topological category (from the name)

English

The topological category is a functor of $\mathrm{GeneratedByTopCat}$ applied to $X$ and the set of topological categories defined as the inclusion of $\operatorname{generatedBy}$ applied to $X$.

TopCat.generatedBydefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then there is an object property of the set of topological categories. Proof. Let $X$ be arbitrary. Let $Y$ be arbitrary. By X. By Y. By TopCat__carrier. By Topology__IsGeneratedBy.

TopCat.toContinuousGeneratedByCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then $\operatorname{toContinuousGeneratedByCat}$ applied to $X$ is a functor of the set of topological categories and $\mathrm{ContinuousGeneratedByCat}$ applied to $X$ defined as the forgetful functor of the set of topological categories and $\mathrm{ContinuousGeneratedByCat}$ applied to $X$.

TopCat.toGeneratedByTopCatdefMathlib.Topology.Convenient.Category, function or constant

Wording

no wording

English

$\operatorname{toGeneratedByTopCat}$ is a functor of the set of topological categories and $\mathrm{GeneratedByTopCat}$ applied to $X$ defined as the composition of $\operatorname{toContinuousGeneratedByCat}$ applied to $X$ and $\operatorname{toGeneratedByTopCat}$.