Definitions: Mathlib.Topology, part 8 of 8

TopCat.Presheaf.IsSheafPairwiseIntersectionsdefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, predicate

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Then $\operatorname{IsSheafPairwiseIntersections}$ holds for $F$, if for all sets $x_{1}$, for all functions $U$ from elements of $x_{1}$ to opens of the set of carriers of $X$, $\mathrm{Nonempty}$ holds for $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of $U$.

TopCat.Presheaf.IsSheafPreservesLimitPairwiseIntersectionsdefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, predicate

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Then $\operatorname{IsSheafPreservesLimitPairwiseIntersections}$ holds for $F$, if for all sets $x_{1}$, for all functions $U$ from elements of $x_{1}$ to opens of the set of carriers of $X$, $\operatorname{PreservesLimit}$ holds for the opposite of the diagram of $U$ and $F$.

TopCat.Presheaf.SheafCondition.pairwiseCoconeIsodefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

the cocone of U (from the docstring)

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then the cocone of $U$ is an isomorphism of the opposite of the cocone of $U$ and the action of the functor of the postcomposition equivalence of the opposite of the diagram in $U$ and the whisker of the opposite of $\operatorname{pairwiseToOpensLeCover}$ applied to $U$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$.

TopCat.Presheaf.SheafCondition.pairwiseDiagramIsodefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

the diagram in U (from the docstring)

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then the diagram in $U$ is an isomorphism of the diagram of $U$ and the composition of $\operatorname{pairwiseToOpensLeCover}$ applied to $U$ and the inclusion of the function that maps $V$ to the proposition that there exists an element $i$ of $x$, such that $V \leq U (i)$.

TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverdefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

no wording

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then $\operatorname{pairwiseToOpensLeCover}$ applied to $U$ is a functor of the set of pairwises of $x$ and $\operatorname{OpensLeCover}$ applied to $U$.

TopCat.Presheaf.isLimitOpensLeCoverEquivPairwisedefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then $\operatorname{isLimitOpensLeCoverEquivPairwise}$ applied to $F$ and $U$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$ to $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of $U$ defined as $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to $\operatorname{trans}$ applied to the inverse of $\operatorname{isLimitWhiskerEquiv}$ applied to the opposite of $\operatorname{pairwiseToOpensLeCover}$ applied to $U$ and the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$ and the equivalence isomorphism limit of the inverse of the map cone whisker of $F$ and the inverse of the postcomposition homomorphism equivalence of the right isomorphism whisker of the opposite of the diagram in $U$ and $F$ and the map cone of $F$ and the whisker of the opposite of $\operatorname{pairwiseToOpensLeCover}$ applied to $U$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$ and the equivalence isomorphism limit of the inverse of the map cone postcomposition equivalence functor of $F$ and the equivalence isomorphism limit of the map isomorphism of the functoriality of the opposite of the diagram of $U$ and $F$ and the inverse of the cocone of $U$.

TopCat.Sheaf.interUnionPullbackConedefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

the intersection union pullback cone of U and V (from the name)

English

Let $F$ be a sheaf of $C$ and $X$. Let $U$ and $V$ be opens of the set of carriers of $X$. Then the intersection union pullback cone of $U$ and $V$ is a pullback cone of the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{inf\_le\_left}$ and the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{inf\_le\_right}$.

TopCat.Sheaf.interUnionPullbackConeLiftdefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

the intersection union pullback cone lift of V and s (from the name)

English

Let $F$ be a sheaf of $C$ and $X$. Let $U$ and $V$ be opens of the set of carriers of $X$. Let $s$ be a pullback cone of the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{inf\_le\_left}$ and the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{inf\_le\_right}$. Then the intersection union pullback cone lift of $V$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and the action of the object of $F$ and $\operatorname{op}$ applied to $\MaxmaxMACRoAF {U}{V}$.

TopCat.Sheaf.isLimitPullbackConedefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

no wording

English

Let $F$ be a sheaf of $C$ and $X$. Let $U$ and $V$ be opens of the set of carriers of $X$. Then $\operatorname{isLimitPullbackCone}$ applied to $F$, $U$ and $V$ is an element of $\operatorname{IsLimit}$ applied to the intersection union pullback cone of $U$ and $V$ defined as $\operatorname{isLimitAux'}$ applied to the intersection union pullback cone of $U$ and $V$ and the function that maps $s$ to the intersection union pullback cone lift of $V$ and $s$.

TopCat.Sheaf.isProductOfDisjointdefMathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections, function or constant

Wording

no wording

English

Let $F$ be a sheaf of $C$ and $X$. Let $U$ and $V$ be opens of the set of carriers of $X$ such that $\MinminMACRoAG {U}{V}$ is equal to the bottom. Then $\operatorname{isProductOfDisjoint}$ applied to $F$, $U$, $V$ and $h$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{mk}$ applied to the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{le\_sup\_left}$ and the map of the object of $F$ and the opposite in the homomorphism of $\mathrm{le\_sup\_right}$.

Mathlib.Topology.Sheaves.SheafCondition.Sites

TopCat.Presheaf.coveringOfPresievedefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the covering of R and x (from the name)

English

Let $U$ be an open of the set of carriers of $X$. Let $R$ be a presieve of $U$. Let $x$ be an element of $\Sigma$ applied to the function that maps $V$ to $\SubtypeSet {f}{R (V , f)}$. Then the covering of $R$ and $x$ is an open of the set of carriers of $X$ defined as $\operatorname{fst}$ applied to $x$.

TopCat.Presheaf.presieveOfCoveringdefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the presieve of U (from the name)

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then the presieve of $U$ is a presieve of the supremum of $U$ defined as $\operatorname{presieveOfCoveringAux}$ applied to $U$ and the supremum of $U$.

TopCat.Presheaf.presieveOfCovering.homOfIndexdefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the homomorphism of U and i (from the name)

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Let $i$ be an element of $x$. Then the homomorphism of $U$ and $i$ is an element of $\Sigma$ applied to the function that maps $V$ to $\SubtypeSet {f}{\operatorname{presieveOfCovering} (U)}$ defined as $\operatorname{mk}$ applied to $U$ applied to $i$ and $\operatorname{leSupr}$ applied to $U$ and $i$.

TopCat.Presheaf.presieveOfCovering.indexOfHomdefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the index of U and f (from the name)

English

Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Let $f$ be an element of $\Sigma$ applied to the function that maps $V$ to $\SubtypeSet {f_{1}}{\operatorname{presieveOfCovering} (U)}$. Then the index of $U$ and $f$ is an element of $x$.

TopCat.Sheaf.isTerminalOfEmptydefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the empty component of F (from the docstring)

English

Let $F$ be a sheaf of $C$ and $X$. Then the empty component of $F$ is an element of $\operatorname{IsTerminal}$ applied to the action of the object of $F$ and $\operatorname{op}$ applied to the bottom.

TopCat.Sheaf.isTerminalOfEqEmptydefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

no wording

English

Let $F$ be a sheaf of $C$ and $X$. Assume that $U$ is equal to the bottom. Then $\operatorname{isTerminalOfEqEmpty}$ applied to $F$ and $h$ is an element of $\operatorname{IsTerminal}$ applied to the action of the object of $F$ and $\operatorname{op}$ applied to $U$.

TopCat.Sheaf.restrictHomEquivHomdefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Let $\mathrm{F'}$ be a sheaf of $C$ and $X$. Assume that the range of $B$ is a basis. Then $\operatorname{restrictHomEquivHom}$ applied to $F$, $\mathrm{F'}$ and $h$ is an equivalence from the set of homomorphisms of the composition of the opposite of the induced functor of $B$ and $F$ and the composition of the opposite of the induced functor of $B$ and the object of $\mathrm{F'}$ to the set of homomorphisms of $F$ and the object of $\mathrm{F'}$ defined as $\operatorname{restrictHomEquivHom}$.

TopologicalSpace.Opens.sheafRestrictdefMathlib.Topology.Sheaves.SheafCondition.Sites, function or constant

Wording

the restriction functor of U (from the docstring)

English

Let $U$ be an open of the set of carriers of $X$. Then the restriction functor of $U$ is a functor of the set of sheaves of the Grothendieck topology of the set of carriers of $X$ and $C$ and the set of sheaves of the Grothendieck topology of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {U}{x_{1}})}$ and $C$.

Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

TopCat.Presheaf.IsCompatibledefMathlib.Topology.Sheaves.SheafCondition.UniqueGluing, predicate

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{3}$ to opens of the set of carriers of $X$. Let $\mathrm{sf}$ be a function from elements $i$ of $x_{3}$ to types of the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$. Then $\operatorname{IsCompatible}$ holds for $F$, $U$, $i$ and $\mathrm{sf}$, if for all elements $i$ and $j$ of $x_{3}$, $\operatorname{hom}$ applied to the map of $F$ and the opposite in $\operatorname{infLELeft}$ applied to $U$ applied to $i$ and $U$ applied to $j$ and $i$ applied to $i$ is equal to $\operatorname{hom}$ applied to the map of $F$ and the opposite in $\operatorname{infLERight}$ applied to $U$ applied to $i$ and $U$ applied to $j$ and $i$ applied to $j$.

TopCat.Presheaf.IsCompatible.sectionPairwisedefMathlib.Topology.Sheaves.SheafCondition.UniqueGluing, function or constant

Wording

the section pairwise of h (from the name)

English

Assume that $\operatorname{IsCompatible}$ holds for $F$, $U$ and $\mathrm{sf}$. Then the section pairwise of $h$ is an element of the section of the composition of the opposite of the diagram of $U$ and $F$ defined as $\operatorname{objPairwiseOfFamily}$ applied to $\mathrm{sf}$.

TopCat.Presheaf.IsGluingdefMathlib.Topology.Sheaves.SheafCondition.UniqueGluing, predicate

Wording

i is a gluing with respect to sf (from the name)

English

Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{3}$ to opens of the set of carriers of $X$. Let $\mathrm{sf}$ be a function from elements $i$ of $x_{3}$ to types of the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$. Let $s$ be a type of the action of $F$ and $\operatorname{op}$ applied to the supremum of $U$. Then $\mathrm{sf}$ is a gluing with respect to $i$, if for all elements $i$ of $x_{3}$, $\operatorname{hom}$ applied to the map of $F$ and the opposite in $\operatorname{leSupr}$ applied to $U$ and $i$ and $\mathrm{sf}$ is equal to $i$ applied to $i$.

TopCat.Presheaf.IsSheafUniqueGluingdefMathlib.Topology.Sheaves.SheafCondition.UniqueGluing, predicate

Wording

F is a sheaf unique gluing (from the name)

English

Let $F$ be a presheaf of $C$ and $X$. Then $F$ is a sheaf unique gluing, if for all sets $x_{3}$, for all functions $U$ from elements of $x_{3}$ to opens of the set of carriers of $X$, for all functions $\mathrm{sf}$ from elements $i$ of $x_{3}$ to types of the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$, if $\operatorname{IsCompatible}$ holds for $F$, $U$ and $\mathrm{sf}$, then $\mathrm{ExistsUnique}$ holds for the function that maps $s$ to the proposition that $s$ is a gluing with respect to $\mathrm{sf}$.

TopCat.Presheaf.objPairwiseOfFamilydefMathlib.Topology.Sheaves.SheafCondition.UniqueGluing, function or constant

Wording

the object pairwise of sf and i1 (from the name)

English

Let $\mathrm{sf}$ be a function from elements $i_{1}$ of $x$ to elements of the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i_{1}$. Let $i$ be an opposite of the set of pairwises of $x$. Then the object pairwise of $i_{1}$ and $\mathrm{sf}$ is an element of the action of the composition of the opposite of the diagram of $U$ and $F$ and $i$.

Mathlib.Topology.Sheaves.SheafOfFunctions

TopCat.sheafToTypedefMathlib.Topology.Sheaves.SheafOfFunctions, function or constant

Wording

the sheaf to type of X and T (from the name)

English

Let $X$ be a topological category. Let $T$ be a set. Then the sheaf to type of $X$ and $T$ is a sheaf of the set of sets and $X$ defined as $\operatorname{mk}$ applied to the presheaf to type of $X$ and $T$ and $\mathrm{TopCat\_\_Presheaf\_\_toType\_isSheaf}$ applied to $X$ and $T$.

TopCat.sheafToTypesdefMathlib.Topology.Sheaves.SheafOfFunctions, function or constant

Wording

the sheaf to type of X and T (from the name)

English

Let $X$ be a topological category. Let $T$ be a function from carriers of $X$ to sets. Then the sheaf to type of $X$ and $T$ is a sheaf of the set of sets and $X$ defined as $\operatorname{mk}$ applied to the presheaf to type of $X$ and $T$ and $\mathrm{TopCat\_\_Presheaf\_\_toTypes\_isSheaf}$ applied to $X$ and $T$.

Mathlib.Topology.Sheaves.Sheafify

TopCat.Presheaf.Sheafify.isGermdefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

no wording

English

Let $F$ be a presheaf of the set of sets and $X$. Then $\operatorname{isGerm}$ applied to $F$ is a prelocal predicate of the function that maps $x$ to the stalk of $F$ and $x$.

TopCat.Presheaf.Sheafify.isLocallyGermdefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

no wording

English

Let $F$ be a presheaf of the set of sets and $X$. Then $\operatorname{isLocallyGerm}$ applied to $F$ is a local predicate of the function that maps $x$ to the stalk of $F$ and $x$ defined as the sheafification of $\operatorname{isGerm}$ applied to $F$.

TopCat.Presheaf.sheafifydefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

the sheafification of F (from the docstring)

English

Let $F$ be a presheaf of the set of sets and $X$. Then the sheafification of $F$ is a sheaf of the set of sets and $X$ defined as the subsheaf to type of $\operatorname{isLocallyGerm}$ applied to $F$.

TopCat.Presheaf.sheafifyStalkIsodefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

the sheafification stalk isomorphism of F and x (from the name)

English

Let $F$ be a presheaf of the set of sets and $X$. Let $x$ be a carrier of $X$. Then the sheafification stalk isomorphism of $F$ and $x$ is an isomorphism of the stalk of the underlying presheaf of the sheafification of $F$ and $x$ and the stalk of $F$ and $x$.

TopCat.Presheaf.stalkToFiberdefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

the stalk to fiber of F and x (from the name)

English

