IsAddQuotientCoveringMap.fundamentalGroupEquivdefMathlib.Topology.Homotopy.Lifting, function or constantWording
the fundamental group equivalence of hp and e (from the name)
English
Assume that $p$ is an additive quotient covering map. Let $e$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fundamental group equivalence of $\mathrm{hp}$ and $e$ is a multiplicative equivalence of the set of fundamental groups of $X$ and $x_{4}$ and the set of multiplicative opposites of the set of multiplicatives of $G$ defined as the fundamental group equivalence of $\operatorname{toMultiplicative}$ applied to $p$, $G$ and $\mathrm{hp}$ and $e$.
IsAddQuotientCoveringMap.fundamentalGroupToMulOppositedefMathlib.Topology.Homotopy.Lifting, function or constantWording
the fundamental group to multiplicative opposite of hp and e (from the name)
English
Assume that $p$ is an additive quotient covering map. Let $e$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fundamental group to multiplicative opposite of $\mathrm{hp}$ and $e$ is a monoid homomorphism of the set of fundamental groups of $X$ and $x_{4}$ and the set of multiplicative opposites of the set of multiplicatives of $G$ defined as the fundamental group to multiplicative opposite of $\operatorname{toMultiplicative}$ applied to $p$, $G$ and $\mathrm{hp}$ and $e$.
IsCoveringMap.liftHomotopydefMathlib.Topology.Homotopy.Lifting, function or constantWording
the lift homotopy of H and f (from the name)
English
Assume that $p$ is a covering map. Let $H$ be a continuous map of $\mathrm{Prod}$ applied to the set of elements of the unit interval and $A$ and $X$. Let $f$ be a continuous map of $A$ and $E$ such that for all elements $a$ of $A$, $\EqtMACRoH {H (\ProdmkMACRoU {0}{a})}{p (f (a))}$. Then the lift homotopy of $H$ and $f$ is a continuous map of $\mathrm{Prod}$ applied to the set of elements of the unit interval and $A$ and $E$.
IsCoveringMap.liftHomotopyReldefMathlib.Topology.Homotopy.Lifting, function or constantWording
the lift homotopy relation of F (from the name)
English
Assume that $p$ is a covering map. Let $F$ be a homotopy relation of $x_{4}$ and $S$. Assume that there exists an element $a$ of $A$, such that $a$ is an element of $S$ and $\EqtMACRoH {x_{5} (a)}{x_{6} (a)}$. Assume that $\operatorname{comp}$ applied to $p$ and $\operatorname{coe}$ applied to $x_{5}$ is equal to $\operatorname{coe}$ applied to $x_{3}$. Assume that $\operatorname{comp}$ applied to $p$ and $\operatorname{coe}$ applied to $x_{6}$ is equal to $\operatorname{coe}$ applied to $x_{4}$. Then the lift homotopy relation of $F$ is a homotopy relation of $x_{6}$ and $S$.
IsCoveringMap.liftPathdefMathlib.Topology.Homotopy.Lifting, function or constantWording
the lift path of x2 and e (from the name)
English
Assume that $p$ is a covering map. Let $x_{2}$ be a continuous map of the set of elements of the unit interval and $X$. Let $e$ be an element of $E$ such that $\EqtMACRoH {x_{2} (0)}{p (e)}$. Then the lift path of $x_{2}$ and $e$ is a continuous map of the set of elements of the unit interval and $E$ defined as $\operatorname{choose}$ applied to $\mathrm{IsCoveringMap\_\_exists\_path\_lifts}$ applied to $\mathrm{cov}$, $x_{2}$, $e$ and $h$.
IsCoveringMap.liftPathQuotientdefMathlib.Topology.Homotopy.Lifting, function or constantWording
the lift path quotient of x3 and e (from the name)
English
Assume that $p$ is a covering map. Let $x_{3}$ be a quotient of $x_{2}$ and $y$. Let $e$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{2}$. Then the lift path quotient of $x_{3}$ and $e$ is a quotient of $e$ and the monodromy of $x_{3}$ and $e$.
IsCoveringMap.monodromydefMathlib.Topology.Homotopy.Lifting, function or constantWording
the monodromy of x3 and x4 (from the name)
English
Assume that $p$ is a covering map. Let $x_{3}$ be a quotient of $x_{2}$ and $y$. Let $x_{4}$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{2}$. Then the monodromy of $x_{3}$ and $x_{4}$ is an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $y$.
IsCoveringMap.monodromyFunctordefMathlib.Topology.Homotopy.Lifting, function or constantWording
the monodromy functor of cov (from the name)
English
Assume that $p$ is a covering map. Then the monodromy functor of $\mathrm{cov}$ is a functor of the set of fundamental groupoids of $X$ and the set of sets.
IsCoveringMap.monodromyPermdefMathlib.Topology.Homotopy.Lifting, function or constantWording
the monodromy permutation of cov and x2 (from the name)
English
Assume that $p$ is a covering map. Let $x_{2}$ be an element of $X$. Then the monodromy permutation of $\mathrm{cov}$ and $x_{2}$ is a monoid homomorphism of the set of fundamental groups of $X$ and $x_{2}$ and the set of permutations of the set of elements of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{2}$ defined as the permutation homomorphism of the set of fundamental groups of $X$ and $x_{2}$ and the set of elements of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{2}$.
IsQuotientCoveringMap.fundamentalGroupEquivdefMathlib.Topology.Homotopy.Lifting, function or constantWording
the fundamental group equivalence of hp and e (from the name)
English
Assume that $p$ is a quotient covering map. Let $e$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fundamental group equivalence of $\mathrm{hp}$ and $e$ is a multiplicative equivalence of the set of fundamental groups of $X$ and $x_{4}$ and the set of multiplicative opposites of $G$.
IsQuotientCoveringMap.fundamentalGroupToMulOppositedefMathlib.Topology.Homotopy.Lifting, function or constantWording
the fundamental group to multiplicative opposite of hp and e (from the name)
English
Assume that $p$ is a quotient covering map. Let $e$ be an element of the preimage of $p$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fundamental group to multiplicative opposite of $\mathrm{hp}$ and $e$ is a monoid homomorphism of the set of fundamental groups of $X$ and $x_{4}$ and the set of multiplicative opposites of $G$.
LocallyContractibleSpacedefMathlib.Topology.Homotopy.LocallyContractible, predicateWording
X is a locally contractible space (from the name)
English
generation took over the time limit
StronglyLocallyContractibleSpaceclassMathlib.Topology.Homotopy.LocallyContractible, predicateEnglish
Let $X$ be a set. Then we can say that $\mathrm{StronglyLocallyContractibleSpace}$ holds for $X$.
ContinuousMap.Homotopy.evalAtdefMathlib.Topology.Homotopy.Path, function or constantEnglish
Let $H$ be a homotopy of $f$ and $g$. Let $x_{2}$ be an element of $X$. Then $\operatorname{evalAt}$ applied to $H$ and $x_{2}$ is a path of $f$ applied to $x_{2}$ and $g$ applied to $x_{2}$.
Path.HomotopicdefMathlib.Topology.Homotopy.Path, predicateWording
x3 is homotopic to x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be paths of $x_{1}$ and $x_{2}$. Then $x_{3}$ is homotopic to $x_{4}$, if $\mathrm{Nonempty}$ holds for the set of homotopies of $x_{3}$ and $x_{4}$.
Path.Homotopic.QuotientdefMathlib.Topology.Homotopy.Path, typeWording
quotient of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be elements of $X$. Then a quotient of $x_{1}$ and $x_{2}$ is an element of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $x_{1}$ and $x_{2}$.
Path.Homotopic.Quotient.castdefMathlib.Topology.Homotopy.Path, function or constantWording
the cast of x2 (from the name)
English
Let $x_{2}$ be a quotient of $x_{1}$ and $y$. Assume that $\EqtMACRoH {\mathrm{x'}}{x_{1}}$. Assume that $\EqtMACRoH {\mathrm{y'}}{y}$. Then the cast of $x_{2}$ is a quotient of $\mathrm{x'}$ and $\mathrm{y'}$ defined as the map of the function that maps $p$ to the cast of $p$ and $x_{2}$.
Path.Homotopic.Quotient.mapdefMathlib.Topology.Homotopy.Path, function or constantWording
the map of x4 and f (from the name)
English
Let $x_{4}$ be a quotient of $x_{2}$ and $x_{3}$. Let $f$ be a continuous map of $X$ and $Y$. Then the map of $x_{4}$ and $f$ is a quotient of $f$ applied to $x_{2}$ and $f$ applied to $x_{3}$ defined as the map of the function that maps $q$ to the map of $q$ and $\operatorname{continuous}$ applied to $f$ and $x_{4}$.
Path.Homotopic.Quotient.mkdefMathlib.Topology.Homotopy.Path, function or constantEnglish
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then $\operatorname{mk}$ applied to $p$ is a quotient of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk'}$ applied to $p$.
Path.Homotopic.Quotient.refldefMathlib.Topology.Homotopy.Path, function or constantWording
the identity of x1 (from the name)
English
Let $x_{1}$ be an element of $X$. Then the identity of $x_{1}$ is a quotient of $x_{1}$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the identity of $x_{1}$.
Path.Homotopic.Quotient.symmdefMathlib.Topology.Homotopy.Path, function or constantWording
the inverse of P (from the name)
English
Let $P$ be a quotient of $x_{1}$ and $x_{2}$. Then the inverse of $P$ is a quotient of $x_{2}$ and $x_{1}$ defined as the map of $\operatorname{symm}$ and $P$.
Path.Homotopic.Quotient.transdefMathlib.Topology.Homotopy.Path, function or constantWording
the composition of x4 and x5 (from the name)
English
Let $x_{4}$ be a quotient of $x_{1}$ and $x_{2}$. Let $x_{5}$ be a quotient of $x_{2}$ and $x_{3}$. Then the composition of $x_{4}$ and $x_{5}$ is a quotient of $x_{1}$ and $x_{3}$ defined as the map of $x_{4}$ and $x_{5}$.
Path.HomotopydefMathlib.Topology.Homotopy.Path, typeWording
homotopy of x3 and x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be paths of $x_{1}$ and $x_{2}$. Then a homotopy of $x_{3}$ and $x_{4}$ is an element of the function that maps $x_{3}$ and $x_{4}$ to the set of homotopy relations of $\operatorname{toContinuousMap}$ applied to $x_{4}$ and $\operatorname{insert}$ applied to $0$ and $\operatorname{singleton}$ applied to $1$.
Path.Homotopy.castdefMathlib.Topology.Homotopy.Path, function or constantWording
the cast of F (from the name)
English
Let $F$ be a homotopy of $x_{3}$ and $x_{4}$. Assume that $\EqtMACRoH {x_{3}}{x_{5}}$. Assume that $\EqtMACRoH {x_{4}}{x_{6}}$. Then the cast of $F$ is a homotopy of $x_{5}$ and $x_{6}$.
Path.Homotopy.evaldefMathlib.Topology.Homotopy.Path, function or constantWording
the evaluation of F and t (from the name)
English
Let $F$ be a homotopy of $x_{3}$ and $x_{4}$. Let $t$ be an element of the unit interval. Then the evaluation of $F$ and $t$ is a path of $x_{1}$ and $x_{2}$.
Path.Homotopy.hcompdefMathlib.Topology.Homotopy.Path, function or constantEnglish
Let $F$ be a homotopy of $x_{4}$ and $x_{5}$. Let $G$ be a homotopy of $x_{6}$ and $x_{7}$. Then $\operatorname{hcomp}$ applied to $F$ and $G$ is a homotopy of the composition of $x_{4}$ and $x_{6}$ and the composition of $x_{5}$ and $x_{7}$.
Path.Homotopy.mapdefMathlib.Topology.Homotopy.Path, function or constantWording
the map of F and f (from the name)
English
Let $F$ be a homotopy of $p$ and $q$. Let $f$ be a continuous map of $X$ and $Y$. Then the map of $F$ and $f$ is a homotopy of the map of $p$ and $\operatorname{continuous}$ applied to $f$ and the map of $q$ and $\operatorname{continuous}$ applied to $f$.
Path.Homotopy.pathCastdefMathlib.Topology.Homotopy.Path, function or constantWording
the path cast of F (from the name)
English
Let $F$ be a homotopy of $p$ and $q$. Assume that $\EqtMACRoH {\mathrm{x'}}{x_{1}}$. Assume that $\EqtMACRoH {\mathrm{y'}}{y}$. Then the path cast of $F$ is a homotopy of the cast of $p$ and the cast of $q$ defined as $F$.
Path.Homotopy.refldefMathlib.Topology.Homotopy.Path, function or constantWording
the identity of p (from the name)
English
Let $p$ be a path of $x_{1}$ and $x_{2}$. Then the identity of $p$ is a homotopy of $p$ and $p$ defined as the identity of $\operatorname{toContinuousMap}$ applied to $p$ and $\operatorname{insert}$ applied to $0$ and $\operatorname{singleton}$ applied to $1$.
Path.Homotopy.reparamdefMathlib.Topology.Homotopy.Path, function or constantEnglish
Let $p$ be a path of $x_{1}$ and $x_{2}$. Let $f$ be a function from elements of the unit interval to elements of the unit interval such that $f$ is continuous, $\EqtMACRoH {f (0)}{0}$ and $\EqtMACRoH {f (1)}{1}$. Then $\operatorname{reparam}$ applied to $p$, $f$, $\mathrm{hf}$, $h$ and $h_{1}$ is a homotopy of $p$ and $\operatorname{reparam}$ applied to $p$, $f$, $\mathrm{hf}$, $h$ and $h_{1}$.
Path.Homotopy.symmdefMathlib.Topology.Homotopy.Path, function or constantWording
the inverse of F (from the name)
English
Let $F$ be a homotopy of $x_{3}$ and $x_{4}$. Then the inverse of $F$ is a homotopy of $x_{4}$ and $x_{3}$ defined as the inverse of $F$.
Path.Homotopy.symm₂defMathlib.Topology.Homotopy.Path, function or constantWording
the inverse of F (from the name)
English
Let $F$ be a homotopy of $p$ and $q$. Then the inverse of $F$ is a homotopy of the inverse of $p$ and the inverse of $q$.
Path.Homotopy.transdefMathlib.Topology.Homotopy.Path, function or constantWording
the composition of F and G (from the name)
English
Let $F$ be a homotopy of $x_{3}$ and $x_{4}$. Let $G$ be a homotopy of $x_{4}$ and $x_{5}$. Then the composition of $F$ and $G$ is a homotopy of $x_{3}$ and $x_{5}$ defined as the composition of $F$ and $G$.
Path.toHomotopyConstdefMathlib.Topology.Homotopy.Path, function or constantWording
the homotopy constant of p (from the name)
English
Let $p$ be a path of $x_{2}$ and $x_{3}$. Then the homotopy constant of $p$ is a homotopy of the constant map of $Y$ and $x_{2}$ and the constant map of $Y$ and $x_{3}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toContinuousMap}$ applied to $p$ and the first component, the function that maps $x_{4}$ to $\operatorname{source}$ applied to $p$ and the function that maps $x_{5}$ to $\operatorname{target}$ applied to $p$.
ContinuousMap.Homotopy.proddefMathlib.Topology.Homotopy.Product, function or constantWording
the product of F and G (from the name)
English
Let $F$ be a homotopy of $x_{5}$ and $x_{6}$. Let $G$ be a homotopy of $x_{7}$ and $x_{8}$. Then the product of $F$ and $G$ is a homotopy of the product of $x_{5}$ and $x_{7}$ and the product of $x_{6}$ and $x_{8}$.
ContinuousMap.HomotopyRel.pidefMathlib.Topology.Homotopy.Product, function or constantWording
the product of homotopies (from the name)
English
Let $\mathrm{homotopies}$ be a function from elements $i$ of $I$ to homotopy relations of $g$ applied to $i$ and $S$. Then the product of $i$ is a homotopy relation of the product of $g$ and $S$.
ContinuousMap.HomotopyRel.proddefMathlib.Topology.Homotopy.Product, function or constantWording
the product of F and G (from the name)
English
Let $F$ be a homotopy relation of $x_{6}$ and $S$. Let $G$ be a homotopy relation of $x_{8}$ and $S$. Then the product of $F$ and $G$ is a homotopy relation of the product of $x_{6}$ and $x_{8}$ and $S$.
Path.Homotopic.pidefMathlib.Topology.Homotopy.Product, function or constantWording
the product of x2 (from the docstring)
English
Let $x_{2}$ be a function from elements $i$ of $x$ to quotients of $\mathrm{as}$ applied to $i$ and $\mathrm{bs}$ applied to $i$. Then the product of $i$ is a quotient of $\mathrm{as}$ and $\mathrm{bs}$.
Path.Homotopic.piHomotopydefMathlib.Topology.Homotopy.Product, function or constantWording
the product homotopy of i2 and x3 (from the name)
English
Let $x_{2}$ be a function from elements $i_{2}$ of $x$ to paths of $\mathrm{as}$ applied to $i_{2}$ and $\mathrm{bs}$ applied to $i_{2}$. Let $x_{3}$ be a function from elements $i_{1}$ of $x$ to paths of $\mathrm{as}$ applied to $i_{1}$ and $\mathrm{bs}$ applied to $i_{1}$. Let $H$ be a function from elements $i$ of $x$ to homotopies of $x_{2}$ applied to $i$ and $x_{3}$ applied to $i$. Then the product homotopy of $x_{2}$ and $i_{1}$ is a homotopy of the product of $x_{2}$ and the product of $x_{3}$ defined as the function that maps $x_{3}$, $i$ and $H$ to the product of $i_{1}$.
Path.Homotopic.proddefMathlib.Topology.Homotopy.Product, function or constantWording
the product of x8 and x9 (from the name)
English
Let $x_{8}$ be a quotient of $x_{4}$ and $x_{5}$. Let $x_{9}$ be a quotient of $x_{6}$ and $x_{7}$. Then the product of $x_{8}$ and $x_{9}$ is a quotient of $\ProdmkMACRoU {x_{4}}{x_{6}}$ and $\ProdmkMACRoU {x_{5}}{x_{7}}$.
Path.Homotopic.prodHomotopydefMathlib.Topology.Homotopy.Product, function or constantWording
the product homotopy of x12 and x13 (from the name)
English
Let $x_{12}$ be a homotopy of $x_{8}$ and $x_{9}$. Let $x_{13}$ be a homotopy of $x_{10}$ and $x_{11}$. Then the product homotopy of $x_{12}$ and $x_{13}$ is a homotopy of the product of $x_{8}$ and $x_{10}$ and the product of $x_{9}$ and $x_{11}$ defined as the product of $x_{12}$ and $x_{13}$.
Path.Homotopic.projdefMathlib.Topology.Homotopy.Product, function or constantWording
the projection of i and p (from the name)
English
Let $i$ be an element of $x$. Let $p$ be a quotient of $\mathrm{as}$ and $\mathrm{bs}$. Then the projection of $i$ and $p$ is a quotient of $\mathrm{as}$ applied to $i$ and $\mathrm{bs}$ applied to $i$ defined as the map of $p$ and $\operatorname{mk}$ applied to the function that maps $p_{1}$ to $p_{1}$ applied to $i$ and $\mathrm{continuous\_apply}$ applied to $i$.
Path.Homotopic.projLeftdefMathlib.Topology.Homotopy.Product, function or constantWording
the left projection of p (from the name)
English
Let $p$ be a quotient of $x_{4}$ and $x_{5}$. Then the left projection of $p$ is a quotient of $\ProdfstMACRoZ {x_{4}}$ and $\ProdfstMACRoZ {x_{5}}$ defined as the map of $p$ and $\operatorname{mk}$ applied to $\ProdfstMACRoZ$ and $\mathrm{continuous\_fst}$.
Path.Homotopic.projRightdefMathlib.Topology.Homotopy.Product, function or constantWording
the right projection of p (from the name)
English
Let $p$ be a quotient of $x_{4}$ and $x_{5}$. Then the right projection of $p$ is a quotient of $\ProdsndMACRoAA {x_{4}}$ and $\ProdsndMACRoAA {x_{5}}$ defined as the map of $p$ and $\operatorname{mk}$ applied to $\ProdsndMACRoAA$ and $\mathrm{continuous\_snd}$.
TopCat.HomotopydefMathlib.Topology.Homotopy.TopCat.Basic, typeWording
homotopy of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then a homotopy of $f$ and $g$ is an element of the function that maps $f$ and $g$ to the set of homotopies of the homomorphism of $f$ and the homomorphism of $g$.
TopCat.Homotopy.compdefMathlib.Topology.Homotopy.TopCat.Basic, function or constantWording
the composition of G and F (from the name)
English
Let $G$ be a homotopy of $x_{2}$ and $x_{3}$. Let $F$ be a homotopy of $x$ and $x_{1}$. Then the composition of $G$ and $F$ is a homotopy of the composition of $x$ and $x_{2}$ and the composition of $x_{1}$ and $x_{3}$ defined as the composition of $G$ and $F$.
TopCat.Homotopy.hdefMathlib.Topology.Homotopy.TopCat.Basic, function or constantEnglish
Let $H$ be a homotopy of $x$ and $x_{1}$. Then $\operatorname{h}$ applied to $H$ is a homomorphism of the tensor object of $X$ and $\operatorname{I}$ and $Y$ defined as the composition of the homomorphism of the braiding natural isomorphism of $X$ and $\operatorname{I}$ and the topological category of the composition of $\operatorname{toContinuousMap}$ applied to $H$ and the product map of the continuous map of the homeomorphism and the identity of the set of carriers of $X$.
TopCat.Homotopy.refldefMathlib.Topology.Homotopy.TopCat.Basic, function or constantWording
the identity homotopy of f (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the identity homotopy of $f$ is a homotopy of the homomorphism of $f$ and the homomorphism of $f$ defined as the identity of the homomorphism of $f$.
TopCat.Homotopy.symmdefMathlib.Topology.Homotopy.TopCat.Basic, function or constantWording
the inverse of F (from the name)
English
Let $F$ be a homotopy of $x$ and $x_{1}$. Then the inverse of $F$ is a homotopy of the homomorphism of $x_{1}$ and the homomorphism of $x$ defined as the inverse of $F$.
TopCat.Homotopy.transdefMathlib.Topology.Homotopy.TopCat.Basic, function or constantWording
the composition of F and G (from the name)
English
Let $F$ be a homotopy of $x$ and $x_{1}$. Let $G$ be a homotopy of $x_{1}$ and $x_{2}$. Then the composition of $F$ and $G$ is a homotopy of the homomorphism of $x$ and the homomorphism of $x_{2}$ defined as the composition of $F$ and $G$.
TopCat.PathstructureMathlib.Topology.Homotopy.TopCat.Path, typeWording
path of x and y (from the name)
English
Let $X$ be a topological category. Let $x$ and $y$ be carriers of $X$. Then the paths of $x$ and $y$ are a basic type.
TopCat.Path.homdefMathlib.Topology.Homotopy.TopCat.Path, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a path of $x$ and $y$. Then the homomorphism of $\mathrm{self}$ is a homomorphism of $\operatorname{I}$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopCat.pathEquivdefMathlib.Topology.Homotopy.TopCat.Path, function or constantWording
the path equivalence (from the name)
English
The path equivalence is an equivalence from the set of paths of $x$ and $y$ to the set of paths of $x$ and $y$.
TopCat.Homotopy.toSSetdefMathlib.Topology.Homotopy.TopCat.ToSSet, function or constantWording
the set of h (from the name)
English
Let $h$ be a homotopy of $f$ and $g$. Then the set of $h$ is a homotopy of the map of the set and $f$ and the map of the set and $g$.
TopCat.toSSetObjEdgeEquivdefMathlib.Topology.Homotopy.TopCat.ZerothHomotopy, function or constantWording
the set object edge equivalence (from the name)
English
The set object edge equivalence is an equivalence from the set of edges of $\operatorname{symm}$ applied to the set object equivalence and $x$ and $\operatorname{symm}$ applied to the set object equivalence and $y$ to the set of paths of $x$ and $y$.
TopCat.toSSetObj₁EquivdefMathlib.Topology.Homotopy.TopCat.ZerothHomotopy, function or constantWording
the set object equivalence (from the name)
English
The set object equivalence is an equivalence from the action of the action of the set and $X$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to $1$ to the set of homomorphisms of $\operatorname{I}$ and $X$.
TopCat.zerothHomotopyEquivdefMathlib.Topology.Homotopy.TopCat.ZerothHomotopy, function or constantWording
the zeroth homotopy equivalence (from the name)
English
The zeroth homotopy equivalence is an equivalence from the set of zeroth homotopies of the set of carriers of $X$ to the set of projections of the action of the set and $X$.
HasSmallInductiveDimensionLEdefMathlib.Topology.InductiveDimension.Classes, predicateEnglish
Let $X$ be a set. Let $n$ be a natural number. Then $\mathrm{HasSmallInductiveDimensionLE}$ holds for $X$ and $n$, if $\mathrm{HasSmallInductiveDimensionLT}$ holds for $X$ and $n + 1$.
HasSmallInductiveDimensionLTclassMathlib.Topology.InductiveDimension.Classes, predicateEnglish
Let $X$ be a set. Let $x_{1}$ be a natural number. Then we can say that $\mathrm{HasSmallInductiveDimensionLT}$ holds for $X$ and $x_{1}$.
ZeroDimensionalSpacedefMathlib.Topology.InductiveDimension.Classes, predicateWording
X is a zero dimensional space (from the name)
English
Let $X$ be a set. Then $X$ is a zero dimensional space, if $\mathrm{HasSmallInductiveDimensionLT}$ holds for $X$ and $1$.
smallInductiveDimensiondefMathlib.Topology.InductiveDimension.Functions, function or constantWording
the small inductive dimension of X (from the docstring)
English
Let $X$ be a set. Then the small inductive dimension of $X$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all natural numbers $i$, if $n < i$, then $\mathrm{HasSmallInductiveDimensionLT}$ holds for $X$ and $i$.
GeneralizingMapdefMathlib.Topology.Inseparable, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{GeneralizingMap}$ holds for $f$, if $\operatorname{Fibration}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Specializes}$ applied to $x_{2}$ and $x_{3}$, the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Specializes}$ applied to $x_{4}$ and $x_{5}$ and $f$.
SeparationQuotient.liftdefMathlib.Topology.Inseparable, function or constantWording
the lift of f and x2 (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $x$ such that for all elements $x_{3}$ and $y$ of $X$, if $\mathrm{Inseparable}$ holds for $x_{3}$ and $y$, then $\EqtMACRoH {f (x_{3})}{f (y)}$. Let $x_{2}$ be a separation quotient of $X$. Then the lift of $f$ and $x_{2}$ is an element of $x$ defined as $\operatorname{liftOn'}$ applied to $x_{2}$, $f$ and $\mathrm{hf}$.
SeparationQuotient.lift₂defMathlib.Topology.Inseparable, function or constantWording
the lift of x3 and x4 (from the name)
English
Let $f$ be a function from elements of $X$ and elements of $Y$ to elements of $x$ such that for all elements $a$ of $X$, for all elements $b$ of $Y$, for all elements $c$ of $X$, for all elements $d$ of $Y$, if $\mathrm{Inseparable}$ holds for $a$ and $c$, then if $\mathrm{Inseparable}$ holds for $b$ and $d$, then $\EqtMACRoH {f (a , b)}{f (c , d)}$. Let $x_{3}$ be a separation quotient of $X$. Let $x_{4}$ be a separation quotient of $Y$. Then the lift of $x_{3}$ and $x_{4}$ is an element of $x$ defined as $\mathrm{Quotient\_\_liftOn\_u2082\_'}$ applied to $x_{3}$, $x_{4}$, $f$ and $\mathrm{hf}$.
SeparationQuotient.mkdefMathlib.Topology.Inseparable, function or constantEnglish
Let $x_{1}$ be an element of $X$. Then $\operatorname{mk}$ applied to $x_{1}$ is a separation quotient of $X$ defined as $\operatorname{mk''}$ applied to $x_{1}$.
SpecializingMapdefMathlib.Topology.Inseparable, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{SpecializingMap}$ holds for $f$, if $\operatorname{Fibration}$ holds for $\mathrm{flip}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Specializes}$ applied to $x_{2}$ and $x_{3}$, $\mathrm{flip}$ applied to the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Specializes}$ applied to $x_{4}$ and $x_{5}$ and $f$.
StableUnderGeneralizationdefMathlib.Topology.Inseparable, predicateWording
s is stable under generalization (from the name)
English
Let $s$ be an element of $\wp X$. Then $s$ is stable under generalization, if for all elements $x_{1}$ and $y$ of $X$, if $\mathrm{Specializes}$ holds for $y$ and $x_{1}$, then if $x_{1}$ is an element of $s$, then $y$ is an element of $s$.
StableUnderSpecializationdefMathlib.Topology.Inseparable, predicateWording
s is stable under specialization (from the name)
English
Let $s$ be an element of $\wp X$. Then $s$ is stable under specialization, if for all elements $x_{1}$ and $y$ of $X$, if $\mathrm{Specializes}$ holds for $x_{1}$ and $y$, then if $x_{1}$ is an element of $s$, then $y$ is an element of $s$.
AddCircledefMathlib.Topology.Instances.AddCircle.Defs, typeWording
additive circle of p (from the name)
English
Let $p$ be an element of $x$. Then an additive circle of $p$ is an element of the function that maps $p$ to the set of quotients of $x$ and $\operatorname{zmultiples}$ applied to $p$.
AddCircle.EndpointIdentinductiveMathlib.Topology.Instances.AddCircle.Defs, predicateEnglish
Let $p$ and $a$ be elements of $x$. Let $x_{3}$ and $x_{4}$ be elements of $\SetIccMACRoP {a}{(a + p)}$. Then we can say that $\operatorname{EndpointIdent}$ holds for $p$, $a$, $x_{3}$ and $x_{4}$.
AddCircle.equivAddCircledefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the equivalence additive circle of p and q (from the name)
English
Let $p$ and $q$ be elements of $x$ such that $p \neq 0$ and $q \neq 0$. Then the equivalence additive circle of $p$ and $q$ is an additive equivalence of the set of additive circles of $p$ and the set of additive circles of $q$.
AddCircle.equivIccQuotdefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the equivalence closed interval quotient of p and a (from the name)
English
Let $p$ and $a$ be elements of $x$. Then the equivalence closed interval quotient of $p$ and $a$ is an equivalence from the set of additive circles of $p$ to $\mathrm{Quot}$ applied to $\operatorname{EndpointIdent}$ applied to $p$ and $a$.
AddCircle.equivIcodefMathlib.Topology.Instances.AddCircle.Defs, function or constantEnglish
Let $p$ and $a$ be elements of $x$. Then $\operatorname{equivIco}$ applied to $p$ and $a$ is an equivalence from the set of additive circles of $p$ to the set of elements of $\operatorname{Ico}$ applied to $a$ and $a + p$.
AddCircle.equivIocdefMathlib.Topology.Instances.AddCircle.Defs, function or constantEnglish
Let $p$ and $a$ be elements of $x$. Then $\operatorname{equivIoc}$ applied to $p$ and $a$ is an equivalence from the set of additive circles of $p$ to the set of elements of $\operatorname{Ioc}$ applied to $a$ and $a + p$.
AddCircle.homeoIccQuotdefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the homeomorphism closed interval quotient of p and a (from the name)
English
Let $p$ and $a$ be elements of $x$. Then the homeomorphism closed interval quotient of $p$ and $a$ is a homeomorphism of the set of additive circles of $p$ and $\mathrm{Quot}$ applied to $\operatorname{EndpointIdent}$ applied to $p$ and $a$.
AddCircle.homeomorphAddCircledefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the homeomorphism additive circle of p and q (from the name)
English
Let $p$ and $q$ be elements of $x$ such that $p \neq 0$ and $q \neq 0$. Then the homeomorphism additive circle of $p$ and $q$ is a homeomorphism of the set of additive circles of $p$ and the set of additive circles of $q$.
AddCircle.liftIcodefMathlib.Topology.Instances.AddCircle.Defs, function or constantEnglish
Let $p$ and $a$ be elements of $x$. Let $f$ be a function from elements of $x$ to elements of $B$. Let $x_{3}$ be an additive circle of $p$. Then $\operatorname{liftIco}$ applied to $p$, $a$, $f$ and $x_{3}$ is an element of $B$ defined as $\operatorname{comp}$ applied to $\operatorname{domRestrict}$ applied to $\operatorname{Ico}$ applied to $a$ and $a + p$ and $f$, $\operatorname{coe}$ applied to $\operatorname{equivIco}$ applied to $p$ and $a$ and $x_{3}$.
AddCircle.liftIocdefMathlib.Topology.Instances.AddCircle.Defs, function or constantEnglish
Let $p$ and $a$ be elements of $x$. Let $f$ be a function from elements of $x$ to elements of $B$. Let $x_{3}$ be an additive circle of $p$. Then $\operatorname{liftIoc}$ applied to $p$, $a$, $f$ and $x_{3}$ is an element of $B$ defined as $\operatorname{comp}$ applied to $\operatorname{domRestrict}$ applied to $\operatorname{Ioc}$ applied to $a$ and $a + p$ and $f$, $\operatorname{coe}$ applied to $\operatorname{equivIoc}$ applied to $p$ and $a$ and $x_{3}$.
AddCircle.openPartialHomeomorphCoedefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the open partial homeomorphism coercion of p and a (from the name)
English
Let $p$ and $a$ be elements of $x$. Then the open partial homeomorphism coercion of $p$ and $a$ is an open partial homeomorphism of $x$ and the set of additive circles of $p$.
AddCircle.setAddOrderOfEquivdefMathlib.Topology.Instances.AddCircle.Defs, function or constantWording
the set additive order of p and hn (from the name)
English
Let $p$ be an element of $x$. Assume that $0 < n$. Then the set additive order of $p$ and $\mathrm{hn}$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $u$ to the proposition that the additive order of $u$ is equal to $n$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $m$ to the proposition that $m < n$ and the greatest common divisor of $m$ and $n$ is equal to $1$.
UnitAddCircledefMathlib.Topology.Instances.AddCircle.Real, typeWording
unit circle (from the docstring)
English
A unit circle is an additive circle of $1$.
UnitAddTorusdefMathlib.Topology.Instances.AddCircle.Real, typeWording
unit additive torus of d (from the name)
English
Let $d$ be a set. Then a unit additive torus of $d$ is an element of the function that maps $d$ to the set of functions from elements of $d$ to unit circles.
ZMod.toAddCircledefMathlib.Topology.Instances.AddCircle.Real, function or constantWording
the additive circle (from the name)
English
The additive circle is an additive monoid homomorphism of $\mathrm{ZMod}$ applied to $N$ and the set of unit circles.
cantorSequencedefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor sequence of x (from the name)
English
Let $x$ be a real number. Then the Cantor sequence of $x$ is an element of $\mathrm{Stream'}$ applied to $\Real$ defined as $\operatorname{iterate}$ applied to $\mathrm{cantorStep}$ and $x$.
cantorSetdefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor set (from the docstring)
English
The Cantor set is an element of $\wp \Real$ defined as the intersection of the function that maps $n$ to the Cantor set of $n$.
cantorSetEquivNatToBooldefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor set equivalence natural to bool (from the name)
English
The Cantor set equivalence natural to bool is an equivalence from the set of elements of the Cantor set to the set of functions from natural numbers to elements of $\mathrm{Bool}$.
cantorSetHomeomorphNatToBooldefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor set homeomorphism natural to bool (from the name)
English
The Cantor set homeomorphism natural to bool is a homeomorphism of the set of elements of the Cantor set and the set of functions from natural numbers to elements of $\mathrm{Bool}$.
cantorSpaceHomeomorphNatToCantorSpacedefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor space (from the docstring)
English
The Cantor space is a homeomorphism of the set of functions from natural numbers to elements of $\mathrm{Bool}$ and the set of functions from natural numbers and natural numbers to elements of $\mathrm{Bool}$ defined as the composition of the left product congruence of the inverse of the pair equivalence and the product curry.
cantorStepdefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor step of x (from the name)
English
Let $x$ be a real number. Then the Cantor step of $x$ is a real number defined as $\iteMACRoG {(\MembershipmemMACRoT {(\SetIccMACRoP {0}{(\frac{ 1}{3})})}{x})}{(3 \times x)}{(3 \times x - 2)}$.
cantorToBinarydefMathlib.Topology.Instances.CantorSet, function or constantEnglish
Let $x$ be a real number. Then $\mathrm{Stream'}$ holds for $\mathrm{Bool}$. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. By 0. By 1. By 3. By div. By Set__Icc. By x1. By Membership__mem. By Bool__false. By Bool__true. By ite. By x. By cantorSequence. By Stream'__map.
cantorToTernarydefMathlib.Topology.Instances.CantorSet, function or constantEnglish
Let $x$ be a real number. Then $\mathrm{Stream'}$ holds for $\mathrm{Fin}$ applied to $3$. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. By x1. By 2. By 0. By cond. By x. By cantorToBinary. By Stream'__map.
preCantorSetdefMathlib.Topology.Instances.CantorSet, function or constantWording
the Cantor set of x (from the name)
English
Let $x$ be a natural number. Then the Cantor set of $x$ is an element of $\wp \Real$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{preCantorSet\_\_\_f}$.
ENNReal.ltTopHomeomorphNNRealdefMathlib.Topology.Instances.ENNReal.Lemmas, function or constantEnglish
$\operatorname{ltTopHomeomorphNNReal}$ is a homeomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is less than the top and $\mathrm{NNReal}$.
ENNReal.neTopHomeomorphNNRealdefMathlib.Topology.Instances.ENNReal.Lemmas, function or constantEnglish
$\operatorname{neTopHomeomorphNNReal}$ is a homeomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is distinct from the top and $\mathrm{NNReal}$.
ENNReal.truncateToRealdefMathlib.Topology.Instances.ENNReal.Lemmas, function or constantEnglish
Let $t$ and $x$ be elements of $\mathrm{ENNReal}$. Then $\operatorname{truncateToReal}$ applied to $t$ and $x$ is a real number defined as $\operatorname{toReal}$ applied to $\MinminMACRoAG {t}{x}$.
EReal.neBotTopHomeomorphRealdefMathlib.Topology.Instances.EReal.Lemmas, function or constantEnglish
$\operatorname{neBotTopHomeomorphReal}$ is a homeomorphism of the set of elements of the complement of $\operatorname{insert}$ applied to the bottom and $\operatorname{singleton}$ applied to the top and $\Real$.
ContinuousMap.realToNNRealdefMathlib.Topology.Instances.NNReal.Lemmas, function or constantEnglish
$\operatorname{realToNNReal}$ is a continuous map of $\Real$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{toNNReal}$ and $\mathrm{continuous\_real\_toNNReal}$.
ENNReal.powOrderIsodefMathlib.Topology.Instances.NNReal.Lemmas, function or constantWording
the power order isomorphism of n and hn (from the name)
English
Let $n$ be a natural number such that $n \neq 0$. Then the power order isomorphism of $n$ and $\mathrm{hn}$ is an order isomorphism of $\mathrm{ENNReal}$ and $\mathrm{ENNReal}$.
NNReal.powOrderIsodefMathlib.Topology.Instances.NNReal.Lemmas, function or constantWording
the power order isomorphism of n and hn (from the name)
English
Let $n$ be a natural number such that $n \neq 0$. Then the power order isomorphism of $n$ and $\mathrm{hn}$ is an order isomorphism of $\mathrm{NNReal}$ and $\mathrm{NNReal}$.
AddEquiv.toRealLinearEquivdefMathlib.Topology.Instances.RealVectorSpace, function or constantWording
the real linear equivalence of e (from the name)
English
Let $e$ be an additive equivalence of $E$ and $F$ such that $\operatorname{coe}$ applied to $e$ and $\operatorname{coe}$ applied to the inverse of $e$ are continuous. Then the real linear equivalence of $e$ is a continuous linear equivalence of $E$ and $F$.
AddMonoidHom.toRealLinearMapdefMathlib.Topology.Instances.RealVectorSpace, function or constantWording
the real linear map of f and hf (from the name)
English
Let $f$ be an additive monoid homomorphism of $E$ and $F$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the real linear map of $f$ and $\mathrm{hf}$ is a continuous linear map of $E$ and $F$.
Shrink.homeomorphdefMathlib.Topology.Instances.Shrink, function or constantWording
the homeomorphism of X (from the name)
English
Let $X$ be a set. Then the homeomorphism of $X$ is a homeomorphism of $X$ and the set of shrinks of $X$ defined as the inverse of the homeomorphism of the inverse of the equivalence shrink of $X$.
TrivSqZeroExt.fstCLMdefMathlib.Topology.Instances.TrivSqZeroExt, function or constantWording
the first component continuous linear map of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the first component continuous linear map of $R$ and $M$ is a strong dual of $R$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.inlCLMdefMathlib.Topology.Instances.TrivSqZeroExt, function or constantWording
the left injection continuous linear map of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the left injection continuous linear map of $R$ and $M$ is a continuous linear map of $R$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.inrCLMdefMathlib.Topology.Instances.TrivSqZeroExt, function or constantWording
the right injection continuous linear map of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the right injection continuous linear map of $R$ and $M$ is a continuous linear map of $M$ and the set of trivial square zero extensions of $R$ and $M$.
TrivSqZeroExt.sndCLMdefMathlib.Topology.Instances.TrivSqZeroExt, function or constantWording
the second component continuous linear map of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the second component continuous linear map of $R$ and $M$ is a continuous linear map of the set of trivial square zero extensions of $R$ and $M$ and $M$.
IrreducibleSpaceclassMathlib.Topology.Irreducible, predicateWording
X is a irreducible space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is an irreducible space.
IsIrreducibledefMathlib.Topology.Irreducible, predicateWording
s is irreducible (from the name)
English
Let $s$ be an element of $\wp X$. Then $s$ is irreducible, if $s$ is nonempty and $\mathrm{IsPreirreducible}$ holds for $s$.
IsPreirreducibledefMathlib.Topology.Irreducible, predicateEnglish
Let $s$ be an element of $\wp X$. Then $\mathrm{IsPreirreducible}$ holds for $s$, if for all elements $u$ and $v$ of $\wp X$, if $u$ is open, then if $v$ is open, then if $\operatorname{inter}$ applied to $s$ and $u$ is nonempty, then if $\operatorname{inter}$ applied to $s$ and $v$ is nonempty, then $\operatorname{inter}$ applied to $s$ and $\operatorname{inter}$ applied to $u$ and $v$ is nonempty.
PreirreducibleSpaceclassMathlib.Topology.Irreducible, predicateEnglish
Let $X$ be a set. Then we can say that $\mathrm{PreirreducibleSpace}$ holds for $X$.
irreducibleComponentdefMathlib.Topology.Irreducible, function or constantWording
the irreducible component of x1 (from the name)
English
Let $x_{1}$ be an element of $X$. Then the irreducible component of $x_{1}$ is an element of $\wp X$.
irreducibleComponentsdefMathlib.Topology.Irreducible, function or constantWording
the irreducible component of X (from the name)
English
Let $X$ be a set. Then the irreducible component of $X$ is an element of $\wp (\wp X)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is maximal with respect to the proposition that $\mathrm{IsIrreducible}$.
irreducibleComponentsEquivOfIsPreirreducibleFiberdefMathlib.Topology.Irreducible, function or constantWording
the irreducible component equivalence of f (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is continuous, $f$ is an open map, for all elements $x_{2}$ of $Y$, $\mathrm{IsPreirreducible}$ holds for the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{2}$ and $\operatorname{Surjective}$ holds for $f$. Then the irreducible component equivalence of $f$ is an order isomorphism of the set of elements of the irreducible component of $Y$ and the set of elements of the irreducible component of $X$.
Homeomorph.preimageImageRestrictdefMathlib.Topology.IsClosedRestrict, function or constantEnglish
Let $x_{1}$ be a function from elements of $x$ to sets. Let $S$ be an element of $\wp x$. Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (j))$. Then $\operatorname{preimageImageRestrict}$ applied to $x_{1}$, $S$ and $s$ is a homeomorphism of the set of elements of the preimage of $\operatorname{domRestrict}$ applied to the complement of $S$ and the image of $\operatorname{domRestrict}$ applied to the complement of $S$ and $s$ and $\mathrm{Prod}$ applied to the set of elements of the image of $\operatorname{domRestrict}$ applied to the complement of $S$ and $s$ and the set of functions from elements $i$ of $S$ to elements of $x_{1}$ applied to $i$.
Topology.reorderRestrictProddefMathlib.Topology.IsClosedRestrict, function or constantEnglish
Let $S$ be an element of $\wp x$. Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (j_{1}))$. Let $p$ be an element of $\mathrm{Prod}$ applied to the set of elements of the image of $\operatorname{domRestrict}$ applied to the complement of $S$ and $s$ and the set of functions from elements $i$ of $S$ to elements of $x_{1}$ applied to $i$. Let $j$ be an element of $x$. Then $\operatorname{reorderRestrictProd}$ applied to $S$, $s$, $p$ and $j$ is an element of $x_{1}$ applied to $j$ defined as $\mathrm{dite}$ applied to $\MembershipmemMACRoT {S}{j}$, the function that maps $h$ to $\ProdsndMACRoAA {p}$ and the function that maps $h_{1}$ to $j$.
IsLocalHomeomorphdefMathlib.Topology.IsLocalHomeomorph, predicateWording
f is a local homeomorphism (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is a local homeomorphism, if for all elements $x_{2}$ of $X$, there exists an open partial homeomorphism $e$ of $X$ and $Y$, such that $x_{2}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $f$ is equal to $\operatorname{toFun'}$ applied to $e$.
IsLocalHomeomorph.localInverseAtdefMathlib.Topology.IsLocalHomeomorph, function or constantEnglish
Assume that $f$ is a local homeomorphism. Let $x_{2}$ be an element of $X$. Then $\operatorname{localInverseAt}$ applied to $\mathrm{hf}$ and $x_{2}$ is an open partial homeomorphism of $Y$ and $X$ defined as the inverse of $\operatorname{choose}$ applied to $\mathrm{hf}$ applied to $x_{2}$.
IsLocalHomeomorph.toHomeomorphOfBijectivedefMathlib.Topology.IsLocalHomeomorph, function or constantWording
the homeomorphism of hf and hb (from the name)
English
Assume that $f$ is a local homeomorphism. Assume that $f$ is bijective. Then the homeomorphism of $\mathrm{hf}$ and $\mathrm{hb}$ is a homeomorphism of $X$ and $Y$ defined as the homeomorphism of the equivalence of $f$ and $\mathrm{hb}$.
IsLocalHomeomorphOndefMathlib.Topology.IsLocalHomeomorph, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Let $s$ be an element of $\wp X$. Then $\mathrm{IsLocalHomeomorphOn}$ holds for $f$ and $s$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then there exists an open partial homeomorphism $e$ of $X$ and $Y$, such that $x_{2}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $f$ is equal to $\operatorname{toFun'}$ applied to $e$.
JacobsonSpaceclassMathlib.Topology.JacobsonSpace, predicateWording
X is a Jacobson space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a Jacobson space.
closedPointsdefMathlib.Topology.JacobsonSpace, function or constantWording
the closed point of X (from the name)
English
Let $X$ be a set. Then the closed point of $X$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $\operatorname{singleton}$ applied to $x_{1}$ is closed.
coheightZeroSetOrderIsoIrreducibleComponentsdefMathlib.Topology.KrullDimension, function or constantEnglish
$\mathrm{coheightZeroSetOrderIsoIrreducibleComponents}$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\EqtMACRoH {\operatorname{coheight} (x_{1})}{0}$ and the set of elements of the irreducible component of $X$.
topologicalKrullDimdefMathlib.Topology.KrullDimension, function or constantWording
the Krull dimension of T (from the docstring)
English
Let $T$ be a set. Then the Krull dimension of $T$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the Krull dimension of $\operatorname{IrreducibleCloseds}$ applied to $T$.
LocallyConstant.charFndefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the characteristic function of Y and hU (from the name)
English
Let $Y$ be a set. Assume that $U$ is a clopen. Then the characteristic function of $Y$ and $\mathrm{hU}$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ defined as the indicator of $1$ and $\mathrm{hU}$.
LocallyConstant.coeFnAddMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the coercion function additive monoid homomorphism (from the name)
English
The coercion function additive monoid homomorphism is an additive monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.
LocallyConstant.coeFnAlgHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the coercion function algebra homomorphism of R (from the name)
English
Let $R$ be a set. Then the coercion function algebra homomorphism of $R$ is an algebra homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.
LocallyConstant.coeFnMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the coercion function monoid homomorphism (from the name)
English
The coercion function monoid homomorphism is a monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.
LocallyConstant.coeFnRingHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the coercion function ring homomorphism (from the name)
English
The coercion function ring homomorphism is a ring homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.
LocallyConstant.coeFnₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the coercion function of R (from the name)
English
Let $R$ be a set. Then the coercion function of $R$ is a linear map of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and the set of functions from elements of $X$ to elements of $Y$.
LocallyConstant.comapAddMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the preimage additive monoid homomorphism of f (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Then the preimage additive monoid homomorphism of $f$ is an additive monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.comapMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the preimage monoid homomorphism of f (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Then the preimage monoid homomorphism of $f$ is a monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.comapRingHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the preimage ring homomorphism of f (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Then the preimage ring homomorphism of $f$ is a ring homomorphism of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.comapₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the preimage of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a continuous map of $X$ and $Y$. Then the preimage of $R$ and $f$ is an algebra homomorphism of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.comapₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the preimage of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a continuous map of $X$ and $Y$. Then the preimage of $R$ and $f$ is a linear map of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.congrLeftRingEquivdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the congruence left ring isomorphism of e (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Then the congruence left ring isomorphism of $e$ is a ring isomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$.
LocallyConstant.congrLeftₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the left congruence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be a homeomorphism of $X$ and $Y$. Then the left congruence of $R$ and $e$ is an algebra isomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$.
LocallyConstant.congrLeftₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the left congruence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be a homeomorphism of $X$ and $Y$. Then the left congruence of $R$ and $e$ is a linear equivalence of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$ and $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$.
LocallyConstant.congrRightRingEquivdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the congruence right ring isomorphism of e (from the name)
English
Let $e$ be a ring isomorphism of $Y$ and $Z$. Then the congruence right ring isomorphism of $e$ is a ring isomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.congrRightₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the right congruence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be an algebra isomorphism of $Y$ and $Z$. Then the right congruence of $R$ and $e$ is an algebra isomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.congrRightₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the right congruence of R and e (from the name)
English
Let $R$ be a set. Let $e$ be a linear equivalence of $Y$ and $Z$. Then the right congruence of $R$ and $e$ is a linear equivalence of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.constAddMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the constant additive monoid homomorphism (from the name)
English
The constant additive monoid homomorphism is an additive monoid homomorphism of $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Y$.
LocallyConstant.constMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the constant monoid homomorphism (from the name)
English
The constant monoid homomorphism is a monoid homomorphism of $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Y$.
LocallyConstant.constRingHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the constant ring homomorphism (from the name)
English
The constant ring homomorphism is a ring homomorphism of $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Y$.
LocallyConstant.constₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the constant of R (from the name)
English
Let $R$ be a set. Then the constant of $R$ is an algebra homomorphism of $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Y$.
LocallyConstant.constₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the constant of R (from the name)
English
Let $R$ be a set. Then the constant of $R$ is a linear map of $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Y$.
LocallyConstant.evalAddMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the evaluation additive monoid homomorphism of x2 (from the name)
English
Let $x_{2}$ be an element of $X$. Then the evaluation additive monoid homomorphism of $x_{2}$ is an additive monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $Y$ defined as the composition of the evaluation additive monoid homomorphism of the function that maps $x_{3}$ to $Y$ and $x_{2}$ and the coercion function additive monoid homomorphism.
LocallyConstant.evalMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the evaluation monoid homomorphism of x2 (from the name)
English
Let $x_{2}$ be an element of $X$. Then the evaluation monoid homomorphism of $x_{2}$ is a monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $Y$ defined as the composition of the evaluation monoid homomorphism of the function that maps $x_{3}$ to $Y$ and $x_{2}$ and the coercion function monoid homomorphism.
LocallyConstant.evalRingHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the evaluation ring homomorphism of x2 (from the name)
English
Let $x_{2}$ be an element of $X$. Then the evaluation ring homomorphism of $x_{2}$ is a ring homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $Y$ defined as the composition of the evaluation ring homomorphism of the function that maps $x_{3}$ to $Y$ and $x_{2}$ and the coercion function ring homomorphism.
LocallyConstant.evalₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the evaluation of R and x4 (from the name)
English
Let $R$ be a set. Let $x_{4}$ be an element of $X$. Then the evaluation of $R$ and $x_{4}$ is an algebra homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $Y$ defined as the composition of the evaluation algebra homomorphism of the function that maps $x_{5}$ to $Y$ and $x_{4}$ and the coercion function algebra homomorphism of $R$.
LocallyConstant.evalₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the evaluation of R and x4 (from the name)
English
Let $R$ be a set. Let $x_{4}$ be an element of $X$. Then the evaluation of $R$ and $x_{4}$ is a linear map of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $Y$ defined as the composition of the projection of $x_{4}$ and the coercion function of $R$.
LocallyConstant.mapAddMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the map additive monoid homomorphism of f (from the name)
English
Let $f$ be an additive monoid homomorphism of $Y$ and $Z$. Then the map additive monoid homomorphism of $f$ is an additive monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.mapMonoidHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the map monoid homomorphism of f (from the name)
English
Let $f$ be a monoid homomorphism of $Y$ and $Z$. Then the map monoid homomorphism of $f$ is a monoid homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.mapRingHomdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the map ring homomorphism of f (from the name)
English
Let $f$ be a ring homomorphism of $Y$ and $Z$. Then the map ring homomorphism of $f$ is a ring homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.mapₐdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the map of R and f (from the name)
English
Let $R$ be a set. Let $f$ be an algebra homomorphism of $Y$ and $Z$. Then the map of $R$ and $f$ is an algebra homomorphism of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.mapₗdefMathlib.Topology.LocallyConstant.Algebra, function or constantWording
the map of R and f (from the name)
English
Let $R$ be a set. Let $f$ be a linear map of $Y$ and $Z$. Then the map of $R$ and $f$ is a linear map of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ and $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
IsLocallyConstantdefMathlib.Topology.LocallyConstant.Basic, predicateWording
f is locally constant (from the docstring)
English
generation took over the time limit
LocallyConstantstructureMathlib.Topology.LocallyConstant.Basic, typeEnglish
Let $X$ and $Y$ be sets. Then the elements of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ are a basic type.
LocallyConstant.comapdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the preimage of f and g (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Let $g$ be an element of $\mathrm{LocallyConstant}$ applied to $Y$ and $Z$. Then the preimage of $f$ and $g$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.congrLeftdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the left congruence of e (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Then the left congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{LocallyConstant} (X , Z)}{\mathrm{LocallyConstant} (Y , Z)}$.
LocallyConstant.congrRightdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the right congruence of e (from the name)
English
Let $e$ be an equivalence from $Y$ to $Z$. Then the right congruence of $e$ is an element of $\EquivMACRoAE {\mathrm{LocallyConstant} (X , Y)}{\mathrm{LocallyConstant} (X , Z)}$.
LocallyConstant.constdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the constant of X and y (from the name)
English
Let $X$ be a set. Let $y$ be an element of $Y$. Then the constant of $X$ and $y$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{const}$ applied to $X$ and $y$ and $\operatorname{const}$ applied to $y$.
LocallyConstant.descdefMathlib.Topology.LocallyConstant.Basic, function or constantEnglish
Let $f$ be a function from elements of $X$ to elements of $x$. Let $h$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $x_{1}$ such that $\operatorname{comp}$ applied to $g$ and $f$ is equal to $\operatorname{coe}$ applied to $h$. Assume that $g$ is injective. Then $\operatorname{desc}$ applied to $f$, $h$, $\mathrm{cond}$ and $\mathrm{inj}$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $x$.
LocallyConstant.equivClopensdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the equivalence clopen of X (from the name)
English
Let $X$ be a set. Then the equivalence clopen of $X$ is an equivalence from $\mathrm{LocallyConstant}$ applied to $X$ and $\mathrm{Fin}$ applied to $2$ to the set of clopens of $X$.
LocallyConstant.evaldefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the evaluation of i (from the name)
English
Let $i$ be an element of $x$. Then the evaluation of $i$ is an element of $\mathrm{LocallyConstant}$ applied to the set of functions from elements $i_{1}$ of $x$ to elements of $X$ applied to $i_{1}$ and $X$ applied to $i$.
LocallyConstant.flipdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the flip of f and a (from the name)
English
Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and the set of functions from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then the flip of $f$ and $a$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $x_{1}$ defined as the map of the function that maps $f_{1}$ to $f_{1}$ applied to $a$ and $f$.
LocallyConstant.indicatordefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the indicator of f and hU (from the name)
English
Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $R$. Assume that $U$ is a clopen. Then the indicator of $f$ and $\mathrm{hU}$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $R$.
LocallyConstant.mapdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the map of f and g (from the name)
English
Let $f$ be a function from elements of $Y$ to elements of $Z$. Let $g$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$. Then the map of $f$ and $g$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.mulIndicatordefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the multiplicative indicator of f and hU (from the name)
English
Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $R$. Assume that $U$ is a clopen. Then the multiplicative indicator of $f$ and $\mathrm{hU}$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $R$.
LocallyConstant.ofIsClopendefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the locally constant function to hU (from the docstring)
English
generation took over the time limit
LocallyConstant.piecewisedefMathlib.Topology.LocallyConstant.Basic, function or constantEnglish
Assume that $x_{1}$ is closed. Assume that $x_{2}$ is closed. Assume that $\UnionunionMACRoAB {x_{1}}{x_{2}}$ is equal to the universal set. Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $x_{1}$ and $Z$. Let $g$ be an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $x_{2}$ and $Z$ such that for all elements $x_{4}$ of $X$, for all elements $\mathrm{hx}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{inter} (x_{1} , x_{2})}{x_{4}}$, $\EqtMACRoH {f (x_{4})}{g (x_{4})}$. Then $\operatorname{piecewise}$ applied to $h$, $h_{1}$, $h_{2}$, $f$, $g$ and $\mathrm{hfg}$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Z$.
LocallyConstant.piecewise'defMathlib.Topology.LocallyConstant.Basic, function or constantEnglish
Assume that $x_{1} \leq \UnionunionMACRoAB {x_{2}}{x_{3}}$. Assume that $x_{2}$ is closed. Assume that $x_{3}$ is closed. Let $x_{4}$ be an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $x_{2}$ and $Z$. Let $x_{5}$ be an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $x_{3}$ and $Z$ such that for all elements $x_{7}$ of $X$, for all elements $\mathrm{hx}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{inter} (x_{2} , x_{3})}{x_{7}}$, $\EqtMACRoH {x_{4} (x_{7})}{x_{5} (x_{7})}$. Then $\operatorname{piecewise'}$ applied to $h$, $h_{1}$, $h_{2}$, $x_{4}$, $x_{5}$ and $\mathrm{hf}$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $x_{1}$ and $Z$.
LocallyConstant.toContinuousMapdefMathlib.Topology.LocallyConstant.Basic, function or constantWording
the continuous map of f (from the name)
English
Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$. Then the continuous map of $f$ is a continuous map of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{continuous}$ applied to $f$.
LocallyConstant.toFundefMathlib.Topology.LocallyConstant.Basic, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $Y$. Let $x_{1}$ be an element of $X$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
LocallyConstant.unflipdefMathlib.Topology.LocallyConstant.Basic, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $\mathrm{LocallyConstant}$ applied to $X$ and $x_{1}$. Then $\operatorname{unflip}$ applied to $f$ is an element of $\mathrm{LocallyConstant}$ applied to $X$ and the set of functions from elements of $x$ to elements of $x_{1}$.
LocallyFinitedefMathlib.Topology.LocallyFinite, predicateWording
f is locally finite (from the name)
English
generation took over the time limit
Function.locallyFinsuppdefMathlib.Topology.LocallyFinsupp, typeWording
locally finitely supported function of X and Y (from the name)
English
generation took over the time limit
Function.locallyFinsuppWithinstructureMathlib.Topology.LocallyFinsupp, typeEnglish
Let $U$ be an element of $\wp X$. Let $Y$ be a set. Then the elements of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ are a basic type.
Function.locallyFinsuppWithin.addSubgroupdefMathlib.Topology.LocallyFinsupp, function or constantWording
the additive subgroup of U (from the name)
English
Let $U$ be an element of $\wp X$. Then the additive subgroup of $U$ is an additive subgroup of the set of functions from elements of $X$ to elements of $Y$.
Function.locallyFinsuppWithin.addSubmonoiddefMathlib.Topology.LocallyFinsupp, function or constantWording
the additive submonoid of U (from the name)
English
Let $U$ be an element of $\wp X$. Then the additive submonoid of $U$ is an additive submonoid of the set of functions from elements of $X$ to elements of $Y$.
Function.locallyFinsuppWithin.mapRangedefMathlib.Topology.LocallyFinsupp, function or constantWording
the map range of f and g (from the name)
English
Let $f$ be a function from elements of $Y$ to elements of $Z$ such that $\EqtMACRoH {f (0)}{0}$. Let $g$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Then the map range of $f$ and $g$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Z$.
Function.locallyFinsuppWithin.mk_of_mem_addSubgroupdefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is an element of the additive subgroup of $U$. Then $\mathrm{Function\_\_locallyFinsuppWithin\_\_mk\_of\_mem\_addSubgroup}$ applied to $f$ and $\mathrm{hf}$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
Function.locallyFinsuppWithin.mk_of_mem_addSubmonoiddefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is an element of the additive submonoid of $U$. Then $\mathrm{Function\_\_locallyFinsuppWithin\_\_mk\_of\_mem\_addSubmonoid}$ applied to $f$ and $\mathrm{hf}$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
Function.locallyFinsuppWithin.restrictdefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $D$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Assume that $V \leq U$. Then $\operatorname{restrict}$ applied to $D$ and $h$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $V$ and $Y$.
Function.locallyFinsuppWithin.restrictLatticeHomdefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Assume that $V \leq U$. Then $\operatorname{restrictLatticeHom}$ applied to $h$ is a lattice homomorphism of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ and $\operatorname{locallyFinsuppWithin}$ applied to $V$ and $Y$.
Function.locallyFinsuppWithin.restrictMonoidHomdefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Assume that $V \leq U$. Then $\operatorname{restrictMonoidHom}$ applied to $h$ is an additive monoid homomorphism of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ and $\operatorname{locallyFinsuppWithin}$ applied to $V$ and $Y$.
Function.locallyFinsuppWithin.restrictOrderMonoidHomdefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Assume that $V \leq U$. Then $\operatorname{restrictOrderMonoidHom}$ applied to $h$ is an order additive monoid homomorphism of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ and $\operatorname{locallyFinsuppWithin}$ applied to $V$ and $Y$.
Function.locallyFinsuppWithin.singledefMathlib.Topology.LocallyFinsupp, function or constantEnglish
generation took over the time limit
Function.locallyFinsuppWithin.supportdefMathlib.Topology.LocallyFinsupp, function or constantWording
the support of D (from the name)
English
Let $D$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Then the support of $D$ is an element of $\wp X$ defined as the support of $\operatorname{coe}$ applied to $D$.
Function.locallyFinsuppWithin.supporteddefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $Y$ be a set. Let $U$ and $s$ be elements of $\wp X$. Then $\operatorname{supported}$ applied to $Y$, $U$ and $s$ is an additive subgroup of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
Function.locallyFinsuppWithin.toFundefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Let $x_{2}$ be an element of $X$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
Function.locallyFinsuppWithin.truncatedefMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $D$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Let $y$ be an element of $Y$ such that $0 \leq y$. Then $\operatorname{truncate}$ applied to $D$, $y$ and $\mathrm{hy}$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
Function.locallyFinsuppWithin.truncateLatticeHomdefMathlib.Topology.LocallyFinsupp, function or constantWording
the truncate lattice homomorphism of U and y (from the name)
English
Let $U$ be an element of $\wp X$. Let $y$ be an element of $Y$ such that $0 \leq y$. Then the truncate lattice homomorphism of $U$ and $y$ is a lattice homomorphism of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ and $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
Function.locallyFinsuppWithin.truncateOrderHomdefMathlib.Topology.LocallyFinsupp, function or constantWording
the truncate order homomorphism of U and y (from the name)
English
Let $U$ be an element of $\wp X$. Let $y$ be an element of $Y$ such that $0 \leq y$. Then the truncate order homomorphism of $U$ and $y$ is an order homomorphism of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ and $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$ defined as $\operatorname{mk}$ applied to the function that maps $D$ to $\operatorname{truncate}$ applied to $D$, $y$ and $\mathrm{hy}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Function\_\_locallyFinsuppWithin\_\_truncate\_mono}$ applied to $y$ and $\mathrm{hy}$.
Function.locallyFinsuppWithin.truncate₁defMathlib.Topology.LocallyFinsupp, function or constantEnglish
Let $D$ be an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$. Then $\mathrm{Function\_\_locallyFinsuppWithin\_\_truncate\_u2081\_}$ applied to $D$ is an element of $\operatorname{locallyFinsuppWithin}$ applied to $U$ and $Y$.
LocallyFiniteSupportdefMathlib.Topology.LocallyFinsupp, predicateWording
f is a locally finite support (from the name)
English
generation took over the time limit
Function.locallyFinsupp.mapdefMathlib.Topology.LocallyFinsupp.Pushforward, function or constantWording
the map of w and c (from the name)
English
generation took over the time limit
IsProperMapstructureMathlib.Topology.Maps.Proper.Basic, predicateWording
f is a proper map (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $f$ is a proper map.
Homeomorph.quotientKerEquivRangedefMathlib.Topology.Maps.Strict.Basic, function or constantWording
the quotient kernel equivalence range of hf (from the name)
English
Assume that $f$ is a strict map. Then the quotient kernel equivalence range of $\mathrm{hf}$ is a homeomorphism of $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $f$ and the set of elements of the range of $f$.
Topology.IsStrictMapdefMathlib.Topology.Maps.Strict.Basic, predicateWording
f is a strict map (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is a strict map, if $\operatorname{rangeFactorization}$ applied to $f$ is a quotient map.
ContinuousAddEquiv.quotientKerEquivRangedefMathlib.Topology.Maps.Strict.Group, function or constantWording
the quotient kernel equivalence range of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to $f$ is a strict map. Then the quotient kernel equivalence range of $\mathrm{hf}$ is a continuous additive equivalence of the set of quotients of $G$ and the additive kernel of $f$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{4}})}$.
ContinuousMulEquiv.quotientKerEquivRangedefMathlib.Topology.Maps.Strict.Group, function or constantWording
the quotient kernel equivalence range of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to $f$ is a strict map. Then the quotient kernel equivalence range of $\mathrm{hf}$ is a continuous multiplicative equivalence of the set of quotients of $G$ and the multiplicative kernel of $f$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{4}})}$.
ContinuousLinearEquiv.quotKerEquivRangedefMathlib.Topology.Maps.Strict.Module, function or constantWording
the quotient kernel equivalence range of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to $x_{6}$ is a strict map. Then the quotient kernel equivalence range of $\mathrm{hf}$ is a continuous linear equivalence of the set of quotients of $M$ and the kernel of $x_{6}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{range} (x_{6})}{x_{9}})}$.
IsBoundedSMulclassMathlib.Topology.MetricSpace.Algebra, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{IsBoundedSMul}$ holds for $x$ and $x_{1}$.
LipschitzAddclassMathlib.Topology.MetricSpace.Algebra, predicateWording
x is a Lipschitz sum (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a Lipschitz sum.
LipschitzAdd.CdefMathlib.Topology.MetricSpace.Algebra, function or constantEnglish
Let $x$ be a set. Then $\operatorname{C}$ applied to $x$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{choose}$ applied to $\mathrm{LipschitzAdd\_\_lipschitz\_add}$.
LipschitzMulclassMathlib.Topology.MetricSpace.Algebra, predicateWording
x is a Lipschitz product (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a Lipschitz product.
LipschitzMul.CdefMathlib.Topology.MetricSpace.Algebra, function or constantEnglish
Let $x$ be a set. Then $\operatorname{C}$ applied to $x$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{choose}$ applied to $\mathrm{LipschitzMul\_\_lipschitz\_mul}$.
AntilipschitzWithdefMathlib.Topology.MetricSpace.Antilipschitz, predicateEnglish
Let $K$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{AntilipschitzWith}$ holds for $K$ and $f$, if for all elements $x_{4}$ and $y$ of $x$, the extended distance of $x_{4}$ and $y$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $K$ and the extended distance of $f$ applied to $x_{4}$ and $f$ applied to $y$.
AntilipschitzWith.kdefMathlib.Topology.MetricSpace.Antilipschitz, function or constantEnglish
Assume that $\mathrm{AntilipschitzWith}$ holds for $K$ and $f$. Then $\operatorname{k}$ applied to $\mathrm{\_hf}$ is an element of $\mathrm{NNReal}$ defined as $K$.
Metric.diamdefMathlib.Topology.MetricSpace.Bounded, function or constantWording
the diameter of s (from the docstring)
English
Let $s$ be an element of $\wp x$. Then the diameter of $s$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{ediam}$ applied to $s$.
PseudoMetricstructureMathlib.Topology.MetricSpace.BundledFun, typeEnglish
Let $X$ and $R$ be sets. Then the elements of $\mathrm{PseudoMetric}$ applied to $X$ and $R$ are a basic type.
PseudoMetric.IsUltraclassMathlib.Topology.MetricSpace.BundledFun, predicateEnglish
Let $d$ be an element of $\mathrm{PseudoMetric}$ applied to $X$ and $R$. Then we can say that $\operatorname{IsUltra}$ holds for $d$.
PseudoMetric.toFundefMathlib.Topology.MetricSpace.BundledFun, function or constantEnglish
Let $\mathrm{self}$ be an element of $\mathrm{PseudoMetric}$ applied to $X$ and $R$. Let $x_{3}$ and $x_{4}$ be elements of $X$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.
CantorScheme.AntitonedefMathlib.Topology.MetricSpace.CantorScheme, predicateWording
A is a antitone (from the name)
English
Let $A$ be a function from lists of elements of $x$ to elements of $\wp x_{1}$. Then $A$ is an antitone, if for all lists $l$ of elements of $x$, for all elements $a$ of $x$, $A (\operatorname{cons} (a , l))\leq A (l)$.
CantorScheme.ClosureAntitonedefMathlib.Topology.MetricSpace.CantorScheme, predicateWording
A is a closure antitone (from the name)
English
Let $A$ be a function from lists of elements of $x$ to elements of $\wp x_{1}$. Then $A$ is a closure antitone, if for all lists $l$ of elements of $x$, for all elements $a$ of $x$, the closure of $A$ applied to $\operatorname{cons}$ applied to $a$ and $l$ is less than or equal to $A$ applied to $l$.
CantorScheme.DisjointdefMathlib.Topology.MetricSpace.CantorScheme, predicateWording
A is disjoint (from the docstring)
English
Let $A$ be a function from lists of elements of $x$ to elements of $\wp x_{1}$. Then $A$ is disjoint, if for all lists $l$ of elements of $x$, the function that maps $a$ and $b$ to the proposition that $A$ applied to $\operatorname{cons}$ applied to $a$ and $l$ is disjoint to $A$ applied to $\operatorname{cons}$ applied to $b$ and $l$ is pairwise.
CantorScheme.VanishingDiamdefMathlib.Topology.MetricSpace.CantorScheme, predicateEnglish
Let $A$ be a function from lists of elements of $x$ to elements of $\wp x_{1}$. Then $\operatorname{VanishingDiam}$ holds for $A$, if for all functions $x_{3}$ from natural numbers to elements of $x$, $\operatorname{Tendsto}$ holds for the function that maps $n$ to $\operatorname{ediam}$ applied to $A$ applied to the restriction of $x_{3}$ and $n$, $\operatorname{atTop}$ and the neighbourhood filter of $0$.
CantorScheme.inducedMapdefMathlib.Topology.MetricSpace.CantorScheme, function or constantWording
the induced map of A (from the name)
English
Let $A$ be a function from lists of elements of $x$ to elements of $\wp x_{1}$. Then the induced map of $A$ is an element of $\Sigma$ applied to the function that maps $s$ to the set of functions from elements of $s$ to elements of $x_{1}$.
CongruentdefMathlib.Topology.MetricSpace.Congruence, predicateWording
x5 is congruent to x6 (from the name)
English
Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{6}$ be a function from elements of $x$ to elements of $x_{2}$. Then $x_{5}$ is congruent to $x_{6}$, if for all elements $x_{7}$ and $x_{8}$ of $x$, the extended distance of $x_{5}$ applied to $x_{7}$ and $x_{5}$ applied to $x_{8}$ is equal to the extended distance of $x_{6}$ applied to $x_{7}$ and $x_{6}$ applied to $x_{8}$.
ContractingWithdefMathlib.Topology.MetricSpace.Contracting, predicateEnglish
Let $K$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $x$ to elements of $x$. Then $\mathrm{ContractingWith}$ holds for $K$ and $f$, if $K < 1$ and $\mathrm{LipschitzWith}$ holds for $K$ and $f$.
ContractingWith.efixedPointdefMathlib.Topology.MetricSpace.Contracting, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$ such that $\mathrm{ContractingWith}$ holds for $K$ and $f$. Let $x_{2}$ be an element of $x$ such that the extended distance of $x_{2}$ and $f$ applied to $x_{2}$ is distinct from the top. Then $\operatorname{efixedPoint}$ applied to $f$, $\mathrm{hf}$, $x_{2}$ and $\mathrm{hx}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{ContractingWith\_\_exists\_fixedPoint}$ applied to $\mathrm{hf}$, $x_{2}$ and $\mathrm{hx}$.
ContractingWith.efixedPoint'defMathlib.Topology.MetricSpace.Contracting, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$. Assume that $s$ is complete. Assume that $\operatorname{MapsTo}$ holds for $f$, $s$ and $s$. Assume that $\mathrm{ContractingWith}$ holds for $K$ and $\operatorname{restrict}$ applied to $f$, $s$, $s$ and $\mathrm{hsf}$. Let $x_{2}$ be an element of $x$ such that $x_{2}$ is an element of $s$ and the extended distance of $x_{2}$ and $f$ applied to $x_{2}$ is distinct from the top. Then $\operatorname{efixedPoint'}$ applied to $f$, $\mathrm{hsc}$, $\mathrm{hsf}$, $\mathrm{hf}$, $x_{2}$, $\mathrm{hxs}$ and $\mathrm{hx}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{ContractingWith\_\_exists\_fixedPoint'}$ applied to $\mathrm{hsc}$, $\mathrm{hsf}$, $\mathrm{hf}$, $\mathrm{hxs}$ and $\mathrm{hx}$.
ContractingWith.fixedPointdefMathlib.Topology.MetricSpace.Contracting, function or constantWording
the unique fixed point of f and hf (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x$ such that $\mathrm{ContractingWith}$ holds for $K$ and $f$. Then the unique fixed point of $f$ and $\mathrm{hf}$ is an element of $x$.
Metric.IsCoverdefMathlib.Topology.MetricSpace.Cover, predicateEnglish
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $s$ and $N$ be elements of $\wp X$. Then we can say that $\operatorname{IsCover}$ holds for $x_{1}$, $s$ and $N$.
Metric.HasCoveringExponentstructureMathlib.Topology.MetricSpace.CoveringExponent, predicateEnglish
Let $A$ be an element of $\wp T$. Let $c$ be an element of $\mathrm{ENNReal}$. Let $d$ be a real number. Then we can say that $\operatorname{HasCoveringExponent}$ holds for $A$, $c$ and $d$.
Metric.coveringNumberdefMathlib.Topology.MetricSpace.CoveringNumbers, function or constantWording
the covering number of x1 and A (from the name)
English
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $A$ be an element of $\wp X$. Then the covering number of $x_{1}$ and $A$ is a natural number defined as the infimum of the function that maps $C$ to the infimum of the function that maps $h$ to the infimum of the function that maps $h_{1}$ to the cardinality in $C$.
Metric.externalCoveringNumberdefMathlib.Topology.MetricSpace.CoveringNumbers, function or constantWording
the external covering number of x1 and A (from the docstring)
English
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $A$ be an element of $\wp X$. Then the external covering number of $x_{1}$ and $A$ is a natural number defined as the infimum of the function that maps $C$ to the infimum of the function that maps $h$ to the cardinality in $C$.
Metric.maximalSeparatedSetdefMathlib.Topology.MetricSpace.CoveringNumbers, function or constantWording
the maximal separated set of x1 and A (from the name)
English
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $A$ be an element of $\wp X$. Then the maximal separated set of $x_{1}$ and $A$ is an element of $\wp X$ defined as $\mathrm{dite}$ applied to the proposition that $\operatorname{packingNumber}$ applied to $x_{1}$ and $A$ is distinct from the top, the function that maps $h$ to $\operatorname{choose}$ applied to $\mathrm{Metric\_\_exists\_set\_encard\_eq\_packingNumber}$ applied to $h$ and the function that maps $h_{1}$ to $\operatorname{emptyCollection}$.
Metric.minimalCoverdefMathlib.Topology.MetricSpace.CoveringNumbers, function or constantWording
the minimal cover of x1 and A (from the name)
English
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $A$ be an element of $\wp X$. Then the minimal cover of $x_{1}$ and $A$ is an element of $\wp X$ defined as $\mathrm{dite}$ applied to the proposition that the covering number of $x_{1}$ and $A$ is distinct from the top, the function that maps $h$ to $\operatorname{choose}$ applied to $\mathrm{Metric\_\_exists\_set\_encard\_eq\_coveringNumber}$ applied to $h$ and the function that maps $h_{1}$ to $\operatorname{emptyCollection}$.
Metric.packingNumberdefMathlib.Topology.MetricSpace.CoveringNumbers, function or constantEnglish
Let $x_{1}$ be an element of $\mathrm{NNReal}$. Let $A$ be an element of $\wp X$. Then $\operatorname{packingNumber}$ applied to $x_{1}$ and $A$ is a natural number defined as the supremum of the function that maps $C$ to the supremum of the function that maps $h$ to the supremum of the function that maps $h_{1}$ to the cardinality in $C$.
MetricSpaceclassMathlib.Topology.MetricSpace.Defs, predicateWording
x is a metric space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a metric space.
DilationstructureMathlib.Topology.MetricSpace.Dilation, typeWording
dilation of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the dilations of $x$ and $x_{1}$ are a basic type.
Dilation.compdefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a dilation of $x_{1}$ and $x_{2}$. Let $f$ be a dilation of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a dilation of $x$ and $x_{2}$.
Dilation.copydefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a dilation 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 dilation of $x$ and $x_{1}$.
Dilation.iddefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the identity of x (from the docstring)
English
Let $x$ be a set. Then the identity of $x$ is a dilation of $x$ and $x$.
Dilation.mkOfDistEqdefMathlib.Topology.MetricSpace.Dilation, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that there exists an element $r$ of $\mathrm{NNReal}$, such that $r \neq 0$ and for all elements $x_{4}$ of $x$, for all elements $y$ of $x$, the distance of $f$ applied to $x_{4}$ and $f$ applied to $y$ is equal to the product of $\operatorname{toReal}$ applied to $r$ and the distance of $x_{4}$ and $y$. Then $\operatorname{mkOfDistEq}$ applied to $f$ and $h$ is a dilation of $x$ and $x_{1}$.
Dilation.mkOfNNDistEqdefMathlib.Topology.MetricSpace.Dilation, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that there exists an element $r$ of $\mathrm{NNReal}$, such that $r \neq 0$ and for all elements $x_{4}$ of $x$, for all elements $y$ of $x$, the distance of $f$ applied to $x_{4}$ and $f$ applied to $y$ is equal to the product of $r$ and the distance of $x_{4}$ and $y$. Then $\operatorname{mkOfNNDistEq}$ applied to $f$ and $h$ is a dilation of $x$ and $x_{1}$.
Dilation.ratiodefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the ratio of f (from the docstring)
English
Let $f$ be an element of $F$. Then the ratio of $f$ is an element of $\mathrm{NNReal}$ defined as $\iteMACRoG {\mathrm{forall} (x , \lambda x_{5} . \mathrm{forall} (x , \lambda y . \mathrm{or} (\EqtMACRoH {\operatorname{edist} (x_{5} , y)}{0}, \EqtMACRoH {\operatorname{edist} (x_{5} , y)}{\operatorname{top}})))}{1}{\operatorname{choose} (\mathrm{DilationClass\_\_edist\_eq'} (f))}$.
Dilation.ratioHomdefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the ratio homomorphism (from the name)
English
The ratio homomorphism is a monoid homomorphism of the set of dilations of $x$ and $x$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ratio}$ and $\mathrm{Dilation\_\_ratio\_one}$ and $\mathrm{Dilation\_\_ratio\_mul}$.
Dilation.toFundefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the dilation of self and x4 (from the name)
English
Let $\mathrm{self}$ be a dilation of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the dilation of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
DilationClassclassMathlib.Topology.MetricSpace.Dilation, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{DilationClass}$ holds for $F$, $x$ and $x_{1}$.
Isometry.toDilationdefMathlib.Topology.MetricSpace.Dilation, function or constantWording
the dilation of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is an isometry. Then the dilation of $f$ and $\mathrm{hf}$ is a dilation of $x$ and $x_{1}$.
DilationEquivstructureMathlib.Topology.MetricSpace.DilationEquiv, typeWording
dilation equivalence of X and Y (from the name)
English
Let $X$ and $Y$ be sets. Then the dilation equivalences of $X$ and $Y$ are a basic type.
DilationEquiv.ratioHomdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the ratio homomorphism (from the name)
English
The ratio homomorphism is a monoid homomorphism of the set of dilation equivalences of $X$ and $X$ and $\mathrm{NNReal}$.
DilationEquiv.refldefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the identity of X (from the name)
English
Let $X$ be a set. Then the identity of $X$ is a dilation equivalence of $X$ and $X$.
DilationEquiv.symmdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the inverse of e (from the name)
English
Let $e$ be a dilation equivalence of $X$ and $Y$. Then the inverse of $e$ is a dilation equivalence of $Y$ and $X$.
DilationEquiv.toDilationdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the dilation of self (from the name)
English
Let $\mathrm{self}$ be a dilation equivalence of $X$ and $Y$. Then the dilation of $\mathrm{self}$ is a dilation of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to $\mathrm{self}$ and $\mathrm{DilationEquiv\_\_edist\_eq'}$ applied to $\mathrm{self}$.
DilationEquiv.toHomeomorphdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be a dilation equivalence of $X$ and $Y$. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$.
DilationEquiv.toPermdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the permutation (from the name)
English
The permutation is a monoid homomorphism of the set of dilation equivalences of $X$ and $X$ and the set of permutations of $X$.
DilationEquiv.transdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the composition of x3 and x4 (from the name)
English
Let $x_{3}$ be a dilation equivalence of $X$ and $Y$. Let $x_{4}$ be a dilation equivalence of $Y$ and $Z$. Then the composition of $x_{3}$ and $x_{4}$ is a dilation equivalence of $X$ and $Z$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toEquiv}$ applied to $x_{3}$ and $\operatorname{toEquiv}$ applied to $x_{4}$ and $\mathrm{Dilation\_\_edist\_eq'}$ applied to the composition of the dilation of $x_{4}$ and the dilation of $x_{3}$.
DilationEquivClassclassMathlib.Topology.MetricSpace.DilationEquiv, predicateEnglish
Let $F$ be a set. Let $X$ and $Y$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{DilationEquivClass}$ holds for $F$, $X$ and $Y$.
IsometryEquiv.toDilationEquivdefMathlib.Topology.MetricSpace.DilationEquiv, function or constantWording
the dilation equivalence of e (from the name)
English
Let $e$ be an isometry equivalence of $X$ and $Y$. Then the dilation equivalence of $e$ is a dilation equivalence of $X$ and $Y$.
Metric.GlueSpacedefMathlib.Topology.MetricSpace.Gluing, typeWording
glue space of h1 and h2 (from the name)
English
Assume that $x_{3}$ is an isometry. Assume that $x_{4}$ is an isometry. Then a glue space of $h_{1}$ and $h_{2}$ is an element of the function that maps $h_{1}$ and $h_{2}$ to the set of separation quotients of $\mathrm{Sum}$ applied to $X$ and $Y$.
Metric.InductiveLimitdefMathlib.Topology.MetricSpace.Gluing, typeWording
inductive limit of I (from the name)
English
Assume that for all natural numbers $n$, $f$ applied to $n$ is an isometry. Then an inductive limit of $I$ is an element of the function that maps $I$ to the set of separation quotients of $\Sigma$ applied to the function that maps $n$ to $X$ applied to $n$.
Metric.Sigma.distdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the distance of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $E$ applied to $i_{1}$. Let $x_{3}$ be an element of $\Sigma$ applied to the function that maps $i$ to $E$ applied to $i$. Then the distance of $x_{2}$ and $x_{3}$ is a real number.
Metric.Sum.distdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the distance of x2 and x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Sum}$ applied to $X$ and $Y$. Then the distance of $x_{2}$ and $x_{3}$ is a real number.
Metric.glueDistdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the glue distance of x5 and x6 (from the name)
English
Let $x_{2}$ be a function from elements of $Z$ to elements of $X$. Let $x_{3}$ be a function from elements of $Z$ to elements of $Y$. Let $x_{4}$ be a real number. Let $x_{5}$ and $x_{6}$ be elements of $\mathrm{Sum}$ applied to $X$ and $Y$. Then the glue distance of $x_{5}$ and $x_{6}$ is a real number.
Metric.inductiveLimitDistdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the inductive limit distance of n2 and x1 (from the name)
English
Let $f$ be a function from natural numbers $n_{2}$ and elements of $X$ applied to $n_{2}$ to elements of $X$ applied to $n_{2} + 1$. Let $x_{1}$ be an element of $\Sigma$ applied to the function that maps $n_{1}$ to $X$ applied to $n_{1}$. Let $y$ be an element of $\Sigma$ applied to the function that maps $n$ to $X$ applied to $n$. Then the inductive limit distance of $f$ and $x_{1}$ is a real number.
Metric.toGlueLdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the glue of x5 (from the name)
English
Assume that $x_{3}$ is an isometry. Assume that $x_{4}$ is an isometry. Let $x_{5}$ be an element of $X$. Then the glue of $x_{5}$ is a glue space of $h_{1}$ and $h_{2}$ defined as $\operatorname{mk''}$ applied to $\operatorname{inl}$ applied to $x_{5}$.
Metric.toGlueRdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the glue of y (from the name)
English
Assume that $x_{3}$ is an isometry. Assume that $x_{4}$ is an isometry. Let $y$ be an element of $Y$. Then the glue of $y$ is a glue space of $h_{1}$ and $h_{2}$ defined as $\operatorname{mk''}$ applied to $\operatorname{inr}$ applied to $y$.
Metric.toInductiveLimitdefMathlib.Topology.MetricSpace.Gluing, function or constantWording
the inductive limit of n and x1 (from the name)
English
Assume that for all natural numbers $n_{1}$, $f$ applied to $n_{1}$ is an isometry. Let $n$ be a natural number. Let $x_{1}$ be an element of $X$ applied to $n$. Then the inductive limit of $n$ and $x_{1}$ is an inductive limit of $I$ defined as $\operatorname{mk''}$ applied to $\operatorname{mk}$ applied to $n$ and $x_{1}$.
GromovHausdorff.AuxGluingStruct.SpacedefMathlib.Topology.MetricSpace.GromovHausdorff, typeWording
space of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{AuxGluingStruct}$ applied to $A$. Then a space of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
GromovHausdorff.AuxGluingStruct.embeddefMathlib.Topology.MetricSpace.GromovHausdorff, function or constantWording
the embed of self and x1 (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{AuxGluingStruct}$ applied to $A$. Let $x_{1}$ be an element of $A$. Then the embed of $\mathrm{self}$ and $x_{1}$ is a space of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{1}$.
GromovHausdorff.GHSpacedefMathlib.Topology.MetricSpace.GromovHausdorff, typeEnglish
An element of $\operatorname{GHSpace}$ is an element of $\mathrm{Quotient}$ applied to $\operatorname{setoid}$.
GromovHausdorff.GHSpace.RepdefMathlib.Topology.MetricSpace.GromovHausdorff, typeWording
representation of p (from the name)
English
Let $p$ be an element of $\operatorname{GHSpace}$. Then a representation of $p$ is an element of the function that maps $p$ to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{out} (p)}{x})}$.
GromovHausdorff.ghDistdefMathlib.Topology.MetricSpace.GromovHausdorff, function or constantEnglish
Let $X$ and $Y$ be sets. Then $\operatorname{ghDist}$ applied to $X$ and $Y$ is a real number defined as the distance of $\operatorname{toGHSpace}$ applied to $X$ and $\operatorname{toGHSpace}$ applied to $Y$.
GromovHausdorff.toGHSpacedefMathlib.Topology.MetricSpace.GromovHausdorff, function or constantEnglish
Let $X$ be a set. Then $\operatorname{toGHSpace}$ applied to $X$ is an element of $\operatorname{GHSpace}$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ and the Kuratowski embedding of $X$.
TopologicalSpace.NonemptyCompacts.toGHSpacedefMathlib.Topology.MetricSpace.GromovHausdorff, function or constantEnglish
Let $p$ be a nonempty compact of $X$. Then $\operatorname{toGHSpace}$ applied to $p$ is an element of $\operatorname{GHSpace}$ defined as $\operatorname{toGHSpace}$ applied to $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {p}{x_{1}})}$.
GromovHausdorff.HDdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $f$ be an element of $\mathrm{\_private\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_GromovHausdorffRealized\_\_0\_\_GromovHausdorff\_\_Cb}$ applied to $X$ and $Y$. Then $\operatorname{HD}$ applied to $f$ is a real number defined as the maximum of the supremum of the function that maps $x_{2}$ to the infimum of the function that maps $y$ to $f$ applied to $\ProdmkMACRoU {\operatorname{inl} (x_{2})}{\operatorname{inr} (y)}$ and the supremum of the function that maps $y_{1}$ to the infimum of the function that maps $x_{3}$ to $f$ applied to $\ProdmkMACRoU {\operatorname{inl} (x_{3})}{\operatorname{inr} (y_{1})}$.
GromovHausdorff.OptimalGHCouplingdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, typeEnglish
Let $X$ and $Y$ be sets. Then an element of $\operatorname{OptimalGHCoupling}$ applied to $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to the set of separation quotients of $\mathrm{Sum}$ applied to $X$ and $Y$.
GromovHausdorff.candidatesdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $X$ and $Y$ be sets. Then $\operatorname{candidates}$ applied to $X$ and $Y$ is an element of $\wp \mathrm{\_private\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_GromovHausdorffRealized\_\_0\_\_GromovHausdorff\_\_ProdSpaceFun} (X , Y)$.
GromovHausdorff.candidatesBDistdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $X$ and $Y$ be sets. Then $\operatorname{candidatesBDist}$ applied to $X$ and $Y$ is an element of $\mathrm{\_private\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_GromovHausdorffRealized\_\_0\_\_GromovHausdorff\_\_Cb}$ applied to $X$ and $Y$.
GromovHausdorff.candidatesBOfCandidatesdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $f$ be an element of $\mathrm{\_private\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_GromovHausdorffRealized\_\_0\_\_GromovHausdorff\_\_ProdSpaceFun}$ applied to $X$ and $Y$ such that $\MembershipmemMACRoT {\operatorname{candidates} (X , Y)}{f}$. Then $\operatorname{candidatesBOfCandidates}$ applied to $f$ and $\mathrm{fA}$ is an element of $\mathrm{\_private\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_GromovHausdorffRealized\_\_0\_\_GromovHausdorff\_\_Cb}$ applied to $X$ and $Y$.
GromovHausdorff.optimalGHInjldefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $X$ and $Y$ be sets. Let $x_{2}$ be an element of $X$. Then $\operatorname{optimalGHInjl}$ applied to $X$, $Y$ and $x_{2}$ is an element of $\operatorname{OptimalGHCoupling}$ applied to $X$ and $Y$ defined as $\operatorname{mk''}$ applied to $\operatorname{inl}$ applied to $x_{2}$.
GromovHausdorff.optimalGHInjrdefMathlib.Topology.MetricSpace.GromovHausdorffRealized, function or constantEnglish
Let $X$ and $Y$ be sets. Let $y$ be an element of $Y$. Then $\operatorname{optimalGHInjr}$ applied to $X$, $Y$ and $y$ is an element of $\operatorname{OptimalGHCoupling}$ applied to $X$ and $Y$ defined as $\operatorname{mk''}$ applied to $\operatorname{inr}$ applied to $y$.
Metric.gromovProductdefMathlib.Topology.MetricSpace.GromovProduct, function or constantEnglish
Let $x_{1}$, $y$ and $z$ be elements of $X$. Then $\operatorname{gromovProduct}$ applied to $x_{1}$, $y$ and $z$ is a real number defined as the quotient of the difference between the sum of the distance of $x_{1}$ and $y$ and the distance of $x_{1}$ and $z$ and the distance of $y$ and $z$ and $2$.
Real.fromBinarydefMathlib.Topology.MetricSpace.HausdorffAlexandroff, function or constantEnglish
Let $x$ be a function from natural numbers to elements of $\mathrm{Bool}$. Then $\operatorname{fromBinary}$ applied to $x$ is an element of the unit interval.
cantorToHilbertdefMathlib.Topology.MetricSpace.HausdorffAlexandroff, function or constantEnglish
Let $x$ be a function from natural numbers to elements of $\mathrm{Bool}$. Let $x_{1}$ be a natural number. Then $\mathrm{cantorToHilbert}$ applied to $x$ and $x_{1}$ is an element of the unit interval defined as the map of $\operatorname{cantorSpaceHomeomorphNatToCantorSpace}$ applied to $x$ and $x_{1}$.
dimHdefMathlib.Topology.MetricSpace.HausdorffDimension, function or constantWording
the dimension of s (from the name)
English
Let $s$ be an element of $\wp X$. Then the dimension of $s$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $d$ to the supremum of the function that maps $h$ to $\operatorname{ofNNReal}$ applied to $d$.
Metric.hausdorffDistdefMathlib.Topology.MetricSpace.HausdorffDistance, function or constantWording
the Hausdorff distance of s and t (from the name)
English
Let $s$ and $t$ be elements of $\wp x$. Then the Hausdorff distance of $s$ and $t$ is a real number defined as $\operatorname{toReal}$ applied to the Hausdorff distance of $s$ and $t$.
Metric.hausdorffEDistdefMathlib.Topology.MetricSpace.HausdorffDistance, function or constantWording
the Hausdorff distance of s and t (from the name)
English
Let $s$ and $t$ be elements of $\wp x$. Then the Hausdorff distance of $s$ and $t$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{Metric\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_HausdorffDistance\_\_433595793\_\_\_hygCtx\_\_\_hyg\_\_2}$, $s$ and $t$.
Metric.infDistdefMathlib.Topology.MetricSpace.HausdorffDistance, function or constantWording
the minimal distance of x2 and s (from the docstring)
English
Let $x_{2}$ be an element of $x$. Let $s$ be an element of $\wp x$. Then the minimal distance of $x_{2}$ and $s$ is a real number defined as $\operatorname{toReal}$ applied to the infimum distance of $x_{2}$ and $s$.
Metric.infEDistdefMathlib.Topology.MetricSpace.HausdorffDistance, function or constantWording
the infimum distance of x2 and s (from the name)
English
Let $x_{2}$ be an element of $x$. Let $s$ be an element of $\wp x$. Then the infimum distance of $x_{2}$ and $s$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $y$ to the infimum of the function that maps $h$ to the extended distance of $x_{2}$ and $y$.
Metric.infNndistdefMathlib.Topology.MetricSpace.HausdorffDistance, function or constantWording
the minimal distance of x2 and s (from the docstring)
English
Let $x_{2}$ be an element of $x$. Let $s$ be an element of $\wp x$. Then the minimal distance of $x_{2}$ and $s$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toNNReal}$ applied to the infimum distance of $x_{2}$ and $s$.
HolderOnWithdefMathlib.Topology.MetricSpace.Holder, predicateEnglish
Let $C$ and $r$ be elements of $\mathrm{NNReal}$. Let $f$ be a function from elements of $X$ to elements of $Y$. Let $s$ be an element of $\wp X$. Then $\mathrm{HolderOnWith}$ holds for $C$, $r$, $f$ and $s$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then for all elements $y$ of $X$, if $y$ is an element of $s$, then the extended distance of $f$ applied to $x_{2}$ and $f$ applied to $y$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $C$ and the exponentiation of the extended distance of $x_{2}$ and $y$ to $\operatorname{toReal}$ applied to $r$.
HolderWithdefMathlib.Topology.MetricSpace.Holder, predicateEnglish
Let $C$ and $r$ be elements of $\mathrm{NNReal}$. Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{HolderWith}$ holds for $C$, $r$ and $f$, if for all elements $x_{2}$ and $y$ of $X$, the extended distance of $f$ applied to $x_{2}$ and $f$ applied to $y$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $C$ and the exponentiation of the extended distance of $x_{2}$ and $y$ to $\operatorname{toReal}$ applied to $r$.
MemHolderdefMathlib.Topology.MetricSpace.HolderNorm, predicateEnglish
Let $r$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{MemHolder}$ holds for $r$ and $f$, if there exists an element $C$ of $\mathrm{NNReal}$, such that $\mathrm{HolderWith}$ holds for $C$, $r$ and $f$.
eHolderNormdefMathlib.Topology.MetricSpace.HolderNorm, function or constantWording
the Holder norm of r and f (from the name)
English
Let $r$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $X$ to elements of $Y$. Then the Holder norm of $r$ and $f$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $C$ to the infimum of the function that maps $h$ to $\operatorname{ofNNReal}$ applied to $C$.
nnHolderNormdefMathlib.Topology.MetricSpace.HolderNorm, function or constantWording
the nonnegative Holder norm of r and f (from the name)
English
Let $r$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $X$ to elements of $Y$. Then the nonnegative Holder norm of $r$ and $f$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toNNReal}$ applied to the Holder norm of $r$ and $f$.
Set.einfsepdefMathlib.Topology.MetricSpace.Infsep, function or constantEnglish
Let $s$ be an element of $\wp x$. Then $\operatorname{einfsep}$ applied to $s$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $x_{2}$ to the infimum of the function that maps $h$ to the infimum of the function that maps $y$ to the infimum of the function that maps $h_{1}$ to the infimum of the function that maps $h_{2}$ to the extended distance of $x_{2}$ and $y$.
Set.infsepdefMathlib.Topology.MetricSpace.Infsep, function or constantEnglish
Let $s$ be an element of $\wp x$. Then $\operatorname{infsep}$ applied to $s$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{einfsep}$ applied to $s$.
IsIsometricSMulclassMathlib.Topology.MetricSpace.IsometricSMul, predicateWording
M is isometric (from the docstring)
English
Let $M$ and $X$ be sets. Then we can say that $M$ is isometric.
IsIsometricVAddclassMathlib.Topology.MetricSpace.IsometricSMul, predicateWording
M is isometric (from the docstring)
English
Let $M$ and $X$ be sets. Then we can say that $M$ is isometric.
IsometryEquiv.addLeftdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantEnglish
Let $c$ be an element of $G$. Then $\operatorname{addLeft}$ applied to $c$ is an isometry equivalence of $G$ and $G$.
IsometryEquiv.addRightdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantEnglish
Let $c$ be an element of $G$. Then $\operatorname{addRight}$ applied to $c$ is an isometry equivalence of $G$ and $G$.
IsometryEquiv.constSMuldefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the constant product of c (from the name)
English
Let $c$ be an element of $G$. Then the constant product of $c$ is an isometry equivalence of $X$ and $X$.
IsometryEquiv.constVAdddefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the constant sum of c (from the name)
English
Let $c$ be an element of $G$. Then the constant sum of $c$ is an isometry equivalence of $X$ and $X$.
IsometryEquiv.divLeftdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the left quotient of c (from the name)
English
Let $c$ be an element of $G$. Then the left quotient of $c$ is an isometry equivalence of $G$ and $G$ defined as $\operatorname{mk}$ applied to the left quotient of $c$ and $\mathrm{edist\_div\_left}$ applied to $c$.
IsometryEquiv.divRightdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the right quotient of c (from the name)
English
Let $c$ be an element of $G$. Then the right quotient of $c$ is an isometry equivalence of $G$ and $G$.
IsometryEquiv.invdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the inverse of G (from the name)
English
Let $G$ be a set. Then the inverse of $G$ is an isometry equivalence of $G$ and $G$ defined as $\operatorname{mk}$ applied to the inverse of $G$ and $\mathrm{edist\_inv\_inv}$.
IsometryEquiv.mulLeftdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the left multiplicative of c (from the name)
English
Let $c$ be an element of $G$. Then the left multiplicative of $c$ is an isometry equivalence of $G$ and $G$.
IsometryEquiv.mulRightdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the right multiplicative of c (from the name)
English
Let $c$ be an element of $G$. Then the right multiplicative of $c$ is an isometry equivalence of $G$ and $G$.
IsometryEquiv.negdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the negation of G (from the name)
English
Let $G$ be a set. Then the negation of $G$ is an isometry equivalence of $G$ and $G$ defined as $\operatorname{mk}$ applied to the negation of $G$ and $\mathrm{edist\_neg\_neg}$.
IsometryEquiv.subLeftdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the left difference of c (from the name)
English
Let $c$ be an element of $G$. Then the left difference of $c$ is an isometry equivalence of $G$ and $G$ defined as $\operatorname{mk}$ applied to the left difference of $c$ and $\mathrm{edist\_sub\_left}$ applied to $c$.
IsometryEquiv.subRightdefMathlib.Topology.MetricSpace.IsometricSMul, function or constantWording
the right difference of c (from the name)
English
Let $c$ be an element of $G$. Then the right difference of $c$ is an isometry equivalence of $G$ and $G$.
Fin.appendIsometrydefMathlib.Topology.MetricSpace.Isometry, function or constantEnglish
Let $m$ and $n$ be natural numbers. Then $\operatorname{appendIsometry}$ applied to $m$ and $n$ is an isometry equivalence of $\mathrm{Prod}$ applied to the set of functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $m + n$ to elements of $x$.
Fin.appendIsometryOfEqdefMathlib.Topology.MetricSpace.Isometry, function or constantEnglish
Assume that $m + l = n$. Then $\operatorname{appendIsometryOfEq}$ applied to $\mathrm{hmln}$ is an isometry equivalence of $\mathrm{Prod}$ applied to the set of functions from elements of $\mathrm{Fin}$ applied to $m$ to elements of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $l$ to elements of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$ defined as the composition of $\operatorname{appendIsometry}$ applied to $m$ and $l$ and the left product congruence of the finite congruence of $\mathrm{hmln}$.
IsometrydefMathlib.Topology.MetricSpace.Isometry, predicateWording
f is a isometry (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is an isometry, if for all elements $x_{11}$ and $x_{21}$ of $x$, the extended distance of $f$ applied to $x_{11}$ and $f$ applied to $x_{21}$ is equal to the extended distance of $x_{11}$ and $x_{21}$.
Isometry.isometryEquivOnRangedefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the isometry equivalence on range of h (from the name)
English
Assume that $f$ is an isometry. Then the isometry equivalence on range of $h$ is an isometry equivalence of $x$ and the set of elements of the range of $f$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and $\operatorname{injective}$ applied to $h$ and $h$.
IsometryClassclassMathlib.Topology.MetricSpace.Isometry, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{IsometryClass}$ holds for $F$, $x$ and $x_{1}$.
IsometryClass.toIsometryEquivdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the isometry equivalence of f (from the name)
English
Let $f$ be an element of $F$. Then the isometry equivalence of $f$ is an isometry equivalence of $x$ and $x_{1}$.
IsometryEquivstructureMathlib.Topology.MetricSpace.Isometry, typeWording
isometry equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the isometry equivalences of $x$ and $x_{1}$ are a basic type.
IsometryEquiv.funUniquedefMathlib.Topology.MetricSpace.Isometry, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $x_{1}$ is an isometry equivalence of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{1}$.
IsometryEquiv.mk'defMathlib.Topology.MetricSpace.Isometry, function or constantEnglish
Let $f$ be a function from elements of $x_{2}$ to elements of $x$. Let $g$ be a function from elements of $x$ to elements of $x_{2}$ such that for all elements $x_{4}$ of $x$, $\EqtMACRoH {f (g (x_{4}))}{x_{4}}$. Assume that $f$ is an isometry. Then $\operatorname{mk'}$ applied to $f$, $g$, $\mathrm{hfg}$ and $\mathrm{hf}$ is an isometry equivalence of $x_{2}$ and $x$.
IsometryEquiv.piCongrLeftdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
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 an isometry equivalence of the set of functions from elements $i$ of $x$ to elements of $Y$ applied to $e$ applied to $i$ and the set of functions from elements $j$ of $x_{1}$ to elements of $Y$ applied to $j$ defined as the inverse of the left product congruence of the inverse of $e$.
IsometryEquiv.piCongrLeft'defMathlib.Topology.MetricSpace.Isometry, function or constantWording
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 an isometry equivalence of the set of functions from elements $i$ of $x$ to elements of $Y$ applied to $i$ and the set of functions from elements $j$ of $x_{1}$ to elements of $Y$ applied to $\operatorname{symm}$ applied to $e$ and $j$.
IsometryEquiv.piFinTwodefMathlib.Topology.MetricSpace.Isometry, function or constantEnglish
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $x$ is an isometry 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$.
IsometryEquiv.refldefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the identity isometry of x (from the docstring)
English
Let $x$ be a set. Then the identity isometry of $x$ is an isometry equivalence of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity of $x$ and $\mathrm{isometry\_id}$.
IsometryEquiv.sumArrowIsometryEquivProdArrowdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the natural isometry (from the docstring)
English
The natural isometry is an isometry equivalence of the set of functions from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to elements of $x_{2}$ and $\mathrm{Prod}$ applied to the set of functions from elements of $x$ to elements of $x_{2}$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$.
IsometryEquiv.symmdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the inverse of h (from the docstring)
English
Let $h$ be an isometry equivalence of $x$ and $x_{1}$. Then the inverse of $h$ is an isometry equivalence of $x_{1}$ and $x$.
IsometryEquiv.toHomeomorphdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the homeomorphism of h (from the name)
English
Let $h$ be an isometry equivalence of $x$ and $x_{1}$. Then the homeomorphism of $h$ is a homeomorphism of $x$ and $x_{1}$.
IsometryEquiv.transdefMathlib.Topology.MetricSpace.Isometry, function or constantWording
the composition of x6 and x7 (from the name)
English
Let $x_{6}$ be an isometry equivalence of $x$ and $x_{1}$. Let $x_{7}$ be an isometry equivalence of $x_{1}$ and $x_{2}$. Then the composition of $x_{6}$ and $x_{7}$ is an isometry equivalence of $x$ and $x_{2}$.
KuratowskiEmbedding.embeddingOfSubsetdefMathlib.Topology.MetricSpace.Kuratowski, function or constantWording
the embedding of x2 and a (from the name)
English
Let $x_{2}$ be a function from elements of $\Natural$ to elements of $x$. Let $a$ be an element of $x$. Then the embedding of $x_{2}$ and $a$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . \Real , \operatorname{top})}{x_{3}})}$ defined as the function that maps $n$ to $\operatorname{dist} (a , x_{2} (n))- \operatorname{dist} (x_{2} (0), x_{2} (n))$.
NonemptyCompacts.kuratowskiEmbeddingdefMathlib.Topology.MetricSpace.Kuratowski, function or constantWording
the Kuratowski embedding of x (from the name)
English
Let $x$ be a set. Then the Kuratowski embedding of $x$ is a nonempty compact of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{3} . \Real , \operatorname{top})}{x_{2}})}$.
kuratowskiEmbeddingdefMathlib.Topology.MetricSpace.Kuratowski, function or constantWording
the Kuratowski embedding of x and x2 (from the docstring)
English
Let $x$ be a set. Let $x_{2}$ be an element of $x$. Then the Kuratowski embedding of $x$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{lp} (\lambda x_{4} . \Real , \operatorname{top})}{x_{3}})}$ defined as $\operatorname{choose}$ applied to $\mathrm{KuratowskiEmbedding\_\_exists\_isometric\_embedding}$ applied to $x$ and $x_{2}$.
LipschitzWith.toLocallyBoundedMapdefMathlib.Topology.MetricSpace.Lipschitz, function or constantWording
the locally bounded map of f and hf (from the name)
English
generation took over the time limit
Metric.AreSeparateddefMathlib.Topology.MetricSpace.MetricSeparated, predicateEnglish
Let $s$ and $t$ be elements of $\wp X$. Then $\operatorname{AreSeparated}$ holds for $s$ and $t$, if there exists an element $r$ of $\mathrm{ENNReal}$, such that $r \neq 0$ and for all elements $x_{1}$ of $X$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $X$, if $y$ is an element of $t$, then $r$ is less than or equal to the extended distance of $x_{1}$ and $y$.
Metric.IsSeparateddefMathlib.Topology.MetricSpace.MetricSeparated, predicateEnglish
Let $x_{1}$ be an element of $\mathrm{ENNReal}$. Let $s$ be an element of $\wp X$. Then $\operatorname{IsSeparated}$ holds for $x_{1}$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the function that maps $x_{2}$ and $x_{3}$ to the proposition that $x_{1}$ is less than the extended distance of $x_{2}$ and $x_{3}$.
Metric.PiNatEmbedstructureMathlib.Topology.MetricSpace.PiNat, typeWording
product natural embed of Y and f (from the name)
English
Let $X$ be a set. Let $Y$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements of $X$ to elements of $Y$ applied to $i$. Then the product natural embeds of $Y$ and $i$ are a basic type.
Metric.PiNatEmbed.distDenseSeqdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the distance dense sequence of n and x1 (from the name)
English
Let $X$ be a set. Let $n$ be a natural number. Let $x_{1}$ be an element of $X$. Then the distance dense sequence of $n$ and $x_{1}$ is an element of the unit interval.
Metric.PiNatEmbed.embeddefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the embed of i1 and x1 (from the name)
English
Let $X$ be a set. Let $Y$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{1}$ of $x$ and elements of $X$ to elements of $Y$ applied to $i_{1}$. Let $x_{1}$ be a product natural embed of $Y$ and $f$. Let $i$ be an element of $x$. Then the embed of $f$ and $x_{1}$ is an element of $Y$ applied to $i$ defined as the function that maps $i$ to $i_{1}$ applied to $x_{1}$, the product natural embed of $f$ and $i$.
Metric.PiNatEmbed.ofPiNatdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the product natural embed of self (from the name)
English
Let $\mathrm{self}$ be a product natural embed of $Y$ and $f$. Then the product natural embed of $\mathrm{self}$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Metric.PiNatEmbed.toPiNatEquivdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the product natural equivalence of Y and f (from the name)
English
Let $X$ be a set. Let $Y$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements of $X$ to elements of $Y$ applied to $i$. Then the product natural equivalence of $Y$ and $i$ is an equivalence from $X$ to the set of product natural embeds of $Y$ and $f$.
Metric.PiNatEmbed.toPiNatHomeodefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the product natural homeomorphism of Y and f (from the name)
English
Let $X$ be a set. Let $Y$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i_{2}$ of $x$ and elements of $X$ to elements of $Y$ applied to $i_{2}$ such that for all elements $i_{1}$ of $x$, $f$ applied to $i_{1}$ is continuous and the function that maps $x_{4}$ and $y$ to the proposition that there exists an element $i$ of $x$ such that $f (i , x_{4})\neq f (i , y)$ is pairwise. Then the product natural homeomorphism of $Y$ and $i_{2}$ is a homeomorphism of $X$ and the set of product natural embeds of $Y$ and $f$.
PiNat.cylinderdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the cylinder of x and n2 (from the name)
English
Let $x$ be a function from natural numbers $n_{2}$ to elements of $E$ applied to $n_{2}$. Let $n$ be a natural number. Then the cylinder of $n_{2}$ and $x$ is an element of $\wp (\mathrm{Elem} (\Natural)\rightarrow E (n_{1}))$ defined as the function that maps $n$ to $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that for all natural numbers $i$, if $i < x$, then $\EqtMACRoH {y (i)}{n_{2} (i)}$ and $n$.
PiNat.firstDiffdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the first difference of x and n1 (from the name)
English
Let $x$ be a function from natural numbers $n_{1}$ to elements of $E$ applied to $n_{1}$. Let $y$ be a function from natural numbers $n$ to elements of $E$ applied to $n$. Then the first difference of $n_{1}$ and $x$ is a natural number defined as the function that maps $n$ and $y$ to $\operatorname{proj0}$ applied to $\mathrm{PiNat\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Topology\_\_MetricSpace\_\_PiNat\_\_2189032603\_\_\_hygCtx\_\_\_hyg\_\_8}$, $n_{1}$, $x$, $n$ and $y$.
PiNat.longestPrefixdefMathlib.Topology.MetricSpace.PiNat, function or constantEnglish
Let $x$ be a function from natural numbers $n_{1}$ to elements of $E$ applied to $n_{1}$. Let $s$ be an element of $\wp (\mathrm{Elem} (\Natural)\rightarrow E (n))$. Then $\operatorname{longestPrefix}$ applied to $n_{1}$, $x$ and $s$ is a natural number defined as the function that maps $s$ to $\mathrm{minus} (\operatorname{shortestPrefixDiff} (n_{1} , x), 1 , s)$.
PiNat.resdefMathlib.Topology.MetricSpace.PiNat, function or constantWording
the restriction of x1 and x2 (from the name)
English
Let $x_{1}$ be a function from natural numbers to elements of $x$. Let $x_{2}$ be a natural number. Then the restriction of $x_{1}$ and $x_{2}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{PiNat\_\_res\_\_\_f}$ applied to $x_{1}$.
PiNat.shortestPrefixDiffdefMathlib.Topology.MetricSpace.PiNat, function or constantEnglish
Let $x$ be a function from natural numbers $n_{1}$ to elements of $E$ applied to $n_{1}$. Let $s$ be an element of $\wp (\mathrm{Elem} (\Natural)\rightarrow E (n))$. Then $\operatorname{shortestPrefixDiff}$ applied to $n_{1}$, $x$ and $s$ is a natural number defined as the function that maps $s$ to $\mathrm{dite}$ applied to the proposition that there exists a natural number $n$, such that $x$ is disjoint to the cylinder of $n_{1}$ and $n$, the function that maps $h$ to $\operatorname{find}$ applied to $h$, the function that maps $h_{1}$ to $0$ and $s$.
PolishSpaceclassMathlib.Topology.MetricSpace.Polish, predicateWording
x is a Polish space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a Polish space.
PolishSpace.IsClopenabledefMathlib.Topology.MetricSpace.Polish, predicateEnglish
Let $s$ be an element of $\wp x$. Then $\operatorname{IsClopenable}$ holds for $s$, if there exists an element $\mathrm{t'}$ of $\mathrm{TopologicalSpace}$ applied to $x$, such that $\mathrm{t'} \leq t$, $x$ is a Polish space and $s$ is closed and open.
TopologicalSpace.Opens.CompleteCopydefMathlib.Topology.MetricSpace.Polish, typeWording
complete copy of s (from the name)
English
Let $s$ be an open of $x$. Then a complete copy of $s$ is an element of the function that maps $s$ to $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$.
ProperSpaceclassMathlib.Topology.MetricSpace.ProperSpace, predicateWording
x is proper (from the docstring)
English
Let $x$ be a set. Then we can say that $x$ is proper.
DistclassMathlib.Topology.MetricSpace.Pseudo.Defs, predicateWording
x is a distance (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a distance.
Dist.distdefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the distance of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the distance of $x_{1}$ and $x_{2}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
Metric.balldefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the ball of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $x$. Let $x_{3}$ be a real number. Then the ball of $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the distance of $y$ and $x_{2}$ is less than $x_{3}$.
Metric.closedBalldefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the closed ball of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $x$. Let $x_{3}$ be a real number. Then the closed ball of $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the distance of $y$ and $x_{2}$ is less than or equal to $x_{3}$.
Metric.spheredefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the sphere of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $x$. Let $x_{3}$ be a real number. Then the sphere of $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the distance of $y$ and $x_{2}$ is equal to $x_{3}$.
NNDistclassMathlib.Topology.MetricSpace.Pseudo.Defs, predicateWording
x is a nonnegative distance (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a nonnegative distance.
NNDist.nndistdefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the distance of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the distance of $x_{1}$ and $x_{2}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
PseudoMetricSpaceclassMathlib.Topology.MetricSpace.Pseudo.Defs, predicateWording
x is a pseudo metric space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a pseudo metric space.
PseudoMetricSpace.edistdefMathlib.Topology.MetricSpace.Pseudo.Defs, function or constantWording
the extended distance of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the extended distance of $x_{1}$ and $x_{2}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
SimilardefMathlib.Topology.MetricSpace.Similarity, predicateWording
x5 is similar to x6 (from the name)
English
Let $x_{5}$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{6}$ be a function from elements of $x$ to elements of $x_{2}$. Then $x_{5}$ is similar to $x_{6}$, if there exists an element $r$ of $\mathrm{NNReal}$, such that $r \neq 0$ and for all elements $x_{7}$ of $x$, for all elements $x_{8}$ of $x$, the extended distance of $x_{5}$ applied to $x_{7}$ and $x_{5}$ applied to $x_{8}$ is equal to the product of $\operatorname{ofNNReal}$ applied to $r$ and the extended distance of $x_{6}$ applied to $x_{7}$ and $x_{6}$ applied to $x_{8}$.
Metric.SnowflakingstructureMathlib.Topology.MetricSpace.Snowflaking, typeEnglish
Let $X$ be a set. Let $x$ be a real number such that $0 < x \leq 1$. Then the elements of $\operatorname{Snowflaking}$ applied to $X$, $x$, $h$ and $h_{1}$ are a basic type.
Metric.Snowflaking.casesOn_toSnowflakingdefMathlib.Topology.MetricSpace.Snowflaking, function or constantEnglish
Let $\mathrm{toSnowflaking}$ be a function from elements $x_{2}$ of $X$ to elements of $\mathrm{motive}$ applied to $\operatorname{toSnowflaking}$ applied to $x_{2}$. Let $x_{1}$ be an element of $\operatorname{Snowflaking}$ applied to $X$, $x$, $h$ and $h_{1}$. Then $\mathrm{Metric\_\_Snowflaking\_\_casesOn\_toSnowflaking}$ applied to $x_{2}$, $\mathrm{toSnowflaking}$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $x_{1}$ defined as the function that maps $x_{1}$ to $x_{2}$ applied to the value of $\mathrm{toSnowflaking}$ and $x_{1}$.
Metric.Snowflaking.homeomorphdefMathlib.Topology.MetricSpace.Snowflaking, function or constantWording
the homeomorphism (from the name)
English
The homeomorphism is a homeomorphism of $\operatorname{Snowflaking}$ applied to $X$, $x$, $h$ and $h_{1}$ and $X$.
Metric.Snowflaking.ofSnowflakingdefMathlib.Topology.MetricSpace.Snowflaking, function or constantEnglish
$\operatorname{ofSnowflaking}$ is an element of $\EquivMACRoAE {\operatorname{Snowflaking} (X , x , h , h_{1})}{X}$.
Metric.Snowflaking.toSnowflakingdefMathlib.Topology.MetricSpace.Snowflaking, function or constantEnglish
$\operatorname{toSnowflaking}$ is an element of $\EquivMACRoAE {X}{\operatorname{Snowflaking} (X , x , h , h_{1})}$ defined as the inverse of $\operatorname{ofSnowflaking}$.
Metric.Snowflaking.valdefMathlib.Topology.MetricSpace.Snowflaking, function or constantWording
the value of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{Snowflaking}$ applied to $X$, $x$, $h$ and $h_{1}$. Then the value of $\mathrm{self}$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
thickenedIndicatordefMathlib.Topology.MetricSpace.ThickenedIndicator, function or constantEnglish
Assume that $0 < x_{2}$. Let $E$ be an element of $\wp x$. Then $\mathrm{thickenedIndicator}$ applied to $h$ and $E$ is a bounded continuous function of $x$ and $\mathrm{NNReal}$.
Metric.cthickeningdefMathlib.Topology.MetricSpace.Thickening, function or constantEnglish
Let $x_{2}$ be a real number. Let $E$ be an element of $\wp x$. Then $\operatorname{cthickening}$ applied to $x_{2}$ and $E$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that the infimum distance of $x_{3}$ and $E$ is less than or equal to $\operatorname{ofReal}$ applied to $x_{2}$.
Metric.thickeningdefMathlib.Topology.MetricSpace.Thickening, function or constantWording
the thickening of x2 and E (from the name)
English
Let $x_{2}$ be a real number. Let $E$ be an element of $\wp x$. Then the thickening of $x_{2}$ and $E$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to the proposition that the infimum distance of $x_{3}$ and $E$ is less than $\operatorname{ofReal}$ applied to $x_{2}$.
IsUltrametricDistclassMathlib.Topology.MetricSpace.Ultra.Basic, predicateWording
X is a ultrametric distance (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a ultrametric distance.
TopologicalSpace.MetrizableSpaceclassMathlib.Topology.Metrizable.Basic, predicateWording
X is metrizable (from the docstring)
English
Let $X$ be a set. Then we can say that $X$ is metrizable.
TopologicalSpace.PseudoMetrizableSpaceclassMathlib.Topology.Metrizable.Basic, predicateWording
X is pseudometrizable (from the docstring)
English
Let $X$ be a set. Then we can say that $X$ is pseudometrizable.
TopologicalSpace.IsCompletelyMetrizableSpaceclassMathlib.Topology.Metrizable.CompletelyMetrizable, predicateWording
X is completely metrizable (from the docstring)
English
generation took over the time limit
TopologicalSpace.IsCompletelyPseudoMetrizableSpaceclassMathlib.Topology.Metrizable.CompletelyMetrizable, predicateWording
X is completely pseudometrizable (from the docstring)
English
generation took over the time limit
TopologicalSpace.UpgradedIsCompletelyMetrizableSpaceclassMathlib.Topology.Metrizable.CompletelyMetrizable, predicateEnglish
Let $X$ be a set. Then we can say that $\operatorname{UpgradedIsCompletelyMetrizableSpace}$ holds for $X$.
TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpaceclassMathlib.Topology.Metrizable.CompletelyMetrizable, predicateEnglish
Let $X$ be a set. Then we can say that $\operatorname{UpgradedIsCompletelyPseudoMetrizableSpace}$ holds for $X$.
TopologicalSpace.NoetherianSpacedefMathlib.Topology.NoetherianSpace, predicateWording
x is a Noetherian space (from the name)
English
Let $x$ be a set. Then $x$ is a Noetherian space, if $\mathrm{WellFoundedGT}$ holds for the set of opens of $x$.
Scott.IsOpendefMathlib.Topology.OmegaCompletePartialOrder, predicateWording
s is open (from the name)
English
Let $x$ be a set. Let $s$ be an element of $\wp x$. Then $s$ is open, if $\mathrm{OmegaCompletePartialOrder\_\_\_u3c9\_ScottContinuous}$ holds for the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$.
Scott.IsωSupdefMathlib.Topology.OmegaCompletePartialOrder, predicateEnglish
Let $c$ be a chain of $x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{Scott\_\_Is\_u3c9\_Sup}$ holds for $c$ and $x_{2}$, if for all natural numbers $i$, $c (i)\leq x_{2}$ and for all elements $y$ of $x$, if for all natural numbers $i_{1}$, $c (i_{1})\leq y$, then $x_{2} \leq y$.
OpenPartialHomeomorph.homeomorphOfImageSubsetSourcedefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$ such that $s$ is less than or equal to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and the image of $\operatorname{toFun'}$ applied to $e$ and $s$ is equal to $t$. Then the homeomorphism of $e$ is a homeomorphism of the set of elements of $s$ and the set of elements of $t$ defined as the homeomorphism of $\operatorname{toPartialHomeomorph}$ applied to $e$.
OpenPartialHomeomorph.ofContinuousOpendefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the open partial homeomorphism of e (from the name)
English
Let $e$ be a partial equivalence of $X$ and $Y$ such that $\mathrm{ContinuousOn}$ holds for $\operatorname{toFun}$ applied to $e$ and the source of $e$, $\operatorname{toFun}$ applied to $e$ is an open map and the source of $e$ is open. Then the open partial homeomorphism of $e$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.ofContinuousOpenRestrictdefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the open partial homeomorphism of e (from the name)
English
Let $e$ be a partial equivalence of $X$ and $Y$ such that $\mathrm{ContinuousOn}$ holds for $\operatorname{toFun}$ applied to $e$ and the source of $e$, $\operatorname{domRestrict}$ applied to the source of $e$ and $\operatorname{toFun}$ applied to $e$ is an open map and the source of $e$ is open. Then the open partial homeomorphism of $e$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.refldefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the identity on the whole space of X (from the docstring)
English
Let $X$ be a set. Then the identity on the whole space of $X$ is an open partial homeomorphism of $X$ and $X$ defined as the open partial homeomorphism of the identity of $X$.
OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUnivdefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$ such that the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is equal to the universal set and the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is equal to the universal set. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$ defined as the homeomorphism of $\operatorname{toPartialHomeomorph}$ applied to $e$.
OpenPartialHomeomorph.toHomeomorphSourceTargetdefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the homeomorphism source target of e (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Then the homeomorphism source target of $e$ is a homeomorphism of the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and the set of elements of the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$.
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoedefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the open partial homeomorphism subtype coercion of s and hs (from the name)
English
Let $s$ be an open of $X$ such that $\mathrm{Nonempty}$ holds for $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$. Then the open partial homeomorphism subtype coercion of $s$ and $\mathrm{hs}$ is an open partial homeomorphism of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $X$.
Topology.IsOpenEmbedding.toOpenPartialHomeomorphdefMathlib.Topology.OpenPartialHomeomorph.Basic, function or constantWording
the open partial homeomorphism of f and h (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is an open embedding. Then the open partial homeomorphism of $f$ and $h$ is an open partial homeomorphism of $X$ and $Y$.
Homeomorph.transOpenPartialHomeomorphdefMathlib.Topology.OpenPartialHomeomorph.Composition, function or constantWording
the composition open partial homeomorphism of e and #2 (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be an open partial homeomorphism of $Y$ and $Z$. Then the composition open partial homeomorphism of $e$ and $\mathrm{f'}$ is an open partial homeomorphism of $X$ and $Z$.
OpenPartialHomeomorph.transdefMathlib.Topology.OpenPartialHomeomorph.Composition, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $\mathrm{e'}$ be an open partial homeomorphism of $Y$ and $Z$. Then the composition of $e$ and $\mathrm{e'}$ is an open partial homeomorphism of $X$ and $Z$.
OpenPartialHomeomorph.trans'defMathlib.Topology.OpenPartialHomeomorph.Composition, function or constantWording
the composition of e and h (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $\mathrm{e'}$ be an open partial homeomorphism of $Y$ and $Z$ such that the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is equal to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\mathrm{e'}$. Then the composition of $e$ and $\mathrm{e'}$ is an open partial homeomorphism of $X$ and $Z$.
OpenPartialHomeomorph.constdefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the constant of ha and hb (from the name)
English
Assume that $\operatorname{singleton}$ applied to $a$ is open. Assume that $\operatorname{singleton}$ applied to $b$ is open. Then the constant of $\mathrm{ha}$ and $\mathrm{hb}$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.disjointUniondefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the disjoint union of e and Hs (from the name)
English
Let $e$ and $\mathrm{e'}$ be open partial homeomorphisms of $X$ and $Y$ such that the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is disjoint to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\mathrm{e'}$ and the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is disjoint to the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\mathrm{e'}$. Then the disjoint union of $e$ and $\mathrm{e'}$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.lift_openEmbeddingdefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the lift open embedding of e and hf (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Z$. Assume that $f$ is an open embedding. Then the lift open embedding of $e$ and $\mathrm{hf}$ is an open partial homeomorphism of $\mathrm{X'}$ and $Z$.
OpenPartialHomeomorph.pidefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the product of ei (from the docstring)
English
Let $\mathrm{ei}$ be a function from elements $i_{2}$ of $x$ to open partial homeomorphisms of $X$ applied to $i_{2}$ and $Y$ applied to $i_{2}$. Then the product of $i_{2}$ is an open partial homeomorphism of the set of functions from elements $i$ of $x$ to elements of $X$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $Y$ applied to $i_{1}$.
OpenPartialHomeomorph.piecewisedefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantEnglish
Let $e$ and $\mathrm{e'}$ be open partial homeomorphisms of $X$ and $Y$. Let $s$ be an element of $\wp X$. Let $t$ be an element of $\wp Y$ such that $\operatorname{IsImage}$ holds for $e$, $s$ and $t$ and $\operatorname{IsImage}$ holds for $\mathrm{e'}$, $s$ and $t$. Assume that $\operatorname{inter}$ applied to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and the frontier of $s$ is equal to $\operatorname{inter}$ applied to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\mathrm{e'}$ and the frontier of $s$. Assume that $\operatorname{EqOn}$ holds for $\operatorname{toFun'}$ applied to $e$, $\operatorname{toFun'}$ applied to $\mathrm{e'}$ and $\operatorname{inter}$ applied to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and the frontier of $s$. Then $\operatorname{piecewise}$ applied to $e$, $\mathrm{e'}$, $s$, $t$, $H$, $\mathrm{H'}$, $\mathrm{Hs}$ and $\mathrm{Heq}$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.proddefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the product of eX and eY (from the name)
English
Let $\mathrm{eX}$ be an open partial homeomorphism of $X$ and $\mathrm{X'}$. Let $\mathrm{eY}$ be an open partial homeomorphism of $Y$ and $\mathrm{Y'}$. Then the product of $\mathrm{eX}$ and $\mathrm{eY}$ is an open partial homeomorphism of $\mathrm{Prod}$ applied to $X$ and $Y$ and $\mathrm{Prod}$ applied to $\mathrm{X'}$ and $\mathrm{Y'}$.
OpenPartialHomeomorph.subtypeRestrdefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the restriction of e and hs (from the docstring)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Assume that $\mathrm{Nonempty}$ holds for $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {s}{x_{3}})}$. Then the restriction of $e$ and $\mathrm{hs}$ is an open partial homeomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})}$ and $Y$ defined as the composition of the open partial homeomorphism subtype coercion of $s$ and $\mathrm{hs}$ and $e$.
OpenPartialHomeomorph.transHomeomorphdefMathlib.Topology.OpenPartialHomeomorph.Constructions, function or constantWording
the composition homeomorphism of e and #2 (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $\mathrm{f'}$ be a homeomorphism of $Y$ and $Z$. Then the composition homeomorphism of $e$ and $\mathrm{f'}$ is an open partial homeomorphism of $X$ and $Z$.
Homeomorph.toOpenPartialHomeomorphdefMathlib.Topology.OpenPartialHomeomorph.Defs, function or constantWording
the open partial homeomorphism of e (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Then the open partial homeomorphism of $e$ is an open partial homeomorphism of $X$ and $Y$.
Homeomorph.toOpenPartialHomeomorphOfImageEqdefMathlib.Topology.OpenPartialHomeomorph.Defs, function or constantWording
the open partial homeomorphism of s and t (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Let $s$ be an open element of $\wp X$. Let $t$ be an element of $\wp Y$ such that the image of $\operatorname{coe}$ applied to $e$ and $s$ is equal to $t$. Then the open partial homeomorphism of $s$ and $t$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorphstructureMathlib.Topology.OpenPartialHomeomorph.Defs, typeWording
open partial homeomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be sets. Then the open partial homeomorphisms of $X$ and $Y$ are a basic type.
OpenPartialHomeomorph.replacePartialEquivdefMathlib.Topology.OpenPartialHomeomorph.Defs, function or constantEnglish
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $\mathrm{e'}$ be a partial equivalence of $X$ and $Y$ such that $\EqtMACRoH {\operatorname{toPartialEquiv} (\operatorname{toPartialHomeomorph} (e))}{\mathrm{e'}}$. Then $\operatorname{replacePartialEquiv}$ applied to $e$, $\mathrm{e'}$ and $h$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.symmdefMathlib.Topology.OpenPartialHomeomorph.Defs, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Then the inverse of $e$ is an open partial homeomorphism of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toPartialHomeomorph}$ applied to $e$, $\mathrm{OpenPartialHomeomorph\_\_open\_target}$ applied to $e$ and $\mathrm{OpenPartialHomeomorph\_\_open\_source}$ applied to $e$.
OpenPartialHomeomorph.toFun'defMathlib.Topology.OpenPartialHomeomorph.Defs, function or constantWording
the function of e and x2 (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $x_{2}$ be an element of $X$. Then the function of $e$ and $x_{2}$ is an element of $Y$ defined as the partial equivalence of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $x_{2}$.