Definitions: Mathlib.Topology, part 5 of 8

Topology.ContinuousGeneratedBydefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, predicate

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $g$ be a function from elements of $Y$ to elements of $Z$. Then $\operatorname{ContinuousGeneratedBy}$ holds for $X$ and $g$, if for all elements $i$ of $x$, for all continuous maps $f$ of $X$ applied to $i$ and $Y$, $\operatorname{comp}$ applied to $g$ and $\operatorname{coe}$ applied to $f$ is continuous.

Topology.ContinuousGeneratedBy.continuousMapdefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

the continuous map of hg (from the name)

English

Assume that $\operatorname{ContinuousGeneratedBy}$ holds for $X$ and $g$. Then the continuous map of $\mathrm{hg}$ is a continuous map of $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$ and $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Z$.

Topology.ContinuousMapGeneratedBystructureMathlib.Topology.Convenient.ContinuousMapGeneratedBy, type

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $Y$ and $Z$ be sets. Then the elements of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Z$ are a basic type.

Topology.ContinuousMapGeneratedBy.compdefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Z$. Let $f$ be an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $T$ and $Y$. Then the composition of $g$ and $f$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $T$ and $Z$.

Topology.ContinuousMapGeneratedBy.iddefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

the identity (from the name)

English

The identity is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Y$.

Topology.ContinuousMapGeneratedBy.toFundefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