Let $F$ be a presheaf of the set of sets and $X$. Let $x$ be a carrier of $X$. Then the stalk to fiber of $F$ and $x$ is a homomorphism of the stalk of the underlying presheaf of the sheafification of $F$ and $x$ and the stalk of $F$ and $x$ defined as the stalk to fiber of $\operatorname{isLocallyGerm}$ applied to $F$ and $x$.

TopCat.Presheaf.toSheafifydefMathlib.Topology.Sheaves.Sheafify, function or constant

Wording

the sheafification of F (from the name)

English

Let $F$ be a presheaf of the set of sets and $X$. Then the sheafification of $F$ is a homomorphism of $F$ and the object of the sheafification of $F$.

Mathlib.Topology.Sheaves.Skyscraper

SkyscraperPresheafFunctor.map'defMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the map of x and f (from the name)

English

Let $x$ be a carrier of $X$. Let $f$ be a homomorphism of $a$ and $b$. Then the map of $x$ and $f$ is a homomorphism of the skyscraper presheaf of $x$ and $a$ and the skyscraper presheaf of $x$ and $b$.

StalkSkyscraperPresheafAdjunctionAuxs.counitdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the counit in x (from the docstring)

English

Let $x$ be a carrier of $X$. Then the counit in $x$ is a homomorphism of the composition of the skyscraper presheaf functor of $x$ and the stalk functor of $C$ and $x$ and the identity of $C$.

StalkSkyscraperPresheafAdjunctionAuxs.fromStalkdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

no wording

English

Let $x$ be a carrier of $X$. Let $f$ be a homomorphism of $x_{3}$ and the skyscraper presheaf of $x$ and $c$. Then $\operatorname{fromStalk}$ applied to $x$ and $f$ is a homomorphism of the stalk of $x_{3}$ and $x$ and $c$.

StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheafdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf of x and f (from the name)

English

Let $x$ be a carrier of $X$. Let $f$ be a homomorphism of the stalk of $x_{3}$ and $x$ and $c$. Then the skyscraper presheaf of $x$ and $f$ is a homomorphism of $x_{3}$ and the skyscraper presheaf of $x$ and $c$.

StalkSkyscraperPresheafAdjunctionAuxs.unitdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the unit in x (from the docstring)

English

Let $x$ be a carrier of $X$. Then the unit in $x$ is a homomorphism of the identity of the set of presheafs of $C$ and $X$ and the composition of the stalk functor of $C$ and $x$ and the skyscraper presheaf functor of $x$.

isTerminalSkyscraperSheafObjObjOfNotMemdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

no wording

English

Assume that $x$ is not an element of the opposite of $U$. Then $\mathrm{isTerminalSkyscraperSheafObjObjOfNotMem}$ applied to $h_{1}$ is an element of $\operatorname{IsTerminal}$ applied to the action of the object of the skyscraper sheaf of $x$ and $A$ and $U$.

skyscraperPresheafdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Then the skyscraper presheaf of $x$ and $A$ is a presheaf of $C$ and $X$.

skyscraperPresheafCoconedefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the cocone at x (from the docstring)

English

Let $x$ and $y$ be carriers of $X$. Let $A$ be an element of $C$. Then the cocone at $x$ is a cocone of the composition of the opposite of the inclusion of $y$ and the skyscraper presheaf of $x$ and $A$.

skyscraperPresheafCoconeIsColimitOfNotSpecializesdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the cocone at x (from the docstring)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that it is not the case that $\mathrm{Specializes}$ holds for $x$ and $y$. Then the cocone at $x$ is an element of $\operatorname{IsColimit}$ applied to the cocone at $x$.

skyscraperPresheafCoconeIsColimitOfSpecializesdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

no wording

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that $\mathrm{Specializes}$ holds for $x$ and $y$. Then $\mathrm{skyscraperPresheafCoconeIsColimitOfSpecializes}$ applied to $x$, $A$ and $h_{1}$ is an element of $\operatorname{IsColimit}$ applied to the skyscraper presheaf cocone of $x$ and $A$.

skyscraperPresheafCoconeOfSpecializesdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf cocone of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that $\mathrm{Specializes}$ holds for $x$ and $y$. Then the skyscraper presheaf cocone of $x$ and $A$ is a cocone of the composition of the opposite of the inclusion of $y$ and the skyscraper presheaf of $x$ and $A$.

skyscraperPresheafFunctordefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf functor of x (from the name)

English

Let $x$ be a carrier of $X$. Then the skyscraper presheaf functor of $x$ is a functor of $C$ and the set of presheafs of $C$ and $X$ defined as $\operatorname{mk}$ applied to $\mathrm{skyscraperPresheaf}$ applied to $x$, the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{map'}$ applied to $x$, the function that maps $x_{5}$ to $\mathrm{SkyscraperPresheafFunctor\_\_map'\_id}$ applied to $x$ and the function that maps $x_{6}$, $x_{7}$ and $x_{8}$ to $\mathrm{SkyscraperPresheafFunctor\_\_map'\_comp}$ applied to $x$.

skyscraperPresheafStalkAdjunctiondefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf stalk adjunction of x (from the name)

English

Let $x$ be a carrier of $X$. Then the skyscraper presheaf stalk adjunction of $x$ is an adjunction of the stalk functor of $C$ and $x$ and the skyscraper presheaf functor of $x$.

skyscraperPresheafStalkOfNotSpecializesdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf stalk of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that it is not the case that $\mathrm{Specializes}$ holds for $x$ and $y$. Then the skyscraper presheaf stalk of $x$ and $A$ is an isomorphism of the stalk of the skyscraper presheaf of $x$ and $A$ and $y$ and $\operatorname{terminal}$ applied to $C$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the cocone at $x$ and the cocone at $x$.

skyscraperPresheafStalkOfNotSpecializesIsTerminaldefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf stalk of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that it is not the case that $\mathrm{Specializes}$ holds for $x$ and $y$. Then the skyscraper presheaf stalk of $x$ and $A$ is an element of $\operatorname{IsTerminal}$ applied to the stalk of the skyscraper presheaf of $x$ and $A$ and $y$ defined as $\operatorname{ofIso}$ applied to $\operatorname{terminalIsTerminal}$ and the inverse of the skyscraper presheaf stalk of $x$ and $A$.

skyscraperPresheafStalkOfSpecializesdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper presheaf stalk of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Assume that $\mathrm{Specializes}$ holds for $x$ and $y$. Then the skyscraper presheaf stalk of $x$ and $A$ is an isomorphism of the stalk of the skyscraper presheaf of $x$ and $A$ and $y$ and $A$ defined as the isomorphism colimit cocone of $\operatorname{mk}$ applied to the skyscraper presheaf cocone of $x$ and $A$ and $\mathrm{skyscraperPresheafCoconeIsColimitOfSpecializes}$ applied to $x$, $A$ and $h_{2}$.

skyscraperSheafdefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper sheaf of x and A (from the name)

English

Let $x$ be a carrier of $X$. Let $A$ be an element of $C$. Then the skyscraper sheaf of $x$ and $A$ is a sheaf of $C$ and $X$ defined as $\operatorname{mk}$ applied to the skyscraper presheaf of $x$ and $A$ and $\mathrm{skyscraperPresheaf\_isSheaf}$ applied to $x$ and $A$.

skyscraperSheafForgetAdjunctiondefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

no wording

English

Let $x$ be a carrier of $X$. Then $\mathrm{skyscraperSheafForgetAdjunction}$ applied to $x$ is an adjunction of the stalk functor of $C$ and $x$ and the composition of the skyscraper sheaf functor of $x$ and $\operatorname{forget}$ applied to $C$ and $X$ defined as the skyscraper presheaf stalk adjunction of $x$.

skyscraperSheafFunctordefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the skyscraper sheaf functor of x (from the name)

English

Let $x$ be a carrier of $X$. Then the skyscraper sheaf functor of $x$ is a functor of $C$ and the set of sheaves of $C$ and $X$.

stalkSkyscraperSheafAdjunctiondefMathlib.Topology.Sheaves.Skyscraper, function or constant

Wording

the stalk skyscraper sheaf adjunction of x (from the name)

English

Let $x$ be a carrier of $X$. Then the stalk skyscraper sheaf adjunction of $x$ is an adjunction of the composition of $\operatorname{forget}$ applied to $C$ and $X$ and the stalk functor of $C$ and $x$ and the skyscraper sheaf functor of $x$.

Mathlib.Topology.Sheaves.Stalks

TopCat.Presheaf.germdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the germ of U and x1 (from the name)

English

Let $F$ be a presheaf of $C$ and $X$. Let $U$ be an open of the set of carriers of $X$. Let $x_{1}$ be a carrier of $X$ such that $x_{1}$ is an element of $U$. Then the germ of $U$ and $x_{1}$ is a homomorphism of the action of $F$ and $\operatorname{op}$ applied to $U$ and the stalk of $F$ and $x_{1}$ defined as the inclusion of the composition of the opposite of the inclusion of $x_{1}$ and $F$ and $\operatorname{op}$ applied to $U$.

TopCat.Presheaf.germToPullbackStalkdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the germ to pullback stalk of U and x1 (from the name)

English

Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a presheaf of $C$ and $Y$. Let $U$ be an open of the set of carriers of $X$. Let $x_{1}$ be a carrier of $X$ such that $x_{1}$ is an element of $U$. Then the germ to pullback stalk of $U$ and $x_{1}$ is a homomorphism of the action of the action of the pullback of $C$ and $f$ and $F$ and $\operatorname{op}$ applied to $U$ and the stalk of $F$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$.

TopCat.Presheaf.stalkdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk of x1 and x2 (from the docstring)

English

Let $x_{1}$ be a presheaf of $C$ and $X$. Let $x_{2}$ be a carrier of $X$. Then the stalk of $x_{1}$ and $x_{2}$ is an element of $C$ defined as the action of the stalk functor of $C$ and $x_{2}$ and $x_{1}$.

TopCat.Presheaf.stalkCongrdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk congruence of F and e (from the name)

English

Let $F$ be a presheaf of $C$ and $X$. Assume that $\mathrm{Inseparable}$ holds for $x_{1}$ and $y$. Then the stalk congruence of $F$ and $e$ is an isomorphism of the stalk of $F$ and $x_{1}$ and the stalk of $F$ and $y$.

TopCat.Presheaf.stalkFunctordefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk functor of C and x1 (from the name)

English

Let $C$ be a set. Let $x_{1}$ be a carrier of $X$. Then the stalk functor of $C$ and $x_{1}$ is a functor of the set of presheafs of $C$ and $X$ and $C$ defined as the composition of the action of the left whiskering of the set of opposites of the set of opens of the set of carriers of $X$ and $C$ and the opposite of the inclusion of $x_{1}$ and the colimit.

TopCat.Presheaf.stalkPullbackHomdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk pullback homomorphism of F and x1 (from the name)

English

Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a presheaf of $C$ and $Y$. Let $x_{1}$ be a carrier of $X$. Then the stalk pullback homomorphism of $F$ and $x_{1}$ is a homomorphism of the stalk of $F$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$ and the stalk of the action of the pullback of $C$ and $f$ and $F$ and $x_{1}$ defined as the composition of the map of the stalk functor of $C$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$ and the component of the unit of the pullback pushforward adjunction of $C$ and $f$ and $F$ and $\operatorname{stalkPushforward}$ applied to $C$, $f$, the action of the pullback of $C$ and $f$ and $F$ and $x_{1}$.

TopCat.Presheaf.stalkPullbackInvdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk pullback inverse of F and x1 (from the name)

English

Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a presheaf of $C$ and $Y$. Let $x_{1}$ be a carrier of $X$. Then the stalk pullback inverse of $F$ and $x_{1}$ is a homomorphism of the stalk of the action of the pullback of $C$ and $f$ and $F$ and $x_{1}$ and the stalk of $F$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$.

TopCat.Presheaf.stalkPullbackIsodefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the stalk pullback isomorphism of F and x1 (from the name)

English

Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a presheaf of $C$ and $Y$. Let $x_{1}$ be a carrier of $X$. Then the stalk pullback isomorphism of $F$ and $x_{1}$ is an isomorphism of the stalk of $F$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$ and the stalk of the action of the pullback of $C$ and $f$ and $F$ and $x_{1}$.

TopCat.Presheaf.stalkPushforwarddefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

no wording

English

Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Let $F$ be a presheaf of $C$ and $X$. Let $x_{1}$ be a carrier of $X$. Then $\operatorname{stalkPushforward}$ applied to $C$, $f$, $F$ and $x_{1}$ is a homomorphism of the stalk of the action of the pushforward functor of $C$ and $f$ and $F$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$ and the stalk of $F$ and $x_{1}$ defined as the composition of the map of the colimit and the right whisker of the opposite of the inverse of the inclusion map isomorphism of $f$ and $x_{1}$ and $F$ and $\operatorname{pre}$ applied to the action of the action of the left whiskering of the set of opposites of the set of opens of the set of carriers of $X$ and $C$ and the opposite of the inclusion of $x_{1}$ and $F$ and the opposite of the map of $f$ and $x_{1}$.

TopCat.Presheaf.stalkSpecializesdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

no wording

English

Let $F$ be a presheaf of $C$ and $X$. Assume that $\mathrm{Specializes}$ holds for $x_{1}$ and $y$. Then $\operatorname{stalkSpecializes}$ applied to $F$ and $h_{1}$ is a homomorphism of the stalk of $F$ and $y$ and the stalk of $F$ and $x_{1}$.

TopCat.Presheaf.ΓgermdefMathlib.Topology.Sheaves.Stalks, function or constant

Wording

the germ of F and x1 (from the docstring)

English

Let $F$ be a presheaf of $C$ and $X$. Let $x_{1}$ be a carrier of $X$. Then the germ of $F$ and $x_{1}$ is a homomorphism of the action of $F$ and $\operatorname{op}$ applied to the top and the stalk of $F$ and $x_{1}$ defined as the germ of the top and $x_{1}$.

Mathlib.Topology.ShrinkingLemma

ShrinkingLemma.PartialRefinement.carrierdefMathlib.Topology.ShrinkingLemma, function or constant

Wording

the carrier of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{PartialRefinement}$ applied to $u$, $s$ and $p$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

ShrinkingLemma.PartialRefinement.chainSupdefMathlib.Topology.ShrinkingLemma, function or constant

Wording

the chain supremum of c (from the name)

English

Let $c$ be an element of $\wp \operatorname{PartialRefinement} (u , s , p)$ such that $\mathrm{IsChain}$ holds for the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Leq} (x_{3} , x_{4})$ and $c$ and $c$ is nonempty. Assume that for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then $\operatorname{ofPred}$ applied to the function that maps $i_{1}$ to $\MembershipmemMACRoT {u (i_{1})}{x_{2}}$ is finite. Assume that $s$ is less than or equal to the union of the function that maps $i$ to $u$ applied to $i$. Then the chain supremum of $c$ is an element of $\operatorname{PartialRefinement}$ applied to $u$, $s$ and $p$.

ShrinkingLemma.PartialRefinement.chainSupCarrierdefMathlib.Topology.ShrinkingLemma, function or constant

Wording

the carrier of the least upper bound of c (from the docstring)

English

Let $c$ be an element of $\wp \operatorname{PartialRefinement} (u , s , p)$. Then the carrier of the least upper bound of $c$ is an element of $\wp x$ defined as the union of the function that maps $v$ to the union of the function that maps $h$ to the carrier of $v$.

ShrinkingLemma.PartialRefinement.finddefMathlib.Topology.ShrinkingLemma, function or constant

Wording

no wording

English

Let $c$ be a nonempty element of $\wp \operatorname{PartialRefinement} (u , s , p)$. Let $i$ be an element of $x$. Then $\operatorname{find}$ applied to $c$, $\mathrm{ne}$ and $i$ is an element of $\operatorname{PartialRefinement}$ applied to $u$, $s$ and $p$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $v$ of $\operatorname{PartialRefinement}$ applied to $u$, $s$ and $p$, such that $v$ is an element of $c$ and $i$ is an element of the carrier of $v$, the function that maps $\mathrm{hi}$ to $\operatorname{choose}$ applied to $\mathrm{hi}$ and the function that maps $\mathrm{hi1}$ to $\operatorname{some}$ applied to $\mathrm{ne}$.

ShrinkingLemma.PartialRefinement.toFundefMathlib.Topology.ShrinkingLemma, function or constant

Wording