the underlying map of self and x4 (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Z$. Let $x_{4}$ be an element of $Y$. Then the underlying map of $\mathrm{self}$ and $x_{4}$ is an element of $Z$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBydefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $Y$ be a set. Then $\operatorname{equivAsContinuousMapGeneratedBy}$ applied to $X$ and $Y$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$ and $Y$.

Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBydefMathlib.Topology.Convenient.ContinuousMapGeneratedBy, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $Y$ be a set. Then $\operatorname{equivSymmAsContinuousMapGeneratedBy}$ applied to $X$ and $Y$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$.

Mathlib.Topology.Convenient.GeneratedBy

Topology.IsGeneratedByclassMathlib.Topology.Convenient.GeneratedBy, predicate

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $Y$ be a set. Then we can say that $\operatorname{IsGeneratedBy}$ holds for $X$ and $Y$.

Topology.IsGeneratedBy.homeomorphdefMathlib.Topology.Convenient.GeneratedBy, function or constant

Wording

the homeomorphism (from the docstring)

English

The homeomorphism is a homeomorphism of $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$ and $Y$.

Topology.WithGeneratedByTopologydefMathlib.Topology.Convenient.GeneratedBy, type

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Let $Y$ be a set. Then an element of $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$ is an element of the function that maps $X$ and $Y$ to $Y$.

Topology.WithGeneratedByTopology.equivdefMathlib.Topology.Convenient.GeneratedBy, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an element of $\EquivMACRoAE {\operatorname{WithGeneratedByTopology} (X , Y)}{Y}$ defined as the identity of $\operatorname{WithGeneratedByTopology}$ applied to $X$ and $Y$.

Mathlib.Topology.Convenient.HomSpace

Topology.ContinuousMapGeneratedBy.curryEquivdefMathlib.Topology.Convenient.HomSpace, function or constant

Wording

the curry equivalence (from the name)

English

The curry equivalence is an element of $\EquivMACRoAE {\operatorname{ContinuousMapGeneratedBy} (X , \mathrm{Prod} (Y , Z), T)}{\operatorname{ContinuousMapGeneratedBy} (X , Z , \operatorname{ContinuousMapGeneratedBy} (X , Y , T))}$.

Topology.ContinuousMapGeneratedBy.evdefMathlib.Topology.Convenient.HomSpace, function or constant

Wording

no wording

English

$\operatorname{ev}$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $\mathrm{Prod}$ applied to $Y$ and $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Z$ and $Z$ defined as $\operatorname{symm}$ applied to the curry equivalence and the identity.

Topology.ContinuousMapGeneratedBy.postcompdefMathlib.Topology.Convenient.HomSpace, function or constant

Wording

the postcomposition of p (from the name)

English

Let $p$ be an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Z$ and $T$. Then the postcomposition of $p$ is an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $Z$ and $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Y$ and $T$ defined as $\operatorname{curryEquiv}$ applied to the composition of $p$ and $\operatorname{ev}$.

Topology.ContinuousMapGeneratedBy.precompdefMathlib.Topology.Convenient.HomSpace, function or constant

Wording

the precomposition of f and x4 (from the name)

English

Let $f$ be a continuous map of $X$ applied to $i$ and $Z$. Let $x_{4}$ be an element of $\operatorname{ContinuousMapGeneratedBy}$ applied to $X$, $Z$ and $T$. Then the precomposition of $f$ and $x_{4}$ is a continuous map of $X$ applied to $i$ and $T$ defined as $\operatorname{mk}$ applied to $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $x_{4}$ and $\operatorname{coe}$ applied to $f$ and $\operatorname{prop}$ applied to $x_{4}$, $i$ and $f$.

Mathlib.Topology.Convenient.Localization

TopCat.morphismPropertyWithGeneratedByTopologyEquivdefMathlib.Topology.Convenient.Localization, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $x$ to sets. Then there is a morphism property of the set of topological categories. Proof. Let $X$ be arbitrary. By GeneratedByTopCat__adjCounit. By CategoryTheory__NatTrans__app. By CategoryTheory__MorphismProperty__ofHoms.

Mathlib.Topology.Covering.Basic

IsCoveringMapdefMathlib.Topology.Covering.Basic, predicate

Wording

f is a covering map (from the name)

English

Let $f$ be a function from elements of $E$ to elements of $X$. Then $f$ is a covering map, if for all elements $x_{2}$ of $X$, $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{2}$ and the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{2}$.

IsCoveringMapOndefMathlib.Topology.Covering.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $X$. Let $s$ be an element of $\wp X$. Then $\mathrm{IsCoveringMapOn}$ holds for $f$ and $s$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{2}$ and the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{2}$.

IsEvenlyCovereddefMathlib.Topology.Covering.Basic, predicate

Wording

no wording

English

Let $f$ be a function from elements of $E$ to elements of $X$. Let $x_{2}$ be an element of $X$. Let $I$ be a set. Then $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{2}$ and $I$, if $I$ is discrete and there exists an element $U$ of $\wp X$ such that $x_{2}$ is an element of $U$ and $U$ is open and the preimage of $f$ and $U$ is open and there exists a homeomorphism $H$ of the set of elements of the preimage of $f$ and $U$ and $\mathrm{Prod}$ applied to the set of elements of $U$ and $I$ such that for all elements $x_{4}$ of the preimage of $f$ and $U$, $\EqtMACRoH {\ProdfstMACRoZ {H (x_{4})}}{f (x_{4})}$.

IsEvenlyCovered.fiberHomeomorphdefMathlib.Topology.Covering.Basic, function or constant

Wording

the fiber homeomorphism of h (from the name)

English

Assume that $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{3}$ and $I$. Then the fiber homeomorphism of $h$ is a homeomorphism of $I$ and the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{3}$.

IsEvenlyCovered.toTrivializationdefMathlib.Topology.Covering.Basic, function or constant

Wording

the trivialization of h1 (from the name)

English

Assume that $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{3}$ and $I$. Then the trivialization of $h_{1}$ is a trivialization of the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{3}$ and $f$ defined as the composition fiber homeomorphism of the trivialization of $h_{1}$ and the fiber homeomorphism of $h_{1}$.

IsEvenlyCovered.toTrivialization'defMathlib.Topology.Covering.Basic, function or constant

Wording

the trivialization of h1 (from the name)

English

Assume that $\mathrm{IsEvenlyCovered}$ holds for $f$, $x_{3}$ and $I$. Then the trivialization of $h_{1}$ is a trivialization of $I$ and $f$.

IsOpen.trivializationDiscretedefMathlib.Topology.Covering.Basic, function or constant

Wording

no wording

English

Let $U$ be a function from elements of $x_{2}$ to elements of $\wp E$. Let $V$ be an element of $\wp X$ such that $V$ is open and for all elements $i_{3}$ of $x_{2}$, for all elements $W$ of $\wp X$, if $W \leq V$, then $W$ is open, if and only if $\operatorname{inter}$ applied to the preimage of $f$ and $W$ and $U$ applied to $i_{3}$ is open. Assume that for all elements $i_{2}$ of $x_{2}$, $f$ is injective on $U$ applied to $i_{2}$. Assume that for all elements $i_{1}$ of $x_{2}$, $\operatorname{SurjOn}$ holds for $f$, $U$ applied to $i_{1}$ and $V$. Assume that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $U$ is pairwise. Assume that the preimage of $f$ and $V$ is less than or equal to the union of the function that maps $i$ to $U$ applied to $i$. Then $\operatorname{trivializationDiscrete}$ applied to $U$, $V$, $\mathrm{open\_V}$, $\mathrm{open\_iff}$, $\mathrm{inj}$, $\mathrm{surj}$, $\mathrm{disjoint}$ and $\mathrm{exhaustive}$ is a trivialization of $x_{2}$ and $f$.

Mathlib.Topology.Covering.Deck

deckdefMathlib.Topology.Covering.Deck, function or constant

Wording

the deck transformation group of p (from the docstring)

English

Let $p$ be a function from elements of $E$ to elements of $X$. Then the deck transformation group of $p$ is a subgroup of the set of homeomorphisms of $E$ and $E$.

Mathlib.Topology.Covering.FundamentalGroupCircle

AddCircle.windingNumberdefMathlib.Topology.Covering.FundamentalGroupCircle, function or constant

Wording

the winding number in x1 (from the docstring)

English

Let $x_{1}$ be a fundamental group of the set of additive circles of $p$ and $x$. Then the winding number in $x_{1}$ is an integer defined as $\operatorname{toAdd}$ applied to $\operatorname{windingNumberIso}$ applied to $x$ and $x_{1}$.

AddCircle.windingNumberIsodefMathlib.Topology.Covering.FundamentalGroupCircle, function or constant

Wording

the winding number isomorphism of x (from the name)

English

Let $x$ be an additive circle of $p$. Then the winding number isomorphism of $x$ is a multiplicative equivalence of the set of fundamental groups of the set of additive circles of $p$ and $x$ and the set of multiplicatives of $\Integer$.

AddCircle.zsmulLoopdefMathlib.Topology.Covering.FundamentalGroupCircle, function or constant

Wording

the loop in p (from the docstring)

English

Let $p$ and $x$ be real numbers. Let $n$ be an integer. Then the loop in $p$ is a path of $\operatorname{mk}$ applied to $x$ and $\operatorname{mk}$ applied to $x$.

Mathlib.Topology.Covering.Quotient

IsAddQuotientCoveringMapstructureMathlib.Topology.Covering.Quotient, predicate

Wording

f is a additive quotient covering map (from the name)

English

Let $f$ be a function from elements of $E$ to elements of $X$. Let $G$ be a set. Then we can say that $f$ is an additive quotient covering map.

IsAddQuotientCoveringMap.fiberEquivAddGroupdefMathlib.Topology.Covering.Quotient, function or constant

Wording

the fiber equivalence additive group of hf and e (from the name)

English

Assume that $f$ is an additive quotient covering map. Let $e$ be an element of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fiber equivalence additive group of $\mathrm{hf}$ and $e$ is an equivalence from the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$ to $G$.

IsQuotientCoveringMapstructureMathlib.Topology.Covering.Quotient, predicate

Wording

f is a quotient covering map (from the name)

English

Let $f$ be a function from elements of $E$ to elements of $X$. Let $G$ be a set. Then we can say that $f$ is a quotient covering map.

IsQuotientCoveringMap.fiberEquivGroupdefMathlib.Topology.Covering.Quotient, function or constant

Wording

the fiber equivalence group of hf and e (from the name)

English

Assume that $f$ is a quotient covering map. Let $e$ be an element of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$. Then the fiber equivalence group of $\mathrm{hf}$ and $e$ is an equivalence from the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$ to $G$.

IsQuotientCoveringMap.toPermFiberdefMathlib.Topology.Covering.Quotient, function or constant

Wording

the permutation fiber of hf and x4 (from the name)

English

Assume that $f$ is a quotient covering map. Let $x_{4}$ be an element of $X$. Then the permutation fiber of $\mathrm{hf}$ and $x_{4}$ is a monoid homomorphism of $G$ and the set of permutations of the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$ defined as the permutation homomorphism of $G$ and the set of elements of the preimage of $f$ and $\operatorname{singleton}$ applied to $x_{4}$.

Topology.IsQuotientMap.trivializationOfSMulDisjointdefMathlib.Topology.Covering.Quotient, function or constant

Wording

the trivialization of U (from the name)

English

Assume that $f$ is a quotient map. Assume that for all elements $x_{6}$ and $x_{7}$ of $E$, $\EqtMACRoH {f (x_{6})}{f (x_{7})}$, if and only if $x_{6}$ is an element of the orbit of $G$ and $x_{7}$. Let $U$ be an element of $\wp E$ such that $U$ is open and for all elements $g$ of $G$, if $\operatorname{inter}$ applied to the image of the function that maps $x_{5}$ to $\HSMulhSMulMACRoAL {g}{x_{5}}$ and $U$ and $U$ is nonempty, then $\EqtMACRoH {g}{1}$. Then the trivialization of $U$ is a trivialization of $G$ and $f$.

Topology.IsQuotientMap.trivializationOfVAddDisjointdefMathlib.Topology.Covering.Quotient, function or constant

Wording

the trivialization of U (from the name)

English

Assume that $f$ is a quotient map. Assume that for all elements $x_{6}$ and $x_{7}$ of $E$, $\EqtMACRoH {f (x_{6})}{f (x_{7})}$, if and only if $x_{6}$ is an element of the orbit of $G$ and $x_{7}$. Let $U$ be an element of $\wp E$ such that $U$ is open and for all elements $g$ of $G$, if $\operatorname{inter}$ applied to the image of the function that maps $x_{5}$ to the sum of $g$ and $x_{5}$ and $U$ and $U$ is nonempty, then $\EqtMACRoH {g}{0}$. Then the trivialization of $U$ is a trivialization of $G$ and $f$.

Mathlib.Topology.Defs.Basic

BaireSpaceclassMathlib.Topology.Defs.Basic, predicate

Wording

X is a Baire space (from the name)

English

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

ContinuousstructureMathlib.Topology.Defs.Basic, predicate

Wording

f is continuous (from the docstring)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $f$ is continuous.

DensedefMathlib.Topology.Defs.Basic, predicate

Wording

s is dense (from the docstring)

English

Let $s$ be an element of $\wp X$. Then $s$ is dense, if for all elements $x_{1}$ of $X$, $x_{1}$ is an element of the closure of $s$.

DenseRangedefMathlib.Topology.Defs.Basic, predicate

Wording

f is a dense range (from the name)

English

Let $f$ be a function from elements of $x_{1}$ to elements of $X$. Then $f$ is a dense range, if the range of $f$ is dense.

IsClopendefMathlib.Topology.Defs.Basic, predicate

Wording

s is a clopen (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is a clopen, if $s$ is closed and open.

IsClosedclassMathlib.Topology.Defs.Basic, predicate

Wording

s is closed (from the docstring)

English

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

IsClosedMapdefMathlib.Topology.Defs.Basic, predicate

Wording

f is a closed map (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is a closed map, if for all elements $U$ of $\wp X$, if $U$ is closed, then the image of $f$ and $U$ is closed.

IsLocallyCloseddefMathlib.Topology.Defs.Basic, predicate

Wording

s is locally closed (from the docstring)

English

generation took over the time limit

IsOpendefMathlib.Topology.Defs.Basic, predicate

Wording

x1 is open (from the name)

English

Let $x_{1}$ be an element of $\wp X$. Then $x_{1}$ is open, if $x_{1}$ is open.

IsOpenMapdefMathlib.Topology.Defs.Basic, predicate

Wording

f is a open map (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is an open map, if for all elements $U$ of $\wp X$, if $U$ is open, then the image of $f$ and $U$ is open.

IsOpenQuotientMapstructureMathlib.Topology.Defs.Basic, predicate

Wording

f is a open quotient 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 an open quotient map.

TopologicalSpaceclassMathlib.Topology.Defs.Basic, predicate

Wording

X is a topological space (from the name)

English

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

TopologicalSpace.IsOpendefMathlib.Topology.Defs.Basic, predicate

Wording

x is open (from the name)

English

Let $x$ be an element of $\wp X$. Then $x$ is open, if $\operatorname{proj0}$ holds for $\mathrm{self}$ and $x$.

Topology.Continuous_ofdefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Topology.IsClopen_ofdefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Topology.IsClosed_ofdefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Topology.IsOpen_ofdefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Topology.closure_ofdefMathlib.Topology.Defs.Basic, function or constant

Wording

the closure (from the name)

English

generation took over the time limit

WithTopologystructureMathlib.Topology.Defs.Basic, type

Wording

no wording

English

Let $X$ be a set such that $X$ is a topological space. Then the elements of $\mathrm{WithTopology}$ applied to $X$ and $t$ are a basic type.

WithTopology.ofTopologydefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{WithTopology}$ applied to $X$ and $t$. Then $\operatorname{ofTopology}$ applied to $\mathrm{self}$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

closuredefMathlib.Topology.Defs.Basic, function or constant

Wording

the closure of s (from the docstring)

English

Let $s$ be an element of $\wp X$. Then the closure of $s$ is an element of $\wp X$ defined as the intersection of $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is closed and $s \leq t$.

coborderdefMathlib.Topology.Defs.Basic, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{coborder}$ applied to $s$ is an element of $\wp X$ defined as the complement of $\operatorname{sdiff}$ applied to the closure of $s$ and $s$.

frontierdefMathlib.Topology.Defs.Basic, function or constant

Wording

the frontier of s (from the docstring)

English

Let $s$ be an element of $\wp X$. Then the frontier of $s$ is an element of $\wp X$ defined as $\operatorname{sdiff}$ applied to the closure of $s$ and the interior of $s$.

interiordefMathlib.Topology.Defs.Basic, function or constant

Wording

the interior of s (from the docstring)

English

Let $s$ be an element of $\wp X$. Then the interior of $s$ is an element of $\wp X$ defined as the union of $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is open and $t \leq s$.

Mathlib.Topology.Defs.Filter

AccPtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $X$. Let $F$ be a filter of $X$. Then $\mathrm{AccPt}$ holds for $x_{1}$ and $F$, if $\operatorname{NeBot}$ holds for the minimum of $\mathrm{nhdsWithin}$ applied to $x_{1}$ and the complement of $\operatorname{singleton}$ applied to $x_{1}$ and $F$.

ClusterPtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $X$. Let $F$ be a filter of $X$. Then $\mathrm{ClusterPt}$ holds for $x_{1}$ and $F$, if $\operatorname{NeBot}$ holds for the minimum of the neighbourhood filter of $x_{1}$ and $F$.

CompactSpaceclassMathlib.Topology.Defs.Filter, predicate

Wording

X is a compact space (from the name)

English

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

ContinuousAtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $x_{2}$ be an element of $X$. Then $\mathrm{ContinuousAt}$ holds for $f$ and $x_{2}$, if $\operatorname{Tendsto}$ holds for $f$, the neighbourhood filter of $x_{2}$ and the neighbourhood filter of $f$ applied to $x_{2}$.

ContinuousOndefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $s$ be an element of $\wp X$. Then $\mathrm{ContinuousOn}$ holds for $f$ and $s$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then $\mathrm{ContinuousWithinAt}$ holds for $f$, $s$ and $x_{2}$.

ContinuousWithinAtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $s$ be an element of $\wp X$. Let $x_{2}$ be an element of $X$. Then $\mathrm{ContinuousWithinAt}$ holds for $f$, $s$ and $x_{2}$, if $\operatorname{Tendsto}$ holds for $f$, $\mathrm{nhdsWithin}$ applied to $x_{2}$ and $s$ and the neighbourhood filter of $f$ applied to $x_{2}$.

Filter.coclosedCompactdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

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

Filter.cocompactdefMathlib.Topology.Defs.Filter, function or constant

Wording

the cocompact of X (from the name)

English

Let $X$ be a set. Then the cocompact of $X$ is a filter of $X$ defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to the principal filter of the complement of $s$.

Filter.limdefMathlib.Topology.Defs.Filter, function or constant

Wording

the limit of f (from the name)

English

Let $f$ be a filter of $X$. Then the limit of $f$ is an element of $X$ defined as $\operatorname{epsilon}$ applied to the function that maps $x_{1}$ to the proposition that $f$ is less than or equal to the neighbourhood filter of $x_{1}$.

Filter.limUnderdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

Let $f$ be a filter of $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $X$. Then $\operatorname{limUnder}$ applied to $f$ and $g$ is an element of $X$ defined as the limit of the forward map of $g$ and $f$.

InseparabledefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $X$. Then $\mathrm{Inseparable}$ holds for $x_{1}$ and $y$, if the neighbourhood filter of $x_{1}$ is equal to the neighbourhood filter of $y$.

IsCompactdefMathlib.Topology.Defs.Filter, predicate

Wording

s is compact (from the name)

English

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

IsLocallyClosedAtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Let $x_{1}$ be an element of $X$. Then $\mathrm{IsLocallyClosedAt}$ holds for $s$ and $x_{1}$, if there exists an element $U$ of $\wp X$, such that $U$ is an element of the neighbourhood filter of $x_{1}$ and there exists an element $Z$ of $\wp X$ such that $Z$ is closed and $\EqtMACRoH {\operatorname{inter} (U , s)}{\operatorname{inter} (U , Z)}$.

LocallyCompactPairclassMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

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

LocallyCompactSpaceclassMathlib.Topology.Defs.Filter, predicate

Wording

X is a locally compact space (from the name)

English

generation took over the time limit

MapClusterPtdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $x_{2}$ be an element of $X$. Let $F$ be a filter of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $X$. Then $\mathrm{MapClusterPt}$ holds for $x_{2}$, $F$ and $u$, if $\mathrm{ClusterPt}$ holds for $x_{2}$ and the forward map of $u$ and $F$.

NoncompactSpaceclassMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

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

SeparationQuotientdefMathlib.Topology.Defs.Filter, type

Wording

separation quotient of X (from the name)

English

Let $X$ be a set. Then a separation quotient of $X$ is an element of the function that maps $X$ to $\mathrm{Quotient}$ applied to $\mathrm{inseparableSetoid}$ applied to $X$.

SpecializesdefMathlib.Topology.Defs.Filter, predicate

Wording

no wording

English

Let $x_{1}$ and $y$ be elements of $X$. Then $\mathrm{Specializes}$ holds for $x_{1}$ and $y$, if the neighbourhood filter of $x_{1}$ is less than or equal to the neighbourhood filter of $y$.

Topology.nhdsGEdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

generation took over the time limit

Topology.nhdsGTdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

generation took over the time limit

Topology.nhdsLEdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

generation took over the time limit

Topology.nhdsLTdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

generation took over the time limit

Topology.nhdsNEdefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

generation took over the time limit

WeaklyLocallyCompactSpaceclassMathlib.Topology.Defs.Filter, predicate

Wording

X is a weakly locally compact space (from the name)

English

generation took over the time limit

nhdsdefMathlib.Topology.Defs.Filter, function or constant

Wording

the neighbourhood filter of x1 (from the name)

English

Let $x_{1}$ be an element of $X$. Then the neighbourhood filter of $x_{1}$ is a filter of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Topology\_\_Defs\_\_Filter\_\_49692738\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{1}$.

nhdsKerdefMathlib.Topology.Defs.Filter, function or constant

Wording

the neighbourhood filter kernel of s (from the name)

English

Let $s$ be an element of $\wp X$. Then the neighbourhood filter kernel of $s$ is an element of $\wp X$ defined as the kernel of the neighbourhood filter set of $s$.

nhdsSetdefMathlib.Topology.Defs.Filter, function or constant

Wording

the neighbourhood filter set of s (from the name)

English

Let $s$ be an element of $\wp X$. Then the neighbourhood filter set of $s$ is a filter of $X$ defined as the supremum of the image of $\mathrm{nhds}$ and $s$.

nhdsSetWithindefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

Let $s$ and $t$ be elements of $\wp X$. Then $\mathrm{nhdsSetWithin}$ applied to $s$ and $t$ is a filter of $X$ defined as the minimum of the neighbourhood filter set of $s$ and the principal filter of $t$.

nhdsWithindefMathlib.Topology.Defs.Filter, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $X$. Let $s$ be an element of $\wp X$. Then $\mathrm{nhdsWithin}$ applied to $x_{1}$ and $s$ is a filter of $X$ defined as the minimum of the neighbourhood filter of $x_{1}$ and the principal filter of $s$.

Mathlib.Topology.Defs.Induced

Topology.IsClosedEmbeddingstructureMathlib.Topology.Defs.Induced, predicate

Wording

f is a closed embedding (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 closed embedding.

Topology.IsCoherentWithstructureMathlib.Topology.Defs.Induced, predicate

Wording

no wording

English

Let $S$ be an element of $\wp (\wp X)$. Then we can say that $\operatorname{IsCoherentWith}$ holds for $S$.

Topology.IsCoinducingstructureMathlib.Topology.Defs.Induced, predicate

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $\operatorname{IsCoinducing}$ holds for $f$.

Topology.IsEmbeddingstructureMathlib.Topology.Defs.Induced, predicate

Wording

f is an embedding (from the docstring)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $f$ is an embedding.

Topology.IsInducingstructureMathlib.Topology.Defs.Induced, predicate

Wording

no wording

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $\operatorname{IsInducing}$ holds for $f$.

Topology.IsOpenEmbeddingstructureMathlib.Topology.Defs.Induced, predicate

Wording

f is a open embedding (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $f$ is an open embedding.

Topology.IsQuotientMapstructureMathlib.Topology.Defs.Induced, predicate

Wording

f is a quotient map (from the docstring)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $f$ is a quotient map.

WithTopology.equivdefMathlib.Topology.Defs.Induced, function or constant

Wording

the equivalence of X and t (from the name)

English

Let $X$ be a set such that $X$ is a topological space. Then the equivalence of $X$ and $t$ is an element of $\EquivMACRoAE {\mathrm{WithTopology} (X , t)}{X}$.

Mathlib.Topology.Defs.Sequences

FrechetUrysohnSpaceclassMathlib.Topology.Defs.Sequences, predicate

Wording

X is a Frechet Urysohn space (from the name)

English

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

IsSeqCloseddefMathlib.Topology.Defs.Sequences, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{IsSeqClosed}$ holds for $s$, if for all functions $x_{1}$ from natural numbers to elements of $X$, for all elements $p$ of $X$, if for all natural numbers $n$, $\MembershipmemMACRoT {s}{x_{1} (n)}$, then if $\operatorname{Tendsto}$ holds for $x_{1}$, $\operatorname{atTop}$ and the neighbourhood filter of $p$, then $p$ is an element of $s$.

IsSeqCompactdefMathlib.Topology.Defs.Sequences, predicate

Wording

s is a sequence compact (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is a sequence compact, if for all functions $x_{1}$ from natural numbers to elements of $X$, if for all natural numbers $n$, $\MembershipmemMACRoT {s}{x_{1} (n)}$, then there exists an element $a$ of $X$, such that $a$ is an element of $s$ and there exists a function $x_{2}$ from natural numbers to natural numbers such that $\mathrm{StrictMono}$ holds for $x_{2}$ and $\operatorname{Tendsto}$ holds for $\operatorname{comp}$ applied to $x_{1}$ and $x_{2}$, $\operatorname{atTop}$ and the neighbourhood filter of $a$.

SeqCompactSpaceclassMathlib.Topology.Defs.Sequences, predicate

Wording

X is a sequence compact space (from the name)

English

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

SeqContinuousdefMathlib.Topology.Defs.Sequences, predicate

Wording

f is sequentially continuous (from the docstring)

English

generation took over the time limit

SequentialSpaceclassMathlib.Topology.Defs.Sequences, predicate

Wording

X is a sequential space (from the name)

English

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

seqClosuredefMathlib.Topology.Defs.Sequences, function or constant

Wording

the sequential closure of s (from the docstring)

English

Let $s$ be an element of $\wp X$. Then the sequential closure of $s$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that there exists a function $x_{1}$ from natural numbers to elements of $X$, such that for all natural numbers $n$, $\MembershipmemMACRoT {s}{x_{1} (n)}$ and $\operatorname{Tendsto}$ holds for $x_{1}$, $\operatorname{atTop}$ and the neighbourhood filter of $a$.

Mathlib.Topology.Defs.Ultrafilter

Ultrafilter.limdefMathlib.Topology.Defs.Ultrafilter, function or constant

Wording

the limit of F (from the name)

English

Let $F$ be a ultrafilter of $X$. Then the limit of $F$ is an element of $X$ defined as the limit of $\operatorname{toFilter}$ applied to $F$.

Mathlib.Topology.DenseEmbedding

Dense.extenddefMathlib.Topology.DenseEmbedding, function or constant

Wording

no wording

English

Assume that $s$ is dense. Let $f$ be a function from elements of $s$ to elements of $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{extend}$ applied to $\mathrm{hs}$, $f$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{extend}$ applied to $\mathrm{Dense\_\_isDenseInducing\_val}$ applied to $\mathrm{hs}$, $f$ and $x_{4}$.

IsDenseEmbeddingstructureMathlib.Topology.DenseEmbedding, predicate

Wording

e is a dense embedding (from the name)

English

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

IsDenseEmbedding.subtypeEmbdefMathlib.Topology.DenseEmbedding, function or constant

Wording

the subtype embedding of e and x3 (from the name)

English

Let $p$ be a function from elements of $x_{2}$ to propositions. Let $e$ be a function from elements of $x_{2}$ to elements of $x$. Let $x_{3}$ be an element of $\SubtypeSet {x_{6}}{p (x_{6})}$. Then the subtype embedding of $e$ and $x_{3}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{closure} (\operatorname{image} (e , \operatorname{ofPred} (\lambda x_{5} . p (x_{5}))))}{x_{4}})}$ defined as $e$ applied to $x_{3}$.

IsDenseInducingstructureMathlib.Topology.DenseEmbedding, predicate

Wording

no wording

English

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

IsDenseInducing.extenddefMathlib.Topology.DenseEmbedding, function or constant

Wording

no wording

English

Assume that $\mathrm{IsDenseInducing}$ holds for $i$. Let $f$ be a function from elements of $x$ to elements of $x_{2}$. Let $b$ be an element of $x_{1}$. Then $\operatorname{extend}$ applied to $\mathrm{di}$, $f$ and $b$ is an element of $x_{2}$ defined as $\operatorname{limUnder}$ applied to the preimage of $i$ and the neighbourhood filter of $b$ and $f$.

Mathlib.Topology.DerivedSet

derivedSetdefMathlib.Topology.DerivedSet, function or constant

Wording

the derived set of A (from the docstring)

English

Let $A$ be an element of $\wp X$. Then the derived set of $A$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to $\mathrm{AccPt}$ applied to $x_{1}$ and the principal filter of $A$.

relDerivedSetdefMathlib.Topology.DerivedSet, function or constant

Wording

the relative derived set (from the name)

English

The relative derived set is an order homomorphism of $\wp X$ and $\wp X$.

Mathlib.Topology.DiscreteQuotient

DiscreteQuotientstructureMathlib.Topology.DiscreteQuotient, type

Wording

discrete quotient of X (from the name)

English

Let $X$ be a set. Then the discrete quotients of $X$ are a basic type.

DiscreteQuotient.LEComapdefMathlib.Topology.DiscreteQuotient, predicate

Wording

no wording

English

Let $f$ be a continuous map of $X$ and $Y$. Let $A$ be a discrete quotient of $X$. Let $B$ be a discrete quotient of $Y$. Then $\operatorname{LEComap}$ holds for $f$, $A$ and $B$, if $A$ is less than or equal to the preimage of $f$ and $B$.

DiscreteQuotient.comapdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the preimage of f and S (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$. Let $S$ be a discrete quotient of $Y$. Then the preimage of $f$ and $S$ is a discrete quotient of $X$.

DiscreteQuotient.equivFinsetClopensdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the equivalence finite set clopen of X (from the name)

English

Let $X$ be a set. Then the equivalence finite set clopen of $X$ is an equivalence from the set of discrete quotients of $X$ to the set of elements of the range of $\operatorname{finsetClopens}$ applied to $X$ defined as the equivalence of $\operatorname{finsetClopens}$ applied to $X$ and $\mathrm{DiscreteQuotient\_\_finsetClopens\_inj}$ applied to $X$.

DiscreteQuotient.finsetClopensdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the finite set clopen of X and d (from the name)

English

Let $X$ be a set. Let $d$ be a discrete quotient of $X$. Then the finite set clopen of $X$ and $d$ is a finite set of the set of clopens of $X$.

DiscreteQuotient.mapdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the map of f and x2 (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$ such that $\operatorname{LEComap}$ holds for $f$, $A$ and $B$. Let $x_{2}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $A$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $B$ defined as the map of $\operatorname{coe}$ applied to $f$ and $x_{2}$.

DiscreteQuotient.ofIsClopendefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the discrete quotient of h (from the name)

English

Assume that $A$ is a clopen. Then the discrete quotient of $h$ is a discrete quotient of $X$.

DiscreteQuotient.ofLEdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the map induced by a refinement of h and x1 (from the docstring)

English

Assume that $A \leq B$. Let $x_{1}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $A$. Then the map induced by a refinement of $h$ and $x_{1}$ is an element of $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $B$ defined as the map of $\mathrm{id}$ and $x_{1}$.

DiscreteQuotient.projdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the projection of S and x1 (from the name)

English

Let $S$ be a discrete quotient of $X$. Let $x_{1}$ be an element of $X$. Then the projection of $S$ and $x_{1}$ is an element of $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $S$ defined as $\operatorname{mk''}$ applied to $x_{1}$.

LocallyConstant.discreteQuotientdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the discrete quotient of f (from the name)

English

Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $x$. Then the discrete quotient of $f$ is a discrete quotient of $X$.

LocallyConstant.liftdefMathlib.Topology.DiscreteQuotient, function or constant

Wording

the lift of f (from the name)

English

Let $f$ be an element of $\mathrm{LocallyConstant}$ applied to $X$ and $x$. Then the lift of $f$ is an element of $\mathrm{LocallyConstant}$ applied to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to the discrete quotient of $f$ and $x$.

Mathlib.Topology.DiscreteSubset

Filter.codiscretedefMathlib.Topology.DiscreteSubset, function or constant

Wording

the codiscrete of X (from the name)

English

Let $X$ be a set. Then the codiscrete of $X$ is a filter of $X$ defined as $\operatorname{codiscreteWithin}$ applied to the universal set.

Filter.codiscreteWithindefMathlib.Topology.DiscreteSubset, function or constant

Wording

no wording

English

Let $S$ be an element of $\wp X$. Then $\operatorname{codiscreteWithin}$ applied to $S$ is a filter of $X$ defined as the supremum of the function that maps $x_{1}$ to the supremum of the function that maps $h$ to $\mathrm{nhdsWithin}$ applied to $x_{1}$ and $\operatorname{sdiff}$ applied to $S$ and $\operatorname{singleton}$ applied to $x_{1}$.

Mathlib.Topology.EMetricSpace.BoundedVariation

BoundedVariationOndefMathlib.Topology.EMetricSpace.BoundedVariation, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $s$ be an element of $\wp x$. Then $\mathrm{BoundedVariationOn}$ holds for $f$ and $s$, if $\mathrm{eVariationOn}$ applied to $f$ and $s$ is distinct from the top.

LocallyBoundedVariationOndefMathlib.Topology.EMetricSpace.BoundedVariation, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $s$ be an element of $\wp x$. Then $\mathrm{LocallyBoundedVariationOn}$ holds for $f$ and $s$, if for all elements $a$ and $b$ of $x$, if $a$ is an element of $s$, then if $b$ is an element of $s$, then $\mathrm{BoundedVariationOn}$ holds for $f$ and $\operatorname{inter}$ applied to $s$ and $\SetIccMACRoP {a}{b}$.

eVariationOndefMathlib.Topology.EMetricSpace.BoundedVariation, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $s$ be an element of $\wp x$. Then $\mathrm{eVariationOn}$ applied to $f$ and $s$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $p$ to $\FinsetSum {\FinsetrangeMACRoN {\ProdfstMACRoZ {p}}}{i}{\operatorname{edist} (f (i + 1), f (i))}$.

Mathlib.Topology.EMetricSpace.Defs

EDistclassMathlib.Topology.EMetricSpace.Defs, predicate

Wording

x is a distance (from the name)

English

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

EDist.edistdefMathlib.Topology.EMetricSpace.Defs, function or constant

Wording

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{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

EMetricSpaceclassMathlib.Topology.EMetricSpace.Defs, predicate

Wording

x is a metric space (from the name)

English

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

Metric.closedEBalldefMathlib.Topology.EMetricSpace.Defs, function or constant

Wording

the closed ball of x1 and x2 (from the name)

English

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be an element of $\mathrm{ENNReal}$. Then the closed ball of $x_{1}$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the extended distance of $y$ and $x_{1}$ is less than or equal to $x_{2}$.

Metric.eballdefMathlib.Topology.EMetricSpace.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{eball}$ applied to $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 extended distance of $y$ and $x_{2}$ is less than $x_{3}$.

PseudoEMetricSpaceclassMathlib.Topology.EMetricSpace.Defs, predicate

Wording

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.

WeakEMetricSpaceclassMathlib.Topology.EMetricSpace.Defs, predicate

Wording

x is a weak metric space (from the name)

English

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

WeakPseudoEMetricSpaceclassMathlib.Topology.EMetricSpace.Defs, predicate

Wording

x is a weak pseudo metric space (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a weak pseudo metric space.

Mathlib.Topology.EMetricSpace.Diam

Metric.ediamdefMathlib.Topology.EMetricSpace.Diam, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\operatorname{ediam}$ applied to $s$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $x_{1}$ to the supremum of the function that maps $h$ to the supremum of the function that maps $y$ to the supremum of the function that maps $h_{1}$ to the extended distance of $x_{1}$ and $y$.

Mathlib.Topology.EMetricSpace.Lipschitz

LipschitzOnWithdefMathlib.Topology.EMetricSpace.Lipschitz, predicate

Wording

no wording

English

Let $K$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{LipschitzOnWith}$ holds for $K$, $f$ and $s$, if for all elements $x_{4}$ of $x$, if $x_{4}$ 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_{4}$ and $f$ applied to $y$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $K$ and the extended distance of $x_{4}$ and $y$.

LipschitzWithdefMathlib.Topology.EMetricSpace.Lipschitz, predicate

Wording

no wording

English

Let $K$ be an element of $\mathrm{NNReal}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{LipschitzWith}$ holds for $K$ and $f$, if for all elements $x_{4}$ and $y$ of $x$, the extended distance of $f$ applied to $x_{4}$ and $f$ applied to $y$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $K$ and the extended distance of $x_{4}$ and $y$.

LocallyLipschitzdefMathlib.Topology.EMetricSpace.Lipschitz, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{LocallyLipschitz}$ holds for $f$, if for all elements $x_{4}$ of $x$, there exists an element $K$ of $\mathrm{NNReal}$, such that there exists an element $t$ of $\wp x$, such that $t$ is an element of the neighbourhood filter of $x_{4}$ and $\mathrm{LipschitzOnWith}$ holds for $K$, $f$ and $t$.

LocallyLipschitzOndefMathlib.Topology.EMetricSpace.Lipschitz, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{LocallyLipschitzOn}$ holds for $s$ and $f$, if for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $s$, then there exists an element $K$ of $\mathrm{NNReal}$, such that there exists an element $t$ of $\wp x$, such that $\MembershipmemMACRoT {\mathrm{nhdsWithin} (x_{4} , s)}{t}$ and $\mathrm{LipschitzOnWith}$ holds for $K$, $f$ and $t$.

Mathlib.Topology.EMetricSpace.PairReduction

PairReduction.logSizeBallSeqdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the logarithm size ball sequence of c and x3 (from the name)

English

Let $J$ be a nonempty finite set of $T$. Let $a$ and $c$ be elements of $\mathrm{ENNReal}$. Let $x_{3}$ be a natural number. Then the logarithm size ball sequence of $c$ and $x_{3}$ is an element of $\operatorname{logSizeBallStruct}$ applied to $T$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{PairReduction\_\_logSizeBallSeq\_\_\_f}$ applied to $J$, $\mathrm{hJ}$, $a$ and $c$.

PairReduction.logSizeBallStructstructureMathlib.Topology.EMetricSpace.PairReduction, type

Wording

no wording

English

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

PairReduction.logSizeBallStruct.balldefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the ball of struct and c (from the name)

English

Let $\mathrm{struct}$ be an element of $\operatorname{logSizeBallStruct}$ applied to $T$. Let $c$ be an element of $\mathrm{ENNReal}$. Then the ball of $\mathrm{struct}$ and $c$ is a finite set of $T$ defined as $\FinsetFilter {x_{2}}{\mathrm{Leq} (\operatorname{edist} (\operatorname{point} (\mathrm{struct}), x_{2}), \operatorname{radius} (\mathrm{struct})\times c)}{\operatorname{finset} (\mathrm{struct})}$.

PairReduction.logSizeBallStruct.finsetdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the underlying finite set of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{logSizeBallStruct}$ applied to $T$. Then the underlying finite set of $\mathrm{self}$ is a finite set of $T$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PairReduction.logSizeBallStruct.pointdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the underlying point of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{logSizeBallStruct}$ applied to $T$. Then the underlying point of $\mathrm{self}$ is an element of $T$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

PairReduction.logSizeBallStruct.radiusdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the underlying radius of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{logSizeBallStruct}$ applied to $T$. Then the underlying radius of $\mathrm{self}$ is a natural number defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

PairReduction.logSizeBallStruct.smallBalldefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the small ball of struct and c (from the name)

English

Let $\mathrm{struct}$ be an element of $\operatorname{logSizeBallStruct}$ applied to $T$. Let $c$ be an element of $\mathrm{ENNReal}$. Then the small ball of $\mathrm{struct}$ and $c$ is a finite set of $T$ defined as $\FinsetFilter {x_{2}}{\mathrm{Leq} (\operatorname{edist} (\operatorname{point} (\mathrm{struct}), x_{2}), (\operatorname{radius} (\mathrm{struct})- 1)\times c)}{\operatorname{finset} (\mathrm{struct})}$.

PairReduction.logSizeRadiusdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the logarithm size radius of a and c (from the name)

English

Let $t$ be an element of $T$. Let $V$ be a finite set of $T$. Let $a$ and $c$ be elements of $\mathrm{ENNReal}$. Then the logarithm size radius of $a$ and $c$ is a natural number defined as $\mathrm{dite}$ applied to $\mathrm{Lt} (1 , a)$, the function that maps $h$ to $\operatorname{find}$ applied to $\mathrm{PairReduction\_\_exists\_radius\_le}$ applied to $t$, $V$, $h$ and $c$ and the function that maps $h_{1}$ to $0$.

PairReduction.pairSetdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the pair set of a and c (from the name)

English

Let $J$ be a finite set of $T$. Let $a$ and $c$ be elements of $\mathrm{ENNReal}$. Then the pair set of $a$ and $c$ is a finite set of $\mathrm{Prod}$ applied to $T$ and $T$ defined as $\operatorname{biUnion}$ applied to the range of the cardinality of $J$ and $\operatorname{pairSetSeq}$ applied to $c$.

PairReduction.pairSetSeqdefMathlib.Topology.EMetricSpace.PairReduction, function or constant

Wording

the pair set sequence of c and n (from the name)

English

Let $J$ be a finite set of $T$. Let $a$ and $c$ be elements of $\mathrm{ENNReal}$. Let $n$ be a natural number. Then the pair set sequence of $c$ and $n$ is a finite set of $\mathrm{Prod}$ applied to $T$ and $T$ defined as $\mathrm{dite}$ applied to the proposition that $J$ is nonempty, the function that maps $\mathrm{hJ}$ to the product of $\operatorname{singleton}$ applied to the underlying point of the logarithm size ball sequence of $c$ and $n$ and the ball of the logarithm size ball sequence of $c$ and $n$ and $c$ and the function that maps $\mathrm{hJ1}$ to $\operatorname{emptyCollection}$.

Mathlib.Topology.EMetricSpace.VariationOnFromTo

variationOnFromTodefMathlib.Topology.EMetricSpace.VariationOnFromTo, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $E$. Let $s$ be an element of $\wp x$. Let $a$ and $b$ be elements of $x$. Then $\mathrm{variationOnFromTo}$ applied to $f$, $s$, $a$ and $b$ is a real number defined as $\iteMACRoG {\mathrm{Leq} (a , b)}{\operatorname{toReal} (\mathrm{eVariationOn} (f , \operatorname{inter} (s , \SetIccMACRoP {a}{b})))}{\operatorname{neg} (\operatorname{toReal} (\mathrm{eVariationOn} (f , \operatorname{inter} (s , \SetIccMACRoP {b}{a}))))}$.

Mathlib.Topology.ExtendFrom

extendFromdefMathlib.Topology.ExtendFrom, function or constant

Wording

no wording

English

Let $A$ be an element of $\wp X$. Let $f$ be a function from elements of $X$ to elements of $Y$. Let $x_{2}$ be an element of $X$. Then $\mathrm{extendFrom}$ applied to $A$, $f$ and $x_{2}$ is an element of $Y$ defined as $\operatorname{limUnder}$ applied to $\mathrm{nhdsWithin}$ applied to $x_{2}$ and $A$ and $f$.

Mathlib.Topology.ExtremallyDisconnected

CompactT2.ProjectivedefMathlib.Topology.ExtremallyDisconnected, predicate

Wording

X is projective (from the name)

English

Let $X$ be a set. Then $X$ is projective, if for all sets $Y$ and $Z$, for all elements $x_{1}$ of $\mathrm{TopologicalSpace}$ applied to $Y$, for all elements $x_{2}$ of $\mathrm{TopologicalSpace}$ applied to $Z$, if $Y$ is a compact space, then if $Y$ is a space, then if $Z$ is a compact space, then if $Z$ is a space, then for all functions $f$ from elements of $X$ to elements of $Z$, for all functions $g$ from elements of $Y$ to elements of $Z$, if $f$ is continuous, then if $g$ is continuous, then if $\operatorname{Surjective}$ holds for $g$, then there exists a function $h_{7}$ from elements of $X$ to elements of $Y$, such that $h_{7}$ is continuous and $\EqtMACRoH {\operatorname{comp} (g , h_{7})}{f}$.

ExtremallyDisconnectedclassMathlib.Topology.ExtremallyDisconnected, predicate

Wording

X is extremally disconnected (from the name)

English

generation took over the time limit

ExtremallyDisconnected.homeoCompactToT2defMathlib.Topology.ExtremallyDisconnected, function or constant

Wording

no wording

English

Assume that $x_{2}$ is continuous. Assume that $\operatorname{Surjective}$ holds for $x_{2}$. Assume that for all elements $x_{3}$ of $\wp E$, if $x_{3}$ is distinct from the universal set, then if $x_{3}$ is closed, then the image of $x_{2}$ and $x_{3}$ is distinct from the universal set. Then $\operatorname{homeoCompactToT2}$ applied to $h_{4}$, $h_{5}$ and $\mathrm{zorn\_subset}$ is a homeomorphism of $E$ and $A$ defined as the homeomorphism of $h_{4}$.

Mathlib.Topology.FiberBundle.Basic

FiberBundleclassMathlib.Topology.FiberBundle.Basic, predicate

Wording

E is a fiber bundle (from the name)

English

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

FiberBundle.extenddefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $F$ be a set. Let $x_{7}$ be an element of $E$ applied to $x_{6}$. Let $\mathrm{x'}$ be an element of $B$. Then $\operatorname{extend}$ applied to $F$, $x_{7}$ and $\mathrm{x'}$ is an element of $E$ applied to $\mathrm{x'}$ defined as the inverse of $\mathrm{x'}$ and the second element of the function of $\operatorname{trivializationAt}$ applied to $F$, $E$ and $x_{6}$ and $\operatorname{mk}$ applied to $x_{6}$ and $x_{7}$.

FiberBundle.homeomorphAtdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Let $b$ be an element of $B$. Then $\operatorname{homeomorphAt}$ applied to $F$, $E$ and $b$ is a homeomorphism of $E$ applied to $b$ and $F$ defined as the composition of the composition of the homeomorphism of $\mathrm{FiberBundle\_\_totalSpaceMk\_isEmbedding}$ applied to $F$, $E$ and $b$ and the set congruence of $\mathrm{Bundle\_\_TotalSpace\_\_range\_mk}$ applied to $b$ and the preimage singleton homeomorphism of $\operatorname{trivializationAt}$ applied to $F$, $E$ and $b$ and $\mathrm{FiberBundle\_\_mem\_baseSet\_trivializationAt'}$ applied to $b$.

FiberBundle.trivializationAtdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Let $b$ be an element of $B$. Then $\operatorname{trivializationAt}$ applied to $F$, $E$ and $b$ is a trivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{trivializationAt'}$ applied to $b$.

FiberBundle.trivializationAt'defMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ be an element of $B$. Then $\operatorname{trivializationAt'}$ applied to $x_{4}$ is a trivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{4}$.

FiberBundle.trivializationAtlasdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

the trivialization atlas of F and E (from the name)

English

Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Then the trivialization atlas of $F$ and $E$ is an element of the power set of the set of trivializations of $F$ and $\operatorname{proj}$ defined as the trivialization atlas.

FiberBundle.trivializationAtlas'defMathlib.Topology.FiberBundle.Basic, function or constant

Wording

the trivialization atlas (from the name)

English

The trivialization atlas is an element of the power set of the set of trivializations of $F$ and $\operatorname{proj}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

FiberBundleCorestructureMathlib.Topology.FiberBundle.Basic, type

Wording

fiber bundle of B and F (from the name)

English

Let $x$, $B$ and $F$ be sets. Then the fiber bundles of $B$ and $F$ are a basic type.

FiberBundleCore.BasedefMathlib.Topology.FiberBundle.Basic, type

Wording

base of _Z (from the name)

English

Let $\mathrm{\_Z}$ be a fiber bundle of $B$ and $F$. Then a base of $\mathrm{\_Z}$ is an element of the function that maps $\mathrm{\_Z}$ to $B$.

FiberBundleCore.FiberdefMathlib.Topology.FiberBundle.Basic, type

Wording

fiber of x3 and _x (from the name)

English

Let $x_{3}$ be a fiber bundle of $B$ and $F$. Let $\mathrm{\_x}$ be an element of $B$. Then a fiber of $x_{3}$ and $\mathrm{\_x}$ is an element of the function that maps $x_{3}$ and $\mathrm{\_x}$ to $F$.

FiberBundleCore.IndexdefMathlib.Topology.FiberBundle.Basic, type

Wording

index of _Z (from the name)

English

Let $\mathrm{\_Z}$ be a fiber bundle of $B$ and $F$. Then an index of $\mathrm{\_Z}$ is an element of the function that maps $\mathrm{\_Z}$ to $x$.

FiberBundleCore.TotalSpacedefMathlib.Topology.FiberBundle.Basic, type

Wording

total space of Z (from the name)

English

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

FiberBundleCore.baseSetdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

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

English

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

FiberBundleCore.coordChangedefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

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

English

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

FiberBundleCore.indexAtdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

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

FiberBundleCore.localTrivdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $Z$ be a fiber bundle of $B$ and $F$. Let $i$ be an element of $x$. Then $\operatorname{localTriv}$ applied to $Z$ and $i$ is a trivialization of $F$ and $\operatorname{proj}$ applied to $Z$.

FiberBundleCore.localTrivAsPartialEquivdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $Z$ be a fiber bundle of $B$ and $F$. Let $i$ be an element of $x$. Then $\operatorname{localTrivAsPartialEquiv}$ applied to $Z$ and $i$ is a partial equivalence of the set of total spaces of $Z$ and $\mathrm{Prod}$ applied to $B$ and $F$.

FiberBundleCore.localTrivAtdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

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

FiberBundleCore.projdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

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

English

Let $Z$ be a fiber bundle of $B$ and $F$. Let $x_{3}$ be a total space of $Z$. Then the projection from the total space of $Z$ and $x_{3}$ is an element of $B$ defined as the projection of $x_{3}$.

FiberBundleCore.trivChangedefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

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

English

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

FiberPrebundlestructureMathlib.Topology.FiberBundle.Basic, type

Wording

no wording

English

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

FiberPrebundle.pretrivializationAtdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\mathrm{FiberPrebundle}$ applied to $F$ and $E$. Let $x_{3}$ be an element of $B$. Then $\operatorname{pretrivializationAt}$ applied to $\mathrm{self}$ and $x_{3}$ is a pretrivialization of $F$ and $\operatorname{proj}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.

FiberPrebundle.pretrivializationAtlasdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

the pretrivialization atlas of self (from the name)

English

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

FiberPrebundle.trivializationOfMemPretrivializationAtlasdefMathlib.Topology.FiberBundle.Basic, function or constant

Wording

the trivialization of a and he (from the name)

English

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

MemTrivializationAtlasclassMathlib.Topology.FiberBundle.Basic, predicate

Wording

e is a membership trivialization atlas (from the name)

English

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

Mathlib.Topology.FiberBundle.Constructions

Bundle.Trivial.homeomorphProddefMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the homeomorphism product of B and F (from the name)

English

Let $B$ and $F$ be sets. Then the homeomorphism product of $B$ and $F$ is a homeomorphism of the set of total spaces of $F$ and $\operatorname{Trivial}$ applied to $B$ and $F$ and $\mathrm{Prod}$ applied to $B$ and $F$ defined as the homeomorphism of the product of $B$ and $F$ and $\mathrm{Bundle\_\_Trivial\_\_isInducing\_toProd}$ applied to $B$ and $F$.

Bundle.Trivial.trivializationdefMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the trivialization of B and F (from the name)

English

Let $B$ and $F$ be sets. Then the trivialization of $B$ and $F$ is a trivialization of $F$ and $\operatorname{proj}$.

Bundle.Trivialization.Prod.invFun'defMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the inverse function of x10 and p (from the name)

English

Let $x_{9}$ be a trivialization of $x_{1}$ and $\operatorname{proj}$. Let $x_{10}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Let $p$ be an element of $\mathrm{Prod}$ applied to $B$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$. Then the inverse function of $x_{10}$ and $p$ is a total space of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and the function that maps $x_{13}$ to $\mathrm{Prod}$ applied to $x_{3}$ applied to $x_{13}$ and $x_{7}$ applied to $x_{13}$ defined as $\operatorname{mk}$ applied to $\ProdfstMACRoZ {p}$ and $\ProdmkMACRoU {\operatorname{symm} (\ProdfstMACRoZ {p}, \ProdfstMACRoZ {\ProdsndMACRoAA {p}})}{\operatorname{symm} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {\ProdsndMACRoAA {p}})}$.

Bundle.Trivialization.Prod.toFun'defMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the function of x10 and x11 (from the name)

English

Let $x_{9}$ be a trivialization of $x_{1}$ and $\operatorname{proj}$. Let $x_{10}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Let $x_{11}$ be a total space of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and the function that maps $x_{12}$ to $\mathrm{Prod}$ applied to $x_{3}$ applied to $x_{12}$ and $x_{7}$ applied to $x_{12}$. Then the function of $x_{10}$ and $x_{11}$ is an element of $\mathrm{Prod}$ applied to $B$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ defined as $\ProdmkMACRoU {\operatorname{proj} (x_{11})}{(\ProdmkMACRoU {\ProdsndMACRoAA {\operatorname{toFun'} (x_{9} , \operatorname{mk} (\operatorname{proj} (x_{11}), \ProdfstMACRoZ {\operatorname{snd} (x_{11})}))}}{\ProdsndMACRoAA {\operatorname{toFun'} (x_{10} , \operatorname{mk} (\operatorname{proj} (x_{11}), \ProdsndMACRoAA {\operatorname{snd} (x_{11})}))}})}$.

Bundle.Trivialization.proddefMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the product of x9 and x10 (from the name)

English

Let $x_{9}$ be a trivialization of $x_{1}$ and $\operatorname{proj}$. Let $x_{10}$ be a trivialization of $x_{5}$ and $\operatorname{proj}$. Then the product of $x_{9}$ and $x_{10}$ is a trivialization of $\mathrm{Prod}$ applied to $x_{1}$ and $x_{5}$ and $\operatorname{proj}$.

Bundle.Trivialization.pullbackdefMathlib.Topology.FiberBundle.Constructions, function or constant

Wording

the pullback of e and f (from the name)

English

Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $f$ be an element of $K$. Then the pullback of $e$ and $f$ is a trivialization of $F$ and $\operatorname{proj}$.

Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle

IsHomeomorphicTrivialFiberBundledefMathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle, predicate

Wording

proj is a homeomorphic trivial fiber bundle (from the name)

English

Let $F$ be a set. Let $\mathrm{proj}$ be a function from elements of $Z$ to elements of $B$. Then $\mathrm{proj}$ is a homeomorphic trivial fiber bundle, if there exists a homeomorphism $e$ of $Z$ and $\mathrm{Prod}$ applied to $B$ and $F$, such that for all elements $x_{3}$ of $Z$, $\EqtMACRoH {\ProdfstMACRoZ {e (x_{3})}}{\mathrm{proj} (x_{3})}$.

Mathlib.Topology.FiberBundle.Trivialization

Bundle.PretrivializationstructureMathlib.Topology.FiberBundle.Trivialization, type

Wording

pretrivialization of F and proj (from the name)

English

Let $F$ be a set. Let $\mathrm{proj}$ be a function from elements of $Z$ to elements of $B$. Then the pretrivializations of $F$ and $\mathrm{proj}$ are a basic type.

Bundle.Pretrivialization.baseSetdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the base set of self (from the name)

English

Let $\mathrm{self}$ be a pretrivialization of $F$ and $\mathrm{proj}$. Then the base set of $\mathrm{self}$ is an element of $\wp B$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Bundle.Pretrivialization.codExtenddefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Assume that $s$ is open. Assume that $s$ is nonempty. Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{codExtend}$ applied to $\mathrm{hs}$, $\mathrm{nonempty}$ and $e$ is a pretrivialization of $F$ and $\operatorname{comp}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\mathrm{proj}$ defined as $\operatorname{codExtend'}$ applied to $\mathrm{hs}$ and $e$.

Bundle.Pretrivialization.codExtend'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Assume that $s$ is open. Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{codExtend'}$ applied to $\mathrm{hs}$ and $e$ is a pretrivialization of $F$ and $\operatorname{comp}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\mathrm{proj}$.

Bundle.Pretrivialization.domExtenddefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $e$ be a pretrivialization of $F$ and the function that maps $z$ to $\mathrm{proj}$ applied to $z$. Then $\operatorname{domExtend}$ applied to $e$ is a pretrivialization of $F$ and $\mathrm{proj}$.

Bundle.Pretrivialization.restrictPreimagedefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the restriction of e and hs (from the docstring)

English

Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$ such that $\operatorname{inter}$ applied to $s$ and the base set of $e$ is nonempty. Then the restriction of $e$ and $\mathrm{hs}$ is a pretrivialization of $F$ and $\operatorname{restrictPreimage}$ applied to $s$ and $\mathrm{proj}$ defined as the restriction of $e$ and $s$.

Bundle.Pretrivialization.restrictPreimage'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the restriction of e and s (from the docstring)

English

Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$. Let $s$ be an element of $\wp B$. Then the restriction of $e$ and $s$ is a pretrivialization of $F$ and $\operatorname{restrictPreimage}$ applied to $s$ and $\mathrm{proj}$.

Bundle.Pretrivialization.setSymmdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the set inverse of e and x2 (from the name)

English

Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$. Let $x_{2}$ be an element of the target of $\operatorname{toPartialEquiv}$ applied to $e$. Then the set inverse of $e$ and $x_{2}$ is an element of $Z$ defined as $\operatorname{domRestrict}$ applied to the target of $\operatorname{toPartialEquiv}$ applied to $e$, $\operatorname{toFun}$ applied to the inverse of $\operatorname{toPartialEquiv}$ applied to $e$ and $x_{2}$.

Bundle.Pretrivialization.symmdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the inverse of b and y (from the name)

English

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

Bundle.Pretrivialization.toFun'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the function of e and x2 (from the name)

English

Let $e$ be a pretrivialization of $F$ and $\mathrm{proj}$. Let $x_{2}$ be an element of $Z$. Then the function of $e$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $B$ and $F$ defined as the partial equivalence of $\operatorname{toPartialEquiv}$ applied to $e$ and $x_{2}$.

Bundle.TrivializationstructureMathlib.Topology.FiberBundle.Trivialization, type

Wording

trivialization of F and proj (from the name)

English

Let $F$ be a set. Let $\mathrm{proj}$ be a function from elements of $Z$ to elements of $B$. Then the trivializations of $F$ and $\mathrm{proj}$ are a basic type.

Bundle.Trivialization.baseSetdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the base set of self (from the name)

English

Let $\mathrm{self}$ be a trivialization of $F$ and $\mathrm{proj}$. Then the base set of $\mathrm{self}$ is an element of $\wp B$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Bundle.Trivialization.cliftdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $T$ be a trivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{clift}$ applied to $T$ is a continuous map of $\mathrm{Prod}$ applied to the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $T$ and the set of continuous maps of $x_{3}$ and the set of elements of the base set of $T$ and the set of continuous maps of $x_{3}$ and the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $T$.

Bundle.Trivialization.codExtenddefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Assume that $s$ is open. Assume that $s$ is nonempty. Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{codExtend}$ applied to $\mathrm{hs}$, $\mathrm{nonempty}$ and $e$ is a trivialization of $F$ and $\operatorname{comp}$ applied to the function that maps $x_{3}$ to $\MembershipmemMACRoT {s}{x_{3}}$ and $\mathrm{proj}$ defined as $\operatorname{codExtend'}$ applied to $\mathrm{hs}$ and $e$.

Bundle.Trivialization.codExtend'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Assume that $s$ is open. Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{codExtend'}$ applied to $\mathrm{hs}$ and $e$ is a trivialization of $F$ and $\operatorname{comp}$ applied to the function that maps $x_{3}$ to $\MembershipmemMACRoT {s}{x_{3}}$ and $\mathrm{proj}$.

Bundle.Trivialization.compHomeomorphdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the composition homeomorphism of e and h (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $h$ be a homeomorphism of $\mathrm{Z'}$ and $Z$. Then the composition homeomorphism of $e$ and $h$ is a trivialization of $F$ and $\operatorname{comp}$ applied to $\mathrm{proj}$ and $\operatorname{coe}$ applied to $h$.

Bundle.Trivialization.coordChangedefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the coordinate change of b and x5 (from the name)

English

Let $x_{3}$ and $x_{4}$ be trivializations of $F$ and $\mathrm{proj}$. Let $b$ be an element of $B$. Let $x_{5}$ be an element of $F$. Then the coordinate change of $b$ and $x_{5}$ is an element of $F$ defined as the second element of the function of $x_{4}$ and the function of the inverse of $\operatorname{toOpenPartialHomeomorph}$ applied to $x_{3}$ and $\ProdmkMACRoU {b}{x_{5}}$.

Bundle.Trivialization.coordChangeHomeomorphdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the coordinate change homeomorphism of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be trivializations of $F$ and $\mathrm{proj}$ such that $b$ is an element of the base set of $x_{3}$ and $b$ is an element of the base set of $x_{4}$. Then the coordinate change homeomorphism of $x_{3}$ and $x_{4}$ is a homeomorphism of $F$ and $F$.

Bundle.Trivialization.disjointUniondefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the disjoint union of e and H (from the name)

English

Let $e$ and $\mathrm{e'}$ be trivializations of $F$ and $\mathrm{proj}$ such that the base set of $e$ is disjoint to the base set of $\mathrm{e'}$. Then the disjoint union of $e$ and $\mathrm{e'}$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.domExtenddefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Assume that the preimage of $\mathrm{proj}$ and $s$ is open. Let $e$ be a trivialization of $F$ and the function that maps $z$ to $\mathrm{proj}$ applied to $z$. Then $\operatorname{domExtend}$ applied to $\mathrm{hps}$ and $e$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.homeomorphCompdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the homeomorphism composition of e and h (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $h$ be a homeomorphism of $B$ and $\mathrm{B'}$. Then the homeomorphism composition of $e$ and $h$ is a trivialization of $F$ and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $h$ and $\mathrm{proj}$.

Bundle.Trivialization.liftdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the lift of z and b (from the name)

English

Let $T$ be a trivialization of $F$ and $\mathrm{proj}$. Let $z$ be an element of $Z$. Let $b$ be an element of $B$. Then the lift of $z$ and $b$ is an element of $Z$ defined as the inverse function of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $T$ and $\ProdmkMACRoU {b}{\ProdsndMACRoAA {\operatorname{toFun'} (T , z)}}$.

Bundle.Trivialization.liftCMdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $T$ be a trivialization of $F$ and $\mathrm{proj}$. Then $\operatorname{liftCM}$ applied to $T$ is a continuous map of $\mathrm{Prod}$ applied to the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $T$ and the set of elements of the base set of $T$ and the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $T$.

Bundle.Trivialization.piecewisedefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $e$ and $\mathrm{e'}$ be trivializations of $F$ and $\mathrm{proj}$. Let $s$ be an element of $\wp B$ such that $\operatorname{inter}$ applied to the base set of $e$ and the frontier of $s$ is equal to $\operatorname{inter}$ applied to the base set of $\mathrm{e'}$ and the frontier of $s$ and $\operatorname{EqOn}$ holds for $\operatorname{toFun'}$ applied to $e$, $\operatorname{toFun'}$ applied to $\mathrm{e'}$ and the preimage of $\mathrm{proj}$ and $\operatorname{inter}$ applied to the base set of $e$ and the frontier of $s$. Then $\operatorname{piecewise}$ applied to $e$, $\mathrm{e'}$, $s$, $\mathrm{Hs}$ and $\mathrm{Heq}$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.piecewiseLedefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $e$ and $\mathrm{e'}$ be trivializations of $F$ and $\mathrm{proj}$. Let $a$ be an element of $B$ such that $a$ is an element of the base set of $e$ and $a$ is an element of the base set of $\mathrm{e'}$. Then $\operatorname{piecewiseLe}$ applied to $e$, $\mathrm{e'}$, $a$, $\mathrm{He}$ and $\mathrm{He'}$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.piecewiseLeOfEqdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

no wording

English

Let $e$ and $\mathrm{e'}$ be trivializations of $F$ and $\mathrm{proj}$. Let $a$ be an element of $B$ such that $a$ is an element of the base set of $e$, $a$ is an element of the base set of $\mathrm{e'}$ and for all elements $p$ of $Z$, if $\EqtMACRoH {\mathrm{proj} (p)}{a}$, then the function of $e$ and $p$ is equal to the function of $\mathrm{e'}$ and $p$. Then $\operatorname{piecewiseLeOfEq}$ applied to $e$, $\mathrm{e'}$, $a$, $\mathrm{He}$, $\mathrm{He'}$ and $\mathrm{Heq}$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.preimageHomeomorphdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the preimage of e and hb (from the docstring)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$ such that $s$ is less than or equal to the base set of $e$. Then the preimage of $e$ and $\mathrm{hb}$ is a homeomorphism of the set of elements of the preimage of $\mathrm{proj}$ and $s$ and $\mathrm{Prod}$ applied to the set of elements of $s$ and $F$ defined as the composition of the homeomorphism of $\operatorname{toOpenPartialHomeomorph}$ applied to $e$ and the composition of the product of $s$ and the universal set and the product congruence of the identity of the set of elements of $s$ and the universal set of $F$.

Bundle.Trivialization.preimageSingletonHomeomorphdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the preimage singleton homeomorphism of e and hb (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$ such that $b$ is an element of the base set of $e$. Then the preimage singleton homeomorphism of $e$ and $\mathrm{hb}$ is a homeomorphism of the set of elements of the preimage of $\mathrm{proj}$ and $\operatorname{singleton}$ applied to $b$ and $F$.

Bundle.Trivialization.restrOpendefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the restriction open of e and s (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $s$ be an open element of $\wp B$. Then the restriction open of $e$ and $s$ is a trivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.restrictPreimagedefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the restriction of e and hs (from the docstring)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$ such that $\operatorname{inter}$ applied to $s$ and the base set of $e$ is nonempty. Then the restriction of $e$ and $\mathrm{hs}$ is a trivialization of $F$ and $\operatorname{restrictPreimage}$ applied to $s$ and $\mathrm{proj}$ defined as the restriction of $e$ and $s$.

Bundle.Trivialization.restrictPreimage'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the restriction of e and s (from the docstring)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $s$ be an element of $\wp B$. Then the restriction of $e$ and $s$ is a trivialization of $F$ and $\operatorname{restrictPreimage}$ applied to $s$ and $\mathrm{proj}$.

Bundle.Trivialization.sourceHomeomorphBaseSetProddefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the source of e (from the docstring)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Then the source of $e$ is a homeomorphism of the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $e$ and $\mathrm{Prod}$ applied to the set of elements of the base set of $e$ and $F$.

Bundle.Trivialization.symmdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the inverse of b and y (from the name)

English

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

Bundle.Trivialization.toFun'defMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the function of e and x3 (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $x_{3}$ be an element of $Z$. Then the function of $e$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to $B$ and $F$ defined as the partial equivalence of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\operatorname{toOpenPartialHomeomorph}$ applied to $e$ and $x_{3}$.

Bundle.Trivialization.toPretrivializationdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the pretrivialization of e (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Then the pretrivialization of $e$ is a pretrivialization of $F$ and $\mathrm{proj}$.

Bundle.Trivialization.transFiberHomeomorphdefMathlib.Topology.FiberBundle.Trivialization, function or constant

Wording

the composition fiber homeomorphism of e and h (from the name)

English

Let $e$ be a trivialization of $F$ and $\mathrm{proj}$. Let $h$ be a homeomorphism of $F$ and $\mathrm{F'}$. Then the composition fiber homeomorphism of $e$ and $h$ is a trivialization of $\mathrm{F'}$ and $\mathrm{proj}$.

Mathlib.Topology.FiberPartition

TopologicalSpace.Fiber.sigmaIncldefMathlib.Topology.FiberPartition, function or constant

Wording

the sigma inclusion of f and a (from the name)

English

Let $f$ be a function from elements of $S$ to elements of $Y$. Let $a$ be a fiber of $f$. Then the sigma inclusion of $f$ and $a$ is a continuous map of the set of elements of $a$ and $S$.

TopologicalSpace.Fiber.sigmaInclIncldefMathlib.Topology.FiberPartition, function or constant

Wording

the sigma inclusion inclusion of a and b (from the name)

English

Let $f$ be a function from elements of $S$ to elements of $Y$. Let $g$ be a function from elements of $Y$ to elements of $X$. Let $a$ be a fiber of $\operatorname{comp}$ applied to $g$ and $f$. Let $b$ be a fiber of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to the sigma inclusion of $\operatorname{comp}$ applied to $g$ and $f$ and $a$. Then the sigma inclusion inclusion of $a$ and $b$ is a continuous map of the set of elements of $b$ and the set of elements of $\operatorname{mk}$ applied to $f$ and the preimage of $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to the sigma inclusion of $\operatorname{comp}$ applied to $g$ and $f$ and $a$ and $b$.

TopologicalSpace.Fiber.sigmaIsoHomdefMathlib.Topology.FiberPartition, function or constant

Wording

the sigma isomorphism homomorphism of f (from the name)

English

Let $f$ be a function from elements of $S$ to elements of $Y$. Then the sigma isomorphism homomorphism of $f$ is a continuous map of $\Sigma$ applied to the function that maps $x_{1}$ to the set of elements of $x_{1}$ and $S$.

Mathlib.Topology.GDelta.Basic

IsGδdefMathlib.Topology.GDelta.Basic, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{IsG\_u3b4\_}$ holds for $s$, if there exists an element $T$ of $\wp (\wp X)$, such that for all elements $t$ of $\wp X$, if $t$ is an element of $T$, then $t$ is open, $T$ is countable and $s$ is equal to the intersection of $T$.

IsMeagredefMathlib.Topology.GDelta.Basic, predicate

Wording

s is meagre (from the name)

English

Let $s$ be an element of $\wp X$. Then $s$ is meagre, if the complement of $s$ is an element of $\mathrm{residual}$ applied to $X$.

IsNowhereDensedefMathlib.Topology.GDelta.Basic, predicate

Wording

no wording

English

Let $s$ be an element of $\wp X$. Then $\mathrm{IsNowhereDense}$ holds for $s$, if the interior of the closure of $s$ is equal to $\operatorname{emptyCollection}$.

residualdefMathlib.Topology.GDelta.Basic, function or constant

Wording

no wording

English

Let $X$ be a set. Then $\mathrm{residual}$ applied to $X$ is a filter of $X$ defined as $\operatorname{countableGenerate}$ applied to $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is open and dense.

Mathlib.Topology.Germ

Filter.Germ.sliceLeftdefMathlib.Topology.Germ, function or constant

Wording

the left slice of P (from the name)

English

Let $P$ be a germ of the neighbourhood filter of $p$ and $Z$. Then the left slice of $P$ is a germ of the neighbourhood filter of $\ProdfstMACRoZ {p}$ and $Z$.

Filter.Germ.sliceRightdefMathlib.Topology.Germ, function or constant

Wording

the right slice of P (from the name)

English

Let $P$ be a germ of the neighbourhood filter of $p$ and $Z$. Then the right slice of $P$ is a germ of the neighbourhood filter of $\ProdsndMACRoAA {p}$ and $Z$.

Filter.Germ.valuedefMathlib.Topology.Germ, function or constant

Wording

the value of x3 (from the name)

English

Let $x_{3}$ be a germ of the neighbourhood filter of $x_{2}$ and $x$. Then the value of $x_{3}$ is an element of $x$.

Filter.Germ.valueAddHomdefMathlib.Topology.Germ, function or constant

Wording

the value additive homomorphism (from the name)

English

The value additive homomorphism is an additive monoid homomorphism of the set of germs of the neighbourhood filter of $x_{2}$ and $E$ and $E$.

Filter.Germ.valueMulHomdefMathlib.Topology.Germ, function or constant

Wording

the value multiplicative homomorphism (from the name)

English

The value multiplicative homomorphism is a monoid homomorphism of the set of germs of the neighbourhood filter of $x_{2}$ and $E$ and $E$.

Filter.Germ.valueOrderRingHomdefMathlib.Topology.Germ, function or constant

Wording

the value order ring homomorphism (from the name)

English

The value order ring homomorphism is an order ring homomorphism of the set of germs of the neighbourhood filter of $x_{3}$ and $E$ and $E$.

Filter.Germ.valueRingHomdefMathlib.Topology.Germ, function or constant

Wording

the value ring homomorphism (from the name)

English

The value ring homomorphism is a ring homomorphism of the set of germs of the neighbourhood filter of $x_{2}$ and $E$ and $E$.

Filter.Germ.valueₗdefMathlib.Topology.Germ, function or constant

Wording

the value (from the name)

English

The value is a linear map of the set of germs of the neighbourhood filter of $x_{5}$ and $E$ and $E$.

RestrictGermPredicatedefMathlib.Topology.Germ, predicate

Wording

no wording

English

Let $P$ be a function from elements $x_{3}$ of $X$ and germs of the neighbourhood filter of $x_{3}$ and $Y$ to propositions. Let $A$ be an element of $\wp X$. Let $x_{1}$ be an element of $X$. Let $x_{2}$ be a germ of the neighbourhood filter of $x_{1}$ and $Y$. Then we can say that $\mathrm{RestrictGermPredicate}$ holds for $x_{3}$, $P$, $A$, $x_{1}$ and $x_{2}$.

Mathlib.Topology.Gluing

TopCat.GlueDatastructureMathlib.Topology.Gluing, type

Wording

glue data (from the name)

English

The glue data are a basic type.

TopCat.GlueData.MkCorestructureMathlib.Topology.Gluing, type

Wording

no wording

English

The elements of $\operatorname{MkCore}$ are a basic type.

TopCat.GlueData.MkCore.JdefMathlib.Topology.Gluing, type

Wording

no wording

English

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

TopCat.GlueData.MkCore.UdefMathlib.Topology.Gluing, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{MkCore}$. Let $x$ be an element of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{U}$ applied to $\mathrm{self}$ and $x$ is a topological category defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.

TopCat.GlueData.MkCore.VdefMathlib.Topology.Gluing, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{MkCore}$. Let $i$ and $x$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{V}$ applied to $\mathrm{self}$, $i$ and $x$ is an open of the set of carriers of $\operatorname{U}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $i$ and $x$.

TopCat.GlueData.MkCore.tdefMathlib.Topology.Gluing, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{MkCore}$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\mathrm{self}$. Then $\operatorname{t}$ applied to $\mathrm{self}$, $i$ and $j$ is a homomorphism of the action of the topological category of $\operatorname{U}$ applied to $\mathrm{self}$ and $i$ and $\operatorname{V}$ applied to $\mathrm{self}$, $i$ and $j$ and the action of the topological category of $\operatorname{U}$ applied to $\mathrm{self}$ and $j$ and $\operatorname{V}$ applied to $\mathrm{self}$, $j$ and $i$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $i$ and $j$.

TopCat.GlueData.MkCore.t'defMathlib.Topology.Gluing, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{MkCore}$. Let $i$, $j$ and $k$ be elements of $\operatorname{J}$ applied to $h$. Then $\operatorname{t'}$ applied to $h$, $i$, $j$ and $k$ is a homomorphism of the pullback of the inclusion of $\operatorname{V}$ applied to $h$, $i$ and $j$ and the inclusion of $\operatorname{V}$ applied to $h$, $i$ and $k$ and the pullback of the inclusion of $\operatorname{V}$ applied to $h$, $j$ and $k$ and the inclusion of $\operatorname{V}$ applied to $h$, $j$ and $i$.

TopCat.GlueData.ReldefMathlib.Topology.Gluing, predicate

Wording

no wording

English

Let $D$ be a glue data. Let $a$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to the set of carriers of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i_{1}$. Let $b$ be an element of $\Sigma$ applied to the function that maps $i$ to the set of carriers of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then $\operatorname{Rel}$ holds for $D$, $a$ and $b$, if there exists a carrier $x$ of $\operatorname{V}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $\ProdmkMACRoU {\operatorname{fst} (a)}{\operatorname{fst} (b)}$, such that $\EqtMACRoH {\operatorname{hom} (\operatorname{f} (\operatorname{toGlueData} (D), \operatorname{fst} (a), \operatorname{fst} (b)), x)}{\operatorname{snd} (a)}$ and $\EqtMACRoH {\operatorname{hom} (\operatorname{f} (\operatorname{toGlueData} (D), \operatorname{fst} (b), \operatorname{fst} (a)), \operatorname{hom} (\operatorname{t} (\operatorname{toGlueData} (D), \operatorname{fst} (a), \operatorname{fst} (b)), x))}{\operatorname{snd} (b)}$.

TopCat.GlueData.fromOpenSubsetsGluedefMathlib.Topology.Gluing, function or constant

Wording

the canonical map from the glue of U (from the docstring)

English

Let $U$ be a function from elements of $J$ to opens of $x$. Then the canonical map from the glue of $U$ is a homomorphism of $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to the glue data of $U$ and $\operatorname{of}$ applied to $x$.

TopCat.GlueData.mk'defMathlib.Topology.Gluing, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{MkCore}$. Then $\operatorname{mk'}$ applied to $h$ is a glue data.

TopCat.GlueData.ofOpenSubsetsdefMathlib.Topology.Gluing, function or constant

Wording

the glue data of U (from the name)

English

Let $U$ be a function from elements of $J$ to opens of $x$. Then the glue data of $U$ is a glue data.

TopCat.GlueData.openCoverGlueHomeodefMathlib.Topology.Gluing, function or constant

Wording

the gluing of U and h (from the docstring)

English

Let $U$ be a function from elements of $J$ to opens of $x$ such that the union of the function that maps $i$ to $U$ applied to $i$ is equal to the universal set. Then the gluing of $U$ and $h$ is a homeomorphism of the set of carriers of $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to the glue data of $U$ and $x$.

Mathlib.Topology.Hom.ContinuousEval

ContinuousEvalclassMathlib.Topology.Hom.ContinuousEval, predicate

Wording

no wording

English

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

Mathlib.Topology.Hom.ContinuousEvalConst

ContinuousEvalConstclassMathlib.Topology.Hom.ContinuousEvalConst, predicate

Wording

no wording

English

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

Mathlib.Topology.Hom.Open

ContinuousOpenMapstructureMathlib.Topology.Hom.Open, type

Wording

continuous open map of x and x1 (from the name)

English

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

ContinuousOpenMap.compdefMathlib.Topology.Hom.Open, function or constant

Wording

the composition of f and g (from the name)

English

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

ContinuousOpenMap.copydefMathlib.Topology.Hom.Open, function or constant

Wording

the copy of f and h (from the name)

English

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

ContinuousOpenMap.iddefMathlib.Topology.Hom.Open, function or constant

Wording

the identity of x (from the name)

English

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

ContinuousOpenMapClassclassMathlib.Topology.Hom.Open, predicate

Wording

no wording

English

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

Mathlib.Topology.Homeomorph.Defs

Equiv.toHomeomorphdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of e and he (from the name)

English

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

Equiv.toHomeomorphOfContinuousCloseddefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be an equivalence from $X$ to $Y$ such that $\operatorname{coe}$ applied to $e$ is continuous and $\operatorname{coe}$ applied to $e$ is a closed map. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$.

Equiv.toHomeomorphOfContinuousOpendefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be an equivalence from $X$ to $Y$ such that $\operatorname{coe}$ applied to $e$ is continuous and $\operatorname{coe}$ applied to $e$ is an open map. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$.

Equiv.toHomeomorphOfDiscretedefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be an equivalence from $X$ to $Y$. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$.

Equiv.toHomeomorphOfIsInducingdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of f and hf (from the name)

English

Let $f$ be an equivalence from $X$ to $Y$ such that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to $f$. Then the homeomorphism of $f$ and $\mathrm{hf}$ is a homeomorphism of $X$ and $Y$.

HomeomorphstructureMathlib.Topology.Homeomorph.Defs, type

Wording

homeomorphism of X and Y (from the name)

English

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

Homeomorph.changeInvdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

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

English

Let $f$ be a homeomorphism of $X$ and $Y$. Let $g$ be a function from elements of $Y$ to elements of $X$ such that $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the change inverse of $f$ and $g$ is a homeomorphism of $X$ and $Y$.

Homeomorph.emptydefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

no wording

English

$\operatorname{empty}$ is a homeomorphism of $X$ and $Y$.

Homeomorph.homeomorphOfUniquedefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the homeomorphism of $X$ and $Y$ is a homeomorphism of $X$ and $Y$.

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

Wording

the homeomorphism of f (from the name)

English

Let $f$ be an element of $F$. Then the homeomorphism of $f$ is a homeomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the equivalence of $f$, $\mathrm{HomeomorphClass\_\_map\_continuous}$ applied to $f$ and $\mathrm{HomeomorphClass\_\_inv\_continuous}$ applied to $f$.

Homeomorph.refldefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be a set. Then the identity of $X$ is a homeomorphism of $X$ and $X$.

Homeomorph.symmdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the inverse of h (from the name)

English

Let $h$ be a homeomorphism of $X$ and $Y$. Then the inverse of $h$ is a homeomorphism of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toEquiv}$ applied to $h$, $\mathrm{Homeomorph\_\_continuous\_invFun}$ applied to $h$ and $\mathrm{Homeomorph\_\_continuous\_toFun}$ applied to $h$.

Homeomorph.transdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the composition of x3 and x4 (from the name)

English

Let $x_{3}$ be a homeomorphism of $X$ and $Y$. Let $x_{4}$ be a homeomorphism of $Y$ and $Z$. Then the composition of $x_{3}$ and $x_{4}$ is a homeomorphism of $X$ and $Z$.

HomeomorphClassclassMathlib.Topology.Homeomorph.Defs, predicate

Wording

no wording

English

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

IsHomeomorphstructureMathlib.Topology.Homeomorph.Defs, predicate

Wording

f is a homeomorphism (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 homeomorphism.

IsHomeomorph.homeomorphdefMathlib.Topology.Homeomorph.Defs, function or constant

Wording

the homeomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is a homeomorphism. Then the homeomorphism of $f$ and $\mathrm{hf}$ is a homeomorphism of $X$ and $Y$.

Mathlib.Topology.Homeomorph.Lemmas

Continuous.homeoOfEquivCompactToT2defMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism of hf (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is continuous. Then the homeomorphism of $\mathrm{hf}$ is a homeomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{Continuous\_\_continuous\_symm\_of\_equiv\_compact\_to\_t2}$ applied to $\mathrm{hf}$.

Fin.appendHomeomorphdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

Let $m$ and $n$ be natural numbers. Then $\operatorname{appendHomeomorph}$ applied to $m$ and $n$ is a homeomorphism 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$.

Homeomorph.Set.proddefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be an element of $\wp X$. Let $t$ be an element of $\wp Y$. Then the product of $s$ and $t$ is a homeomorphism of the set of elements of $\operatorname{sprod}$ applied to $s$ and $t$ and $\mathrm{Prod}$ applied to the set of elements of $s$ and the set of elements of $t$.

Homeomorph.Set.univdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the universal set of X (from the name)

English

Let $X$ be a set. Then the universal set of $X$ is a homeomorphism of the set of elements of the universal set and $X$.

Homeomorph.finTwoArrowdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

$\operatorname{finTwoArrow}$ is a homeomorphism of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $X$ and $\mathrm{Prod}$ applied to $X$ and $X$.

Homeomorph.funSplitAtdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

Let $Y$ be a set. Let $i$ be an element of $x_{1}$. Then $\operatorname{funSplitAt}$ applied to $Y$ and $i$ is a homeomorphism of the set of functions from elements of $x_{1}$ to elements of $Y$ and $\mathrm{Prod}$ applied to $Y$ and the set of functions from elements of $\SubtypeSet {j}{\mathrm{Neq} (j , i)}$ to elements of $Y$ defined as $\operatorname{piSplitAt}$ applied to $i$ and the function that maps $x_{3}$ to $Y$.

Homeomorph.funUniquedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

Let $x$ and $X$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $X$ is a homeomorphism of the set of functions from elements of $x$ to elements of $X$ and $X$.

Homeomorph.imagedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the image of e and s (from the name)

English

Let $e$ be a homeomorphism of $X$ and $Y$. Let $s$ be an element of $\wp X$. Then the image of $e$ and $s$ is a homeomorphism of the set of elements of $s$ and the set of elements of the image of $\operatorname{coe}$ applied to $e$ and $s$.

Homeomorph.ofDiscretedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism of f (from the name)

English

Let $f$ be an equivalence from $X$ to $Y$. Then the homeomorphism of $f$ is a homeomorphism of $X$ and $Y$.

Homeomorph.piCongrdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

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

English

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

Homeomorph.piCongrLeftdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the left product congruence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $e$ is a homeomorphism 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$.

Homeomorph.piCongrRightdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the right product congruence of F (from the name)

English

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

Homeomorph.piEquivPiSubtypeProddefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the product equivalence product subtype product of p and Y (from the name)

English

Let $p$ be a function from elements of $x$ to propositions. Let $Y$ be a function from elements of $x$ to sets. Then the product equivalence product subtype product of $p$ and $Y$ is a homeomorphism of the set of functions from elements $i$ of $x$ to elements of $Y$ applied to $i$ and $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{3}}{p (x_{3})}$ to elements of $Y$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{4}}{\mathrm{not} (p (x_{4}))}$ to elements of $Y$ applied to $i_{2}$.

Homeomorph.piFinTwodefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

Let $X$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $X$ is a homeomorphism 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$.

Homeomorph.piSplitAtdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Let $Y$ be a function from elements of $x$ to sets. Then $\operatorname{piSplitAt}$ applied to $i$ and $Y$ is a homeomorphism of the set of functions from elements $j$ of $x$ to elements of $Y$ applied to $j$ and $\mathrm{Prod}$ applied to $Y$ applied to $i$ and the set of functions from elements $j_{1}$ of $\SubtypeSet {j_{2}}{\mathrm{Neq} (j_{2} , i)}$ to elements of $Y$ applied to $j_{1}$.

Homeomorph.piUniquedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the product of f (from the docstring)

English

Let $f$ be a function from elements of $x$ to sets. Then the product of $f$ is a homeomorphism of the set of functions from elements $t$ of $x$ to elements of $f$ applied to $t$ and $f$ applied to $\operatorname{default}$.

Homeomorph.prodUniquedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

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

Homeomorph.setCongrdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the set congruence of h (from the name)

English

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

Homeomorph.setsdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the set of h and h_eq (from the name)

English

Let $h$ be a homeomorphism of $X$ and $Y$ such that $s$ is equal to the preimage of $\operatorname{coe}$ applied to $h$ and $t$. Then the set of $h$ and $\mathrm{h\_eq}$ is a homeomorphism of the set of elements of $s$ and the set of elements of $t$.

Homeomorph.sigmaProdDistribdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

no wording

English

$\operatorname{sigmaProdDistrib}$ is a homeomorphism of $\mathrm{Prod}$ applied to $\Sigma$ applied to the function that maps $i$ to $X$ applied to $i$ and $Y$ and $\Sigma$ applied to the function that maps $i_{1}$ to $\mathrm{Prod}$ applied to $X$ applied to $i_{1}$ and $Y$.

Homeomorph.subtypedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the subtype of h and h_iff (from the name)

English

Let $h$ be a homeomorphism of $X$ and $Y$ such that for all elements $x_{3}$ of $X$, $p$ holds for $x_{3}$, if and only if $q$ holds for $h$ applied to $x_{3}$. Then the subtype of $h$ and $\mathrm{h\_iff}$ is a homeomorphism of $\SubtypeSet {x_{2}}{p (x_{2})}$ and $\SubtypeSet {y}{q (y)}$.

Homeomorph.sumArrowHomeomorphProdArrowdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the natural homeomorphism (from the docstring)

English

The natural homeomorphism is a homeomorphism of the set of functions from elements of $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ to elements of $X$ and $\mathrm{Prod}$ applied to the set of functions from elements of $x_{1}$ to elements of $X$ and the set of functions from elements of $x_{2}$ to elements of $X$.

Homeomorph.sumPiEquivProdPidefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

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

English

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

Homeomorph.uliftdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the lift (from the name)

English

The lift is a homeomorphism of $\mathrm{ULift}$ applied to $X$ and $X$.

Homeomorph.uniqueProddefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the unique product of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the unique product of $X$ and $Y$ is a homeomorphism of $\mathrm{Prod}$ applied to $X$ and $Y$ and $Y$ defined as the composition of $\operatorname{prodComm}$ applied to $X$ and $Y$ and $\operatorname{prodUnique}$ applied to $Y$ and $X$.

Topology.IsCoinducing.connectedComponentsHomeomorphdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the connected component homeomorphism of hf and #2 (from the name)

English

Assume that $\operatorname{IsCoinducing}$ holds for $f$. Assume that for all elements $y$ of $Y$, the preimage of $f$ and $\operatorname{singleton}$ applied to $y$ is connected. Then the connected component homeomorphism of $\mathrm{hf}$ and $\mathrm{hf'}$ is a homeomorphism of the set of connected components of $X$ and the set of connected components of $Y$.

Topology.IsEmbedding.homeomorphImagedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism image of hf and s (from the name)

English

Assume that $f$ is an embedding. Let $s$ be an element of $\wp X$. Then the homeomorphism image of $\mathrm{hf}$ and $s$ is a homeomorphism of the set of elements of $s$ and the set of elements of the image of $f$ and $s$.

Topology.IsEmbedding.homeomorphOfSubsetRangedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism of hf and hs (from the name)

English

Assume that $f$ is an embedding. Assume that $s$ is less than or equal to the range of $f$. Then the homeomorphism of $\mathrm{hf}$ and $\mathrm{hs}$ is a homeomorphism of the set of elements of the preimage of $f$ and $s$ and the set of elements of $s$ defined as the composition of the homeomorphism image of $\mathrm{hf}$ and the preimage of $f$ and $s$ and the set congruence of $\mathrm{Set\_\_image\_preimage\_eq\_of\_subset}$ applied to $\mathrm{hs}$.

Topology.IsEmbedding.toHomeomorphdefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism of hf (from the name)

English

Assume that $f$ is an embedding. Then the homeomorphism of $\mathrm{hf}$ is a homeomorphism of $X$ and the set of elements of the range of $f$.

Topology.IsEmbedding.toHomeomorphOfSurjectivedefMathlib.Topology.Homeomorph.Lemmas, function or constant

Wording

the homeomorphism of hf and hsurj (from the name)

English

Assume that $f$ is an embedding. Assume that $\operatorname{Surjective}$ holds for $f$. Then the homeomorphism of $\mathrm{hf}$ and $\mathrm{hsurj}$ is a homeomorphism of $X$ and $Y$.

Mathlib.Topology.Homeomorph.Quotient

Homeomorph.Quot.congrdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

the congruence of e and eq (from the name)

English

Let $e$ be a homeomorphism of $X$ and $Y$ such that for all elements $x_{2}$ and $x_{3}$ of $X$, $\mathrm{rX}$ holds for $x_{2}$ and $x_{3}$, if and only if $\mathrm{rY}$ holds for $e$ applied to $x_{2}$ and $e$ applied to $x_{3}$. Then the congruence of $e$ and $\mathrm{eq}$ is a homeomorphism of $\mathrm{Quot}$ applied to $\mathrm{rX}$ and $\mathrm{Quot}$ applied to $\mathrm{rY}$.

Homeomorph.Quot.congrLeftdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

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 a homeomorphism of $\mathrm{Quot}$ applied to $r$ and $\mathrm{Quot}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $r$ applied to $\operatorname{symm}$ applied to $e$ and $x_{2}$ and $\operatorname{symm}$ applied to $e$ and $x_{3}$.

Homeomorph.Quot.congrRightdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

the right congruence of eq (from the name)

English

Assume that for all elements $x_{1}$ and $x_{2}$ of $X$, $r$ holds for $x_{1}$ and $x_{2}$, if and only if $\mathrm{r'}$ holds for $x_{1}$ and $x_{2}$. Then the right congruence of $\mathrm{eq}$ is a homeomorphism of $\mathrm{Quot}$ applied to $r$ and $\mathrm{Quot}$ applied to $\mathrm{r'}$ defined as the congruence of the identity of $X$ and $\mathrm{eq}$.

Homeomorph.Quotient.congrdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

the congruence of e and eq (from the name)

English

Let $e$ be a homeomorphism of $X$ and $Y$ such that for all elements $x_{2}$ and $x_{3}$ of $X$, $\operatorname{r}$ holds for $x_{2}$ and $x_{3}$, if and only if $\operatorname{r}$ holds for $e$ applied to $x_{2}$ and $e$ applied to $x_{3}$. Then the congruence of $e$ and $\mathrm{eq}$ is a homeomorphism of $\mathrm{Quotient}$ applied to $\mathrm{rX}$ and $\mathrm{Quotient}$ applied to $\mathrm{rY}$ defined as the congruence of $e$ and $\mathrm{eq}$.

Homeomorph.Quotient.congrRightdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

the right congruence of eq (from the name)

English

Assume that for all elements $x_{1}$ and $x_{2}$ of $X$, $\operatorname{r}$ holds for $x_{1}$ and $x_{2}$, if and only if $\operatorname{r}$ holds for $x_{1}$ and $x_{2}$. Then the right congruence of $\mathrm{eq}$ is a homeomorphism of $\mathrm{Quotient}$ applied to $r$ and $\mathrm{Quotient}$ applied to $\mathrm{r'}$ defined as the right congruence of $\mathrm{eq}$.

Homeomorph.quotientBotdefMathlib.Topology.Homeomorph.Quotient, function or constant

Wording

the quotient by the trivial relation (from the docstring)

English

The quotient by the trivial relation is a homeomorphism of $\mathrm{Quotient}$ applied to the bottom and $X$.

Mathlib.Topology.Homeomorph.TransferInstance

Equiv.homeomorphdefMathlib.Topology.Homeomorph.TransferInstance, function or constant

Wording

the homeomorphism of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the homeomorphism of $e$ is a homeomorphism of $x$ and $x_{1}$.

Mathlib.Topology.Homotopy.Affine

ContinuousMap.Homotopy.affinedefMathlib.Topology.Homotopy.Affine, function or constant

Wording

the affine of f and g (from the name)

English

Let $f$ and $g$ be continuous maps of $X$ and $E$. Then the affine of $f$ and $g$ is a homotopy of $f$ and $g$.

Mathlib.Topology.Homotopy.Basic

ContinuousMap.HomotopicdefMathlib.Topology.Homotopy.Basic, predicate

Wording

x2 is homotopic to x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Then $x_{2}$ is homotopic to $x_{3}$, if $\mathrm{Nonempty}$ holds for the set of homotopies of $x_{2}$ and $x_{3}$.

ContinuousMap.HomotopicReldefMathlib.Topology.Homotopy.Basic, predicate

Wording

x3 is a homotopic relation with respect to S (from the name)

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Let $S$ be an element of $\wp X$. Then $x_{3}$ is a homotopic relation with respect to $S$, if $\mathrm{Nonempty}$ holds for the set of homotopy relations of $x_{3}$ and $S$.

ContinuousMap.HomotopicWithdefMathlib.Topology.Homotopy.Basic, predicate

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Let $P$ be a function from continuous maps of $X$ and $Y$ to propositions. Then $\operatorname{HomotopicWith}$ holds for $x_{2}$, $x_{3}$ and $P$, if $\mathrm{Nonempty}$ holds for $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and $P$.

ContinuousMap.HomotopystructureMathlib.Topology.Homotopy.Basic, type

Wording

homotopy of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Then the homotopies of $x_{2}$ and $x_{3}$ are a basic type.

ContinuousMap.Homotopy.castdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the cast of F (from the name)

English

Let $F$ be a homotopy of $x_{2}$ and $x_{3}$. Assume that $\EqtMACRoH {x_{2}}{x_{4}}$. Assume that $\EqtMACRoH {x_{3}}{x_{5}}$. Then the cast of $F$ is a homotopy of $x_{4}$ and $x_{5}$.

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

Wording

the composition of G and F (from the name)

English

Let $G$ be a homotopy of $x_{5}$ and $x_{6}$. Let $F$ be a homotopy of $x_{3}$ and $x_{4}$. Then the composition of $G$ and $F$ is a homotopy of the composition of $x_{5}$ and $x_{3}$ and the composition of $x_{6}$ and $x_{4}$.

ContinuousMap.Homotopy.compContinuousMapdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the composition continuous map of G and f (from the name)

English

Let $G$ be a homotopy of $x_{3}$ and $x_{4}$. Let $f$ be a continuous map of $X$ and $Y$. Then the composition continuous map of $G$ and $f$ is a homotopy of the composition of $x_{3}$ and $f$ and the composition of $x_{4}$ and $f$ defined as the composition of $G$ and the identity of $f$.

ContinuousMap.Homotopy.currydefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the curry of F (from the name)

English

Let $F$ be a homotopy of $x_{2}$ and $x_{3}$. Then the curry of $F$ is a continuous map of the set of elements of the unit interval and the set of continuous maps of $X$ and $Y$ defined as the curried form of $\operatorname{toContinuousMap}$ applied to $F$.

ContinuousMap.Homotopy.extenddefMathlib.Topology.Homotopy.Basic, function or constant

Wording

no wording

English

Let $F$ be a homotopy of $x_{2}$ and $x_{3}$. Then $\operatorname{extend}$ applied to $F$ is a continuous map of $\Real$ and the set of continuous maps of $X$ and $Y$.

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

Wording

the product of F (from the name)

English

Let $F$ be a function from elements $i$ of $x$ to homotopies of $x_{3}$ applied to $i$ and $x_{4}$ applied to $i$. Then the product of $i$ is a homotopy of the product of $x_{3}$ and the product of $x_{4}$.

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

Wording

the product map of F (from the name)

English

Let $F$ be a function from elements $i$ of $x$ to homotopies of $x_{3}$ applied to $i$ and $x_{4}$ applied to $i$. Then the product map of $i$ is a homotopy of the product map of $x_{3}$ and the product map of $x_{4}$ defined as the function that maps $F$ to the product of the function that maps $i$ to the composition continuous map of $i$ applied to $i$ and the evaluation of $i$.

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

Wording

the product map of F and G (from the name)

English

Let $F$ be a homotopy of $x_{4}$ and $x_{5}$. Let $G$ be a homotopy of $x_{6}$ and $x_{7}$. Then the product map of $F$ and $G$ is a homotopy of the product map of $x_{4}$ and $x_{6}$ and the product map of $x_{5}$ and $x_{7}$ defined as the product of the composition continuous map of $F$ and the first component and the composition continuous map of $G$ and the second component.

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

Wording

the product 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_{5}$ and $x_{6}$. Then the product of $F$ and $G$ is a homotopy of the product of $x_{3}$ and $x_{5}$ and the product of $x_{4}$ and $x_{6}$.

ContinuousMap.Homotopy.refldefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the identity of f (from the name)

English

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

ContinuousMap.Homotopy.symmdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the inverse of F (from the name)

English

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

ContinuousMap.Homotopy.transdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the composition of F and G (from the name)

English

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

ContinuousMap.HomotopyLikeclassMathlib.Topology.Homotopy.Basic, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{outParam}$ applied to the set of continuous maps of $X$ and $Y$. Then we can say that $\operatorname{HomotopyLike}$ holds for $F$, $x_{2}$ and $x_{3}$.

ContinuousMap.HomotopyReldefMathlib.Topology.Homotopy.Basic, type

Wording

homotopy relation of x3 and S (from the name)

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Let $S$ be an element of $\wp X$. Then a homotopy relation of $x_{3}$ and $S$ is an element of the function that maps $x_{2}$, $x_{3}$ and $S$ to $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and the function that maps $f$ to the proposition that for all elements $x_{4}$ of $X$, if $x_{4}$ is an element of $S$, then $\EqtMACRoH {f (x_{4})}{x_{2} (x_{4})}$.

ContinuousMap.HomotopyRel.castdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the cast of F (from the name)

English

Let $F$ be a homotopy relation of $x_{3}$ and $S$. Assume that $\EqtMACRoH {x_{2}}{x_{4}}$. Assume that $\EqtMACRoH {x_{3}}{x_{5}}$. Then the cast of $F$ is a homotopy relation of $x_{5}$ and $S$.

ContinuousMap.HomotopyRel.compContinuousMapdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the composition continuous map of F and g (from the name)

English

Let $F$ be a homotopy relation of $x_{4}$ and $S$. Let $g$ be a continuous map of $Y$ and $Z$. Then the composition continuous map of $F$ and $g$ is a homotopy relation of the composition of $g$ and $x_{4}$ and $S$.

ContinuousMap.HomotopyRel.refldefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the identity of f and S (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$. Let $S$ be an element of $\wp X$. Then the identity of $f$ and $S$ is a homotopy relation of $f$ and $S$.

ContinuousMap.HomotopyRel.symmdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the inverse of F (from the name)

English

Let $F$ be a homotopy relation of $x_{3}$ and $S$. Then the inverse of $F$ is a homotopy relation of $x_{2}$ and $S$.

ContinuousMap.HomotopyRel.transdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the composition of F and G (from the name)

English

Let $F$ be a homotopy relation of $x_{3}$ and $S$. Let $G$ be a homotopy relation of $x_{4}$ and $S$. Then the composition of $F$ and $G$ is a homotopy relation of $x_{4}$ and $S$.

ContinuousMap.HomotopyWithstructureMathlib.Topology.Homotopy.Basic, type

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be continuous maps of $X$ and $Y$. Let $P$ be a function from continuous maps of $X$ and $Y$ to propositions. Then the elements of $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and $P$ are a basic type.

ContinuousMap.HomotopyWith.castdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the cast of F (from the name)

English

Let $F$ be an element of $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and $P$. Assume that $\EqtMACRoH {x_{2}}{x_{4}}$. Assume that $\EqtMACRoH {x_{3}}{x_{5}}$. Then the cast of $F$ is an element of $\operatorname{HomotopyWith}$ applied to $x_{4}$, $x_{5}$ and $P$ defined as $\operatorname{mk}$ applied to the cast of $\operatorname{toHomotopy}$ applied to $F$ and $\operatorname{prop}$ applied to $F$.

ContinuousMap.HomotopyWith.refldefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the identity of f and hf (from the name)

English

Let $f$ be a continuous map of $X$ and $Y$ such that $P$ holds for $f$. Then the identity of $f$ and $\mathrm{hf}$ is an element of $\operatorname{HomotopyWith}$ applied to $f$, $f$ and $P$ defined as $\operatorname{mk}$ applied to the identity of $f$ and the function that maps $x_{2}$ to $\mathrm{hf}$.

ContinuousMap.HomotopyWith.symmdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the inverse of F (from the name)

English

Let $F$ be an element of $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and $P$. Then the inverse of $F$ is an element of $\operatorname{HomotopyWith}$ applied to $x_{3}$, $x_{2}$ and $P$.

ContinuousMap.HomotopyWith.transdefMathlib.Topology.Homotopy.Basic, function or constant

Wording

the composition of F and G (from the name)

English

Let $F$ be an element of $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{3}$ and $P$. Let $G$ be an element of $\operatorname{HomotopyWith}$ applied to $x_{3}$, $x_{4}$ and $P$. Then the composition of $F$ and $G$ is an element of $\operatorname{HomotopyWith}$ applied to $x_{2}$, $x_{4}$ and $P$.

Mathlib.Topology.Homotopy.Contractible

ContinuousMap.NullhomotopicdefMathlib.Topology.Homotopy.Contractible, predicate

Wording

no wording

English

Let $f$ be a continuous map of $X$ and $Y$. Then $\operatorname{Nullhomotopic}$ holds for $f$, if there exists an element $y$ of $Y$, such that $f$ is homotopic to the constant map of $X$ and $y$.

ContractibleSpaceclassMathlib.Topology.Homotopy.Contractible, predicate

Wording

X is a contractible space (from the name)

English

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

Mathlib.Topology.Homotopy.Equiv

ContinuousMap.HomotopyEquivstructureMathlib.Topology.Homotopy.Equiv, type

Wording

homotopy equivalence of X and Y (from the name)

English

Let $X$ and $Y$ be sets. Then the homotopy equivalences of $X$ and $Y$ are a basic type.

ContinuousMap.HomotopyEquiv.invFundefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the inverse function of self (from the name)

English

Let $\mathrm{self}$ be a homotopy equivalence of $X$ and $Y$. Then the inverse function of $\mathrm{self}$ is a continuous map of $Y$ and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

ContinuousMap.HomotopyEquiv.piCongrRightdefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the right product congruence of h (from the name)

English

Let $h$ be a function from elements $i_{2}$ of $x$ to homotopy equivalences of $X$ applied to $i_{2}$ and $Y$ applied to $i_{2}$. Then the right product congruence of $i_{2}$ is a homotopy equivalence 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}$.

ContinuousMap.HomotopyEquiv.prodCongrdefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

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

English

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

ContinuousMap.HomotopyEquiv.refldefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the identity of X (from the name)

English

Let $X$ be a set. Then the identity of $X$ is a homotopy equivalence of $X$ and $X$ defined as the homotopy equivalence of the identity of $X$.

ContinuousMap.HomotopyEquiv.symmdefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the inverse of h (from the name)

English

Let $h$ be a homotopy equivalence of $X$ and $Y$. Then the inverse of $h$ is a homotopy equivalence of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the inverse function of $h$, the forward map of $h$, $\mathrm{ContinuousMap\_\_HomotopyEquiv\_\_right\_inv}$ applied to $h$ and $\mathrm{ContinuousMap\_\_HomotopyEquiv\_\_left\_inv}$ applied to $h$.

ContinuousMap.HomotopyEquiv.toFundefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the forward map of self (from the docstring)

English

Let $\mathrm{self}$ be a homotopy equivalence of $X$ and $Y$. Then the forward map of $\mathrm{self}$ is a continuous map of $X$ and $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ContinuousMap.HomotopyEquiv.transdefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the composition of x3 and x4 (from the name)

English

Let $x_{3}$ be a homotopy equivalence of $X$ and $Y$. Let $x_{4}$ be a homotopy equivalence of $Y$ and $Z$. Then the composition of $x_{3}$ and $x_{4}$ is a homotopy equivalence of $X$ and $Z$.

Homeomorph.toHomotopyEquivdefMathlib.Topology.Homotopy.Equiv, function or constant

Wording

the homotopy equivalence of h (from the name)

English

Let $h$ be a homeomorphism of $X$ and $Y$. Then the homotopy equivalence of $h$ is a homotopy equivalence of $X$ and $Y$.

Mathlib.Topology.Homotopy.HSpaces

HSpaceclassMathlib.Topology.Homotopy.HSpaces, predicate

Wording

X is a space (from the name)

English

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

HSpace.edefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

no wording

English

$\operatorname{e}$ is an element of $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

HSpace.eHmuldefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

no wording

English

$\operatorname{eHmul}$ is a homotopy relation of the identity of $X$ and $\operatorname{singleton}$ applied to $\operatorname{e}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

HSpace.hmuldefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

no wording

English

$\operatorname{hmul}$ is a continuous map of $\mathrm{Prod}$ applied to $X$ and $X$ and $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

HSpace.hmulEdefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

no wording

English

$\operatorname{hmulE}$ is a homotopy relation of the identity of $X$ and $\operatorname{singleton}$ applied to $\operatorname{e}$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Path.delayReflLeftdefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

the left delay identity of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of the unit interval. Let $x_{3}$ be a path of $x_{1}$ and $y$. Then the left delay identity of $x_{2}$ and $x_{3}$ is a path of $x_{1}$ and $y$ defined as the inverse of the right delay identity of $x_{2}$ and the inverse of $x_{3}$.

Path.delayReflRightdefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

the right delay identity of x2 and x3 (from the name)

English

Let $x_{2}$ be an element of the unit interval. Let $x_{3}$ be a path of $x_{1}$ and $y$. Then the right delay identity of $x_{2}$ and $x_{3}$ is a path of $x_{1}$ and $y$.

unitInterval.qRightdefMathlib.Topology.Homotopy.HSpaces, function or constant

Wording

the right of p (from the name)

English

Let $p$ be an element of $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of elements of the unit interval. Then the right of $p$ is an element of the unit interval.

Mathlib.Topology.Homotopy.HomotopyGroup

Cube.boundarydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the boundary of N (from the name)

English

Let $N$ be a set. Then the boundary of $N$ is an element of the power set of the set of functions from elements of $N$ to elements of the unit interval defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that there exists an element $i$ of $N$, such that $\EqtMACRoH {y (i)}{0}$ or $\EqtMACRoH {y (i)}{1}$.

Cube.insertAtdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Then $\operatorname{insertAt}$ applied to $i$ is a homeomorphism of $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of functions from elements of $\SubtypeSet {j}{\mathrm{Neq} (j , i)}$ to elements of the unit interval and the set of functions from elements of $N$ to elements of the unit interval defined as the inverse of $\operatorname{funSplitAt}$ applied to the set of elements of the unit interval and $i$.

Cube.splitAtdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Then $\operatorname{splitAt}$ applied to $i$ is a homeomorphism of the set of functions from elements of $N$ to elements of the unit interval and $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of functions from elements of $\SubtypeSet {j}{\mathrm{Neq} (j , i)}$ to elements of the unit interval defined as $\operatorname{funSplitAt}$ applied to the set of elements of the unit interval and $i$.

GenLoopdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the generator loop of x1 (from the name)

English

Let $N$ and $X$ be sets. Let $x_{1}$ be an element of $X$. Then the generator loop of $x_{1}$ is an element of the power set of the set of continuous maps of the set of functions from elements of $N$ to elements of the unit interval and $X$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that for all functions $y$ from elements of $N$ to elements of the unit interval, if $y$ is an element of the boundary of $N$, then $\EqtMACRoH {p (y)}{x_{1}}$.

GenLoop.HomotopicdefMathlib.Topology.Homotopy.HomotopyGroup, predicate

Wording

f is homotopic to g (from the name)

English

Let $f$ and $g$ be elements of the generator loop of $x_{1}$. Then $f$ is homotopic to $g$, if $g$ is a homotopic relation with respect to the boundary of $N$.

GenLoop.cCompInsertdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Then $\operatorname{cCompInsert}$ applied to $i$ is a continuous map of the set of continuous maps of the set of functions from elements of $N$ to elements of the unit interval and $X$ and the set of continuous maps of $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of functions from elements of $\SubtypeSet {j}{\mathrm{Neq} (j , i)}$ to elements of the unit interval and $X$.

GenLoop.congrdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the congruence of x1 and e (from the name)

English

Let $x_{1}$ be an element of $X$. Let $e$ be an equivalence from $M$ to $N$. Then the congruence of $x_{1}$ and $e$ is a homeomorphism of the set of elements of the generator loop of $x_{1}$ and the set of elements of the generator loop of $x_{1}$.

GenLoop.constdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the constant (from the docstring)

English

The constant is an element of the generator loop of $x_{1}$ defined as the constant map of the set of functions from elements of $N$ to elements of the unit interval and $x_{1}$.

GenLoop.copydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the copy of f and g (from the name)

English

Let $f$ be an element of the generator loop of $x_{1}$. Let $g$ be a function from functions from elements of $N$ to elements of the unit interval to elements of $X$ such that $g$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $g$ is an element of the generator loop of $x_{1}$.

GenLoop.currySumdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the curry sum of x1 and q (from the name)

English

Let $x_{1}$ be an element of $X$. Let $q$ be an element of the generator loop of $x_{1}$. Then the curry sum of $x_{1}$ and $q$ is a continuous map of the set of functions from elements of $M$ to elements of the unit interval and the set of elements of the generator loop of $x_{1}$.

GenLoop.fromLoopdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Let $p$ be a loop space of the set of elements of the generator loop of $x_{1}$ and the constant. Then $\operatorname{fromLoop}$ applied to $i$ and $p$ is an element of the generator loop of $x_{1}$.

GenLoop.genLoopGenLoopEquivdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the generator loop generator loop equivalence of x1 (from the name)

English

Let $x_{1}$ be an element of $X$. Then the generator loop generator loop equivalence of $x_{1}$ is a homeomorphism of the set of elements of the generator loop of the constant and the set of elements of the generator loop of $x_{1}$.

GenLoop.homotopyFromdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Let $H$ be a homotopy of the loop of $i$ and $p$ and the loop of $i$ and $q$. Then $\operatorname{homotopyFrom}$ applied to $i$ and $H$ is a continuous map of $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of functions from elements of $N$ to elements of the unit interval and $X$.

GenLoop.homotopyTodefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Let $H$ be a homotopy relation of $q$ and the boundary of $N$. Then $\operatorname{homotopyTo}$ applied to $i$ and $H$ is a continuous map of $\mathrm{Prod}$ applied to the set of elements of the unit interval and the set of elements of the unit interval and the set of continuous maps of the set of functions from elements of $\SubtypeSet {j}{\mathrm{Neq} (j , i)}$ to elements of the unit interval and $X$.

GenLoop.loopHomeodefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the loop homeomorphism of i (from the name)

English

Let $i$ be an element of $N$. Then the loop homeomorphism of $i$ is a homeomorphism of the set of elements of the generator loop of $x_{1}$ and the set of loop spaces of the set of elements of the generator loop of $x_{1}$ and the constant.

GenLoop.symmAtdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Let $f$ be an element of the generator loop of $x_{1}$. Then $\operatorname{symmAt}$ applied to $i$ and $f$ is an element of the generator loop of $x_{1}$.

GenLoop.toLoopdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the loop of i and p (from the name)

English

Let $i$ be an element of $N$. Let $p$ be an element of the generator loop of $x_{1}$. Then the loop of $i$ and $p$ is a loop space of the set of elements of the generator loop of $x_{1}$ and the constant.

GenLoop.transAtdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $i$ be an element of $N$. Let $f$ and $g$ be elements of the generator loop of $x_{1}$. Then $\operatorname{transAt}$ applied to $i$, $f$ and $g$ is an element of the generator loop of $x_{1}$.

GenLoop.uncurrydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $X$. Let $p$ be an element of the generator loop of the constant. Then $\operatorname{uncurry}$ applied to $x_{1}$ and $p$ is a continuous map of $\mathrm{Prod}$ applied to the set of functions from elements of $M$ to elements of the unit interval and the set of functions from elements of $N$ to elements of the unit interval and $X$.

HomotopyGroupdefMathlib.Topology.Homotopy.HomotopyGroup, type

Wording

homotopy group of X and x1 (from the name)

English

Let $N$ and $X$ be sets. Let $x_{1}$ be an element of $X$. Then a homotopy group of $X$ and $x_{1}$ is an element of the function that maps $N$, $X$ and $x_{1}$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $N$ and $x_{1}$.

HomotopyGroup.PidefMathlib.Topology.Homotopy.HomotopyGroup, type

Wording

product of X and x1 (from the name)

English

Let $n$ be a natural number. Let $X$ be a set. Let $x_{1}$ be an element of $X$. Then a product of $X$ and $x_{1}$ is an element of the function that maps $n$, $X$ and $x_{1}$ to the set of homotopy groups of $X$ and $x_{1}$.

HomotopyGroup.homotopyGroupOfUniqueMulEquivFundamentalGroupdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the homotopy group of N (from the name)

English

Let $N$ be a set. Then the homotopy group of $N$ is a multiplicative equivalence of the set of homotopy groups of $X$ and $x_{1}$ and the set of fundamental groups of $X$ and $x_{1}$.

HomotopyGroup.pi0EquivZerothHomotopydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the product equivalence zeroth homotopy (from the name)

English

The product equivalence zeroth homotopy is an equivalence from the set of products of $X$ and $x_{1}$ to the set of zeroth homotopies of $X$ defined as the homotopy group equivalence zeroth homotopy of $\mathrm{Fin}$ applied to $0$ and $x_{1}$.

HomotopyGroup.pi1EquivFundamentalGroupdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the product equivalence fundamental group (from the name)

English

The product equivalence fundamental group is an equivalence from the set of products of $X$ and $x_{1}$ to the set of fundamental groups of $X$ and $x_{1}$ defined as the homotopy group equivalence fundamental group of $\mathrm{Fin}$ applied to $1$.

HomotopyGroup.pi1MulEquivFundamentalGroupdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the product multiplicative equivalence fundamental group (from the name)

English

The product multiplicative equivalence fundamental group is a multiplicative equivalence of the set of products of $X$ and $x_{1}$ and the set of fundamental groups of $X$ and $x_{1}$.

LoopSpacedefMathlib.Topology.Homotopy.HomotopyGroup, type

Wording

loop space of X and x1 (from the name)

English

Let $X$ be a set. Let $x_{1}$ be an element of $X$. Then a loop space of $X$ and $x_{1}$ is an element of the function that maps $X$ and $x_{1}$ to the set of paths of $x_{1}$ and $x_{1}$.

genLoopEquivOfUniquedefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the generator loop equivalence of N (from the name)

English

Let $N$ be a set. Then the generator loop equivalence of $N$ is an equivalence from the set of elements of the generator loop of $x_{1}$ to the set of loop spaces of $X$ and $x_{1}$.

genLoopHomeoOfIsEmptydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the generator loop homeomorphism of N and x1 (from the name)

English

Let $N$ be a set. Let $x_{1}$ be an element of $X$. Then the generator loop homeomorphism of $N$ and $x_{1}$ is a homeomorphism of the set of elements of the generator loop of $x_{1}$ and $X$.

homotopyGroupEquivFundamentalGroupdefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the homotopy group equivalence fundamental group of i (from the name)

English

Let $i$ be an element of $N$. Then the homotopy group equivalence fundamental group of $i$ is an equivalence from the set of homotopy groups of $X$ and $x_{1}$ to the set of fundamental groups of the set of elements of the generator loop of $x_{1}$ and the constant.

homotopyGroupEquivFundamentalGroupOfUniquedefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the homotopy group equivalence fundamental group of N (from the name)

English

Let $N$ be a set. Then the homotopy group equivalence fundamental group of $N$ is an equivalence from the set of homotopy groups of $X$ and $x_{1}$ to the set of fundamental groups of $X$ and $x_{1}$.

homotopyGroupEquivZerothHomotopyOfIsEmptydefMathlib.Topology.Homotopy.HomotopyGroup, function or constant

Wording

the homotopy group equivalence zeroth homotopy of N and x1 (from the name)

English

Let $N$ be a set. Let $x_{1}$ be an element of $X$. Then the homotopy group equivalence zeroth homotopy of $N$ and $x_{1}$ is an equivalence from the set of homotopy groups of $X$ and $x_{1}$ to the set of zeroth homotopies of $X$.