the partial refinement of self and x2 (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{PartialRefinement}$ applied to $u$, $s$ and $p$. Let $x_{2}$ be an element of $x$. Then the partial refinement of $\mathrm{self}$ and $x_{2}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Mathlib.Topology.Sober

IsGenericPointdefMathlib.Topology.Sober, predicate

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Let $S$ be an element of $\wp x$. Then $\mathrm{IsGenericPoint}$ holds for $x_{2}$ and $S$, if the closure of $\operatorname{singleton}$ applied to $x_{2}$ is equal to $S$.

IsIrreducible.genericPointdefMathlib.Topology.Sober, function or constant

Wording

the generic point of hS (from the name)

English

Assume that $S$ is irreducible. Then the generic point of $\mathrm{hS}$ is an element of $x$.

QuasiSoberclassMathlib.Topology.Sober, predicate

Wording

no wording

English

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

genericPointdefMathlib.Topology.Sober, function or constant

Wording

the generic point of x (from the name)

English

Let $x$ be a set. Then the generic point of $x$ is an element of $x$ defined as the generic point of $\mathrm{IrreducibleSpace\_\_isIrreducible\_univ}$ applied to $x$.

genericPointsdefMathlib.Topology.Sober, function or constant

Wording

the generic point of x (from the name)

English

Let $x$ be a set. Then the generic point of $x$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that the closure of $\operatorname{singleton}$ applied to $x_{2}$ is an element of the irreducible component of $x$.

genericPoints.componentdefMathlib.Topology.Sober, function or constant

Wording

the irreducible component of x2 (from the docstring)

English

Let $x_{2}$ be an element of the generic point of $x$. Then the irreducible component of $x_{2}$ is an element of the irreducible component of $x$ defined as the closure of $\operatorname{singleton}$ applied to $x_{2}$.

genericPoints.equivdefMathlib.Topology.Sober, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from the set of elements of the generic point of $x$ to the set of elements of the irreducible component of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{component}$, $\operatorname{ofComponent}$, $\mathrm{genericPoints\_\_ofComponent\_component}$ and $\mathrm{genericPoints\_\_component\_ofComponent}$.

genericPoints.ofComponentdefMathlib.Topology.Sober, function or constant

Wording

the generic point of x2 (from the docstring)

English

Let $x_{2}$ be an element of the irreducible component of $x$. Then the generic point of $x_{2}$ is an element of the generic point of $x$.

irreducibleSetEquivPointsdefMathlib.Topology.Sober, function or constant

Wording

the irreducible set equivalence point (from the name)

English

The irreducible set equivalence point is an order isomorphism of $\operatorname{IrreducibleCloseds}$ applied to $x$ and $x$.

Mathlib.Topology.Specialization

SpecializationdefMathlib.Topology.Specialization, type

Wording

specialization of x (from the name)

English

Let $x$ be a set. Then a specialization of $x$ is an element of the function that maps $x$ to $x$.

Specialization.mapdefMathlib.Topology.Specialization, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Then the map of $f$ is an order homomorphism of the set of specializations of $x$ and the set of specializations of $x_{1}$.

Specialization.ofEquivdefMathlib.Topology.Specialization, function or constant

Wording

the specialization (from the name)

English

The specialization is an equivalence from the set of specializations of $x$ to $x$ defined as the identity of the set of specializations of $x$.

Specialization.toEquivdefMathlib.Topology.Specialization, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an equivalence from $x$ to the set of specializations of $x$ defined as the identity of $x$.

homeoWithUpperSetTopologyorderIsodefMathlib.Topology.Specialization, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\mathrm{homeoWithUpperSetTopologyorderIso}$ applied to $x$ is a homeomorphism of $x$ and $\operatorname{WithUpperSet}$ applied to the set of specializations of $x$.

orderIsoSpecializationWithUpperSetTopologydefMathlib.Topology.Specialization, function or constant

Wording

the order isomorphism specialization with upper set topology of x (from the name)

English

Let $x$ be a set. Then the order isomorphism specialization with upper set topology of $x$ is an order isomorphism of $x$ and the set of specializations of $\operatorname{WithUpperSet}$ applied to $x$.

topToPreorddefMathlib.Topology.Specialization, function or constant

Wording

no wording

English

$\mathrm{topToPreord}$ is a functor of the set of topological categories and $\mathrm{Preord}$.

Mathlib.Topology.Spectral.Basic

SpectralSpaceclassMathlib.Topology.Spectral.Basic, predicate

Wording

X is spectral (from the docstring)

English

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

Mathlib.Topology.Spectral.ConstructibleTopology

WithConstructibleTopologydefMathlib.Topology.Spectral.ConstructibleTopology, type

Wording

no wording

English

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

constructibleTopologySubbasisdefMathlib.Topology.Spectral.ConstructibleTopology, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\mathrm{constructibleTopologySubbasis}$ applied to $X$ is an element of $\wp (\wp X)$ defined as the union of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is open and compact and $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to the proposition that $s_{1}$ is closed and the complement of $s_{1}$ is compact.

Mathlib.Topology.Spectral.Hom

IsSpectralMapstructureMathlib.Topology.Spectral.Hom, predicate

Wording

f is spectral (from the docstring)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $f$ is spectral.

SpectralMapstructureMathlib.Topology.Spectral.Hom, type

Wording

spectral map of x and x1 (from the name)

English

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

SpectralMap.compdefMathlib.Topology.Spectral.Hom, function or constant

Wording

the composition of f and g (from the name)

English

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

SpectralMap.copydefMathlib.Topology.Spectral.Hom, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a spectral 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 spectral map of $x$ and $x_{1}$.

SpectralMap.iddefMathlib.Topology.Spectral.Hom, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a spectral map of $x$ and $x$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and $\mathrm{isSpectralMap\_id}$.

SpectralMap.toContinuousMapdefMathlib.Topology.Spectral.Hom, function or constant

Wording

the continuous map of f (from the name)

English

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

SpectralMap.toFundefMathlib.Topology.Spectral.Hom, function or constant

Wording

the spectral map of self and x4 (from the name)

English

Let $\mathrm{self}$ be a spectral map of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the spectral map of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

SpectralMapClassclassMathlib.Topology.Spectral.Hom, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{SpectralMapClass}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Topology.Spectral.Prespectral

PrespectralSpaceclassMathlib.Topology.Spectral.Prespectral, predicate

Wording

no wording

English

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

PrespectralSpace.opensEquivdefMathlib.Topology.Spectral.Prespectral, function or constant

Wording

the open equivalence (from the name)

English

The open equivalence is an order isomorphism of the set of opens of $X$ and the set of ideals of the set of compact opens of $X$.

Mathlib.Topology.Subpath

Path.Homotopy.concatdefMathlib.Topology.Subpath, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $X$. Let $F$ be a function from elements $k_{2}$ of $\mathrm{Fin}$ applied to $n$ to paths of $p$ applied to $\operatorname{castSucc}$ applied to $k_{2}$ and $p$ applied to $\operatorname{succ}$ applied to $k_{2}$. Let $G$ be a function from elements $k_{1}$ of $\mathrm{Fin}$ applied to $n$ to paths of $p$ applied to $\operatorname{castSucc}$ applied to $k_{1}$ and $p$ applied to $\operatorname{succ}$ applied to $k_{1}$. Let $H$ be a function from elements $k$ of $\mathrm{Fin}$ applied to $n$ to homotopies of $F$ applied to $k$ and $G$ applied to $k$. Then $\operatorname{concat}$ applied to $p$, $k_{2}$, $F$, $k_{1}$, $G$, $k$ and $H$ is a homotopy of $\operatorname{concat}$ applied to $p$ and $F$ and $\operatorname{concat}$ applied to $p$ and $G$.

Path.Homotopy.concatSubpathdefMathlib.Topology.Subpath, function or constant

Wording

no wording

English

Let $x_{1}$ be a path of $a$ and $b$. Let $t$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of the unit interval. Then $\operatorname{concatSubpath}$ applied to $x_{1}$ and $t$ is a homotopy of $\operatorname{concat}$ applied to $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $x_{1}$ and $t$ and the function that maps $k$ to the subpath of $x_{1}$ and the subpath of $x_{1}$.

Path.Homotopy.subpathTransSubpathdefMathlib.Topology.Subpath, function or constant

Wording

the subpath composition subpath of x3 and x4 (from the name)

English

Let $x_{1}$ be a path of $a$ and $b$. Let $x_{2}$, $x_{3}$ and $x_{4}$ be elements of the unit interval. Then the subpath composition subpath of $x_{3}$ and $x_{4}$ is a homotopy of the composition of the subpath of $x_{1}$ and the subpath of $x_{1}$ and the subpath of $x_{1}$ defined as the composition of $\operatorname{subpathTransSubpathRefl}$ applied to $x_{1}$, $x_{2}$, $x_{3}$ and $x_{4}$ and the composition identity of the subpath of $x_{1}$.

Path.concatdefMathlib.Topology.Subpath, function or constant

Wording

no wording

English

Let $p$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $X$. Let $F$ be a function from elements $k$ of $\mathrm{Fin}$ applied to $n$ to paths of $p$ applied to $\operatorname{castSucc}$ applied to $k$ and $p$ applied to $\operatorname{succ}$ applied to $k$. Then $\operatorname{concat}$ applied to $p$, $k$ and $F$ is a path of $p$ applied to $0$ and $p$ applied to $\operatorname{last}$ applied to $n$ defined as the function that maps $F$ to $\operatorname{dfoldl}$ applied to $n$, the function that maps $i$ to the set of paths of $p$ applied to $0$ and $p$ applied to $i$, the function that maps $i_{1}$ and $\mathrm{ih}$ to the composition of $\mathrm{ih}$ and $k$ applied to $i_{1}$, the identity of $p$ applied to $0$ and $F$.

Path.subpathdefMathlib.Topology.Subpath, function or constant

Wording

the subpath of x1 (from the docstring)

English

Let $x_{1}$ be a path of $a$ and $b$. Let $x_{2}$ and $x_{3}$ be elements of the unit interval. Then the subpath of $x_{1}$ is a path of $x_{1}$ applied to $x_{2}$ and $x_{1}$ applied to $x_{3}$.

Mathlib.Topology.TietzeExtension

TietzeExtensionclassMathlib.Topology.TietzeExtension, predicate

Wording

no wording

English

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

Mathlib.Topology.UniformSpace.AbstractCompletion

AbstractCompletionstructureMathlib.Topology.UniformSpace.AbstractCompletion, type

Wording

abstract completion of x (from the name)

English

Let $x$ be a set. Then the abstract completions of $x$ are a basic type.

AbstractCompletion.coedefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the coercion of self and x2 (from the name)

English

Let $\mathrm{self}$ be an abstract completion of $x$. Let $x_{2}$ be an element of $x$. Then the coercion of $\mathrm{self}$ and $x_{2}$ is a space of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

AbstractCompletion.comparedefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

no wording

English

Let $\mathrm{pkg}$ and $\mathrm{pkg'}$ be abstract completions of $x$. Let $x_{2}$ be a space of $\mathrm{pkg}$. Then $\operatorname{compare}$ applied to $\mathrm{pkg}$, $\mathrm{pkg'}$ and $x_{2}$ is a space of $\mathrm{pkg'}$ defined as $\operatorname{extend}$ applied to $\mathrm{pkg}$, $\operatorname{coe}$ applied to $\mathrm{pkg'}$ and $x_{2}$.

AbstractCompletion.compareEquivdefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

no wording

English

Let $\mathrm{pkg}$ and $\mathrm{pkg'}$ be abstract completions of $x$. Then $\operatorname{compareEquiv}$ applied to $\mathrm{pkg}$ and $\mathrm{pkg'}$ is a uniform equivalence of the set of spaces of $\mathrm{pkg}$ and the set of spaces of $\mathrm{pkg'}$.

AbstractCompletion.extenddefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

no wording

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{4}$ be a space of $\mathrm{pkg}$. Then $\operatorname{extend}$ applied to $\mathrm{pkg}$, $f$ and $x_{4}$ is an element of $x_{2}$ defined as $\iteMACRoG {\mathrm{UniformContinuous} (f)}{\operatorname{extend} (\operatorname{isDenseInducing} (\mathrm{pkg}), f)}{x_{4}}{f (\operatorname{some} (\operatorname{dense} (\mathrm{pkg}), x_{4}))}$.

AbstractCompletion.extend₂defMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

no wording

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $\mathrm{pkg'}$ be an abstract completion of $x_{2}$. Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{4}$. Let $x_{6}$ be a space of $\mathrm{pkg}$. Let $x_{7}$ be a space of $\mathrm{pkg'}$. Then $\mathrm{AbstractCompletion\_\_extend\_u2082\_}$ applied to $\mathrm{pkg}$, $\mathrm{pkg'}$, $f$, $x_{6}$ and $x_{7}$ is an element of $x_{4}$ defined as $\operatorname{curry}$ applied to $\operatorname{extend}$ applied to the product of $\mathrm{pkg}$ and $\mathrm{pkg'}$ and $\operatorname{uncurry}$ applied to $f$, $x_{6}$ and $x_{7}$.

AbstractCompletion.mapdefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the map of x4 and #4 (from the name)

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $\mathrm{pkg'}$ be an abstract completion of $x_{2}$. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{4}$ be a space of $\mathrm{pkg}$. Then the map of $f$ and $x_{4}$ is a space of $\mathrm{pkg'}$ defined as $\operatorname{extend}$ applied to $\mathrm{pkg}$, $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $\mathrm{pkg'}$ and $f$ and $x_{4}$.

AbstractCompletion.mapEquivdefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the map equivalence of e and #3 (from the name)

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $\mathrm{pkg'}$ be an abstract completion of $x_{2}$. Let $e$ be a uniform equivalence of $x$ and $x_{2}$. Then the map equivalence of $\mathrm{pkg'}$ and $e$ is a uniform equivalence of the set of spaces of $\mathrm{pkg}$ and the set of spaces of $\mathrm{pkg'}$.

AbstractCompletion.map₂defMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the map of #5 and #6 (from the name)

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $\mathrm{pkg'}$ be an abstract completion of $x_{2}$. Let $\mathrm{pkg''}$ be an abstract completion of $x_{4}$. Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{4}$. Let $x_{6}$ be a space of $\mathrm{pkg}$. Let $x_{7}$ be a space of $\mathrm{pkg'}$. Then the map of $x_{6}$ and $x_{7}$ is a space of $\mathrm{pkg''}$ defined as $\mathrm{AbstractCompletion\_\_extend\_u2082\_}$ applied to $\mathrm{pkg}$, $\mathrm{pkg'}$, $\operatorname{bicompr}$ applied to $\operatorname{coe}$ applied to $\mathrm{pkg''}$ and $f$, $x_{6}$ and $x_{7}$.

AbstractCompletion.ofCompletedefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the abstract completion (from the name)

English

The abstract completion is an abstract completion of $x$.

AbstractCompletion.proddefMathlib.Topology.UniformSpace.AbstractCompletion, function or constant

Wording

the product of pkg and #2 (from the name)

English

Let $\mathrm{pkg}$ be an abstract completion of $x$. Let $\mathrm{pkg'}$ be an abstract completion of $x_{2}$. Then the product of $\mathrm{pkg}$ and $\mathrm{pkg'}$ is an abstract completion of $\mathrm{Prod}$ applied to $x$ and $x_{2}$.

AbstractCompletion.spacedefMathlib.Topology.UniformSpace.AbstractCompletion, type

Wording

space of self (from the name)

English

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

Mathlib.Topology.UniformSpace.Basic

UniformContinuous₂defMathlib.Topology.UniformSpace.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Then $\mathrm{UniformContinuous\_u2082\_}$ holds for $f$, if $\mathrm{UniformContinuous}$ holds for $\operatorname{uncurry}$ applied to $f$.

UniformSpace.giGenerateFilterdefMathlib.Topology.UniformSpace.Basic, function or constant

Wording

no wording

English

$\operatorname{giGenerateFilter}$ is a Galois insertion of $\operatorname{generateFilter}$ and the uniformity of $x$.

entourageProddefMathlib.Topology.UniformSpace.Basic, function or constant

Wording

the entourage product of u and v (from the name)

English

Let $u$ be a set relation of $x$ and $x$. Let $v$ be a set relation of $x_{1}$ and $x_{1}$. Then the entourage product of $u$ and $v$ is a set relation of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

Mathlib.Topology.UniformSpace.Cauchy

CauchydefMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

no wording

English

Let $f$ be a filter of $x$. Then $\mathrm{Cauchy}$ holds for $f$, if $\operatorname{NeBot}$ holds for $f$ and $\operatorname{sprod}$ applied to $f$ and $f$ is less than or equal to the uniformity of $x$.

CauchySeqdefMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

u is a Cauchy sequence (from the name)

English

Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then $u$ is a Cauchy sequence, if $\mathrm{Cauchy}$ holds for the forward map of $u$ and $\operatorname{atTop}$.

CompleteSpaceclassMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

x is a complete space (from the name)

English

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

DiscreteUniformity.cauchyConstdefMathlib.Topology.UniformSpace.Cauchy, function or constant

Wording

the Cauchy constant of hf (from the name)

English

Assume that $\mathrm{Cauchy}$ holds for $f$. Then the Cauchy constant of $\mathrm{hf}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{DiscreteUniformity\_\_eq\_pure\_of\_cauchy}$ applied to $\mathrm{hf}$.

Filter.TotallyBoundeddefMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

f is totally bounded (from the name)

English

generation took over the time limit

IsCompletedefMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

s is complete (from the name)

English

Let $s$ be an element of $\wp x$. Then $s$ is complete, if for all filters $f$ of $x$, if $\mathrm{Cauchy}$ holds for $f$, 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 $f$ is less than or equal to the neighbourhood filter of $x_{1}$.

SequentiallyComplete.seqdefMathlib.Topology.UniformSpace.Cauchy, function or constant

Wording

the sequence of n (from the name)

English

SequentiallyComplete.setSeqdefMathlib.Topology.UniformSpace.Cauchy, function or constant

Wording

the set sequence of n (from the name)

English

Assume that $\mathrm{Cauchy}$ holds for $f$. Assume that for all natural numbers $n_{1}$, $U$ applied to $n_{1}$ is an element of the uniformity of $x$. Let $n$ be a natural number. Then the set sequence of $n$ is an element of $\wp x$ defined as the intersection of the function that maps $m$ to the intersection of the function that maps $h$ to $\operatorname{setSeqAux}$ applied to $\mathrm{hf}$, $\mathrm{U\_mem}$ and $m$.

TotallyBoundeddefMathlib.Topology.UniformSpace.Cauchy, predicate

Wording

s is totally bounded (from the name)

English

generation took over the time limit

interUnionBallsdefMathlib.Topology.UniformSpace.Cauchy, function or constant

Wording

the intersection union ball of u and V (from the name)

English

Let $\mathrm{xs}$ be a function from natural numbers to elements of $x$. Let $u$ be a function from natural numbers to natural numbers. Let $V$ be a function from natural numbers to set relations of $x$ and $x$. Then the intersection union ball of $u$ and $V$ is an element of $\wp x$ defined as the intersection of the function that maps $n$ to the union of the function that maps $m$ to the union of the function that maps $h$ to the ball of $\mathrm{xs}$ applied to $m$ and the preimage of $\operatorname{swap}$ and $V$ applied to $n$.

Mathlib.Topology.UniformSpace.Closeds

hausdorffEntouragedefMathlib.Topology.UniformSpace.Closeds, function or constant

Wording

the Hausdorff entourage of U (from the name)

English

Let $U$ be a set relation of $x$ and $x$. Then the Hausdorff entourage of $U$ is a set relation of $\wp x$ and $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $\ProdfstMACRoZ {x_{1}}$ is less than or equal to the preimage of $U$ and $\ProdsndMACRoAA {x_{1}}$ and $\ProdsndMACRoAA {x_{1}}$ is less than or equal to the image of $U$ and $\ProdfstMACRoZ {x_{1}}$.

Mathlib.Topology.UniformSpace.CompactConvergence

ContinuousMap.toUniformOnFunIsCompactdefMathlib.Topology.UniformSpace.CompactConvergence, function or constant

Wording

no wording

English

Let $f$ be a continuous map of $x$ and $x_{1}$. Then $\mathrm{UniformOnFun}$ holds for $x$, $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $K$ to the proposition that $K$ is compact. Proof. Let $f$ be arbitrary. Let $K_{1}$ be arbitrary. By K1. By IsCompact. By Set__ofPred. By f. By DFunLike__coe. By UniformOnFun__ofFun__app.

UniformEquiv.arrowCongrdefMathlib.Topology.UniformSpace.CompactConvergence, function or constant

Wording

the arrow congruence of x8 and x9 (from the name)

English

Let $x_{8}$ be a homeomorphism of $x$ and $x_{4}$. Let $x_{9}$ be a uniform equivalence of $x_{1}$ and $x_{5}$. Then the arrow congruence of $x_{8}$ and $x_{9}$ is a uniform equivalence of the set of continuous maps of $x$ and $x_{1}$ and the set of continuous maps of $x_{4}$ and $x_{5}$.

Mathlib.Topology.UniformSpace.CompareReals

CompareReals.BourbakiℝdefMathlib.Topology.UniformSpace.CompareReals, type

Wording

no wording

English

An element of $\mathrm{CompareReals\_\_Bourbaki\_u211d\_}$ is a completion of $\operatorname{Q}$.

CompareReals.QdefMathlib.Topology.UniformSpace.CompareReals, type

Wording

no wording

English

An element of $\operatorname{Q}$ is a rational number.

CompareReals.bourbakiPkgdefMathlib.Topology.UniformSpace.CompareReals, function or constant

Wording

no wording

English

$\operatorname{bourbakiPkg}$ is an abstract completion of $\operatorname{Q}$ defined as $\operatorname{cPkg}$.

CompareReals.compareEquivdefMathlib.Topology.UniformSpace.CompareReals, function or constant

Wording

no wording

English

$\operatorname{compareEquiv}$ is a uniform equivalence of $\mathrm{CompareReals\_\_Bourbaki\_u211d\_}$ and $\Real$ defined as $\operatorname{compareEquiv}$ applied to $\operatorname{bourbakiPkg}$ and $\mathrm{rationalCauSeqPkg}$.

rationalCauSeqPkgdefMathlib.Topology.UniformSpace.CompareReals, function or constant

Wording

no wording

English

$\mathrm{rationalCauSeqPkg}$ is an abstract completion of $\Rational$.

Mathlib.Topology.UniformSpace.Completion

CauchyFilterdefMathlib.Topology.UniformSpace.Completion, type

Wording

Cauchy filter of x (from the name)

English

Let $x$ be a set. Then a Cauchy filter of $x$ is an element of the function that maps $x$ to $\SubtypeSet {f}{\mathrm{Cauchy} (f)}$.

CauchyFilter.extenddefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{4}$ be a Cauchy filter of $x$. Then $\operatorname{extend}$ applied to $f$ and $x_{4}$ is an element of $x_{2}$.

CauchyFilter.gendefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the generator of s (from the name)

English

Let $s$ be a set relation of $x$ and $x$. Then the generator of $s$ is a set relation of the set of Cauchy filters of $x$ and the set of Cauchy filters of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\MembershipmemMACRoT {\operatorname{sprod} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p})}{s}$.

CauchyFilter.pureCauchydefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{pureCauchy}$ applied to $a$ is a Cauchy filter of $x$ defined as $\operatorname{pure}$ applied to $a$.

UniformSpace.CompletiondefMathlib.Topology.UniformSpace.Completion, type

Wording

completion of x (from the name)

English

Let $x$ be a set. Then a completion of $x$ is an element of the function that maps $x$ to the set of separation quotients of the set of Cauchy filters of $x$.

UniformSpace.Completion.UniformCompletion.completeEquivSelfdefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the complete equivalence self (from the name)

English

The complete equivalence self is a uniform equivalence of the set of completions of $x$ and $x$ defined as $\operatorname{compareEquiv}$ applied to $\operatorname{cPkg}$ and the abstract completion.

UniformSpace.Completion.cPkgdefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

no wording

English

$\operatorname{cPkg}$ is an abstract completion of $x$.

UniformSpace.Completion.coe'defMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the coercion of x2 (from the name)

English

Let $x_{2}$ be an element of $x$. Then the coercion of $x_{2}$ is a completion of $x$ defined as $\operatorname{comp}$ applied to $\operatorname{mk}$, $\operatorname{pureCauchy}$ and $x_{2}$.

UniformSpace.Completion.completionSeparationQuotientEquivdefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the isomorphism between the completion of x (from the docstring)

English

Let $x$ be a set. Then the isomorphism between the completion of $x$ is an equivalence from the set of completions of the set of separation quotients of $x$ to the set of completions of $x$.

UniformSpace.Completion.extensiondefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the extension of f and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{4}$ be a completion of $x$. Then the extension of $f$ and $x_{4}$ is an element of $x_{2}$ defined as $\operatorname{extend}$ applied to $\operatorname{cPkg}$, $f$ and $x_{4}$.

UniformSpace.Completion.extension₂defMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the extension of x6 and x7 (from the name)

English

Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{4}$. Let $x_{6}$ be a completion of $x$. Let $x_{7}$ be a completion of $x_{2}$. Then the extension of $x_{6}$ and $x_{7}$ is an element of $x_{4}$ defined as $\mathrm{AbstractCompletion\_\_extend\_u2082\_}$ applied to $\operatorname{cPkg}$, $\operatorname{cPkg}$, $f$, $x_{6}$ and $x_{7}$.

UniformSpace.Completion.mapdefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the map of f and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{4}$ be a completion of $x$. Then the map of $f$ and $x_{4}$ is a completion of $x_{2}$ defined as the map of $f$ and $x_{4}$.

UniformSpace.Completion.mapEquivdefMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the map equivalence of e (from the name)

English

Let $e$ be a uniform equivalence of $x$ and $x_{2}$. Then the map equivalence of $e$ is a uniform equivalence of the set of completions of $x$ and the set of completions of $x_{2}$ defined as the map equivalence of $\operatorname{cPkg}$ and $e$.

UniformSpace.Completion.map₂defMathlib.Topology.UniformSpace.Completion, function or constant

Wording

the map of x6 and x7 (from the name)

English

Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{4}$. Let $x_{6}$ be a completion of $x$. Let $x_{7}$ be a completion of $x_{2}$. Then the map of $x_{6}$ and $x_{7}$ is a completion of $x_{4}$ defined as the map of $x_{6}$ and $x_{7}$.

Mathlib.Topology.UniformSpace.Defs

IsUniformEmbeddingstructureMathlib.Topology.UniformSpace.Defs, predicate

Wording

f is a uniform embedding (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $f$ is a uniform embedding.

IsUniformInducingstructureMathlib.Topology.UniformSpace.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{IsUniformInducing}$ holds for $f$.

UniformContinuousdefMathlib.Topology.UniformSpace.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{UniformContinuous}$ holds for $f$, if $\operatorname{Tendsto}$ holds for the function that maps $x_{4}$ to $\ProdmkMACRoU {f (\ProdfstMACRoZ {x_{4}})}{f (\ProdsndMACRoAA {x_{4}})}$, the uniformity of $x$ and the uniformity of $x_{1}$.

UniformContinuousOndefMathlib.Topology.UniformSpace.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{UniformContinuousOn}$ holds for $f$ and $s$, if $\operatorname{Tendsto}$ holds for the function that maps $x_{4}$ to $\ProdmkMACRoU {f (\ProdfstMACRoZ {x_{4}})}{f (\ProdsndMACRoAA {x_{4}})}$, the minimum of the uniformity of $x$ and the principal filter of $\operatorname{sprod}$ applied to $s$ and $s$ and the uniformity of $x_{1}$.

UniformSpaceclassMathlib.Topology.UniformSpace.Defs, predicate

Wording

x is a uniform space (from the name)

English

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

UniformSpace.CorestructureMathlib.Topology.UniformSpace.Defs, type

Wording

no wording

English

Let $x$ be a set. Then the elements of $\operatorname{Core}$ applied to $x$ are a basic type.

UniformSpace.Core.mk'defMathlib.Topology.UniformSpace.Defs, function or constant

Wording

no wording

English

Let $U$ be a filter of $\mathrm{Prod}$ applied to $x$ and $x$ such that for all elements $r_{2}$ of $\wp \mathrm{Prod} (x , x)$, if $r_{2}$ is an element of $U$, then for all elements $x_{1}$ of $x$, $\ProdmkMACRoU {x_{1}}{x_{1}}$ is an element of $r_{2}$, for all elements $r_{1}$ of $\wp \mathrm{Prod} (x , x)$, if $r_{1}$ is an element of $U$, then the preimage of $\operatorname{swap}$ and $r_{1}$ is an element of $U$ and for all elements $r$ of $\wp \mathrm{Prod} (x , x)$, if $r$ is an element of $U$, then there exists an element $t$ of $\wp \mathrm{Prod} (x , x)$ such that $t$ is an element of $U$ and the composition of $t$ and $t$ is less than or equal to $r$. Then $\operatorname{mk'}$ applied to $U$, $\mathrm{refl}$, $\mathrm{symm}$ and $\mathrm{comp}$ is an element of $\operatorname{Core}$ applied to $x$.

UniformSpace.Core.mkOfBasisdefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

no wording

English

Let $B$ be a filter basis of $\mathrm{Prod}$ applied to $x$ and $x$ such that for all elements $r_{2}$ of $\wp \mathrm{Prod} (x , x)$, if $r_{2}$ is an element of $B$, then for all elements $x_{1}$ of $x$, $\MembershipmemMACRoT {r_{2}}{\ProdmkMACRoU {x_{1}}{x_{1}}}$, for all elements $r_{1}$ of $\wp \mathrm{Prod} (x , x)$, if $r_{1}$ is an element of $B$, then there exists an element $t_{1}$ of $\wp \mathrm{Prod} (x , x)$ such that $t_{1}$ is an element of $B$ and $t_{1}$ is less than or equal to the preimage of $\operatorname{swap}$ and $r_{1}$ and for all elements $r$ of $\wp \mathrm{Prod} (x , x)$, if $\MembershipmemMACRoT {B}{r}$, then there exists an element $t$ of $\wp \mathrm{Prod} (x , x)$ such that $\MembershipmemMACRoT {B}{t}$ and the composition of $t$ and $t$ is less than or equal to $r$. Then $\operatorname{mkOfBasis}$ applied to $B$, $\mathrm{refl}$, $\mathrm{symm}$ and $\mathrm{comp}$ is an element of $\operatorname{Core}$ applied to $x$.

UniformSpace.Core.uniformitydefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

the uniformity filter of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{Core}$ applied to $x$. Then the uniformity filter of $\mathrm{self}$ is a filter of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

UniformSpace.balldefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

the ball of x1 and V (from the name)

English

Let $x_{1}$ be an element of $x$. Let $V$ be an element of $\wp \mathrm{Prod} (x , x)$. Then the ball of $x_{1}$ and $V$ is an element of $\wp x$ defined as the ball of the inverse of $V$ and $x_{1}$.

UniformSpace.toCoredefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

no wording

English

Assume that $x$ is a uniform space. Then $\operatorname{toCore}$ applied to $u$ is an element of $\operatorname{Core}$ applied to $x$.

UniformSpace.uniformitydefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

the uniformity filter (from the docstring)

English

The uniformity filter is a filter of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

uniformitydefMathlib.Topology.UniformSpace.Defs, function or constant

Wording

the uniformity of x (from the docstring)

English

Let $x$ be a set. Then the uniformity of $x$ is a filter of $\mathrm{Prod}$ applied to $x$ and $x$ defined as the uniformity filter.

Mathlib.Topology.UniformSpace.DiscreteUniformity

DiscreteUniformityclassMathlib.Topology.UniformSpace.DiscreteUniformity, predicate

Wording

X is a discrete uniformity (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a discrete uniformity.

Mathlib.Topology.UniformSpace.Equicontinuity

EquicontinuousdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

F is equicontinuous (from the name)

English

Let $F$ be a function from elements of $x$ and elements of $X$ to elements of $x_{1}$. Then $F$ is equicontinuous, if for all elements $x_{3}$ of $X$, $\mathrm{EquicontinuousAt}$ holds for $F$ and $x_{3}$.

EquicontinuousAtdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x$ and elements of $X$ to elements of $x_{1}$. Let $x_{3}$ be an element of $X$. Then $\mathrm{EquicontinuousAt}$ holds for $F$ and $x_{3}$, if for all elements $U$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $U$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $x_{4}$ to the proposition that for all elements $i$ of $x$, $\ProdmkMACRoU {F (i , x_{3})}{F (i , x_{4})}$ is an element of $U$ and the neighbourhood filter of $x_{3}$.

EquicontinuousOndefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x$ and elements of $X$ to elements of $x_{1}$. Let $S$ be an element of $\wp X$. Then $\mathrm{EquicontinuousOn}$ holds for $F$ and $S$, if for all elements $x_{3}$ of $X$, if $x_{3}$ is an element of $S$, then $\mathrm{EquicontinuousWithinAt}$ holds for $F$, $S$ and $x_{3}$.

EquicontinuousWithinAtdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x$ and elements of $X$ to elements of $x_{1}$. Let $S$ be an element of $\wp X$. Let $x_{3}$ be an element of $X$. Then $\mathrm{EquicontinuousWithinAt}$ holds for $F$, $S$ and $x_{3}$, if for all elements $U$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $U$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $x_{4}$ to the proposition that for all elements $i$ of $x$, $\ProdmkMACRoU {F (i , x_{3})}{F (i , x_{4})}$ is an element of $U$ and $\mathrm{nhdsWithin}$ applied to $x_{3}$ and $S$.

Set.EquicontinuousdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

H is equicontinuous (from the name)

English

Let $H$ be an element of $\wp (\mathrm{Elem} (X)\rightarrow x)$. Then $H$ is equicontinuous, if the function that maps $x_{2}$ to $\MembershipmemMACRoT {H}{x_{2}}$ is equicontinuous.

Set.EquicontinuousAtdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $H$ be an element of $\wp (\mathrm{Elem} (X)\rightarrow x)$. Let $x_{2}$ be an element of $X$. Then $\operatorname{EquicontinuousAt}$ holds for $H$ and $x_{2}$, if $\mathrm{EquicontinuousAt}$ holds for the function that maps $x_{3}$ to $\MembershipmemMACRoT {H}{x_{3}}$ and $x_{2}$.

Set.EquicontinuousOndefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $H$ be an element of $\wp (\mathrm{Elem} (X)\rightarrow x)$. Let $S$ be an element of $\wp X$. Then $\operatorname{EquicontinuousOn}$ holds for $H$ and $S$, if $\mathrm{EquicontinuousOn}$ holds for the function that maps $x_{2}$ to $\MembershipmemMACRoT {H}{x_{2}}$ and $S$.

Set.EquicontinuousWithinAtdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $H$ be an element of $\wp (\mathrm{Elem} (X)\rightarrow x)$. Let $S$ be an element of $\wp X$. Let $x_{2}$ be an element of $X$. Then $\operatorname{EquicontinuousWithinAt}$ holds for $H$, $S$ and $x_{2}$, if $\mathrm{EquicontinuousWithinAt}$ holds for the function that maps $x_{3}$ to $\MembershipmemMACRoT {H}{x_{3}}$, $S$ and $x_{2}$.

Set.UniformEquicontinuousdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $H$ be an element of $\wp (\mathrm{Elem} (x_{1})\rightarrow x)$. Then $\operatorname{UniformEquicontinuous}$ holds for $H$, if $\mathrm{UniformEquicontinuous}$ holds for the function that maps $x_{4}$ to $\MembershipmemMACRoT {H}{x_{4}}$.

Set.UniformEquicontinuousOndefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $H$ be an element of $\wp (\mathrm{Elem} (x_{1})\rightarrow x)$. Let $S$ be an element of $\wp x_{1}$. Then $\operatorname{UniformEquicontinuousOn}$ holds for $H$ and $S$, if $\mathrm{UniformEquicontinuousOn}$ holds for the function that maps $x_{4}$ to $\MembershipmemMACRoT {H}{x_{4}}$ and $S$.

UniformEquicontinuousdefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{1}$. Then $\mathrm{UniformEquicontinuous}$ holds for $F$, if for all elements $U$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $U$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $\mathrm{xy}$ to the proposition that for all elements $i$ of $x$, $\ProdmkMACRoU {F (i , \ProdfstMACRoZ {\mathrm{xy}})}{F (i , \ProdsndMACRoAA {\mathrm{xy}})}$ is an element of $U$ and the uniformity of $x_{2}$.

UniformEquicontinuousOndefMathlib.Topology.UniformSpace.Equicontinuity, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $x_{1}$. Let $S$ be an element of $\wp x_{2}$. Then $\mathrm{UniformEquicontinuousOn}$ holds for $F$ and $S$, if for all elements $U$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $U$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $\mathrm{xy}$ to the proposition that for all elements $i$ of $x$, $\ProdmkMACRoU {F (i , \ProdfstMACRoZ {\mathrm{xy}})}{F (i , \ProdsndMACRoAA {\mathrm{xy}})}$ is an element of $U$ and the minimum of the uniformity of $x_{2}$ and the principal filter of $\operatorname{sprod}$ applied to $S$ and $S$.

Mathlib.Topology.UniformSpace.Equiv

AddOpposite.opUniformEquivdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the opposite uniform equivalence (from the name)

English

The opposite uniform equivalence is a uniform equivalence of $x$ and the set of additive opposites of $x$ defined as $\operatorname{mk}$ applied to the opposite equivalence, $\mathrm{AddOpposite\_\_uniformContinuous\_op}$ and $\mathrm{AddOpposite\_\_uniformContinuous\_unop}$.

Equiv.toUniformEquivOfIsUniformInducingdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the uniform equivalence of f and hf (from the name)

English

Let $f$ be an equivalence from $x$ to $x_{1}$ such that $\mathrm{IsUniformInducing}$ holds for $\operatorname{coe}$ applied to $f$. Then the uniform equivalence of $f$ and $\mathrm{hf}$ is a uniform equivalence of $x$ and $x_{1}$.

MulOpposite.opUniformEquivdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the opposite uniform equivalence (from the name)

English

The opposite uniform equivalence is a uniform equivalence of $x$ and the set of multiplicative opposites of $x$ defined as $\operatorname{mk}$ applied to the opposite equivalence, $\mathrm{MulOpposite\_\_uniformContinuous\_op}$ and $\mathrm{MulOpposite\_\_uniformContinuous\_unop}$.

UniformEquivstructureMathlib.Topology.UniformSpace.Equiv, type

Wording

uniform equivalence of x and x1 (from the name)

English

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

UniformEquiv.changeInvdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the change inverse of f and g (from the name)

English

Let $f$ be a uniform equivalence of $x$ and $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the change inverse of $f$ and $g$ is a uniform equivalence of $x$ and $x_{1}$.

UniformEquiv.finTwoArrowdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{finTwoArrow}$ applied to $x$ is a uniform equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $x$ and $\mathrm{Prod}$ applied to $x$ and $x$.

UniformEquiv.funUniquedefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $x_{1}$ is a uniform equivalence of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{1}$.

UniformEquiv.imagedefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the image of e and s (from the name)

English

Let $e$ be a uniform equivalence of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then the image of $e$ and $s$ is a uniform equivalence of the set of elements of $s$ and the set of elements of the image of $\operatorname{coe}$ applied to $e$ and $s$.

UniformEquiv.ofIsUniformEmbeddingdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the uniform equivalence of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is a uniform embedding. Then the uniform equivalence of $f$ and $\mathrm{hf}$ is a uniform equivalence of $x$ and the set of elements of the range of $f$.

UniformEquiv.piCongrdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the product congruence of e and F (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Let $F$ be a function from elements $x_{8}$ of $x$ to uniform equivalences of $x_{2}$ applied to $x_{8}$ and $x_{3}$ applied to $e$ applied to $x_{8}$. Then the product congruence of $e$ and $x_{8}$ is a uniform equivalence of the set of functions from elements $x_{6}$ of $x$ to elements of $x_{2}$ applied to $x_{6}$ and the set of functions from elements $x_{7}$ of $x_{1}$ to elements of $x_{3}$ applied to $x_{7}$ defined as the function that maps $F$ to the composition of the right product congruence of $x_{8}$ and the left product congruence of $e$.

UniformEquiv.piCongrLeftdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the left product congruence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $e$ is a uniform equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{2}$ applied to $e$ applied to $i$ and the set of functions from elements $j$ of $x_{1}$ to elements of $x_{2}$ applied to $j$.

UniformEquiv.piCongrRightdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the right product congruence of F (from the name)

English

Let $F$ be a function from elements $i_{2}$ of $x$ to uniform equivalences of $x_{1}$ applied to $i_{2}$ and $x_{2}$ applied to $i_{2}$. Then the right product congruence of $i_{2}$ is a uniform equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$.

UniformEquiv.piFinTwodefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

no wording

English

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

UniformEquiv.prodAssocdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

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

English

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

UniformEquiv.prodCommdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{prodComm}$ applied to $x$ and $x_{1}$ is a uniform equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$.

UniformEquiv.prodCongrdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the product congruence of x8 and x9 (from the name)

English

Let $x_{8}$ be a uniform equivalence of $x$ and $x_{1}$. Let $x_{9}$ be a uniform equivalence of $x_{2}$ and $x_{3}$. Then the product congruence of $x_{8}$ and $x_{9}$ is a uniform equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.

UniformEquiv.prodPUnitdefMathlib.Topology.UniformSpace.Equiv, 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 uniform equivalence of $\mathrm{Prod}$ applied to $x$ and $\mathrm{PUnit}$ and $x$.

UniformEquiv.punitProddefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

no wording

English

Let $x$ be a set. Then $\operatorname{punitProd}$ applied to $x$ is a uniform equivalence 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$.

UniformEquiv.refldefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a uniform equivalence of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity of $x$, $\mathrm{uniformContinuous\_id}$ and $\mathrm{uniformContinuous\_id}$.

UniformEquiv.setCongrdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the set congruence of h (from the name)

English

Assume that $\EqtMACRoH {s}{t}$. Then the set congruence of $h$ is a uniform equivalence of the set of elements of $s$ and the set of elements of $t$.

UniformEquiv.subtypedefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the subtype of e and h (from the name)

English

Let $e$ be a uniform equivalence of $x$ and $x_{1}$ such that for all elements $a_{1}$ of $x$, $p$ holds for $a_{1}$, if and only if $q$ holds for $e$ applied to $a_{1}$. Then the subtype of $e$ and $h$ is a uniform equivalence of $\SubtypeSet {a}{p (a)}$ and $\SubtypeSet {b}{q (b)}$.

UniformEquiv.symmdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the inverse of h (from the name)

English

Let $h$ be a uniform equivalence of $x$ and $x_{1}$. Then the inverse of $h$ is a uniform equivalence of $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toEquiv}$ applied to $h$, $\mathrm{UniformEquiv\_\_uniformContinuous\_invFun}$ applied to $h$ and $\mathrm{UniformEquiv\_\_uniformContinuous\_toFun}$ applied to $h$.

UniformEquiv.toHomeomorphdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be a uniform equivalence of $x$ and $x_{1}$. Then the homeomorphism of $e$ is a homeomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $e$, $\operatorname{continuous}$ applied to $e$ and $\mathrm{UniformEquiv\_\_continuous\_symm}$ applied to $e$.

UniformEquiv.transdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the composition of x6 and x7 (from the name)

English

Let $x_{6}$ be a uniform equivalence of $x$ and $x_{1}$. Let $x_{7}$ be a uniform equivalence of $x_{1}$ and $x_{2}$. Then the composition of $x_{6}$ and $x_{7}$ is a uniform equivalence of $x$ and $x_{2}$.

UniformEquiv.uliftdefMathlib.Topology.UniformSpace.Equiv, function or constant

Wording

the lift of x (from the name)

English

Let $x$ be a set. Then the lift of $x$ is a uniform equivalence of $\mathrm{ULift}$ applied to $x$ and $x$.

Mathlib.Topology.UniformSpace.LocallyUniformConvergence

TendstoLocallyUniformlydefMathlib.Topology.UniformSpace.LocallyUniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Then $\mathrm{TendstoLocallyUniformly}$ holds for $F$, $f$ and $p$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then for all elements $x_{5}$ of $x$, there exists an element $t$ of $\wp x$, such that $t$ is an element of the neighbourhood filter of $x_{5}$ and $\operatorname{Eventually}$ holds for the function that maps $n$ to the proposition that for all elements $y$ of $x$, if $y$ is an element of $t$, then $\ProdmkMACRoU {f (y)}{F (n , y)}$ is an element of $u$ and $p$.

TendstoLocallyUniformlyOndefMathlib.Topology.UniformSpace.LocallyUniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{TendstoLocallyUniformlyOn}$ holds for $F$, $f$, $p$ and $s$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then for all elements $x_{5}$ of $x$, if $x_{5}$ is an element of $s$, then there exists an element $t$ of $\wp x$, such that $\MembershipmemMACRoT {\mathrm{nhdsWithin} (x_{5} , s)}{t}$ and $\operatorname{Eventually}$ holds for the function that maps $n$ to the proposition that for all elements $y$ of $x$, if $y$ is an element of $t$, then $\ProdmkMACRoU {f (y)}{F (n , y)}$ is an element of $u$ and $p$.

Mathlib.Topology.UniformSpace.ProdApproximation

ContinuousMap.prodMuldefMathlib.Topology.UniformSpace.ProdApproximation, function or constant

Wording

the product product (from the name)

English

The product product is a linear map of the set of continuous maps of $X$ and $R$ and the set of linear maps of the set of continuous maps of $Y$ and $R$ and the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$.

ContinuousMap.tensorHomdefMathlib.Topology.UniformSpace.ProdApproximation, function or constant

Wording

the tensor homomorphism (from the name)

English

The tensor homomorphism is a linear map of the set of tensor products of the set of continuous maps of $X$ and $R$ and the set of continuous maps of $Y$ and $R$ and the set of continuous maps of $\mathrm{Prod}$ applied to $X$ and $Y$ and $R$ defined as the lift of the product product.

Mathlib.Topology.UniformSpace.Real

ContinuousMap.coeNNRealRealdefMathlib.Topology.UniformSpace.Real, function or constant

Wording

no wording

English

$\operatorname{coeNNRealReal}$ is a continuous map of $\mathrm{NNReal}$ and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{toReal}$ and $\mathrm{NNReal\_\_continuous\_coe}$.

Mathlib.Topology.UniformSpace.Separation

SeparationQuotient.lift'defMathlib.Topology.UniformSpace.Separation, function or constant

Wording

the lift of f and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a separation quotient of $x$. Then the lift of $f$ and $x_{4}$ is an element of $x_{1}$.

SeparationQuotient.mapdefMathlib.Topology.UniformSpace.Separation, function or constant

Wording

the map of f and x4 (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a separation quotient of $x$. Then the map of $f$ and $x_{4}$ is a separation quotient of $x_{1}$ defined as the lift of $\operatorname{comp}$ applied to $\operatorname{mk}$ and $f$ and $x_{4}$.

Mathlib.Topology.UniformSpace.Ultra.Basic

IsUltraUniformityclassMathlib.Topology.UniformSpace.Ultra.Basic, predicate

Wording

X is ultrametric (from the docstring)

English

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

Mathlib.Topology.UniformSpace.UniformConvergence

TendstoUniformlydefMathlib.Topology.UniformSpace.UniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Then $\mathrm{TendstoUniformly}$ holds for $F$, $f$ and $p$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $n$ to the proposition that for all elements $x_{4}$ of $x$, $\ProdmkMACRoU {f (x_{4})}{F (n , x_{4})}$ is an element of $u$ and $p$.

TendstoUniformlyOndefMathlib.Topology.UniformSpace.UniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{TendstoUniformlyOn}$ holds for $F$, $f$, $p$ and $s$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $n$ to the proposition that for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $s$, then $\ProdmkMACRoU {f (x_{4})}{F (n , x_{4})}$ is an element of $u$ and $p$.

TendstoUniformlyOnFilterdefMathlib.Topology.UniformSpace.UniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Let $\mathrm{p'}$ be a filter of $x$. Then $\mathrm{TendstoUniformlyOnFilter}$ holds for $F$, $f$, $p$ and $\mathrm{p'}$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $n$ to $\MembershipmemMACRoT {u}{(\ProdmkMACRoU {f (\ProdsndMACRoAA {n})}{F (\ProdfstMACRoZ {n}, \ProdsndMACRoAA {n})})}$ and $\operatorname{sprod}$ applied to $p$ and $\mathrm{p'}$.

UniformCauchySeqOndefMathlib.Topology.UniformSpace.UniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{UniformCauchySeqOn}$ holds for $F$, $p$ and $s$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $m$ to the proposition that for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $s$, then $\ProdmkMACRoU {F (\ProdfstMACRoZ {m}, x_{4})}{F (\ProdsndMACRoAA {m}, x_{4})}$ is an element of $u$ and $\operatorname{sprod}$ applied to $p$ and $p$.

UniformCauchySeqOnFilterdefMathlib.Topology.UniformSpace.UniformConvergence, predicate

Wording

no wording

English

Let $F$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $p$ be a filter of $x_{2}$. Let $\mathrm{p'}$ be a filter of $x$. Then $\mathrm{UniformCauchySeqOnFilter}$ holds for $F$, $p$ and $\mathrm{p'}$, if for all elements $u$ of $\wp \mathrm{Prod} (x_{1} , x_{1})$, if $u$ is an element of the uniformity of $x_{1}$, then $\operatorname{Eventually}$ holds for the function that maps $m$ to $\MembershipmemMACRoT {u}{(\ProdmkMACRoU {F (\ProdfstMACRoZ {\ProdfstMACRoZ {m}}, \ProdsndMACRoAA {m})}{F (\ProdsndMACRoAA {\ProdfstMACRoZ {m}}, \ProdsndMACRoAA {m})})}$ and $\operatorname{sprod}$ applied to $\operatorname{sprod}$ applied to $p$ and $p$ and $\mathrm{p'}$.

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

UniformFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, type

Wording

uniform function of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then a uniform function of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of functions from elements of $x$ to elements of $x_{1}$.

UniformFun.basisdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the basis of x2 (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be a filter of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{1}$. Then the basis of $x_{2}$ is a filter basis of $\mathrm{Prod}$ applied to the set of uniform functions of $x$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{1}$ defined as the filter basis of $\mathrm{UniformFun\_\_isBasis\_gen}$ applied to $x$, $x_{1}$ and $x_{2}$.

UniformFun.congrLeftdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the left congruence of e (from the name)

English

Let $e$ be an equivalence from $x_{2}$ to $x$. Then the left congruence of $e$ is a uniform equivalence of the set of uniform functions of $x_{2}$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{1}$.

UniformFun.congrRightdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the right congruence of e (from the name)

English

Let $e$ be a uniform equivalence of $x_{2}$ and $x_{1}$. Then the right congruence of $e$ is a uniform equivalence of the set of uniform functions of $x$ and $x_{2}$ and the set of uniform functions of $x$ and $x_{1}$.

UniformFun.filterdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the filter of x2 (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be a filter of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{1}$. Then the filter of $x_{2}$ is a filter of $\mathrm{Prod}$ applied to the set of uniform functions of $x$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{1}$ defined as the filter of the basis of $x_{2}$.

UniformFun.gendefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the generator of V (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $V$ be an element of $\wp \mathrm{Prod} (x_{1} , x_{1})$. Then the generator of $V$ is an element of the power set of $\mathrm{Prod}$ applied to the set of uniform functions of $x$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{uv}$ to the proposition that for all elements $x_{2}$ of $x$, $\ProdmkMACRoU {\operatorname{toFun} (\ProdfstMACRoZ {\mathrm{uv}}, x_{2})}{\operatorname{toFun} (\ProdsndMACRoAA {\mathrm{uv}}, x_{2})}$ is an element of $V$.

UniformFun.ofFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the uniform function (from the name)

English

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

UniformFun.phidefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Let $\mathrm{uvx}$ be an element of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to the set of uniform functions of $x$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{1}$ and $x$. Then $\operatorname{phi}$ applied to $x$, $x_{1}$ and $\mathrm{uvx}$ is an element of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{1}$ defined as $\ProdmkMACRoU {\ProdfstMACRoZ {\ProdfstMACRoZ {\mathrm{uvx}}}}{\ProdsndMACRoAA {\ProdfstMACRoZ {\mathrm{uvx}}}}$.

UniformFun.toFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the uniform function (from the name)

English

The uniform function is an equivalence from the set of uniform functions of $x$ and $x_{1}$ to the set of functions from elements of $x$ to elements of $x_{1}$ defined as the inverse of the uniform function.

UniformFun.uniformCoredefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{uniformCore}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{Core}$ applied to the set of uniform functions of $x$ and $x_{1}$.

UniformFun.uniformEquivPiCommdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x$ be a set. Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Then $\operatorname{uniformEquivPiComm}$ applied to $x$ and $x_{2}$ is a uniform equivalence of the set of uniform functions of $x$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ to uniform functions of $x$ and $x_{2}$ applied to $i_{1}$.

UniformFun.uniformEquivProdArrowdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the uniform equivalence product arrow (from the name)

English

The uniform equivalence product arrow is a uniform equivalence of the set of uniform functions of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to the set of uniform functions of $x$ and $x_{1}$ and the set of uniform functions of $x$ and $x_{2}$.

UniformOnFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, type

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be an element of $\wp (\wp x)$. Then an element of $\mathrm{UniformOnFun}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of the function that maps $x$, $x_{1}$ and $x_{2}$ to the set of functions from elements of $x$ to elements of $x_{1}$.

UniformOnFun.congrLeftdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the left congruence of e (from the name)

English

Let $e$ be an equivalence from $x_{2}$ to $x$ such that $x_{5}$ is less than or equal to the preimage of $\operatorname{image}$ applied to $\operatorname{coe}$ applied to $e$ and $x_{4}$ and $x_{4}$ is less than or equal to the preimage of $\operatorname{preimage}$ applied to $\operatorname{coe}$ applied to $e$ and $x_{5}$. Then the left congruence of $e$ is a uniform equivalence of $\mathrm{UniformOnFun}$ applied to $x_{2}$, $x_{1}$ and $x_{5}$ and $\mathrm{UniformOnFun}$ applied to $x$, $x_{1}$ and $x_{4}$.

UniformOnFun.congrRightdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the right congruence of e (from the name)

English

Let $e$ be a uniform equivalence of $x_{2}$ and $x_{1}$. Then the right congruence of $e$ is a uniform equivalence of $\mathrm{UniformOnFun}$ applied to $x$, $x_{2}$ and $x_{4}$ and $\mathrm{UniformOnFun}$ applied to $x$, $x_{1}$ and $x_{4}$.

UniformOnFun.gendefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the generator of S and V (from the name)

English

Let $x_{2}$ be an element of $\wp (\wp x)$. Let $S$ be an element of $\wp x$. Let $V$ be an element of $\wp \mathrm{Prod} (x_{1} , x_{1})$. Then the generator of $S$ and $V$ is an element of $\wp \mathrm{Prod} (\mathrm{UniformOnFun} (x , x_{1} , x_{2}), \mathrm{UniformOnFun} (x , x_{1} , x_{2}))$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{uv}$ to the proposition that for all elements $x_{3}$ of $x$, if $x_{3}$ is an element of $S$, then $\ProdmkMACRoU {\operatorname{toFun} (x_{2} , \ProdfstMACRoZ {\mathrm{uv}}, x_{3})}{\operatorname{toFun} (x_{2} , \ProdsndMACRoAA {\mathrm{uv}}, x_{3})}$ is an element of $V$.

UniformOnFun.ofFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\wp (\wp x)$. Then $\operatorname{ofFun}$ applied to $x_{2}$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow x_{1})}{\mathrm{UniformOnFun} (x , x_{1} , x_{2})}$.

UniformOnFun.toFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\wp (\wp x)$. Then $\operatorname{toFun}$ applied to $x_{2}$ is an element of $\EquivMACRoAE {\mathrm{UniformOnFun} (x , x_{1} , x_{2})}{(\mathrm{Elem} (x)\rightarrow x_{1})}$ defined as the inverse of $\operatorname{ofFun}$ applied to $x_{2}$.

UniformOnFun.uniformEquivPiCommdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $\wp (\wp x)$. Let $x_{3}$ be a function from elements of $x_{1}$ to sets. Then $\operatorname{uniformEquivPiComm}$ applied to $x_{2}$ and $x_{3}$ is a uniform equivalence of $\mathrm{UniformOnFun}$ applied to $x$, the set of functions from elements $i$ of $x_{1}$ to elements of $x_{3}$ applied to $i$ and $x_{2}$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $\mathrm{UniformOnFun}$ applied to $x$, $x_{3}$ applied to $i_{1}$ and $x_{2}$.

UniformOnFun.uniformEquivProdArrowdefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the uniform equivalence product arrow (from the name)

English

The uniform equivalence product arrow is a uniform equivalence of $\mathrm{UniformOnFun}$ applied to $x$, $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{4}$ and $\mathrm{Prod}$ applied to $\mathrm{UniformOnFun}$ applied to $x$, $x_{1}$ and $x_{4}$ and $\mathrm{UniformOnFun}$ applied to $x$, $x_{2}$ and $x_{4}$.

UniformOnFun.uniformEquivUniformFundefMathlib.Topology.UniformSpace.UniformConvergenceTopology, function or constant

Wording

the uniform equivalence uniform function of x3 (from the name)

English

Let $x_{1}$ be a set. Let $x_{3}$ be an element of $\wp (\wp x)$ such that the universal set is an element of $x_{3}$. Then the uniform equivalence uniform function of $x_{3}$ is a uniform equivalence of $\mathrm{UniformOnFun}$ applied to $x$, $x_{1}$ and $x_{3}$ and the set of uniform functions of $x$ and $x_{1}$.

Mathlib.Topology.UnitInterval

Set.Icc.addNSMuldefMathlib.Topology.UnitInterval, function or constant

Wording

no wording

English

Assume that $a \leq b$. Let $x_{3}$ be an element of $x$. Let $n$ be a natural number. Then $\operatorname{addNSMul}$ applied to $h$, $x_{3}$ and $n$ is an element of $\SetIccMACRoP {a}{b}$ defined as the projection closed interval of $b$ and $a + \HSMulhSMulMACRoAL {n}{x_{3}}$.

Set.Icc.convexCombdefMathlib.Topology.UnitInterval, function or constant

Wording

the convex comb of y and t (from the name)

English

Let $x$ and $y$ be elements of $\SetIccMACRoP {a}{b}$. Let $t$ be an element of the unit interval. Then the convex comb of $y$ and $t$ is an element of $\SetIccMACRoP {a}{b}$ defined as $(1 - t)\times x + t \times y$.

Set.Icc.convexComb_assoc_coeff₁defMathlib.Topology.UnitInterval, function or constant

Wording

the convex comb associator coefficient of s and t (from the name)

English

Let $s$ and $t$ be elements of the unit interval. Then the convex comb associator coefficient of $s$ and $t$ is an element of the unit interval defined as $\frac{ s \times (1 - t)}{1 - s \times t}$.

Set.Icc.convexComb_assoc_coeff₁'defMathlib.Topology.UnitInterval, function or constant

Wording

the convex comb associator coefficient of s and t (from the name)

English

Let $s$ and $t$ be elements of the unit interval. Then the convex comb associator coefficient of $s$ and $t$ is an element of the unit interval defined as the inverse of the convex comb associator coefficient of the inverse of $t$ and the inverse of $s$.

Set.Icc.convexComb_assoc_coeff₂defMathlib.Topology.UnitInterval, function or constant

Wording

the convex comb associator coefficient of s and t (from the name)

English

Let $s$ and $t$ be elements of the unit interval. Then the convex comb associator coefficient of $s$ and $t$ is an element of the unit interval defined as $s \times t$.

Set.Icc.convexComb_assoc_coeff₂'defMathlib.Topology.UnitInterval, function or constant

Wording

the convex comb associator coefficient of s and t (from the name)

English

iccHomeoIdefMathlib.Topology.UnitInterval, function or constant

Wording

the closed interval homeomorphism of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$ such that $a < b$. Then the closed interval homeomorphism of $a$ and $b$ is a homeomorphism of the set of elements of $\SetIccMACRoP {a}{b}$ and the set of elements of $\SetIccMACRoP {0}{1}$.

unitIntervaldefMathlib.Topology.UnitInterval, function or constant

Wording

the unit interval (from the docstring)

English

The unit interval is an element of $\wp \Real$ defined as $\SetIccMACRoP {0}{1}$.

unitInterval.submonoiddefMathlib.Topology.UnitInterval, function or constant

Wording

the submonoid (from the name)

English

The submonoid is a submonoid of $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the unit interval and the function that maps $x$ and $x_{1}$ to $\mathrm{unitInterval\_\_mul\_mem}$ and $\mathrm{unitInterval\_\_one\_mem}$.

unitInterval.symmdefMathlib.Topology.UnitInterval, function or constant

Wording

the inverse of x (from the name)

English

Let $x$ be an element of the unit interval. Then the inverse of $x$ is an element of the unit interval defined as $1 - x$.

unitInterval.symmHomeomorphdefMathlib.Topology.UnitInterval, function or constant

Wording

the inverse homeomorphism (from the name)

English

The inverse homeomorphism is a homeomorphism of the set of elements of the unit interval and the set of elements of the unit interval.

unitInterval.toNNRealdefMathlib.Topology.UnitInterval, function or constant

Wording

no wording

English

Let $x$ be an element of the unit interval. Then $\operatorname{toNNReal}$ applied to $x$ is an element of $\mathrm{NNReal}$ defined as $x$.

Mathlib.Topology.UrysohnsLemma

Urysohns.CU.CdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{CU}$ applied to $P$. Then $\operatorname{C}$ applied to $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Urysohns.CU.UdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{CU}$ applied to $P$. Then $\operatorname{U}$ applied to $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Urysohns.CU.approxdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

no wording

English

Let $x_{1}$ be a natural number. Let $x_{2}$ be an element of $\operatorname{CU}$ applied to $P$. Let $x_{3}$ be an element of $X$. Then $\operatorname{approx}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a real number defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Urysohns\_\_CU\_\_approx\_\_\_f}$, $x_{2}$ and $x_{3}$.

Urysohns.CU.leftdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

the left of c (from the name)

English

Let $c$ be an element of $\operatorname{CU}$ applied to $P$. Then the left of $c$ is an element of $\operatorname{CU}$ applied to $P$.

Urysohns.CU.limdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

the limit of c and x1 (from the name)

English

Let $c$ be an element of $\operatorname{CU}$ applied to $P$. Let $x_{1}$ be an element of $X$. Then the limit of $c$ and $x_{1}$ is a real number defined as the supremum of the function that maps $n$ to $\operatorname{approx}$ applied to $n$, $c$ and $x_{1}$.

Urysohns.CU.rightdefMathlib.Topology.UrysohnsLemma, function or constant

Wording

the right of c (from the name)

English

Let $c$ be an element of $\operatorname{CU}$ applied to $P$. Then the right of $c$ is an element of $\operatorname{CU}$ applied to $P$.

Mathlib.Topology.VectorBundle.Basic

Bundle.Pretrivialization.IsLinearclassMathlib.Topology.VectorBundle.Basic, predicate

Wording

e is linear (from the name)

English

Let $R$ be a set. Let $e$ be a pretrivialization of $F$ and $\operatorname{proj}$. Then we can say that $e$ is linear.

Bundle.Pretrivialization.linearEquivAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a pretrivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$ such that $b$ is an element of the base set of $e$. Then $\operatorname{linearEquivAt}$ applied to $R$, $e$, $b$ and $\mathrm{hb}$ is a linear equivalence of $E$ applied to $b$ and $F$.

Bundle.Pretrivialization.linearMapAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a pretrivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then $\operatorname{linearMapAt}$ applied to $R$, $e$ and $b$ is a linear map of $E$ applied to $b$ and $F$ defined as $\mathrm{dite}$ applied to the proposition that $b$ is an element of the base set of $e$, the function that maps $\mathrm{hb}$ to $\operatorname{toLinearMap}$ applied to $\operatorname{linearEquivAt}$ applied to $R$, $e$, $b$ and $\mathrm{hb}$ and the function that maps $\mathrm{hb1}$ to $0$.

Bundle.Pretrivialization.symmₗdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the inverse of e and b (from the name)

English

Let $R$ be a set. Let $e$ be a pretrivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the inverse of $e$ and $b$ is a linear map of $F$ and $E$ applied to $b$.

Bundle.Trivialization.IsLinearclassMathlib.Topology.VectorBundle.Basic, predicate

Wording

e is linear (from the name)

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Then we can say that $e$ is linear.

Bundle.Trivialization.continuousLinearEquivAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$ such that $b$ is an element of the base set of $e$. Then $\operatorname{continuousLinearEquivAt}$ applied to $R$, $e$, $b$ and $\mathrm{hb}$ is a continuous linear equivalence of $E$ applied to $b$ and $F$.

Bundle.Trivialization.continuousLinearMapAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then $\operatorname{continuousLinearMapAt}$ applied to $R$, $e$ and $b$ is a continuous linear map of $E$ applied to $b$ and $F$.

Bundle.Trivialization.coordChangeLdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the coordinate change of b and #4 (from the name)

English

Let $R$ be a set. Let $e$ and $\mathrm{e'}$ be trivializations of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the coordinate change of $\mathrm{e'}$ and $b$ is a continuous linear equivalence of $F$ and $F$.

Bundle.Trivialization.linearEquivAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$ such that $b$ is an element of the base set of $e$. Then $\operatorname{linearEquivAt}$ applied to $R$, $e$, $b$ and $\mathrm{hb}$ is a linear equivalence of $E$ applied to $b$ and $F$ defined as $\operatorname{linearEquivAt}$ applied to $R$, the pretrivialization of $e$, $b$ and $\mathrm{hb}$.

Bundle.Trivialization.linearMapAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then $\operatorname{linearMapAt}$ applied to $R$, $e$ and $b$ is a linear map of $E$ applied to $b$ and $F$ defined as $\operatorname{linearMapAt}$ applied to $R$, the pretrivialization of $e$ and $b$.

Bundle.Trivialization.symmLdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the inverse of e and b (from the name)

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the inverse of $e$ and $b$ is a continuous linear map of $F$ and $E$ applied to $b$.

Bundle.Trivialization.symmₗdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the inverse of e and b (from the name)

English

Let $R$ be a set. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the inverse of $e$ and $b$ is a linear map of $F$ and $E$ applied to $b$ defined as the inverse of the pretrivialization of $e$ and $b$.

Bundle.zeroSectiondefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the zero section of E and x1 (from the name)

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Let $x_{1}$ be an element of $B$. Then the zero section of $E$ and $x_{1}$ is a total space of $F$ and $E$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $0$.

ContinuousLinearMap.inCoordinatesdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $F$ and $\mathrm{F'}$ be sets. Let $E$ be a function from elements of $B$ to sets. Let $\mathrm{E'}$ be a function from elements of $\mathrm{B'}$ to sets. Let $x_{21}$ and $x_{22}$ be elements of $B$. Let $x_{23}$ and $y$ be elements of $\mathrm{B'}$. Let $x_{24}$ be a continuous linear map of $E$ applied to $x_{22}$ and $\mathrm{E'}$ applied to $y$. Then $\operatorname{inCoordinates}$ applied to $F$, $E$, $\mathrm{F'}$, $\mathrm{E'}$, $x_{21}$, $x_{22}$, $x_{23}$, $y$ and $x_{24}$ is a continuous linear map of $F$ and $\mathrm{F'}$ defined as the composition of $\operatorname{continuousLinearMapAt}$ applied to $x_{5}$, $\operatorname{trivializationAt}$ applied to $\mathrm{F'}$, $\mathrm{E'}$ and $x_{23}$ and $y$ and the composition of $x_{24}$ and the inverse of $\operatorname{trivializationAt}$ applied to $F$, $E$ and $x_{21}$ and $x_{22}$.

VectorBundleclassMathlib.Topology.VectorBundle.Basic, predicate

Wording

E is a vector bundle (from the name)

English

Let $R$ and $F$ be sets. Let $E$ be a function from elements of $B$ to sets. Then we can say that $E$ is a vector bundle.

VectorBundle.continuousLinearEquivAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $R$ and $F$ be sets. Let $E$ be a function from elements of $B$ to sets. Let $b$ be an element of $B$. Then $\operatorname{continuousLinearEquivAt}$ applied to $R$, $F$, $E$ and $b$ is a continuous linear equivalence of $E$ applied to $b$ and $F$.

VectorBundleCorestructureMathlib.Topology.VectorBundle.Basic, type

Wording

vector bundle of F and x4 (from the name)

English

Let $R$, $B$, $F$ and $x_{4}$ be sets. Then the vector bundles of $F$ and $x_{4}$ are a basic type.

VectorBundleCore.BasedefMathlib.Topology.VectorBundle.Basic, type

Wording

base space (from the docstring)

English

A base space is an element of $B$.

VectorBundleCore.FiberdefMathlib.Topology.VectorBundle.Basic, type

Wording

fiber of Z and x5 (from the name)

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Let $x_{5}$ be an element of $B$. Then a fiber of $Z$ and $x_{5}$ is an element of the function that maps $Z$ and $x_{5}$ to the set of fibers of the fiber bundle of $Z$ and $x_{5}$.

VectorBundleCore.IndexdefMathlib.Topology.VectorBundle.Basic, type

Wording

index set (from the docstring)

English

An index set is an element of $x$.

VectorBundleCore.TotalSpacedefMathlib.Topology.VectorBundle.Basic, type

Wording

total space of Z (from the name)

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Then a total space of $Z$ is an element of the function that maps $Z$ to the set of total spaces of $F$ and the set of elements of $\operatorname{Fiber}$ applied to $Z$.

VectorBundleCore.baseSetdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the base set of self and x5 (from the name)

English

Let $\mathrm{self}$ be a vector bundle of $F$ and $x_{4}$. Let $x_{5}$ be an element of $x_{4}$. Then the base set of $\mathrm{self}$ and $x_{5}$ is an element of $\wp B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.

VectorBundleCore.coordChangedefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the coordinate change of x6 and x7 (from the name)

English

Let $\mathrm{self}$ be a vector bundle of $F$ and $x_{4}$. Let $x_{5}$ and $x_{6}$ be elements of $x_{4}$. Let $x_{7}$ be an element of $B$. Then the coordinate change of $x_{6}$ and $x_{7}$ is a continuous linear map of $F$ and $F$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $x_{5}$, $x_{6}$ and $x_{7}$.

VectorBundleCore.indexAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a vector bundle of $F$ and $x_{4}$. Let $x_{5}$ be an element of $B$. Then $\operatorname{indexAt}$ applied to $\mathrm{self}$ and $x_{5}$ is an element of $x_{4}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{5}$.

VectorBundleCore.localTrivdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Let $i$ be an element of $x_{4}$. Then $\operatorname{localTriv}$ applied to $Z$ and $i$ is a trivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{localTriv}$ applied to the fiber bundle of $Z$ and $i$.

VectorBundleCore.localTrivAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Let $b$ be an element of $B$. Then $\operatorname{localTrivAt}$ applied to $Z$ and $b$ is a trivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{localTriv}$ applied to $Z$ and $\operatorname{indexAt}$ applied to $Z$ and $b$.

VectorBundleCore.projdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the projection from the total space of Z and x5 (from the docstring)

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Let $x_{5}$ be a total space of $F$ and the set of elements of $\operatorname{Fiber}$ applied to $Z$. Then the projection from the total space of $Z$ and $x_{5}$ is an element of $B$ defined as the projection of $x_{5}$.

VectorBundleCore.toFiberBundleCoredefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the fiber bundle of Z (from the name)

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Then the fiber bundle of $Z$ is a fiber bundle of $B$ and $F$.

VectorBundleCore.trivChangedefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the trivial change of i and j (from the name)

English

Let $Z$ be a vector bundle of $F$ and $x_{4}$. Let $i$ and $j$ be elements of $x_{4}$. Then the trivial change of $i$ and $j$ is an open partial homeomorphism of $\mathrm{Prod}$ applied to $B$ and $F$ and $\mathrm{Prod}$ applied to $B$ and $F$ defined as the trivial change of $i$ and $j$.

VectorPrebundlestructureMathlib.Topology.VectorBundle.Basic, type

Wording

no wording

English

Let $R$ and $F$ be sets. Let $E$ be a function from elements of $B$ to sets. Then the elements of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$ are a basic type.

VectorPrebundle.coordChangedefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the coordinate change of a and #4 (from the name)

English

Let $a$ be an element of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$ such that $e$ is an element of the pretrivialization atlas of $a$ and $\mathrm{e'}$ is an element of the pretrivialization atlas of $a$. Let $b$ be an element of $B$. Then the coordinate change of $a$ and $b$ is a continuous linear map of $F$ and $F$ defined as $\operatorname{choose}$ applied to $\mathrm{VectorPrebundle\_\_exists\_coordChange}$ applied to $a$, $e$, $\mathrm{he}$, $\mathrm{e'}$ and $\mathrm{he'}$ and $b$.

VectorPrebundle.pretrivializationAtdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$. Let $x_{7}$ be an element of $B$. Then $\operatorname{pretrivializationAt}$ applied to $\mathrm{self}$ and $x_{7}$ is a pretrivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{7}$.

VectorPrebundle.pretrivializationAtlasdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the pretrivialization atlas of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$. Then the pretrivialization atlas of $\mathrm{self}$ is an element of the power set of the set of pretrivializations of $F$ and $\operatorname{proj}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

VectorPrebundle.toFiberPrebundledefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$. Then $\operatorname{toFiberPrebundle}$ applied to $a$ is an element of $\mathrm{FiberPrebundle}$ applied to $F$ and $E$.

VectorPrebundle.trivializationOfMemPretrivializationAtlasdefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the trivialization of a and he (from the name)

English

Let $a$ be an element of $\mathrm{VectorPrebundle}$ applied to $R$, $F$ and $E$ such that $e$ is an element of the pretrivialization atlas of $a$. Then the trivialization of $a$ and $\mathrm{he}$ is a trivialization of $F$ and $\operatorname{proj}$ defined as the trivialization of $\operatorname{toFiberPrebundle}$ applied to $a$ and $\mathrm{he}$.

trivialVectorBundleCoredefMathlib.Topology.VectorBundle.Basic, function or constant

Wording

the trivial vector bundle of F and x4 (from the name)

English

Let $R$, $B$, $F$ and $x_{4}$ be sets. Then the trivial vector bundle of $F$ and $x_{4}$ is a vector bundle of $F$ and $x_{4}$.

Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Bundle.ContinuousAlternatingMap.vectorPrebundledefMathlib.Topology.VectorBundle.ContinuousAlternatingMap, function or constant

Wording

no wording

English

Let $x$, $x_{1}$, $x_{5}$ and $x_{14}$ be sets. Let $x_{8}$ and $x_{17}$ be functions from elements of $B$ to sets. Then $\operatorname{vectorPrebundle}$ applied to $x$, $x_{1}$, $x_{5}$, $x_{8}$, $x_{14}$ and $x_{17}$ is an element of $\mathrm{VectorPrebundle}$ applied to $x$, the set of continuous alternating maps of $x_{14}$ and $x_{1}$ and the function that maps $x_{23}$ to the set of continuous alternating maps of $x_{17}$ applied to $x_{23}$ and $x_{1}$.

Bundle.Pretrivialization.continuousAlternatingMapdefMathlib.Topology.VectorBundle.ContinuousAlternatingMap, function or constant

Wording

the continuous alternating map of x22 and x23 (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $x_{22}$ be a trivialization of $x_{4}$ and $\operatorname{proj}$. Let $x_{23}$ be a trivialization of $x_{11}$ and $\operatorname{proj}$. Then the continuous alternating map of $x_{22}$ and $x_{23}$ is a pretrivialization of the set of continuous alternating maps of $x_{11}$ and $x_{1}$ and $\operatorname{proj}$.

Bundle.Pretrivialization.continuousAlternatingMapCoordChangedefMathlib.Topology.VectorBundle.ContinuousAlternatingMap, function or constant

Wording

the continuous alternating map coordinate change of x21 and b (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $x_{18}$ and $x_{19}$ be trivializations of $x_{4}$ and $\operatorname{proj}$. Let $x_{20}$ and $x_{21}$ be trivializations of $x_{11}$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the continuous alternating map coordinate change of $x_{21}$ and $b$ is a continuous linear map of the set of continuous alternating maps of $x_{11}$ and $x_{1}$ and the set of continuous alternating maps of $x_{11}$ and $x_{1}$ defined as the continuous linear map of the continuous alternating map congruence of the inverse of the coordinate change of $x_{18}$ and $b$ and the coordinate change of $x_{21}$ and $b$.

Bundle.Trivialization.continuousAlternatingMapdefMathlib.Topology.VectorBundle.ContinuousAlternatingMap, function or constant

Wording

the continuous alternating map of x23 and x24 (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $x_{23}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Let $x_{24}$ be a trivialization of $x_{14}$ and $\operatorname{proj}$. Then the continuous alternating map of $x_{23}$ and $x_{24}$ is a trivialization of the set of continuous alternating maps of $x_{14}$ and $x_{1}$ and $\operatorname{proj}$.

ContinuousAlternatingMap.inCoordinatesdefMathlib.Topology.VectorBundle.ContinuousAlternatingMap, function or constant

Wording

no wording

English

Let $x_{4}$ and $x_{15}$ be sets. Let $x_{25}$ and $x_{26}$ be elements of $x_{3}$. Let $x_{27}$ and $y$ be elements of $x_{14}$. Let $x_{28}$ be a continuous alternating map of $x_{18}$ applied to $y$ and $x_{1}$. Then $\operatorname{inCoordinates}$ applied to $x_{4}$, $x_{15}$, $x_{25}$, $x_{26}$, $x_{27}$, $y$ and $x_{28}$ is a continuous alternating map of $x_{15}$ and $x_{1}$ defined as the composition continuous linear map of the composition continuous alternating map of $\operatorname{continuousLinearMapAt}$ applied to $x$, $\operatorname{trivializationAt}$ applied to $x_{15}$, $x_{18}$ and $x_{27}$ and $y$ and $x_{28}$ and the inverse of $\operatorname{trivializationAt}$ applied to $x_{4}$, $x_{7}$ and $x_{25}$ and $x_{26}$.

Mathlib.Topology.VectorBundle.Hom

Bundle.ContinuousLinearMap.vectorPrebundledefMathlib.Topology.VectorBundle.Hom, function or constant

Wording

no wording

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{2}$. Let $x_{5}$ and $x_{12}$ be sets. Let $x_{8}$ and $x_{15}$ be functions from elements of $B$ to sets. Then $\operatorname{vectorPrebundle}$ applied to $x_{4}$, $x_{5}$, $x_{8}$, $x_{12}$ and $x_{15}$ is an element of $\mathrm{VectorPrebundle}$ applied to $x_{2}$, the set of continuous linear maps of $x_{5}$ and $x_{12}$ and the function that maps $x_{24}$ to the set of continuous linear maps of $x_{8}$ applied to $x_{24}$ and $x_{15}$ applied to $x_{24}$.

Bundle.Pretrivialization.continuousLinearMapdefMathlib.Topology.VectorBundle.Hom, function or constant

Wording

the continuous linear map of x20 and x21 (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{2}$. Let $x_{20}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Let $x_{21}$ be a trivialization of $x_{12}$ and $\operatorname{proj}$. Then the continuous linear map of $x_{20}$ and $x_{21}$ is a pretrivialization of the set of continuous linear maps of $x_{5}$ and $x_{12}$ and $\operatorname{proj}$.

Bundle.Pretrivialization.continuousLinearMapCoordChangedefMathlib.Topology.VectorBundle.Hom, function or constant

Wording

the continuous linear map coordinate change of x23 and b (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{2}$. Let $x_{20}$ and $x_{21}$ be trivializations of $x_{5}$ and $\operatorname{proj}$. Let $x_{22}$ and $x_{23}$ be trivializations of $x_{12}$ and $\operatorname{proj}$. Let $b$ be an element of $B$. Then the continuous linear map coordinate change of $x_{23}$ and $b$ is a continuous linear map of the set of continuous linear maps of $x_{5}$ and $x_{12}$ and the set of continuous linear maps of $x_{5}$ and $x_{12}$ defined as the continuous linear map of $\operatorname{arrowCongrSL}$ applied to the inverse of the coordinate change of $x_{20}$ and $b$ and the coordinate change of $x_{23}$ and $b$.

Bundle.Trivialization.continuousLinearMapdefMathlib.Topology.VectorBundle.Hom, function or constant

Wording

the continuous linear map of x20 and x21 (from the name)

English

Let $x_{4}$ be a ring homomorphism of $x$ and $x_{2}$. Let $x_{20}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Let $x_{21}$ be a trivialization of $x_{12}$ and $\operatorname{proj}$. Then the continuous linear map of $x_{20}$ and $x_{21}$ is a trivialization of the set of continuous linear maps of $x_{5}$ and $x_{12}$ and $\operatorname{proj}$.

Mathlib.Topology.VectorBundle.Riemannian

Bundle.ContinuousRiemannianMetricstructureMathlib.Topology.VectorBundle.Riemannian, type

Wording

no wording

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Then the elements of $\operatorname{ContinuousRiemannianMetric}$ applied to $F$ and $E$ are a basic type.

Bundle.ContinuousRiemannianMetric.innerdefMathlib.Topology.VectorBundle.Riemannian, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{ContinuousRiemannianMetric}$ applied to $F$ and $E$. Let $b$ be an element of $B$. Then $\operatorname{inner}$ applied to $\mathrm{self}$ and $b$ is a continuous linear map of $E$ applied to $b$ and the set of continuous linear maps of $E$ applied to $b$ and $\Real$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $b$.

Bundle.ContinuousRiemannianMetric.toRiemannianMetricdefMathlib.Topology.VectorBundle.Riemannian, function or constant

Wording

no wording

English

Let $g$ be an element of $\operatorname{ContinuousRiemannianMetric}$ applied to $F$ and $E$. Then $\operatorname{toRiemannianMetric}$ applied to $g$ is an element of $\operatorname{RiemannianMetric}$ applied to $E$.

Bundle.RiemannianBundleclassMathlib.Topology.VectorBundle.Riemannian, predicate

Wording

no wording

English

Let $E$ be a function from elements of $B$ to sets. Then we can say that $\operatorname{RiemannianBundle}$ holds for $E$.

Bundle.RiemannianBundle.gdefMathlib.Topology.VectorBundle.Riemannian, function or constant

Wording

no wording

English

$\operatorname{g}$ is an element of $\operatorname{RiemannianMetric}$ applied to $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Bundle.RiemannianMetricstructureMathlib.Topology.VectorBundle.Riemannian, type

Wording

no wording

English

Let $E$ be a function from elements of $B$ to sets. Then the elements of $\operatorname{RiemannianMetric}$ applied to $E$ are a basic type.

Bundle.RiemannianMetric.innerdefMathlib.Topology.VectorBundle.Riemannian, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{RiemannianMetric}$ applied to $E$. Let $b$ be an element of $B$. Then $\operatorname{inner}$ applied to $\mathrm{self}$ and $b$ is a continuous linear map of $E$ applied to $b$ and the set of continuous linear maps of $E$ applied to $b$ and $\Real$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $b$.