Definitions: Mathlib.Topology, part 3 of 8

390 definitions of 56 modules, Mathlib.Topology.Bornology.Hom to Mathlib.Topology.Category.TopCommRingCat. ‹ previous next ›

Mathlib.Topology.Bornology.Hom

LocallyBoundedMapstructureMathlib.Topology.Bornology.Hom, type
Wording
locally bounded map of x and x1 (from the name)
English
generation took over the time limit
LocallyBoundedMap.compdefMathlib.Topology.Bornology.Hom, function or constant
Wording
the composition of f and g (from the name)
English
generation took over the time limit
LocallyBoundedMap.copydefMathlib.Topology.Bornology.Hom, function or constant
Wording
the copy of f and h (from the name)
English
generation took over the time limit
LocallyBoundedMap.iddefMathlib.Topology.Bornology.Hom, function or constant
Wording
the identity of x (from the name)
English
generation took over the time limit
LocallyBoundedMap.ofMapBoundeddefMathlib.Topology.Bornology.Hom, function or constant
Wording
the locally bounded map of f and h (from the name)
English
generation took over the time limit
LocallyBoundedMap.toFundefMathlib.Topology.Bornology.Hom, function or constant
Wording
the locally bounded map of self and x4 (from the name)
English
generation took over the time limit
LocallyBoundedMapClassclassMathlib.Topology.Bornology.Hom, 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{LocallyBoundedMapClass}$ holds for $F$, $x$ and $x_{1}$.
LocallyBoundedMapClass.toLocallyBoundedMapdefMathlib.Topology.Bornology.Hom, function or constant
Wording
the locally bounded map of f (from the name)
English
generation took over the time limit

Mathlib.Topology.CWComplex.Abstract.Basic

TopCat.CWComplexdefMathlib.Topology.CWComplex.Abstract.Basic, type
Wording
no wording
English
Let $X$ be a topological category. Then an element of $\operatorname{CWComplex}$ applied to $X$ is an element of the function that maps $X$ to $\operatorname{RelativeCWComplex}$ applied to $\operatorname{to}$ applied to $X$.
TopCat.RelativeCWComplexdefMathlib.Topology.CWComplex.Abstract.Basic, type
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Then an element of $\operatorname{RelativeCWComplex}$ applied to $f$ is an element of the function that maps $f$ to the set of relative cell complexes of $\operatorname{basicCell}$ and $f$.
TopCat.RelativeCWComplex.basicCelldefMathlib.Topology.CWComplex.Abstract.Basic, function or constant
Wording
no wording
English
Let $n$ be a natural number. Let $x$ be an element of $\mathrm{Unit}$. Then $\operatorname{basicCell}$ applied to $n$ and $x$ is a homomorphism of the disk boundary of $n$ and the disk of $n$ defined as the inclusion of $n$.

Mathlib.Topology.CWComplex.Classical.Basic

Topology.CWComplexclassMathlib.Topology.CWComplex.Classical.Basic, predicate
Wording
no wording
English
Let $C$ be an element of $\wp X$. Then we can say that $\operatorname{CWComplex}$ holds for $C$.
Topology.CWComplex.Subcomplex.mk'defMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $C$ and $E$ be elements of $\wp X$. Let $I$ be a function from natural numbers $n_{2}$ to elements of the power set of the set of cells of $C$ and $n_{2}$ such that for all natural numbers $n_{1}$, for all elements $i$ of $I$ applied to $n_{1}$, the closed cell of $n_{1}$ and $i$ is less than or equal to $E$. Assume that the union of the function that maps $n$ to the union of the function that maps $j$ to the open cell of $n$ and $j$ is equal to $E$. Then $\operatorname{mk'}$ applied to $C$, $E$, $n_{2}$, $I$, $\mathrm{closedCell\_subset}$ and $\mathrm{union}$ is a subcomplex of $C$.
Topology.CWComplex.Subcomplex.mk''defMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $C$ and $E$ be elements of $\wp X$. Let $I$ be a function from natural numbers $n_{1}$ to elements of the power set of the set of cells of $C$ and $n_{1}$. Assume that the union of the function that maps $n$ to the union of the function that maps $j$ to the open cell of $n$ and $j$ is equal to $E$. Then $\operatorname{mk''}$ applied to $C$, $E$, $n_{1}$, $I$ and $\mathrm{union}$ is a subcomplex of $C$.
Topology.CWComplex.celldefMathlib.Topology.CWComplex.Classical.Basic, type
Wording
cell of C and n (from the name)
English
Let $C$ be an element of $\wp X$. Let $n$ be a natural number. Then a cell of $C$ and $n$ is an element of the function that maps $C$ and $n$ to $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.
Topology.CWComplex.mapdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the map of n and i (from the name)
English
Let $n$ be a natural number. Let $i$ be a cell of $C$ and $n$. Then the map of $n$ and $i$ is a partial equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $n$ and $i$.
Topology.RelCWComplexclassMathlib.Topology.CWComplex.Classical.Basic, predicate
Wording
no wording
English
Let $C$ be an element of $\wp X$. Let $D$ be an element of $\mathrm{outParam}$ applied to $\wp X$. Then we can say that $\operatorname{RelCWComplex}$ holds for $C$ and $D$.
Topology.RelCWComplex.SubcomplexstructureMathlib.Topology.CWComplex.Classical.Basic, type
Wording
subcomplex of C (from the name)
English
Let $C$ be an element of $\wp X$. Then the subcomplexes of $C$ are a basic type.
Topology.RelCWComplex.Subcomplex.IdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a subcomplex of $C$. Let $n$ be a natural number. Then $\operatorname{I}$ applied to $\mathrm{self}$ and $n$ is an element of the power set of the set of cells of $C$ and $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $n$.
Topology.RelCWComplex.Subcomplex.carrierdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a subcomplex of $C$. Then the carrier of $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Topology.RelCWComplex.Subcomplex.copydefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the copy of F and J (from the name)
English
Let $E$ be a subcomplex of $C$. Let $F$ be an element of $\wp X$ such that $\EqtMACRoH {F}{E}$. Let $J$ be a function from natural numbers $n_{1}$ to elements of the power set of the set of cells of $C$ and $n_{1}$ such that $\EqtMACRoH {J}{\operatorname{I} (E)}$. Then the copy of $F$ and $n_{1}$ is a subcomplex of $C$.
Topology.RelCWComplex.Subcomplex.mk'defMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $C$ and $E$ be elements of $\wp X$. Let $I$ be a function from natural numbers $n_{2}$ to elements of the power set of the set of cells of $C$ and $n_{2}$ such that for all natural numbers $n_{1}$, for all elements $i$ of $I$ applied to $n_{1}$, the closed cell of $n_{1}$ and $i$ is less than or equal to $E$. Assume that the union of $D$ and the union of the function that maps $n$ to the union of the function that maps $j$ to the open cell of $n$ and $j$ is equal to $E$. Then $\operatorname{mk'}$ applied to $C$, $E$, $n_{2}$, $I$, $\mathrm{closedCell\_subset}$ and $\mathrm{union}$ is a subcomplex of $C$.
Topology.RelCWComplex.Subcomplex.mk''defMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $C$ and $E$ be elements of $\wp X$. Let $I$ be a function from natural numbers $n_{1}$ to elements of the power set of the set of cells of $C$ and $n_{1}$. Assume that the union of $D$ and the union of the function that maps $n$ to the union of the function that maps $j$ to the open cell of $n$ and $j$ is equal to $E$. Then $\operatorname{mk''}$ applied to $C$, $E$, $n_{1}$, $I$ and $\mathrm{union}$ is a subcomplex of $C$ defined as the function that maps $\mathrm{union}$ to $\operatorname{mk}$ applied to $E$, $n_{1}$, $\operatorname{isClosed}$, $I$ and $\mathrm{union}$.
Topology.RelCWComplex.celldefMathlib.Topology.CWComplex.Classical.Basic, type
Wording
cell of C and n (from the name)
English
Let $C$ be an element of $\wp X$. Let $n$ be a natural number. Then a cell of $C$ and $n$ is an element of the function that maps $C$ and $n$ to $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.
Topology.RelCWComplex.cellFrontierdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the cell frontier of n and i (from the name)
English
Let $n$ be a natural number. Let $i$ be a cell of $C$ and $n$. Then the cell frontier of $n$ and $i$ is an element of $\wp X$ defined as the image of $\operatorname{toFun}$ applied to the map of $n$ and $i$ and the sphere of $0$ and $1$.
Topology.RelCWComplex.closedCelldefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the closed cell of n and i (from the name)
English
Let $n$ be a natural number. Let $i$ be a cell of $C$ and $n$. Then the closed cell of $n$ and $i$ is an element of $\wp X$ defined as the image of $\operatorname{toFun}$ applied to the map of $n$ and $i$ and the closed ball of $0$ and $1$.
Topology.RelCWComplex.mapdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the map of n and i (from the name)
English
Let $n$ be a natural number. Let $i$ be a cell of $C$ and $n$. Then the map of $n$ and $i$ is a partial equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers and $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $n$ and $i$.
Topology.RelCWComplex.openCelldefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the open cell of n and i (from the name)
English
Let $n$ be a natural number. Let $i$ be a cell of $C$ and $n$. Then the open cell of $n$ and $i$ is an element of $\wp X$ defined as the image of $\operatorname{toFun}$ applied to the map of $n$ and $i$ and the ball of $0$ and $1$.
Topology.RelCWComplex.skeletondefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
the skeleton of C and n (from the name)
English
Let $C$ be an element of $\wp X$. Let $n$ be a natural number. Then the skeleton of $C$ and $n$ is a subcomplex of $C$ defined as $\operatorname{skeletonLT}$ applied to $C$ and $n + 1$.
Topology.RelCWComplex.skeletonLTdefMathlib.Topology.CWComplex.Classical.Basic, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp X$. Let $n$ be a natural number. Then $\operatorname{skeletonLT}$ applied to $C$ and $n$ is a subcomplex of $C$.

Mathlib.Topology.CWComplex.Classical.Finite

Topology.RelCWComplex.FiniteclassMathlib.Topology.CWComplex.Classical.Finite, predicate
Wording
C is finite (from the docstring)
English
Let $C$ be an element of $\wp X$. Then we can say that $C$ is finite.
Topology.RelCWComplex.FiniteDimensionalclassMathlib.Topology.CWComplex.Classical.Finite, predicate
Wording
no wording
English
Let $C$ be an element of $\wp X$. Then we can say that $\operatorname{FiniteDimensional}$ holds for $C$.
Topology.RelCWComplex.FiniteTypeclassMathlib.Topology.CWComplex.Classical.Finite, predicate
Wording
C is a finite type (from the name)
English
Let $C$ be an element of $\wp X$. Then we can say that $C$ is a finite type.

Mathlib.Topology.CWComplex.Classical.Graph

Topology.CWComplex.OneSkeletonGraphdefMathlib.Topology.CWComplex.Classical.Graph, function or constant
Wording
the one skeleton graph of C (from the name)
English
Let $C$ be an element of $\wp X$. Then the one skeleton graph of $C$ is a graph of the set of cells of $C$ and $0$ and the set of cells of $C$ and $1$.

Mathlib.Topology.CantorBendixson

CantorBendixson.iteratedDerivedSetdefMathlib.Topology.CantorBendixson, function or constant
Wording
the iterated derived set of s and x1 (from the name)
English
Let $s$ be an element of $\wp X$. Let $x_{1}$ be an ordinal. Then the iterated derived set of $s$ and $x_{1}$ is an element of $\wp X$ defined as $\operatorname{gfpApprox}$ applied to the relative derived set, $s$ and $x_{1}$.
CantorBendixson.perfectKerneldefMathlib.Topology.CantorBendixson, function or constant
Wording
the perfect kernel of s (from the docstring)
English
Let $s$ be an element of $\wp X$. Then the perfect kernel of $s$ is an element of $\wp X$ defined as the intersection of the function that maps $a$ to the iterated derived set of $s$ and $a$.

Mathlib.Topology.Category.Born

BornstructureMathlib.Topology.Category.Born, type
Wording
no wording
English
The elements of $\mathrm{Born}$ are a basic type.
Born.carrierdefMathlib.Topology.Category.Born, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{Born}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Category.CompHaus.Basic

CompHausdefMathlib.Topology.Category.CompHaus.Basic, type
Wording
no wording
English
An element of $\mathrm{CompHaus}$ is an element of $\mathrm{CompHausLike}$ applied to the function that maps $x$ to $\mathrm{True}$.
CompHaus.limitConedefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and $\mathrm{CompHaus}$. Then the limit cone of $F$ is a cone of $F$.
CompHaus.limitConeIsLimitdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
the limit cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and $\mathrm{CompHaus}$. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.
CompHaus.ofdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{CompHaus}$ defined as $\operatorname{of}$ applied to the function that maps $x_{1}$ to $\mathrm{True}$ and $X$.
compHausLikeToCompHausdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Then $\mathrm{compHausLikeToCompHaus}$ applied to $P$ is a functor of $\mathrm{CompHausLike}$ applied to $P$ and $\mathrm{CompHaus}$.
compHausToTopdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
no wording
English
$\mathrm{compHausToTop}$ is a functor of $\mathrm{CompHaus}$ and the set of topological categories defined as $\operatorname{compHausLikeToTop}$ applied to the function that maps $x$ to $\mathrm{True}$.
stoneCechEquivalencedefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
the Stone Cech equivalence of X and Y (from the name)
English
Let $X$ be a topological category. Let $Y$ be an element of $\mathrm{CompHaus}$. Then the Stone Cech equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the Stone Cech object of $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $\mathrm{compHausToTop}$ and $Y$.
stoneCechObjdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
the Stone Cech object of X (from the name)
English
Let $X$ be a topological category. Then the Stone Cech object of $X$ is an element of $\mathrm{CompHaus}$ defined as $\operatorname{of}$ applied to the set of Stone Ceches of the set of carriers of $X$.
topToCompHausdefMathlib.Topology.Category.CompHaus.Basic, function or constant
Wording
no wording
English
$\mathrm{topToCompHaus}$ is a functor of the set of topological categories and $\mathrm{CompHaus}$.

Mathlib.Topology.Category.CompHaus.Frm

topCatOpToFrmdefMathlib.Topology.Category.CompHaus.Frm, function or constant
Wording
no wording
English
$\mathrm{topCatOpToFrm}$ is a functor of the set of opposites of the set of topological categories and $\mathrm{Frm}$.

Mathlib.Topology.Category.CompHaus.Limits

CompHaus.isTerminalPUnitdefMathlib.Topology.Category.CompHaus.Limits, function or constant
Wording
no wording
English
$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{isTerminalPUnit}$.

Mathlib.Topology.Category.CompHaus.Projective

CompHaus.projectivePresentationdefMathlib.Topology.Category.CompHaus.Projective, function or constant
Wording
the projective presentation of X (from the name)
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then the projective presentation of $X$ is a projective presentation of $X$.

Mathlib.Topology.Category.CompHausLike.Basic

CompHausLikestructureMathlib.Topology.Category.CompHausLike.Basic, type
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Then the elements of $\mathrm{CompHausLike}$ applied to $P$ are a basic type.
CompHausLike.HasPropclassMathlib.Topology.Category.CompHausLike.Basic, predicate
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Let $X$ be a set. Then we can say that $\operatorname{HasProp}$ holds for $P$ and $X$.
CompHausLike.compHausLikeToTopdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Then $\operatorname{compHausLikeToTop}$ applied to $P$ is a functor of $\mathrm{CompHausLike}$ applied to $P$ and the set of topological categories defined as the induced functor of $\operatorname{toTop}$.
CompHausLike.constdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the constant of T and s (from the name)
English
Let $T$ be an element of $\mathrm{CompHausLike}$ applied to $P$. Let $s$ be a carrier of the underlying topological space of $S$. Then the constant of $T$ and $s$ is a homomorphism of $T$ and $S$ defined as $\operatorname{ofHom}$ applied to $P$ and the constant map of the set of carriers of $\operatorname{proj0}$ applied to $T$ and $s$.
CompHausLike.fullyFaithfulCompHausLikeToTopdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Then $\operatorname{fullyFaithfulCompHausLikeToTop}$ applied to $P$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{compHausLikeToTop}$ applied to $P$ defined as the induced functor of $\operatorname{toTop}$.
CompHausLike.fullyFaithfulToCompHausLikedefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Assume that for all elements $X$ of $\mathrm{CompHausLike}$ applied to $P$, if $P$ holds for the underlying topological space of $X$, then $\mathrm{P'}$ holds for the underlying topological space of $X$. Then $\operatorname{fullyFaithfulToCompHausLike}$ applied to $h$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{toCompHausLike}$ applied to $h$.
CompHausLike.homeoOfIsodefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the homeomorphism of f (from the name)
English
Let $f$ be an isomorphism of $X$ and $Y$. Then the homeomorphism of $f$ is a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$ defined as the homeomorphism of the map isomorphism of $\operatorname{compHausLikeToTop}$ applied to $P$ and $f$.
CompHausLike.isoEquivHomeodefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the isomorphism equivalence homeomorphism (from the name)
English
The isomorphism equivalence homeomorphism is an equivalence from the set of isomorphisms of $X$ and $Y$ to the set of homeomorphisms of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$.
CompHausLike.isoOfBijectivedefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the isomorphism of f and bij (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$ such that $\operatorname{coe}$ applied to the homomorphism of $f$ is bijective. Then the isomorphism of $f$ and $\mathrm{bij}$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{asIso}$ applied to $f$.
CompHausLike.isoOfHomeodefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the isomorphism of f (from the name)
English
Let $f$ be a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$ defined as the unique isomorphism of $\operatorname{fullyFaithfulCompHausLikeToTop}$ applied to $P$ and the isomorphism of $f$.
CompHausLike.ofdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Let $X$ be a set. Then $\operatorname{of}$ applied to $P$ and $X$ is an element of $\mathrm{CompHausLike}$ applied to $P$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$ and $\operatorname{hasProp}$.
CompHausLike.ofHomdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Let $P$ be a function from topological categories to propositions. Let $f$ be a continuous map of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $P$ and $f$ is a homomorphism of $\operatorname{of}$ applied to $P$ and $X$ and $\operatorname{of}$ applied to $P$ and $Y$ defined as the concrete category of $f$.
CompHausLike.toCompHausLikedefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
no wording
English
Assume that for all elements $X$ of $\mathrm{CompHausLike}$ applied to $P$, if $P$ holds for the underlying topological space of $X$, then $\mathrm{P'}$ holds for the underlying topological space of $X$. Then $\operatorname{toCompHausLike}$ applied to $h$ is a functor of $\mathrm{CompHausLike}$ applied to $P$ and $\mathrm{CompHausLike}$ applied to $\mathrm{P'}$.
CompHausLike.toTopdefMathlib.Topology.Category.CompHausLike.Basic, function or constant
Wording
the underlying topological space of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\mathrm{CompHausLike}$ applied to $P$. Then the underlying topological space of $\mathrm{self}$ is a topological category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Category.CompHausLike.Cartesian

CompHausLike.coproductCoconedefMathlib.Topology.Category.CompHausLike.Cartesian, function or constant
Wording
the coproduct cocone of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{CompHausLike}$ applied to $P$. Then the coproduct cocone of $X$ and $Y$ is a binary cofan of $X$ and $Y$.
CompHausLike.coproductIsColimitdefMathlib.Topology.Category.CompHausLike.Cartesian, function or constant
Wording
no wording
English
Let $X$ and $Y$ be elements of $\mathrm{CompHausLike}$ applied to $P$. Then $\operatorname{coproductIsColimit}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to the coproduct cocone of $X$ and $Y$.
CompHausLike.productConedefMathlib.Topology.Category.CompHausLike.Cartesian, function or constant
Wording
the product cone of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{CompHausLike}$ applied to $P$. Then the product cone of $X$ and $Y$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$.
CompHausLike.productIsLimitdefMathlib.Topology.Category.CompHausLike.Cartesian, function or constant
Wording
no wording
English
Let $X$ and $Y$ be elements of $\mathrm{CompHausLike}$ applied to $P$. Then $\operatorname{productIsLimit}$ applied to $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to the product cone of $X$ and $Y$.

Mathlib.Topology.Category.CompHausLike.EffectiveEpi

CompHausLike.effectiveEpiStructdefMathlib.Topology.Category.CompHausLike.EffectiveEpi, function or constant
Wording
no wording
English
Let $x$ be a homomorphism of $X$ and $B$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to the homomorphism of $x$. Then $\operatorname{effectiveEpiStruct}$ applied to $x$ and $h$ is an element of $\operatorname{EffectiveEpiStruct}$ applied to $x$.

Mathlib.Topology.Category.CompHausLike.Limits

CompHausLike.HasExplicitFiniteCoproductdefMathlib.Topology.Category.CompHausLike.Limits, predicate
Wording
X has explicit finite coproducts (from the name)
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Then $X$ has explicit finite coproducts, if $\operatorname{HasProp}$ holds for $P$ and $\Sigma$ applied to the function that maps $a$ to the set of carriers of the underlying topological space of $X$ applied to $a$.
CompHausLike.HasExplicitFiniteCoproductsclassMathlib.Topology.Category.CompHausLike.Limits, predicate
Wording
P has explicit finite coproducts (from the name)
English
Let $P$ be a function from topological categories to propositions. Then we can say that $P$ has explicit finite coproducts.
CompHausLike.HasExplicitPullbackdefMathlib.Topology.Category.CompHausLike.Limits, predicate
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then $\operatorname{HasExplicitPullback}$ holds for $f$ and $g$, if $\operatorname{HasProp}$ holds for $P$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $\mathrm{xy}$ to $\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {\mathrm{xy}})}{\operatorname{hom} (g , \ProdsndMACRoAA {\mathrm{xy}})}$.
CompHausLike.HasExplicitPullbacksclassMathlib.Topology.Category.CompHausLike.Limits, predicate
Wording
P has explicit pullbacks (from the name)
English
Let $P$ be a function from topological categories to propositions. Then we can say that $P$ has explicit pullbacks.
CompHausLike.HasExplicitPullbacksOfInclusionsclassMathlib.Topology.Category.CompHausLike.Limits, predicate
Wording
P has explicit pullbacks of inclusions (from the name)
English
Let $P$ be a function from topological categories to propositions. Then we can say that $P$ has explicit pullbacks of inclusions.
CompHausLike.finiteCoproductdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the coproduct in X (from the docstring)
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Then the coproduct in $X$ is an element of $\mathrm{CompHausLike}$ applied to $P$ defined as $\operatorname{of}$ applied to $P$ and $\Sigma$ applied to the function that maps $a$ to the set of carriers of the underlying topological space of $X$ applied to $a$.
CompHausLike.finiteCoproduct.cofandefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the cofan of X (from the name)
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Then the cofan of $X$ is a cofan of $X$ defined as $\operatorname{mk}$ applied to the coproduct in $X$ and $\mathrm{CompHausLike\_\_finiteCoproduct\_\_\_u3b9\_}$ applied to $X$.
CompHausLike.finiteCoproduct.descdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
no wording
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Let $e$ be a function from elements $a$ of $x$ to homomorphisms of $X$ applied to $a$ and $B$. Then $\operatorname{desc}$ applied to $X$, $a$ and $e$ is a homomorphism of the coproduct in $X$ and $B$.
CompHausLike.finiteCoproduct.isColimitdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
no wording
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Then $\operatorname{isColimit}$ applied to $X$ is an element of $\operatorname{IsColimit}$ applied to the cofan of $X$.
CompHausLike.finiteCoproduct.ιdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the inclusion of X and a (from the name)
English
Let $X$ be a function from elements of $x$ to elements of $\mathrm{CompHausLike}$ applied to $P$. Let $a$ be an element of $x$. Then the inclusion of $X$ and $a$ is a homomorphism of $X$ applied to $a$ and the coproduct in $X$.
CompHausLike.isTerminalPUnitdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
no wording
English
$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $P$ and $\mathrm{PUnit}$.
CompHausLike.pullbackdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the pullback of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then the pullback of $f$ and $g$ is an element of $\mathrm{CompHausLike}$ applied to $P$ defined as $\operatorname{of}$ applied to $P$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $\mathrm{xy}$ to $\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {\mathrm{xy}})}{\operatorname{hom} (g , \ProdsndMACRoAA {\mathrm{xy}})}$.
CompHausLike.pullback.conedefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the cone of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then the cone of $f$ and $g$ is a pullback cone of $f$ and $g$ defined as $\operatorname{mk}$ applied to the projection from the pullback to the first component of $f$ and $g$, the projection from the pullback to the second component of $f$ and $g$ and $\operatorname{condition}$ applied to $f$ and $g$.
CompHausLike.pullback.fstdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the projection from the pullback to the first component of f and g (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then the projection from the pullback to the first component of $f$ and $g$ is a homomorphism of the pullback of $f$ and $g$ and $X$.
CompHausLike.pullback.isLimitdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then $\operatorname{isLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the cone of $f$ and $g$.
CompHausLike.pullback.liftdefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the lift of a and b (from the name)
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Let $a$ be a homomorphism of $Z$ and $X$. Let $b$ be a homomorphism of $Z$ and $Y$ such that the composition of $a$ and $f$ is equal to the composition of $b$ and $g$. Then the lift of $a$ and $b$ is a homomorphism of $Z$ and the pullback of $f$ and $g$.
CompHausLike.pullback.snddefMathlib.Topology.Category.CompHausLike.Limits, function or constant
Wording
the projection from the pullback to the second component of f and g (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $B$. Let $g$ be a homomorphism of $Y$ and $B$. Then the projection from the pullback to the second component of $f$ and $g$ is a homomorphism of the pullback of $f$ and $g$ and $Y$.

Mathlib.Topology.Category.CompHausLike.SigmaComparison

CompHausLike.sigmaComparisondefMathlib.Topology.Category.CompHausLike.SigmaComparison, function or constant
Wording
the comparison map from the value of X and x1 (from the docstring)
English
Let $X$ be a functor of the set of opposites of $\mathrm{CompHausLike}$ applied to $P$ and the set of sets. Let $x_{1}$ be a function from elements of $x$ to sets. Then the comparison map from the value of $X$ and $x_{1}$ is a homomorphism of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $\Sigma$ applied to the function that maps $a$ to $x_{1}$ applied to $a$ and the set of functions from elements $a_{1}$ of $x$ to elements of the action of $X$ and $\operatorname{op}$ applied to $\operatorname{of}$ applied to $P$ and $x_{1}$ applied to $a_{1}$ defined as the type category of the function that maps $x_{3}$ and $a$ to $\operatorname{hom}$ applied to the map of $X$ and the opposite in $\operatorname{ofHom}$ applied to $P$ and $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $a$ and $\mathrm{continuous\_sigmaMk}$ and $x_{3}$.

Mathlib.Topology.Category.CompactlyGenerated

CompactlyGeneratedstructureMathlib.Topology.Category.CompactlyGenerated, type
Wording
no wording
English
The elements of $\mathrm{CompactlyGenerated}$ are a basic type.
CompactlyGenerated.compactlyGeneratedToTopdefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
no wording
English
$\operatorname{compactlyGeneratedToTop}$ is a functor of $\mathrm{CompactlyGenerated}$ and the set of topological categories defined as the induced functor of $\operatorname{toTop}$.
CompactlyGenerated.fullyFaithfulCompactlyGeneratedToTopdefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
no wording
English
$\operatorname{fullyFaithfulCompactlyGeneratedToTop}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{compactlyGeneratedToTop}$ defined as the induced functor of $\operatorname{toTop}$.
CompactlyGenerated.homeoOfIsodefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
the homeomorphism of f (from the name)
English
Let $f$ be an isomorphism of $X$ and $Y$. Then the homeomorphism of $f$ is a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$.
CompactlyGenerated.isoEquivHomeodefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
the isomorphism equivalence homeomorphism (from the name)
English
The isomorphism equivalence homeomorphism is an equivalence from the set of isomorphisms of $X$ and $Y$ to the set of homeomorphisms of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$.
CompactlyGenerated.isoOfHomeodefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
the isomorphism of f (from the name)
English
Let $f$ be a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$.
CompactlyGenerated.ofdefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{CompactlyGenerated}$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$.
CompactlyGenerated.ofHomdefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
no wording
English
Let $f$ be a continuous map of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
CompactlyGenerated.toTopdefMathlib.Topology.Category.CompactlyGenerated, function or constant
Wording
the underlying topological space of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\mathrm{CompactlyGenerated}$. Then the underlying topological space of $\mathrm{self}$ is a topological category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Category.Compactum

CompactumdefMathlib.Topology.Category.Compactum, type
Wording
compactum (from the name)
English
A compactum is an algebra of the category theory of the set of elements of $\mathrm{Ultrafilter}$.
Compactum.adjdefMathlib.Topology.Category.Compactum, function or constant
Wording
the adjoint (from the name)
English
The adjoint is an adjunction of the free and $\operatorname{forget}$ defined as the adjoint of the category theory of the set of elements of $\mathrm{Ultrafilter}$.
Compactum.forgetdefMathlib.Topology.Category.Compactum, function or constant
Wording
no wording
English
$\operatorname{forget}$ is a functor of the set of compactums and the set of sets defined as $\operatorname{forget}$ applied to the category theory of the set of elements of $\mathrm{Ultrafilter}$.
Compactum.freedefMathlib.Topology.Category.Compactum, function or constant
Wording
the free (from the name)
English
The free is a functor of the set of sets and the set of compactums defined as the free of the category theory of the set of elements of $\mathrm{Ultrafilter}$.
Compactum.homOfContinuousdefMathlib.Topology.Category.Compactum, function or constant
Wording
the homomorphism of f and cont (from the name)
English
Let $f$ be a continuous function from elements of $\operatorname{A}$ applied to $X$ to elements of $\operatorname{A}$ applied to $Y$. Then the homomorphism of $f$ and $\mathrm{cont}$ is a homomorphism of $X$ and $Y$.
Compactum.incldefMathlib.Topology.Category.Compactum, function or constant
Wording
the inclusion of X and x (from the name)
English
Let $X$ be a compactum. Let $x$ be an element of $\operatorname{A}$ applied to $X$. Then the inclusion of $X$ and $x$ is a ultrafilter of $\operatorname{A}$ applied to $X$ defined as the coercion of the homomorphism of the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3b7\_}$ applied to the category theory of the set of elements of $\mathrm{Ultrafilter}$ and $\operatorname{proj0}$ applied to $X$ and $x$.
Compactum.joindefMathlib.Topology.Category.Compactum, function or constant
Wording
the monadic join of X and x (from the docstring)
English
Let $X$ be a compactum. Let $x$ be a ultrafilter of the set of ultrafilters of $\operatorname{A}$ applied to $X$. Then the monadic join of $X$ and $x$ is a ultrafilter of $\operatorname{A}$ applied to $X$ defined as the coercion of the homomorphism of the component of $\mathrm{CategoryTheory\_\_Monad\_\_\_u3bc\_}$ applied to the category theory of the set of elements of $\mathrm{Ultrafilter}$ and $\operatorname{A}$ applied to $X$ and $x$.
Compactum.ofTopologicalSpacedefMathlib.Topology.Category.Compactum, function or constant
Wording
the compactum of X (from the name)
English
Let $X$ be a set. Then the compactum of $X$ is a compactum.
Compactum.strdefMathlib.Topology.Category.Compactum, function or constant
Wording
no wording
English
Let $X$ be a compactum. Let $x$ be a ultrafilter of $\operatorname{A}$ applied to $X$. Then $\operatorname{str}$ applied to $X$ and $x$ is an element of $\operatorname{A}$ applied to $X$ defined as the coercion of the homomorphism of $\operatorname{a}$ applied to $X$ and $x$.
compactumToCompHausdefMathlib.Topology.Category.Compactum, function or constant
Wording
no wording
English
$\mathrm{compactumToCompHaus}$ is a functor of the set of compactums and $\mathrm{CompHaus}$.
compactumToCompHaus.isoOfTopologicalSpacedefMathlib.Topology.Category.Compactum, function or constant
Wording
the isomorphism (from the name)
English
The isomorphism is an isomorphism of the action of $\mathrm{compactumToCompHaus}$ and the compactum of the set of carriers of the underlying topological space of $D$ and $D$.
compactumToCompHausCompForgetdefMathlib.Topology.Category.Compactum, function or constant
Wording
no wording
English
$\mathrm{compactumToCompHausCompForget}$ is an isomorphism of the composition of $\mathrm{compactumToCompHaus}$ and the forgetful functor of $\mathrm{CompHaus}$ and $\operatorname{forget}$.

Mathlib.Topology.Category.DeltaGenerated

DeltaGenerateddefMathlib.Topology.Category.DeltaGenerated, type
Wording
no wording
English
An element of $\mathrm{DeltaGenerated}$ is an element of $\mathrm{GeneratedByTopCat}$ applied to the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers.
DeltaGenerated.coreflectorAdjunctiondefMathlib.Topology.Category.DeltaGenerated, function or constant
Wording
the adjunction between the forgetful functor (from the docstring)
English
The adjunction between the forgetful functor is an adjunction of $\operatorname{deltaGeneratedToTop}$ and $\operatorname{toDeltaGenerated}$ defined as the adjoint.
DeltaGenerated.deltaGeneratedToTopdefMathlib.Topology.Category.DeltaGenerated, function or constant
Wording
no wording
English
$\operatorname{deltaGeneratedToTop}$ is a functor of $\mathrm{DeltaGenerated}$ and the set of topological categories defined as the topological category.
DeltaGenerated.fullyFaithfulDeltaGeneratedToTopdefMathlib.Topology.Category.DeltaGenerated, function or constant
Wording
no wording
English
$\operatorname{fullyFaithfulDeltaGeneratedToTop}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{deltaGeneratedToTop}$ defined as $\operatorname{fullyFaithfulToTopCat}$ applied to the function that maps $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers.
DeltaGenerated.ofdefMathlib.Topology.Category.DeltaGenerated, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{DeltaGenerated}$ defined as $\operatorname{of}$ applied to $X$.
TopCat.toDeltaGenerateddefMathlib.Topology.Category.DeltaGenerated, function or constant
Wording
no wording
English
$\operatorname{toDeltaGenerated}$ is a functor of the set of topological categories and $\mathrm{DeltaGenerated}$ defined as $\operatorname{toGeneratedByTopCat}$.

Mathlib.Topology.Category.FinTopCat

FinTopCatstructureMathlib.Topology.Category.FinTopCat, type
Wording
finite topological category (from the name)
English
The finite topological categories are a basic type.
FinTopCat.ofdefMathlib.Topology.Category.FinTopCat, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is a finite topological category defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$.
FinTopCat.toTopdefMathlib.Topology.Category.FinTopCat, function or constant
Wording
the top of self (from the name)
English
Let $\mathrm{self}$ be a finite topological category. Then the top of $\mathrm{self}$ is a topological category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Category.LightProfinite.AsLimit

LightProfinite.asLimitdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
no wording
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{asLimit}$ applied to $S$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{asLimitCone}$ applied to $S$.
LightProfinite.asLimitConedefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
no wording
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{asLimitCone}$ applied to $S$ is a cone of the diagram of $S$.
LightProfinite.componentdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the component of S and n (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Let $n$ be a natural number. Then the component of $S$ and $n$ is an element of $\mathrm{LightProfinite}$ defined as the action of the diagram of $S$ and $\operatorname{op}$ applied to $n$.
LightProfinite.diagramdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the diagram of $S$ is a functor of the set of opposites of $\Natural$ and $\mathrm{LightProfinite}$ defined as the composition of the finite type diagram of $S$ and $\operatorname{toLightProfinite}$.
LightProfinite.fintypeDiagramdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the finite type diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the finite type diagram of $S$ is a functor of the set of opposites of $\Natural$ and the set of finite type categories defined as the indexing diagram of the light diagram of $S$.
LightProfinite.limdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the limit of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the limit of $S$ is a limit cone of the diagram of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{asLimitCone}$ applied to $S$ and $\operatorname{asLimit}$ applied to $S$.
LightProfinite.projdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the projection of S and n (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Let $n$ be a natural number. Then the projection of $S$ and $n$ is a homomorphism of $S$ and the action of the diagram of $S$ and $\operatorname{op}$ applied to $n$ defined as the component of the projection of $\operatorname{asLimitCone}$ applied to $S$ and $\operatorname{op}$ applied to $n$.
LightProfinite.transitionMapdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
the transition map of S and n (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Let $n$ be a natural number. Then the transition map of $S$ and $n$ is a homomorphism of the component of $S$ and $n + 1$ and the component of $S$ and $n$.
LightProfinite.transitionMapLEdefMathlib.Topology.Category.LightProfinite.AsLimit, function or constant
Wording
no wording
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Assume that $n \leq m$. Then $\operatorname{transitionMapLE}$ applied to $S$ and $h$ is a homomorphism of the component of $S$ and $m$ and the component of $S$ and $n$ defined as the map of the diagram of $S$ and $\operatorname{op}$ applied to the homomorphism of $h$.

Mathlib.Topology.Category.LightProfinite.Basic

FintypeCat.toLightProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toLightProfinite}$ is a functor of the set of finite type categories and $\mathrm{LightProfinite}$.
FintypeCat.toLightProfiniteFullyFaithfuldefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toLightProfiniteFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{toLightProfinite}$.
LightDiagramstructureMathlib.Topology.Category.LightProfinite.Basic, type
Wording
light diagram (from the name)
English
The light diagrams are a basic type.
LightDiagram'structureMathlib.Topology.Category.LightProfinite.Basic, type
Wording
light diagram (from the name)
English
The light diagrams are a basic type.
LightDiagram'.diagramdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the diagram of self (from the name)
English
Let $\mathrm{self}$ be a light diagram. Then the diagram of $\mathrm{self}$ is a functor of the set of opposites of $\Natural$ and the set of skeletons defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
LightDiagram'.toLightFunctordefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the light functor (from the name)
English
The light functor is a functor of the set of light diagrams and the set of light diagrams.
LightDiagram'.toProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
Let $S$ be a light diagram. Then $\operatorname{toProfinite}$ applied to $S$ is an element of $\mathrm{Profinite}$ defined as the limit of the composition of the diagram of $S$ and the composition of the functor of the equivalence and $\operatorname{toProfinite}$.
LightDiagram.conedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the limit cone of self (from the docstring)
English
Let $\mathrm{self}$ be a light diagram. Then the limit cone of $\mathrm{self}$ is a cone of the composition of the indexing diagram of $\mathrm{self}$ and $\operatorname{toProfinite}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
LightDiagram.diagramdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the indexing diagram of self (from the docstring)
English
Let $\mathrm{self}$ be a light diagram. Then the indexing diagram of $\mathrm{self}$ is a functor of the set of opposites of $\Natural$ and the set of finite type categories defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
LightDiagram.equivSmalldefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the equivalence small (from the name)
English
The equivalence small is an equivalence of the set of light diagrams and the set of light diagrams defined as the inverse of $\operatorname{asEquivalence}$ applied to the light functor.
LightDiagram.isLimitdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the limit cone of self (from the docstring)
English
Let $\mathrm{self}$ be a light diagram. Then the limit cone of $\mathrm{self}$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $\mathrm{self}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
LightDiagram.toProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
Let $S$ be a light diagram. Then $\operatorname{toProfinite}$ applied to $S$ is an element of $\mathrm{Profinite}$ defined as $\operatorname{pt}$ applied to the limit cone of $S$.
LightProfinitedefMathlib.Topology.Category.LightProfinite.Basic, type
Wording
no wording
English
generation took over the time limit
LightProfinite.equivDiagramdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the equivalence diagram (from the name)
English
The equivalence diagram is an equivalence of $\mathrm{LightProfinite}$ and the set of light diagrams.
LightProfinite.isoOfBijectivedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the isomorphism of f and bij (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$ such that $\operatorname{coe}$ applied to the homomorphism of $f$ is bijective. Then the isomorphism of $f$ and $\mathrm{bij}$ is an isomorphism of $X$ and $Y$ defined as $\operatorname{asIso}$ applied to $f$.
LightProfinite.limitConedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and $\mathrm{LightProfinite}$. Then the limit cone of $F$ is a cone of $F$.
LightProfinite.limitConeIsLimitdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the limit cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and $\mathrm{LightProfinite}$. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.
LightProfinite.ofdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
generation took over the time limit
LightProfinite.toLightDiagramdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the light diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the light diagram of $S$ is a light diagram defined as $\operatorname{mk}$ applied to the composition of the initial functor of the set of discrete quotients of the set of carriers of the underlying topological space of the action of $\mathrm{lightToProfinite}$ and $S$ and the finite type diagram of the action of $\mathrm{lightToProfinite}$ and $S$, the cone of the limit cone composition of the initial functor of the set of discrete quotients of the set of carriers of the underlying topological space of the action of $\mathrm{lightToProfinite}$ and $S$ and the limit of the action of $\mathrm{lightToProfinite}$ and $S$ and $\operatorname{isLimit}$ applied to the limit cone composition of the initial functor of the set of discrete quotients of the set of carriers of the underlying topological space of the action of $\mathrm{lightToProfinite}$ and $S$ and the limit of the action of $\mathrm{lightToProfinite}$ and $S$.
LightProfinite.toTopCatdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the topological category (from the name)
English
generation took over the time limit
lightDiagramToLightProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\mathrm{lightDiagramToLightProfinite}$ is a functor of the set of light diagrams and $\mathrm{LightProfinite}$.
lightDiagramToProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\mathrm{lightDiagramToProfinite}$ is a functor of the set of light diagrams and $\mathrm{Profinite}$ defined as the induced functor of $\operatorname{toProfinite}$.
lightProfiniteToCompHausdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
generation took over the time limit
lightProfiniteToLightDiagramdefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
the light profinite to light diagram (from the name)
English
The light profinite to light diagram is a functor of $\mathrm{LightProfinite}$ and the set of light diagrams.
lightToProfinitedefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\mathrm{lightToProfinite}$ is a functor of $\mathrm{LightProfinite}$ and $\mathrm{Profinite}$.
lightToProfiniteFullyFaithfuldefMathlib.Topology.Category.LightProfinite.Basic, function or constant
Wording
no wording
English
$\mathrm{lightToProfiniteFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to $\mathrm{lightToProfinite}$.

Mathlib.Topology.Category.LightProfinite.Extend

LightProfinite.Extend.coconedefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the cocone of G and S (from the name)
English
Let $G$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and $C$. Let $S$ be an element of $\mathrm{LightProfinite}$. Then the cocone of $G$ and $S$ is a cocone of the composition of the projection of the opposite of $\operatorname{toLightProfinite}$ and $\operatorname{op}$ applied to $S$ and the composition of the opposite of $\operatorname{toLightProfinite}$ and $G$.
LightProfinite.Extend.conedefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the cone of G and S (from the name)
English
Let $G$ be a functor of $\mathrm{LightProfinite}$ and $C$. Let $S$ be an element of $\mathrm{LightProfinite}$. Then the cone of $G$ and $S$ is a cone of the composition of the projection of $S$ and $\operatorname{toLightProfinite}$ and the composition of $\operatorname{toLightProfinite}$ and $G$.
LightProfinite.Extend.functordefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the functor of c (from the name)
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toLightProfinite}$. Then the functor of $c$ is a functor of the set of opposites of $\Natural$ and the set of structured arrows of $\operatorname{pt}$ applied to $c$ and $\operatorname{toLightProfinite}$.
LightProfinite.Extend.functorOpdefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the functor opposite of c (from the name)
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toLightProfinite}$. Then the functor opposite of $c$ is a functor of $\Natural$ and the set of costructured arrows of the opposite of $\operatorname{toLightProfinite}$ and $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ defined as the composition of the right opposite of the functor of $c$ and the costructured arrow of $\operatorname{toLightProfinite}$ and $\operatorname{pt}$ applied to $c$.
LightProfinite.Extend.isColimitCoconedefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toLightProfinite}$. Let $G$ be a functor of the set of opposites of $\mathrm{LightProfinite}$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $G$ and the opposite of $c$. Then $\operatorname{isColimitCocone}$ applied to $c$, $G$, $\mathrm{hc}$ and $\mathrm{hc'}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $G$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{isColimitWhiskerEquiv}$ applied to the composition of the functor of the double opposite category of $\Natural$ and the functor opposite of $c$, the cocone of $G$ and $\operatorname{pt}$ applied to $c$ and $\mathrm{hc'}$.
LightProfinite.Extend.isLimitConedefMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toLightProfinite}$. Let $G$ be a functor of $\mathrm{LightProfinite}$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $G$ and $c$. Then $\operatorname{isLimitCone}$ applied to $c$, $G$, $\mathrm{hc}$ and $\mathrm{hc'}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $G$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{isLimitWhiskerEquiv}$ applied to the functor of $c$, the cone of $G$ and $\operatorname{pt}$ applied to $c$ and $\mathrm{hc'}$.
LightProfinite.asLimit'defMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the limit cone of S (from the docstring)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the limit cone of $S$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{asLimitCone'}$ applied to $S$ defined as $\operatorname{isLimitCone}$ applied to $\operatorname{asLimitCone}$ applied to $S$, the identity of $\mathrm{LightProfinite}$, $\operatorname{asLimit}$ applied to $S$ and $\operatorname{asLimit}$ applied to $S$.
LightProfinite.asLimitCone'defMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
no wording
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then $\operatorname{asLimitCone'}$ applied to $S$ is a cone of the diagram of $S$ defined as the cone of the identity of $\mathrm{LightProfinite}$ and $S$.
LightProfinite.diagram'defMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the diagram of $S$ is a functor of the set of structured arrows of $S$ and $\operatorname{toLightProfinite}$ and $\mathrm{LightProfinite}$ defined as the composition of the finite type diagram of $S$ and $\operatorname{toLightProfinite}$.
LightProfinite.fintypeDiagram'defMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the finite type diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the finite type diagram of $S$ is a functor of the set of structured arrows of $S$ and $\operatorname{toLightProfinite}$ and the set of finite type categories defined as the projection of $S$ and $\operatorname{toLightProfinite}$.
LightProfinite.lim'defMathlib.Topology.Category.LightProfinite.Extend, function or constant
Wording
the limit of S (from the name)
English
Let $S$ be an element of $\mathrm{LightProfinite}$. Then the limit of $S$ is a limit cone of the diagram of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{asLimitCone'}$ applied to $S$ and the limit cone of $S$.

Mathlib.Topology.Category.LightProfinite.Limits

LightProfinite.isTerminalPUnitdefMathlib.Topology.Category.LightProfinite.Limits, function or constant
Wording
no wording
English
$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{isTerminalPUnit}$.

Mathlib.Topology.Category.LightProfinite.Sequence

LightProfinite.NatUnionInftydefMathlib.Topology.Category.LightProfinite.Sequence, function or constant
Wording
the one point compactification of the natural numbers (from the docstring)
English
The one point compactification of the natural numbers is an element of $\mathrm{LightProfinite}$ defined as $\operatorname{of}$ applied to the set of one points of $\Natural$.
LightProfinite.natUnionInftyEmbeddingdefMathlib.Topology.Category.LightProfinite.Sequence, function or constant
Wording
the natural union infty embedding (from the name)
English
The natural union infty embedding is a continuous map of the set of one points of $\Natural$ and $\Real$.

Mathlib.Topology.Category.Locale

LocaledefMathlib.Topology.Category.Locale, type
Wording
locale (from the name)
English
A locale is an opposite of $\mathrm{Frm}$.
Locale.ofdefMathlib.Topology.Category.Locale, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is a locale defined as $\operatorname{op}$ applied to $\operatorname{of}$ applied to $x$.
topToLocaledefMathlib.Topology.Category.Locale, function or constant
Wording
the top to locale (from the name)
English
The top to locale is a functor of the set of topological categories and the set of locales defined as the right opposite of $\mathrm{topCatOpToFrm}$.

Mathlib.Topology.Category.Profinite.AsLimit

Profinite.asLimitdefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{Profinite}$. Then $\operatorname{asLimit}$ applied to $X$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{asLimitCone}$ applied to $X$ defined as $\operatorname{ofIsoLimit}$ applied to the limit cone of the diagram of $X$ and the inverse of $\operatorname{asLimitConeIso}$ applied to $X$.
Profinite.asLimitConedefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{Profinite}$. Then $\operatorname{asLimitCone}$ applied to $X$ is a cone of the diagram of $X$.
Profinite.asLimitConeIsodefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{Profinite}$. Then $\operatorname{asLimitConeIso}$ applied to $X$ is an isomorphism of $\operatorname{asLimitCone}$ applied to $X$ and the limit cone of the diagram of $X$.
Profinite.diagramdefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
the diagram of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the diagram of $X$ is a functor of the set of discrete quotients of the set of carriers of the underlying topological space of $X$ and $\mathrm{Profinite}$ defined as the composition of the finite type diagram of $X$ and $\operatorname{toProfinite}$.
Profinite.fintypeDiagramdefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
the finite type diagram of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the finite type diagram of $X$ is a functor of the set of discrete quotients of the set of carriers of the underlying topological space of $X$ and the set of finite type categories.
Profinite.isoAsLimitConeLiftdefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
the isomorphism as limit cone lift of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the isomorphism as limit cone lift of $X$ is an isomorphism of $X$ and $\operatorname{pt}$ applied to the limit cone of the diagram of $X$ defined as $\operatorname{asIso}$ applied to the lift of the limit cone of the diagram of $X$ and $\operatorname{asLimitCone}$ applied to $X$.
Profinite.limdefMathlib.Topology.Category.Profinite.AsLimit, function or constant
Wording
the limit of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the limit of $X$ is a limit cone of the diagram of $X$ defined as $\operatorname{mk}$ applied to $\operatorname{asLimitCone}$ applied to $X$ and $\operatorname{asLimit}$ applied to $X$.

Mathlib.Topology.Category.Profinite.Basic

CompHaus.toProfinitedefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toProfinite}$ is a functor of $\mathrm{CompHaus}$ and $\mathrm{Profinite}$.
CompHaus.toProfiniteObjdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
the profinite object of X (from the name)
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then the profinite object of $X$ is an element of $\mathrm{Profinite}$.
FintypeCat.toProfinitedefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toProfinite}$ is a functor of the set of finite type categories and $\mathrm{Profinite}$.
FintypeCat.toProfiniteFullyFaithfuldefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toProfiniteFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{toProfinite}$.
ProfinitedefMathlib.Topology.Category.Profinite.Basic, type
Wording
no wording
English
generation took over the time limit
Profinite.limitConedefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and $\mathrm{Profinite}$. Then the limit cone of $F$ is a cone of $F$.
Profinite.limitConeIsLimitdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
the limit cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and $\mathrm{Profinite}$. Then the limit cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.
Profinite.ofdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
generation took over the time limit
Profinite.pidefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
the product of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to elements of $\mathrm{Profinite}$. Then the product of $x_{1}$ is an element of $\mathrm{Profinite}$ defined as $\operatorname{of}$ applied to the set of functions from elements $a$ of $x$ to carriers of the underlying topological space of $x_{1}$ applied to $a$.
Profinite.toCompHausEquivalencedefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{CompHaus}$. Let $Y$ be an element of $\mathrm{Profinite}$. Then $\operatorname{toCompHausEquivalence}$ applied to $X$ and $Y$ is an equivalence from the set of homomorphisms of the profinite object of $X$ and $Y$ to the set of homomorphisms of $X$ and the action of $\mathrm{profiniteToCompHaus}$ and $Y$.
Profinite.toProfiniteAdjToCompHausdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
$\operatorname{toProfiniteAdjToCompHaus}$ is an adjunction of $\operatorname{toProfinite}$ and $\mathrm{profiniteToCompHaus}$.
Profinite.toTopCatdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
the topological category (from the name)
English
generation took over the time limit
profiniteToCompHausdefMathlib.Topology.Category.Profinite.Basic, function or constant
Wording
no wording
English
generation took over the time limit

Mathlib.Topology.Category.Profinite.EffectiveEpi

Profinite.profiniteToCompHausEffectivePresentationdefMathlib.Topology.Category.Profinite.EffectiveEpi, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then $\operatorname{profiniteToCompHausEffectivePresentation}$ applied to $X$ is an effective presentation of $\mathrm{profiniteToCompHaus}$ and $X$.

Mathlib.Topology.Category.Profinite.Extend

Profinite.Extend.coconedefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the cocone of G and S (from the name)
English
Let $G$ be a functor of the set of opposites of $\mathrm{Profinite}$ and $C$. Let $S$ be an element of $\mathrm{Profinite}$. Then the cocone of $G$ and $S$ is a cocone of the composition of the projection of the opposite of $\operatorname{toProfinite}$ and $\operatorname{op}$ applied to $S$ and the composition of the opposite of $\operatorname{toProfinite}$ and $G$.
Profinite.Extend.conedefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the cone of G and S (from the name)
English
Let $G$ be a functor of $\mathrm{Profinite}$ and $C$. Let $S$ be an element of $\mathrm{Profinite}$. Then the cone of $G$ and $S$ is a cone of the composition of the projection of $S$ and $\operatorname{toProfinite}$ and the composition of $\operatorname{toProfinite}$ and $G$.
Profinite.Extend.functordefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the functor of c (from the name)
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toProfinite}$. Then the functor of $c$ is a functor of $I$ and the set of structured arrows of $\operatorname{pt}$ applied to $c$ and $\operatorname{toProfinite}$.
Profinite.Extend.functorOpdefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the functor opposite of c (from the name)
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toProfinite}$. Then the functor opposite of $c$ is a functor of the set of opposites of $I$ and the set of costructured arrows of the opposite of $\operatorname{toProfinite}$ and $\operatorname{op}$ applied to $\operatorname{pt}$ applied to $c$ defined as the composition of the opposite of the functor of $c$ and the costructured arrow of $\operatorname{toProfinite}$ and $\operatorname{pt}$ applied to $c$.
Profinite.Extend.isColimitCoconedefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toProfinite}$. Let $G$ be a functor of the set of opposites of $\mathrm{Profinite}$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsColimit}$ applied to the map cocone of $G$ and the opposite of $c$. Then $\operatorname{isColimitCocone}$ applied to $c$, $G$, $\mathrm{hc}$ and $\mathrm{hc'}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $G$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{isColimitWhiskerEquiv}$ applied to the functor opposite of $c$, the cocone of $G$ and $\operatorname{pt}$ applied to $c$ and $\mathrm{hc'}$.
Profinite.Extend.isLimitConedefMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and $\operatorname{toProfinite}$. Let $G$ be a functor of $\mathrm{Profinite}$ and $C$. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Let $\mathrm{hc'}$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $G$ and $c$. Then $\operatorname{isLimitCone}$ applied to $c$, $G$, $\mathrm{hc}$ and $\mathrm{hc'}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $G$ and $\operatorname{pt}$ applied to $c$ defined as $\operatorname{isLimitWhiskerEquiv}$ applied to the functor of $c$, the cone of $G$ and $\operatorname{pt}$ applied to $c$ and $\mathrm{hc'}$.
Profinite.asLimit'defMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the limit cone of S (from the docstring)
English
Let $S$ be an element of $\mathrm{Profinite}$. Then the limit cone of $S$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{asLimitCone'}$ applied to $S$ defined as $\operatorname{isLimitCone}$ applied to $\operatorname{asLimitCone}$ applied to $S$, the identity of $\mathrm{Profinite}$, $\operatorname{asLimit}$ applied to $S$ and $\operatorname{asLimit}$ applied to $S$.
Profinite.asLimitCone'defMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
no wording
English
Let $S$ be an element of $\mathrm{Profinite}$. Then $\operatorname{asLimitCone'}$ applied to $S$ is a cone of the diagram of $S$ defined as the cone of the identity of $\mathrm{Profinite}$ and $S$.
Profinite.diagram'defMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{Profinite}$. Then the diagram of $S$ is a functor of the set of structured arrows of $S$ and $\operatorname{toProfinite}$ and $\mathrm{Profinite}$ defined as the composition of the finite type diagram of $S$ and $\operatorname{toProfinite}$.
Profinite.fintypeDiagram'defMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the finite type diagram of S (from the name)
English
Let $S$ be an element of $\mathrm{Profinite}$. Then the finite type diagram of $S$ is a functor of the set of structured arrows of $S$ and $\operatorname{toProfinite}$ and the set of finite type categories defined as the projection of $S$ and $\operatorname{toProfinite}$.
Profinite.lim'defMathlib.Topology.Category.Profinite.Extend, function or constant
Wording
the limit of S (from the name)
English
Let $S$ be an element of $\mathrm{Profinite}$. Then the limit of $S$ is a limit cone of the diagram of $S$ defined as $\operatorname{mk}$ applied to $\operatorname{asLimitCone'}$ applied to $S$ and the limit cone of $S$.

Mathlib.Topology.Category.Profinite.Limits

Profinite.isTerminalPUnitdefMathlib.Topology.Category.Profinite.Limits, function or constant
Wording
no wording
English
$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{isTerminalPUnit}$.

Mathlib.Topology.Category.Profinite.Nobeling.Basic

Profinite.NobelingProof.GoodProductsdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the good product of C (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Then the good product of $C$ is an element of the power set of the set of products of $I$ defined as $\operatorname{ofPred}$ applied to the function that maps $l$ to $\operatorname{isGood}$ applied to $C$ and $l$.
Profinite.NobelingProof.GoodProducts.equiv_rangedefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the equivalence range of C (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Then the equivalence range of $C$ is an equivalence from the set of elements of the good product of $C$ to the set of elements of the range of $C$ defined as the equivalence of $\operatorname{eval}$ applied to $C$ and $\operatorname{injective}$ applied to $C$.
Profinite.NobelingProof.GoodProducts.evaldefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the evaluation of C and l (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $l$ be an element of $\SubtypeSet {l_{1}}{\operatorname{isGood} (C , l_{1})}$. Then the evaluation of $C$ and $l$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as the evaluation of $C$ and $l$.
Profinite.NobelingProof.GoodProducts.rangedefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the range of C (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Then the range of $C$ is an element of the power set of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as the range of $\operatorname{eval}$ applied to $C$.
Profinite.NobelingProof.PdefMathlib.Topology.Category.Profinite.Nobeling.Basic, predicate
Wording
no wording
English
Let $I$ be a set. Let $o$ be an ordinal. Then $\operatorname{P}$ holds for $I$ and $o$, if if $o$ is less than or equal to the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$, then for all elements $C$ of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$, if $C$ is closed, then if $\operatorname{contained}$ holds for $C$ and $o$, then $\mathrm{LinearIndependent}$ holds for $\Integer$ and $\operatorname{eval}$ applied to $C$.
Profinite.NobelingProof.ProductsdefMathlib.Topology.Category.Profinite.Nobeling.Basic, type
Wording
product of I (from the name)
English
Let $I$ be a set. Then a product of $I$ is an element of the function that maps $I$ to $\SubtypeSet {l}{\operatorname{IsChain} (\lambda x_{1} . \lambda x_{2} . \mathrm{Gt} (x_{1} , x_{2}), l)}$.
Profinite.NobelingProof.Products.evaldefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the evaluation of C and l (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $l$ be a product of $I$. Then the evaluation of $C$ and $l$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as $\operatorname{prod}$ applied to $\operatorname{map}$ applied to $\operatorname{e}$ applied to $C$ and $l$.
Profinite.NobelingProof.Products.isGooddefMathlib.Topology.Category.Profinite.Nobeling.Basic, predicate
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $l$ be a product of $I$. Then $\operatorname{isGood}$ holds for $C$ and $l$, if the evaluation of $C$ and $l$ is not an element of the span of $\Integer$ and the image of $\operatorname{eval}$ applied to $C$ and $\operatorname{ofPred}$ applied to the function that maps $m$ to $\mathrm{Lt} (m , l)$.
Profinite.NobelingProof.ProjdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the projection of x1 and x2 (from the name)
English
Let $J$ be a function from elements of $I$ to propositions. Let $x_{1}$ be a function from elements of $I$ to elements of $\mathrm{Bool}$. Let $x_{2}$ be an element of $I$. Then the projection of $x_{1}$ and $x_{2}$ is an element of $\mathrm{Bool}$ defined as $\iteMACRoG {J (x_{2})}{x_{1} (x_{2})}{\operatorname{false}}$.
Profinite.NobelingProof.ProjRestrictdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the restriction of C (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $J$ be a function from elements of $I$ to propositions. Let $x_{1}$ be an element of $C$. Then the restriction of $C$ is an element of the projection of $C$ and $J$.
Profinite.NobelingProof.ProjRestrictsdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that for all elements $i$ of $I$, if $J$ holds for $i$, then $K$ holds for $i$. Let $x_{2}$ be an element of the projection of $C$ and $K$. Then $\operatorname{ProjRestricts}$ applied to $C$, $h$ and $x_{2}$ is an element of the projection of $C$ and $J$ defined as $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the set congruence of $\mathrm{Profinite\_\_NobelingProof\_\_proj\_eq\_of\_subset}$ applied to $C$, $J$, $K$ and $h$, the restriction of the projection of $C$ and $K$ and $x_{2}$.
Profinite.NobelingProof.containeddefMathlib.Topology.Category.Profinite.Nobeling.Basic, predicate
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $o$ be an ordinal. Then $\operatorname{contained}$ holds for $C$ and $o$, if for all functions $f$ from elements of $I$ to elements of $\mathrm{Bool}$, if $f$ is an element of $C$, then for all elements $i$ of $I$, if $\EqtMACRoH {f (i)}{\operatorname{true}}$, then the order of $I$ and $i$ is less than $o$.
Profinite.NobelingProof.edefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $i$ be an element of $I$. Then $\operatorname{e}$ applied to $C$ and $i$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$.
Profinite.NobelingProof.iso_mapdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the objectwise map in the isomorphism of C and J (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $J$ be a function from elements of $I$ to propositions. Then the objectwise map in the isomorphism of $C$ and $J$ is a continuous map of the set of elements of the projection of $C$ and $J$ and the set of elements of the object part of the functor of $C$ and $J$.
Profinite.NobelingProof.orddefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the order of I and i (from the name)
English
Let $I$ be a set. Let $i$ be an element of $I$. Then the order of $I$ and $i$ is an ordinal defined as $\operatorname{toRelEmbedding}$ applied to the order type of the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (x_{5} , x_{6})$ and $i$.
Profinite.NobelingProof.spanConedefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the span cone of hC (from the name)
English
Assume that $C$ is compact. Then the span cone of $\mathrm{hC}$ is a cone of the span functor of $\mathrm{hC}$.
Profinite.NobelingProof.spanCone_isLimitdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the limit cone of hC (from the docstring)
English
Assume that $C$ is compact. Then the limit cone of $\mathrm{hC}$ is an element of $\operatorname{IsLimit}$ applied to the span cone of $\mathrm{hC}$.
Profinite.NobelingProof.spanFunctordefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the span functor of hC (from the name)
English
Assume that $C$ is compact. Then the span functor of $\mathrm{hC}$ is a functor of the set of opposites of the set of finite sets of $I$ and $\mathrm{Profinite}$.
Profinite.NobelingProof.spanFunctorIsoIndexFunctordefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the isomorphism of hC (from the docstring)
English
Assume that $C$ is compact. Then the isomorphism of $\mathrm{hC}$ is an isomorphism of the span functor of $\mathrm{hC}$ and the index functor of $\mathrm{hC}$.
Profinite.NobelingProof.πdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the projection of C and J (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $J$ be a function from elements of $I$ to propositions. Then the projection of $C$ and $J$ is an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ defined as the image of $\operatorname{Proj}$ and $C$.
Profinite.NobelingProof.πsdefMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the projection of C and o (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $o$ be an ordinal. Then the projection of $C$ and $o$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{1}$ to the proposition that the order of $I$ and $x_{1}$ is less than $o$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$.
Profinite.NobelingProof.πs'defMathlib.Topology.Category.Profinite.Nobeling.Basic, function or constant
Wording
the projection of C and h1 (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $x_{1} \leq x_{2}$. Then the projection of $C$ and $h_{1}$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{3}$ to the proposition that the order of $I$ and $x_{3}$ is less than $x_{1}$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{4}$ to the proposition that the order of $I$ and $x_{4}$ is less than $x_{2}$ and $\Integer$.

Mathlib.Topology.Category.Profinite.Nobeling.Induction

Profinite.Nobeling.ιdefMathlib.Topology.Category.Profinite.Nobeling.Induction, function or constant
Wording
the inclusion of x and x1 (from the name)
English
Let $S$ be an element of $\mathrm{Profinite}$. Let $x$ be a carrier of the underlying topological space of $S$. Let $x_{1}$ be an element of $\SubtypeSet {C}{\mathrm{IsClopen} (C)}$. Then the inclusion of $x$ and $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{decide}$ applied to $\MembershipmemMACRoT {x_{1}}{x}$.
Profinite.NobelingProof.GoodProducts.BasisdefMathlib.Topology.Category.Profinite.Nobeling.Induction, function or constant
Wording
the basis of C and hC (from the name)
English
Let $C$ be a closed element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Then the basis of $C$ and $\mathrm{hC}$ is a basis of $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as $\operatorname{mk}$ applied to $\operatorname{linearIndependent}$ applied to $C$ and $\mathrm{hC}$ and $\operatorname{span}$ applied to $C$ and $\mathrm{hC}$.

Mathlib.Topology.Category.Profinite.Nobeling.Span

Profinite.NobelingProof.factorsdefMathlib.Topology.Category.Profinite.Nobeling.Span, function or constant
Wording
the factor of s and x1 (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $s$ be a finite set of $I$. Let $x_{1}$ be an element of the projection of $C$ and the function that maps $x_{3}$ to $\MembershipmemMACRoT {s}{x_{3}}$. Then the factor of $s$ and $x_{1}$ is a list of elements of $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\Integer$ defined as $\operatorname{map}$ applied to the function that maps $i$ to $\iteMACRoG {(\EqtMACRoH {i}{\operatorname{true}})}{\operatorname{e} (\mathrm{Profinite\_\_NobelingProof\_\_\_u3c0\_} (C , \lambda x_{2} . \MembershipmemMACRoT {s}{x_{2}}), i)}{(1 - \operatorname{e} (\mathrm{Profinite\_\_NobelingProof\_\_\_u3c0\_} (C , \lambda x_{3} . \MembershipmemMACRoT {s}{x_{3}}), i))}$ and the sort of $s$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Geq} (x_{4} , x_{5})$.
Profinite.NobelingProof.spanFinBasisdefMathlib.Topology.Category.Profinite.Nobeling.Span, function or constant
Wording
the span finite basis of s and x1 (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $s$ be a finite set of $I$. Let $x_{1}$ be an element of the projection of $C$ and the function that maps $x_{3}$ to $\MembershipmemMACRoT {s}{x_{3}}$. Then the span finite basis of $s$ and $x_{1}$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$ and $\Integer$.
Profinite.NobelingProof.πJdefMathlib.Topology.Category.Profinite.Nobeling.Span, function or constant
Wording
the projection of C and s (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $s$ be a finite set of $I$. Then the projection of $C$ and $s$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of the projection of $C$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$.

Mathlib.Topology.Category.Profinite.Nobeling.Successor

Profinite.NobelingProof.C'defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Then $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$ is an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ defined as $\operatorname{inter}$ applied to $\operatorname{C0}$ applied to $C$ and $\mathrm{ho}$ and the projection of $\operatorname{C1}$ applied to $C$ and $\mathrm{ho}$ and the function that maps $x_{1}$ to the proposition that the order of $I$ and $x_{1}$ is less than $o$.
Profinite.NobelingProof.C0defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Then $\operatorname{C0}$ applied to $C$ and $\mathrm{ho}$ is an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ defined as $\operatorname{inter}$ applied to $C$ and $\operatorname{ofPred}$ applied to the function that maps $f$ to $\EqtMACRoH {f (\operatorname{term} (I , \mathrm{ho}))}{\operatorname{false}}$.
Profinite.NobelingProof.C1defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Then $\operatorname{C1}$ applied to $C$ and $\mathrm{ho}$ is an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ defined as $\operatorname{inter}$ applied to $C$ and $\operatorname{ofPred}$ applied to the function that maps $f$ to $\EqtMACRoH {f (\operatorname{term} (I , \mathrm{ho}))}{\operatorname{true}}$.
Profinite.NobelingProof.CC'₀defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Let $x_{1}$ be an element of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$. Then $\mathrm{Profinite\_\_NobelingProof\_\_CC'\_u2080\_}$ applied to $C$, $\mathrm{ho}$ and $x_{1}$ is an element of $C$ defined as $x_{1}$.
Profinite.NobelingProof.CC'₁defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ such that $\operatorname{contained}$ holds for $C$ and the successor of $o$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Let $x_{1}$ be an element of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$. Then $\mathrm{Profinite\_\_NobelingProof\_\_CC'\_u2081\_}$ applied to $C$, $\mathrm{hsC}$, $\mathrm{ho}$ and $x_{1}$ is an element of $C$ defined as $\operatorname{SwapTrue}$ applied to $o$ and $x_{1}$.
Profinite.NobelingProof.GoodProducts.MaxProductsdefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
the maximum product of C and ho (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$. Then the maximum product of $C$ and $\mathrm{ho}$ is an element of the power set of the set of products of $I$ defined as $\operatorname{ofPred}$ applied to the function that maps $l$ to the proposition that $\operatorname{isGood}$ holds for $C$ and $l$ and $\MembershipmemMACRoT {l}{\operatorname{term} (I , \mathrm{ho})}$.
Profinite.NobelingProof.GoodProducts.MaxToGooddefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ such that $C$ is closed and $\operatorname{contained}$ holds for $C$ and the successor of $o$. Assume that $o$ is less than the order type of the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Lt} (x_{3} , x_{4})$. Assume that the top is less than or equal to the span of $\Integer$ and the range of $\operatorname{eval}$ applied to the projection of $C$ and the function that maps $x_{2}$ to the proposition that the order of $I$ and $x_{2}$ is less than $o$. Let $x_{1}$ be an element of the maximum product of $C$ and $\mathrm{ho}$. Then $\operatorname{MaxToGood}$ applied to $C$, $\mathrm{hC}$, $\mathrm{hsC}$, $\mathrm{ho}$, $h_{1}$ and $x_{1}$ is an element of the good product of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$ defined as the tail of $x_{1}$.
Profinite.NobelingProof.GoodProducts.SumEvaldefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
the sum evaluation of C and x1 (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Lt} (x_{3} , x_{4})$. Let $x_{1}$ be an element of $\mathrm{Sum}$ applied to the set of elements of the good product of the projection of $C$ and the function that maps $x_{2}$ to the proposition that the order of $I$ and $x_{2}$ is less than $o$ and the set of elements of the maximum product of $C$ and $\mathrm{ho}$. Then the sum evaluation of $C$ and $x_{1}$ is an element of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as $\operatorname{elim}$ applied to the function that maps $l$ to the evaluation of $C$ and $l$, the function that maps $l_{1}$ to the evaluation of $C$ and $l_{1}$ and $x_{1}$.
Profinite.NobelingProof.GoodProducts.sum_equivdefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
the equivalence from the sum of C (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ such that $\operatorname{contained}$ holds for $C$ and the successor of $o$. Assume that $o$ is less than the order type of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$. Then the equivalence from the sum of $C$ is an equivalence from $\mathrm{Sum}$ applied to the set of elements of the good product of the projection of $C$ and the function that maps $x_{1}$ to the proposition that the order of $I$ and $x_{1}$ is less than $o$ and the set of elements of the maximum product of $C$ and $\mathrm{ho}$ to the set of elements of the good product of $C$.
Profinite.NobelingProof.GoodProducts.sum_todefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
the inclusion map from the sum of C (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Lt} (x_{3} , x_{4})$. Let $x_{1}$ be an element of $\mathrm{Sum}$ applied to the set of elements of the good product of the projection of $C$ and the function that maps $x_{2}$ to the proposition that the order of $I$ and $x_{2}$ is less than $o$ and the set of elements of the maximum product of $C$ and $\mathrm{ho}$. Then the inclusion map from the sum of $C$ is a product of $I$ defined as $\operatorname{elim}$ applied to the function that maps $x_{1}$ to the proposition that $x_{1}$ is an element of the good product of the projection of $C$ and the function that maps $x_{2}$ to the proposition that the order of $I$ and $x_{2}$ is less than $o$, the function that maps $x_{3}$ to the proposition that $x_{3}$ is an element of the maximum product of $C$ and $\mathrm{ho}$ and $x_{1}$.
Profinite.NobelingProof.Linear_CC'defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ such that $\operatorname{contained}$ holds for $C$ and the successor of $o$. Assume that $o$ is less than the order type of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$. Then $\mathrm{Profinite\_\_NobelingProof\_\_Linear\_CC'}$ applied to $C$, $\mathrm{hsC}$ and $\mathrm{ho}$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$ and $\Integer$ defined as $\mathrm{Profinite\_\_NobelingProof\_\_Linear\_CC'\_u2081\_} (C , \mathrm{hsC} , \mathrm{ho})- \mathrm{Profinite\_\_NobelingProof\_\_Linear\_CC'\_u2080\_} (C , \mathrm{ho})$.
Profinite.NobelingProof.Linear_CC'₀defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is less than the order type of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$. Then $\mathrm{Profinite\_\_NobelingProof\_\_Linear\_CC'\_u2080\_}$ applied to $C$ and $\mathrm{ho}$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$ and $\Integer$ defined as the preimage of $\Integer$ and $\operatorname{mk}$ applied to $\mathrm{Profinite\_\_NobelingProof\_\_CC'\_u2080\_}$ applied to $C$ and $\mathrm{ho}$ and $\mathrm{Profinite\_\_NobelingProof\_\_continuous\_CC'\_u2080\_}$ applied to $C$ and $\mathrm{ho}$.
Profinite.NobelingProof.Linear_CC'₁defMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$ such that $\operatorname{contained}$ holds for $C$ and the successor of $o$. Assume that $o$ is less than the order type of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$. Then $\mathrm{Profinite\_\_NobelingProof\_\_Linear\_CC'\_u2081\_}$ applied to $C$, $\mathrm{hsC}$ and $\mathrm{ho}$ is a linear map of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ and $\mathrm{LocallyConstant}$ applied to the set of elements of $\operatorname{C'}$ applied to $C$ and $\mathrm{ho}$ and $\Integer$ defined as the preimage of $\Integer$ and $\operatorname{mk}$ applied to $\mathrm{Profinite\_\_NobelingProof\_\_CC'\_u2081\_}$ applied to $C$, $\mathrm{hsC}$ and $\mathrm{ho}$ and $\mathrm{Profinite\_\_NobelingProof\_\_continuous\_CC'\_u2081\_}$ applied to $C$, $\mathrm{hsC}$ and $\mathrm{ho}$.
Profinite.NobelingProof.Products.TaildefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
the tail of l (from the name)
English
Let $l$ be a product of $I$. Then the tail of $l$ is a product of $I$ defined as $\operatorname{tail}$ applied to $l$.
Profinite.NobelingProof.SwapTruedefMathlib.Topology.Category.Profinite.Nobeling.Successor, function or constant
Wording
no wording
English
Let $o$ be an ordinal. Let $x_{1}$ be a function from elements of $I$ to elements of $\mathrm{Bool}$. Let $x_{2}$ be an element of $I$. Then $\operatorname{SwapTrue}$ applied to $o$, $x_{1}$ and $x_{2}$ is an element of $\mathrm{Bool}$ defined as $\iteMACRoG {(\EqtMACRoH {\operatorname{ord} (I , x_{2})}{o})}{\operatorname{true}}{x_{1} (x_{2})}$.

Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Profinite.NobelingProof.GoodProducts.range_equivdefMathlib.Topology.Category.Profinite.Nobeling.ZeroLimit, function or constant
Wording
the range equivalence of C (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Assume that $o$ is a successor limit. Assume that $\operatorname{contained}$ holds for $C$ and $o$. Then the range equivalence of $C$ is an equivalence from the set of elements of the range of $C$ to the set of elements of the union of the function that maps $e$ to $\operatorname{smaller}$ applied to $C$ and $e$ defined as the equivalence of $\operatorname{union}$ applied to $C$, $\mathrm{ho}$ and $\mathrm{hsC}$.
Profinite.NobelingProof.GoodProducts.range_equiv_smallerdefMathlib.Topology.Category.Profinite.Nobeling.ZeroLimit, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $o$ be an ordinal. Then $\mathrm{Profinite\_\_NobelingProof\_\_GoodProducts\_\_range\_equiv\_smaller}$ applied to $C$ and $o$ is an equivalence from the set of elements of the range of the projection of $C$ and the function that maps $x_{1}$ to the proposition that the order of $I$ and $x_{1}$ is less than $o$ to the set of elements of $\operatorname{smaller}$ applied to $C$ and $o$ defined as the equivalence of $\mathrm{Profinite\_\_NobelingProof\_\_GoodProducts\_\_range\_equiv\_smaller\_toFun}$ applied to $C$ and $o$ and $\mathrm{Profinite\_\_NobelingProof\_\_GoodProducts\_\_range\_equiv\_smaller\_toFun\_bijective}$ applied to $C$ and $o$.
Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFundefMathlib.Topology.Category.Profinite.Nobeling.ZeroLimit, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $o$ be an ordinal. Let $x_{1}$ be an element of the range of the projection of $C$ and the function that maps $x_{2}$ to the proposition that the order of $I$ and $x_{2}$ is less than $o$. Then $\mathrm{Profinite\_\_NobelingProof\_\_GoodProducts\_\_range\_equiv\_smaller\_toFun}$ applied to $C$, $o$ and $x_{1}$ is an element of $\operatorname{smaller}$ applied to $C$ and $o$ defined as $\mathrm{Profinite\_\_NobelingProof\_\_\_u3c0\_s\_\_app}$ applied to $C$, $o$ and $x_{1}$.
Profinite.NobelingProof.GoodProducts.smallerdefMathlib.Topology.Category.Profinite.Nobeling.ZeroLimit, function or constant
Wording
no wording
English
Let $C$ be an element of $\wp (\mathrm{Elem} (I)\rightarrow \mathrm{Bool})$. Let $o$ be an ordinal. Then $\operatorname{smaller}$ applied to $C$ and $o$ is an element of the power set of $\mathrm{LocallyConstant}$ applied to the set of elements of $C$ and $\Integer$ defined as the image of $\operatorname{coe}$ applied to the projection of $C$ and $o$ and the range of the projection of $C$ and the function that maps $x_{1}$ to the proposition that the order of $I$ and $x_{1}$ is less than $o$.
Profinite.NobelingProof.Products.nildefMathlib.Topology.Category.Profinite.Nobeling.ZeroLimit, function or constant
Wording
no wording
English
$\operatorname{nil}$ is a product of $I$ defined as $\operatorname{nil}$.

Mathlib.Topology.Category.Profinite.Product

Profinite.IndexFunctor.mapdefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the map of C and i1 (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow X (i_{1}))$. Assume that for all elements $i$ of $x$, if $J$ holds for $i$, then $K$ holds for $i$. Then the map of $C$ and $h$ is a continuous map of the set of elements of the object part of the functor of $C$ and $K$ and the set of elements of the object part of the functor of $C$ and $J$.
Profinite.IndexFunctor.objdefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the object part of the functor of C and i2 (from the docstring)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow X (i_{2}))$. Let $J$ be a function from elements of $x$ to propositions. Then the object part of the functor of $C$ and $J$ is an element of $\wp (\mathrm{Elem} (\SubtypeSet {i_{1}}{J (i_{1})})\rightarrow X (i))$ defined as the image of $\operatorname{coe}$ applied to the precomposition of $J$ and $C$.
Profinite.IndexFunctor.π_appdefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the projection application of C and i (from the name)
English
Let $C$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow X (i))$. Let $J$ be a function from elements of $x$ to propositions. Then the projection application of $C$ and $J$ is a continuous map of the set of elements of $C$ and the set of elements of the object part of the functor of $C$ and $J$.
Profinite.asLimitindexConeIsodefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
no wording
English
Assume that $C$ is compact. Then $\operatorname{asLimitindexConeIso}$ applied to $\mathrm{hC}$ is an isomorphism of the limit cone on $\mathrm{hC}$ and the limit cone of the index functor of $\mathrm{hC}$.
Profinite.indexConedefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the limit cone on hC (from the docstring)
English
Assume that $C$ is compact. Then the limit cone on $\mathrm{hC}$ is a cone of the index functor of $\mathrm{hC}$.
Profinite.indexCone_isLimitdefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the limit cone of hC (from the docstring)
English
Assume that $C$ is compact. Then the limit cone of $\mathrm{hC}$ is an element of $\operatorname{IsLimit}$ applied to the limit cone on $\mathrm{hC}$ defined as $\operatorname{ofIsoLimit}$ applied to the limit cone of the index functor of $\mathrm{hC}$ and the inverse of $\operatorname{asLimitindexConeIso}$ applied to $\mathrm{hC}$.
Profinite.indexFunctordefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
the index functor of hC (from the name)
English
Assume that $C$ is compact. Then the index functor of $\mathrm{hC}$ is a functor of the set of opposites of the set of finite sets of $x$ and $\mathrm{Profinite}$.
Profinite.isoindexConeLiftdefMathlib.Topology.Category.Profinite.Product, function or constant
Wording
no wording
English
Assume that $C$ is compact. Then $\operatorname{isoindexConeLift}$ applied to $\mathrm{hC}$ is an isomorphism of $\operatorname{of}$ applied to the set of elements of $C$ and $\operatorname{pt}$ applied to the limit cone of the index functor of $\mathrm{hC}$ defined as $\operatorname{asIso}$ applied to the lift of the limit cone of the index functor of $\mathrm{hC}$ and the limit cone on $\mathrm{hC}$.

Mathlib.Topology.Category.Profinite.Projective

Profinite.projectivePresentationdefMathlib.Topology.Category.Profinite.Projective, function or constant
Wording
the projective presentation of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the projective presentation of $X$ is a projective presentation of $X$.

Mathlib.Topology.Category.Sequential

SequentialstructureMathlib.Topology.Category.Sequential, type
Wording
no wording
English
The elements of $\mathrm{Sequential}$ are a basic type.
Sequential.fullyFaithfulSequentialToTopdefMathlib.Topology.Category.Sequential, function or constant
Wording
no wording
English
$\operatorname{fullyFaithfulSequentialToTop}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{sequentialToTop}$ defined as the induced functor of $\operatorname{toTop}$.
Sequential.homeoOfIsodefMathlib.Topology.Category.Sequential, function or constant
Wording
the homeomorphism of f (from the name)
English
Let $f$ be an isomorphism of $X$ and $Y$. Then the homeomorphism of $f$ is a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$.
Sequential.isoEquivHomeodefMathlib.Topology.Category.Sequential, function or constant
Wording
the isomorphism equivalence homeomorphism (from the name)
English
The isomorphism equivalence homeomorphism is an equivalence from the set of isomorphisms of $X$ and $Y$ to the set of homeomorphisms of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$.
Sequential.isoOfHomeodefMathlib.Topology.Category.Sequential, function or constant
Wording
the isomorphism of f (from the name)
English
Let $f$ be a homeomorphism of the set of carriers of the underlying topological space of $X$ and the set of carriers of the underlying topological space of $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$.
Sequential.ofdefMathlib.Topology.Category.Sequential, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{Sequential}$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$.
Sequential.sequentialToTopdefMathlib.Topology.Category.Sequential, function or constant
Wording
no wording
English
$\operatorname{sequentialToTop}$ is a functor of $\mathrm{Sequential}$ and the set of topological categories defined as the induced functor of $\operatorname{toTop}$.
Sequential.toTopdefMathlib.Topology.Category.Sequential, function or constant
Wording
the underlying topological space of self (from the docstring)
English
Let $\mathrm{self}$ be an element of $\mathrm{Sequential}$. Then the underlying topological space of $\mathrm{self}$ is a topological category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Topology.Category.Stonean.Adjunctions

Stonean.stoneCechAdjunctiondefMathlib.Topology.Category.Stonean.Adjunctions, function or constant
Wording
the Stone Cech adjunction (from the name)
English
The Stone Cech adjunction is an adjunction of $\mathrm{typeToStonean}$ and the forgetful functor of $\mathrm{Stonean}$.
Stonean.stoneCechEquivalencedefMathlib.Topology.Category.Stonean.Adjunctions, function or constant
Wording
the Stone Cech equivalence of X and Y (from the name)
English
Let $X$ be a set. Let $Y$ be an element of $\mathrm{Stonean}$. Then the Stone Cech equivalence of $X$ and $Y$ is an equivalence from the set of homomorphisms of the Stone Cech object of $X$ and $Y$ to the set of homomorphisms of $X$ and the set of carriers of the underlying topological space of $Y$ defined as the composition of the equivalence of $\operatorname{fullyFaithfulToCompHaus}$ and the composition of the Stone Cech equivalence of $\operatorname{of}$ applied to $X$ and the action of $\operatorname{toCompHaus}$ and $Y$ and the homomorphism equivalence of $X$ and the action of $\mathrm{compHausToTop}$ and the action of $\operatorname{toCompHaus}$ and $Y$.
Stonean.stoneCechObjdefMathlib.Topology.Category.Stonean.Adjunctions, function or constant
Wording
the Stone Cech object of X (from the name)
English
Let $X$ be a set. Then the Stone Cech object of $X$ is an element of $\mathrm{Stonean}$ defined as $\operatorname{of}$ applied to the set of Stone Ceches of $X$.
typeToStoneandefMathlib.Topology.Category.Stonean.Adjunctions, function or constant
Wording
no wording
English
$\mathrm{typeToStonean}$ is a functor of the set of sets and $\mathrm{Stonean}$.

Mathlib.Topology.Category.Stonean.Basic

CompHaus.liftdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the lift of e and f (from the name)
English
Let $e$ be a homomorphism of $\operatorname{compHaus}$ applied to $Z$ and $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the lift of $e$ and $f$ is a homomorphism of $\operatorname{compHaus}$ applied to $Z$ and $X$ defined as $\operatorname{factorThru}$ applied to $e$ and $f$.
CompHaus.presentationdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the presentation of X (from the name)
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then the presentation of $X$ is an element of $\mathrm{Stonean}$.
CompHaus.presentation.πdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the projection of X (from the name)
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then the projection of $X$ is a homomorphism of the action of $\operatorname{toCompHaus}$ and the presentation of $X$ and $X$ defined as $\operatorname{f}$ applied to the projective presentation of $X$.
CompHaus.toStoneandefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then $\operatorname{toStonean}$ applied to $X$ is an element of $\mathrm{Stonean}$.
Profinite.liftdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the lift of e and f (from the name)
English
Let $e$ be a homomorphism of the action of $\operatorname{toProfinite}$ and $Z$ and $Y$. Let $f$ be a homomorphism of $X$ and $Y$. Then the lift of $e$ and $f$ is a homomorphism of the action of $\operatorname{toProfinite}$ and $Z$ and $X$ defined as $\operatorname{factorThru}$ applied to $e$ and $f$.
Profinite.presentationdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the presentation of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the presentation of $X$ is an element of $\mathrm{Stonean}$.
Profinite.presentation.πdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
the projection of X (from the name)
English
Let $X$ be an element of $\mathrm{Profinite}$. Then the projection of $X$ is a homomorphism of the action of $\operatorname{toProfinite}$ and the presentation of $X$ and $X$ defined as the homomorphism of the homomorphism of $\operatorname{f}$ applied to the projective presentation of the action of $\mathrm{profiniteToCompHaus}$ and $X$.
StoneandefMathlib.Topology.Category.Stonean.Basic, type
Wording
no wording
English
generation took over the time limit
Stonean.compHausdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{Stonean}$. Then $\operatorname{compHaus}$ applied to $X$ is an element of $\mathrm{CompHaus}$ defined as the action of $\operatorname{toCompHaus}$ and $X$.
Stonean.fullyFaithfulToCompHausdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
$\operatorname{fullyFaithfulToCompHaus}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{toCompHaus}$.
Stonean.mkFinitedefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
Let $X$ be a set. Then $\operatorname{mkFinite}$ applied to $X$ is an element of $\mathrm{Stonean}$.
Stonean.ofdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
generation took over the time limit
Stonean.toCompHausdefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
generation took over the time limit
Stonean.toProfinitedefMathlib.Topology.Category.Stonean.Basic, function or constant
Wording
no wording
English
$\operatorname{toProfinite}$ is a functor of $\mathrm{Stonean}$ and $\mathrm{Profinite}$.

Mathlib.Topology.Category.Stonean.EffectiveEpi

Stonean.stoneanToCompHausEffectivePresentationdefMathlib.Topology.Category.Stonean.EffectiveEpi, function or constant
Wording
no wording
English
Let $X$ be an element of $\mathrm{CompHaus}$. Then $\operatorname{stoneanToCompHausEffectivePresentation}$ applied to $X$ is an effective presentation of $\operatorname{toCompHaus}$ and $X$.

Mathlib.Topology.Category.TopCat.Adjunctions

TopCat.adj₁defMathlib.Topology.Category.TopCat.Adjunctions, function or constant
Wording
the adjoint (from the name)
English
The adjoint is an adjunction of the discrete topology and the forgetful functor of the set of topological categories.
TopCat.adj₂defMathlib.Topology.Category.TopCat.Adjunctions, function or constant
Wording
the adjoint (from the name)
English
The adjoint is an adjunction of the forgetful functor of the set of topological categories and the trivial topology.

Mathlib.Topology.Category.TopCat.Basic

TopCatstructureMathlib.Topology.Category.TopCat.Basic, type
Wording
topological category (from the name)
English
The topological categories are a basic type.
TopCat.HomstructureMathlib.Topology.Category.TopCat.Basic, type
Wording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be topological categories. Then the homomorphisms of $X$ and $Y$ are a basic type.
TopCat.Hom.equivContinuousMapdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the equivalence continuous map of X and Y (from the name)
English
Let $X$ and $Y$ be topological categories. Then the equivalence continuous map of $X$ and $Y$ is an equivalence from the set of homomorphisms of $X$ and $Y$ to the set of continuous maps of the set of carriers of $X$ and the set of carriers of $Y$.
TopCat.Hom.homdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a continuous map of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
TopCat.Hom.hom'defMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a continuous map of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopCat.carrierdefMathlib.Topology.Category.TopCat.Basic, type
Wording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a topological category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopCat.constdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the constant morphism of y (from the docstring)
English
Let $y$ be a carrier of $Y$. Then the constant morphism of $y$ is a homomorphism of $X$ and $Y$.
TopCat.discretedefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the discrete topology (from the docstring)
English
The discrete topology is a functor of the set of sets and the set of topological categories.
TopCat.homeoOfIsodefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the homeomorphism of f (from the name)
English
Let $f$ be an isomorphism of $X$ and $Y$. Then the homeomorphism of $f$ is a homeomorphism of the set of carriers of $X$ and the set of carriers of $Y$.
TopCat.isEmbeddingdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
no wording
English
There is a morphism property of the set of topological categories. Proof. Let $A$ be arbitrary. Let $X$ be arbitrary. Let $f$ be arbitrary. By f. By TopCat__Hom__hom. By DFunLike__coe. By Topology__IsEmbedding.
TopCat.isoOfHomeodefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the isomorphism of f (from the name)
English
Let $f$ be a homeomorphism of the set of carriers of $X$ and the set of carriers of $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$.
TopCat.ofHomdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the topological category of f (from the name)
English
Let $f$ be a continuous map of $X$ and $Y$. Then the topological category of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
TopCat.trivialdefMathlib.Topology.Category.TopCat.Basic, function or constant
Wording
the trivial topology (from the docstring)
English
The trivial topology is a functor of the set of sets and the set of topological categories.

Mathlib.Topology.Category.TopCat.GrothendieckTopology

TopCat.grothendieckTopologydefMathlib.Topology.Category.TopCat.GrothendieckTopology, function or constant
Wording
the Grothendieck topology (from the name)
English
The Grothendieck topology is a Grothendieck topology of the set of topological categories defined as $\operatorname{toGrothendieck}$ applied to the precoverage.
TopCat.isOpenEmbeddingdefMathlib.Topology.Category.TopCat.GrothendieckTopology, function or constant
Wording
no wording
English
There is a morphism property of the set of topological categories. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. Let $f$ be arbitrary. By f. By CategoryTheory__ConcreteCategory__hom. By DFunLike__coe. By Topology__IsOpenEmbedding.
TopCat.precoveragedefMathlib.Topology.Category.TopCat.GrothendieckTopology, function or constant
Wording
the precoverage (from the name)
English
generation took over the time limit

Mathlib.Topology.Category.TopCat.Limits.Basic

TopCat.coconeOfCoconeForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
the cocone of c (from the name)
English
Let $c$ be a cocone of the composition of $F$ and the forgetful functor of the set of topological categories. Then the cocone of $c$ is a cocone of $F$.
TopCat.coconePtOfCoconeForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, type
Wording
no wording
English
Let $c$ be a cocone of the composition of $F$ and the forgetful functor of the set of topological categories. Then an element of $\operatorname{coconePtOfCoconeForget}$ applied to $c$ is an element of the function that maps $c$ to $\operatorname{pt}$ applied to $c$.
TopCat.coneOfConeForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
the cone of c (from the name)
English
Let $c$ be a cone of the composition of $F$ and the forgetful functor of the set of topological categories. Then the cone of $c$ is a cone of $F$.
TopCat.conePtOfConeForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, type
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and the forgetful functor of the set of topological categories. Then an element of $\operatorname{conePtOfConeForget}$ applied to $c$ is an element of the function that maps $c$ to $\operatorname{pt}$ applied to $c$.
TopCat.initialIsoPEmptydefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
no wording
English
$\operatorname{initialIsoPEmpty}$ is an isomorphism of $\operatorname{initial}$ applied to the set of topological categories and $\operatorname{of}$ applied to $\mathrm{PEmpty}$ defined as $\operatorname{uniqueUpToIso}$ applied to $\operatorname{initialIsInitial}$ and $\operatorname{isInitialPEmpty}$.
TopCat.isColimitCoconeOfForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
no wording
English
Let $c$ be a cocone of the composition of $F$ and the forgetful functor of the set of topological categories. Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCoconeOfForget}$ applied to $c$ and $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $c$.
TopCat.isInitialPEmptydefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
no wording
English
$\operatorname{isInitialPEmpty}$ is an element of $\operatorname{IsInitial}$ applied to $\operatorname{of}$ applied to $\mathrm{PEmpty}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $\mathrm{PEmpty}$.
TopCat.isLimitConeOfForgetdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
no wording
English
Let $c$ be a cone of the composition of $F$ and the forgetful functor of the set of topological categories. Let $\mathrm{hc}$ be an element of $\operatorname{IsLimit}$ applied to $c$. Then $\operatorname{isLimitConeOfForget}$ applied to $c$ and $\mathrm{hc}$ is an element of $\operatorname{IsLimit}$ applied to the cone of $c$.
TopCat.isTerminalPUnitdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
no wording
English
$\operatorname{isTerminalPUnit}$ is an element of $\operatorname{IsTerminal}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{of}$ applied to $\mathrm{PUnit}$.
TopCat.limitConedefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
the limit cone of F (from the name)
English
Let $F$ be a functor of $J$ and the set of topological categories. Then the limit cone of $F$ is a cone of $F$.
TopCat.limitConeIsLimitdefMathlib.Topology.Category.TopCat.Limits.Basic, function or constant
Wording
the chosen cone of F (from the docstring)
English
Let $F$ be a functor of $J$ and the set of topological categories. Then the chosen cone of $F$ is an element of $\operatorname{IsLimit}$ applied to the limit cone of $F$.

Mathlib.Topology.Category.TopCat.Limits.Konig

TopCat.partialSectionsdefMathlib.Topology.Category.TopCat.Limits.Konig, function or constant
Wording
the partial section of F and H (from the name)
English
Let $F$ be a functor of $J$ and the set of topological categories. Let $H$ be a finite set of $\mathrm{\_private\_\_Mathlib\_\_Topology\_\_Category\_\_TopCat\_\_Limits\_\_Konig\_\_0\_\_TopCat\_\_FiniteDiagramArrow}$ applied to $G$. Then the partial section of $F$ and $H$ is an element of the power set of the set of functions from elements $j$ of $J$ to carriers of the action of $F$ and $j$.

Mathlib.Topology.Category.TopCat.Limits.Products

TopCat.binaryCofandefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the binary cofan of X and Y (from the name)
English
Let $X$ and $Y$ be topological categories. Then the binary cofan of $X$ and $Y$ is a binary cofan of $X$ and $Y$.
TopCat.binaryCofanIsColimitdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $X$ and $Y$ be topological categories. Then $\operatorname{binaryCofanIsColimit}$ applied to $X$ and $Y$ is an element of $\operatorname{IsColimit}$ applied to the binary cofan of $X$ and $Y$.
TopCat.piFandefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then $\operatorname{piFan}$ applied to $x_{1}$ is an element of $\operatorname{Fan}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to the set of functions from elements $i$ of $x$ to carriers of $x_{1}$ applied to $i$ and $\mathrm{TopCat\_\_pi\_u3c0\_}$ applied to $x_{1}$.
TopCat.piFanIsLimitdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then $\operatorname{piFanIsLimit}$ applied to $x_{1}$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{piFan}$ applied to $x_{1}$.
TopCat.piIsoPidefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the product of x1 (from the docstring)
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then the product of $x_{1}$ is an isomorphism of the product object of $x_{1}$ and $\operatorname{of}$ applied to the set of functions from elements $i$ of $x$ to carriers of $x_{1}$ applied to $i$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the functor of $x_{1}$ and $\operatorname{piFanIsLimit}$ applied to $x_{1}$.
TopCat.piπdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the projection from the product of x1 and i (from the docstring)
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Let $i$ be an element of $x$. Then the projection from the product of $x_{1}$ and $i$ is a homomorphism of $\operatorname{of}$ applied to the set of functions from elements $i_{1}$ of $x$ to carriers of $x_{1}$ applied to $i_{1}$ and $x_{1}$ applied to $i$.
TopCat.prodBinaryFandefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $X$ and $Y$ be topological categories. Then $\operatorname{prodBinaryFan}$ applied to $X$ and $Y$ is an element of $\operatorname{BinaryFan}$ applied to $X$ and $Y$ defined as $\operatorname{mk}$ applied to the first projection from the product and the second projection from the product.
TopCat.prodBinaryFanIsLimitdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $X$ and $Y$ be topological categories. Then $\operatorname{prodBinaryFanIsLimit}$ applied to $X$ and $Y$ is an element of $\operatorname{IsLimit}$ applied to $\operatorname{prodBinaryFan}$ applied to $X$ and $Y$.
TopCat.prodFstdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the first projection from the product (from the docstring)
English
The first projection from the product is a homomorphism of $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $X$ and the set of carriers of $Y$ and $X$.
TopCat.prodIsoProddefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the product isomorphism product of X and Y (from the name)
English
Let $X$ and $Y$ be topological categories. Then the product isomorphism product of $X$ and $Y$ is an isomorphism of the product of $X$ and $Y$ and $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the pair of $X$ and $Y$ and $\operatorname{prodBinaryFanIsLimit}$ applied to $X$ and $Y$.
TopCat.prodSnddefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the second projection from the product (from the docstring)
English
The second projection from the product is a homomorphism of $\operatorname{of}$ applied to $\mathrm{Prod}$ applied to the set of carriers of $X$ and the set of carriers of $Y$ and $Y$.
TopCat.sigmaCofandefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the explicit cofan of x1 (from the docstring)
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then the explicit cofan of $x_{1}$ is a cofan of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $\Sigma$ applied to the function that maps $i$ to the set of carriers of $x_{1}$ applied to $i$ and $\mathrm{TopCat\_\_sigma\_u3b9\_}$ applied to $x_{1}$.
TopCat.sigmaCofanIsColimitdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
no wording
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then $\operatorname{sigmaCofanIsColimit}$ applied to $x_{1}$ is an element of $\operatorname{IsColimit}$ applied to the explicit cofan of $x_{1}$.
TopCat.sigmaIsoSigmadefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the sigma isomorphism sigma of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Then the sigma isomorphism sigma of $x_{1}$ is an isomorphism of the sigma object of $x_{1}$ and $\operatorname{of}$ applied to $\Sigma$ applied to the function that maps $i$ to the set of carriers of $x_{1}$ applied to $i$ defined as $\operatorname{coconePointUniqueUpToIso}$ applied to $\operatorname{isColimit}$ applied to the functor of $x_{1}$ and $\operatorname{sigmaCofanIsColimit}$ applied to $x_{1}$.
TopCat.sigmaιdefMathlib.Topology.Category.TopCat.Limits.Products, function or constant
Wording
the inclusion to the coproduct of x1 and i (from the docstring)
English
Let $x_{1}$ be a function from elements of $x$ to topological categories. Let $i$ be an element of $x$. Then the inclusion to the coproduct of $x_{1}$ and $i$ is a homomorphism of $x_{1}$ applied to $i$ and $\operatorname{of}$ applied to $\Sigma$ applied to the function that maps $i_{1}$ to the set of carriers of $x_{1}$ applied to $i_{1}$.

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

TopCat.pullbackConedefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
the pullback cone of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.
TopCat.pullbackConeIsLimitdefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then $\operatorname{pullbackConeIsLimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$.
TopCat.pullbackFstdefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
the first projection from the pullback of f and g (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the first projection from the pullback of $f$ and $g$ is a homomorphism of $\operatorname{of}$ applied to $\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {p})}{\operatorname{hom} (g , \ProdsndMACRoAA {p})})}$ and $X$.
TopCat.pullbackHomeoPreimagedefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
the pullback homeomorphism preimage of f and g (from the name)
English
Let $f$ be a continuous function from elements of $X$ to elements of $Z$. Let $g$ be a function from elements of $Y$ to elements of $Z$ such that $g$ is an embedding. Then the pullback homeomorphism preimage of $f$ and $g$ is a homeomorphism of $\SubtypeSet {p}{(\EqtMACRoH {f (\ProdfstMACRoZ {p})}{g (\ProdsndMACRoAA {p})})}$ and the set of elements of the preimage of $f$ and the range of $g$.
TopCat.pullbackIsoProdSubtypedefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
the pullback isomorphism product subtype of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback isomorphism product subtype of $f$ and $g$ is an isomorphism of the pullback of $f$ and $g$ and $\operatorname{of}$ applied to $\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {p})}{\operatorname{hom} (g , \ProdsndMACRoAA {p})})}$ defined as $\operatorname{conePointUniqueUpToIso}$ applied to $\operatorname{isLimit}$ applied to the cospan of $f$ and $g$ and $\operatorname{pullbackConeIsLimit}$ applied to $f$ and $g$.
TopCat.pullbackSnddefMathlib.Topology.Category.TopCat.Limits.Pullbacks, function or constant
Wording
the second projection from the pullback of f and g (from the docstring)
English
Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the second projection from the pullback of $f$ and $g$ is a homomorphism of $\operatorname{of}$ applied to $\SubtypeSet {p}{(\EqtMACRoH {\operatorname{hom} (f , \ProdfstMACRoZ {p})}{\operatorname{hom} (g , \ProdsndMACRoAA {p})})}$ and $Y$.

Mathlib.Topology.Category.TopCat.Monoidal

TopCat.IdefMathlib.Topology.Category.TopCat.Monoidal, function or constant
Wording
no wording
English
$\operatorname{I}$ is a topological category defined as $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the unit interval.
TopCat.I.homeomorphdefMathlib.Topology.Category.TopCat.Monoidal, function or constant
Wording
the homeomorphism (from the name)
English
The homeomorphism is a homeomorphism of the set of carriers of $\operatorname{I}$ and the set of elements of the unit interval defined as the lift.
TopCat.I.symmdefMathlib.Topology.Category.TopCat.Monoidal, function or constant
Wording
the inverse (from the name)
English
The inverse is a homomorphism of $\operatorname{I}$ and $\operatorname{I}$.
TopCat.ι₀defMathlib.Topology.Category.TopCat.Monoidal, function or constant
Wording
the inclusion (from the docstring)
English
The inclusion is a homomorphism of $X$ and the tensor object of $X$ and $\operatorname{I}$ defined as the lift of the identity morphism of $X$ and the constant morphism of $0$.
TopCat.ι₁defMathlib.Topology.Category.TopCat.Monoidal, function or constant
Wording
the inclusion (from the docstring)
English
The inclusion is a homomorphism of $X$ and the tensor object of $X$ and $\operatorname{I}$ defined as the lift of the identity morphism of $X$ and the constant morphism of $1$.

Mathlib.Topology.Category.TopCat.OpenNhds

IsOpenMap.adjunctionNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the adjunction neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Let $x$ be a carrier of $X$. Then the adjunction neighbourhood filter of $h$ and $x$ is an adjunction of the functor neighbourhood filter of $h$ and $x$ and the map of $f$ and $x$.
IsOpenMap.functorNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the functor neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Let $x$ be a carrier of $X$. Then the functor neighbourhood filter of $h$ and $x$ is a functor of the set of open neighbourhood filters of $x$ and the set of open neighbourhood filters of $\operatorname{hom}$ applied to $f$ and $x$.
TopologicalSpace.OpenNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, type
Wording
open neighbourhood filter of x (from the name)
English
Let $x$ be a carrier of $X$. Then an open neighbourhood filter of $x$ is an element of the function that maps $x$ to $\SubtypeSet {U}{(\MembershipmemMACRoT {U}{x})}$.
TopologicalSpace.OpenNhds.inclusiondefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the inclusion of x (from the name)
English
Let $x$ be a carrier of $X$. Then the inclusion of $x$ is a functor of the set of open neighbourhood filters of $x$ and the set of opens of the set of carriers of $X$.
TopologicalSpace.OpenNhds.inclusionMapIsodefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the inclusion map isomorphism of f and x (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of $X$. Then the inclusion map isomorphism of $f$ and $x$ is an isomorphism of the composition of the inclusion of $\operatorname{hom}$ applied to $f$ and $x$ and the map of $f$ and the composition of the map of $f$ and $x$ and the inclusion of $x$.
TopologicalSpace.OpenNhds.infLELeftdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
no wording
English
Let $U$ and $V$ be open neighbourhood filters of $x$. Then $\operatorname{infLELeft}$ applied to $U$ and $V$ is a homomorphism of $\MinminMACRoAG {U}{V}$ and $U$.
TopologicalSpace.OpenNhds.infLERightdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
no wording
English
Let $U$ and $V$ be open neighbourhood filters of $x$. Then $\operatorname{infLERight}$ applied to $U$ and $V$ is a homomorphism of $\MinminMACRoAG {U}{V}$ and $V$.
TopologicalSpace.OpenNhds.mapdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the map of f and x (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of $X$. Then the map of $f$ and $x$ is a functor of the set of open neighbourhood filters of $\operatorname{hom}$ applied to $f$ and $x$ and the set of open neighbourhood filters of $x$.
Topology.IsInducing.adjunctionNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the adjunction neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Let $x$ be a carrier of $X$. Then the adjunction neighbourhood filter of $h$ and $x$ is an adjunction of the map of $f$ and $x$ and the functor neighbourhood filter of $h$ and $x$.
Topology.IsInducing.functorNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the functor neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Let $x$ be a carrier of $X$. Then the functor neighbourhood filter of $h$ and $x$ is a functor of the set of open neighbourhood filters of $x$ and the set of open neighbourhood filters of $\operatorname{hom}$ applied to $f$ and $x$.
Topology.IsOpenEmbedding.adjunctionNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the adjunction neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Let $x$ be a carrier of $X$. Then the adjunction neighbourhood filter of $h$ and $x$ is an adjunction of the functor neighbourhood filter of $\operatorname{isOpenMap}$ applied to $h$ and $x$ and the map of $f$ and $x$.
Topology.IsOpenEmbedding.functorNhdsdefMathlib.Topology.Category.TopCat.OpenNhds, function or constant
Wording
the functor neighbourhood filter of h and x (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Let $x$ be a carrier of $X$. Then the functor neighbourhood filter of $h$ and $x$ is a functor of the set of open neighbourhood filters of $x$ and the set of open neighbourhood filters of $\operatorname{hom}$ applied to $f$ and $x$.

Mathlib.Topology.Category.TopCat.Opens

IsOpenMap.adjunctiondefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the adjunction of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Then the adjunction of $\mathrm{hf}$ is an adjunction of the functor of $\mathrm{hf}$ and the map of $f$.
IsOpenMap.functordefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the functor of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Then the functor of $\mathrm{hf}$ is a functor of the set of opens of the set of carriers of $X$ and the set of opens of the set of carriers of $Y$.
IsOpenMap.functorMapdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the functor map of HV and le (from the name)
English
Assume that the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $U$ is open. Assume that the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $V$ is open. Assume that $U \leq V$. Then the functor map of $\mathrm{HV}$ and $\mathrm{le}$ is a homomorphism of $\operatorname{mk}$ applied to the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $U$ and $\mathrm{HU}$ and $\operatorname{mk}$ applied to the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $V$ and $\mathrm{HV}$.
TopCat.Hom.frameHomdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the frame homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the frame homomorphism of $f$ is a frame homomorphism of the set of opens of the set of carriers of $Y$ and the set of opens of the set of carriers of $X$.
TopologicalSpace.Opens.botLEdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $U$ be an open of the set of carriers of $X$. Then $\operatorname{botLE}$ applied to $U$ is a homomorphism of the bottom and $U$.
TopologicalSpace.Opens.inclusion'defMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the inclusion of U (from the name)
English
Let $U$ be an open of the set of carriers of $X$. Then the inclusion of $U$ is a homomorphism of the action of the topological category of $X$ and $U$ and $X$.
TopologicalSpace.Opens.inclusionTopIsodefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the inclusion top isomorphism of X (from the name)
English
Let $X$ be a topological category. Then the inclusion top isomorphism of $X$ is an isomorphism of the action of the topological category of $X$ and the top and $X$.
TopologicalSpace.Opens.infLELeftdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $U$ and $V$ be opens of the set of carriers of $X$. Then $\operatorname{infLELeft}$ applied to $U$ and $V$ is a homomorphism of $\MinminMACRoAG {U}{V}$ and $U$.
TopologicalSpace.Opens.infLERightdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $U$ and $V$ be opens of the set of carriers of $X$. Then $\operatorname{infLERight}$ applied to $U$ and $V$ is a homomorphism of $\MinminMACRoAG {U}{V}$ and $V$.
TopologicalSpace.Opens.leMapTopdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of the set of carriers of $X$. Then $\operatorname{leMapTop}$ applied to $f$ and $U$ is a homomorphism of $U$ and the action of the map of $f$ and the top defined as $\operatorname{leTop}$ applied to $U$.
TopologicalSpace.Opens.leSuprdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Let $i$ be an element of $x$. Then $\operatorname{leSupr}$ applied to $U$ and $i$ is a homomorphism of $U$ applied to $i$ and the supremum of $U$.
TopologicalSpace.Opens.leTopdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Let $U$ be an open of the set of carriers of $X$. Then $\operatorname{leTop}$ applied to $U$ is a homomorphism of $U$ and the top.
TopologicalSpace.Opens.mapdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the map of $f$ is a functor of the set of opens of the set of carriers of $Y$ and the set of opens of the set of carriers of $X$ defined as the functor of the order homomorphism of the frame homomorphism of $f$.
TopologicalSpace.Opens.mapCompdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the map composition of f and g (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the map composition of $f$ and $g$ is an isomorphism of the map of the composition of $f$ and $g$ and the composition of the map of $g$ and the map of $f$.
TopologicalSpace.Opens.mapIddefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the map identity of X (from the name)
English
Let $X$ be a topological category. Then the map identity of $X$ is an isomorphism of the map of the identity morphism of $X$ and the identity of the set of opens of the set of carriers of $X$.
TopologicalSpace.Opens.mapIsodefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the map isomorphism of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $X$ and $Y$ such that $\EqtMACRoH {f}{g}$. Then the map isomorphism of $f$ and $g$ is an isomorphism of the map of $f$ and the map of $g$.
TopologicalSpace.Opens.mapMapIsodefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the map map isomorphism of H (from the name)
English
Let $H$ be an isomorphism of $X$ and $Y$. Then the map map isomorphism of $H$ is an equivalence of the set of opens of the set of carriers of $Y$ and the set of opens of the set of carriers of $X$ defined as the inverse of the equivalence of the open congruence of the homeomorphism of $H$.
TopologicalSpace.Opens.toTopCatdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the topological category of X (from the name)
English
Let $X$ be a topological category. Then the topological category of $X$ is a functor of the set of opens of the set of carriers of $X$ and the set of topological categories.
Topology.IsInducing.adjunctiondefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the adjunction of hf (from the name)
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the adjunction of $\mathrm{hf}$ is an adjunction of the map of $f$ and the functor of $\mathrm{hf}$.
Topology.IsInducing.functordefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the functor of hf (from the name)
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then the functor of $\mathrm{hf}$ is a functor of the set of opens of the set of carriers of $X$ and the set of opens of the set of carriers of $Y$.
Topology.IsInducing.functorObjdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the functor object of h and U (from the name)
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Let $U$ be an open of the set of carriers of $X$. Then the functor object of $h$ and $U$ is an open of the set of carriers of $Y$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that the action of the map of $f$ and $s$ is equal to $U$.
Topology.IsInducing.opensGIdefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
no wording
English
Assume that $\operatorname{IsInducing}$ holds for $\operatorname{coe}$ applied to the homomorphism of $f$. Then $\operatorname{opensGI}$ applied to $\mathrm{hf}$ is a Galois insertion of $\operatorname{obj}$ applied to the map of $f$ and $\operatorname{functorObj}$ applied to $\mathrm{hf}$.
Topology.IsOpenEmbedding.functordefMathlib.Topology.Category.TopCat.Opens, function or constant
Wording
the functor of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the functor of $\mathrm{hf}$ is a functor of the set of opens of the set of carriers of $X$ and the set of opens of the set of carriers of $Y$.

Mathlib.Topology.Category.TopCat.Sphere

TopCat.balldefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the ball of n (from the name)
English
Let $n$ be a natural number. Then the ball of $n$ is a topological category defined as $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the ball of $0$ and $1$.
TopCat.ballInclusiondefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the inclusion of n (from the docstring)
English
Let $n$ be a natural number. Then the inclusion of $n$ is a homomorphism of the ball of $n$ and the disk of $n$.
TopCat.diskdefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the disk of n (from the name)
English
Let $n$ be a natural number. Then the disk of $n$ is a topological category defined as $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the closed ball of $0$ and $1$.
TopCat.diskBoundarydefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the disk boundary of n (from the name)
English
Let $n$ be a natural number. Then the disk boundary of $n$ is a topological category defined as $\operatorname{of}$ applied to $\mathrm{ULift}$ applied to the set of elements of the sphere of $0$ and $1$.
TopCat.diskBoundaryInclusiondefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the inclusion of n (from the docstring)
English
Let $n$ be a natural number. Then the inclusion of $n$ is a homomorphism of the disk boundary of $n$ and the disk of $n$.
TopCat.spheredefMathlib.Topology.Category.TopCat.Sphere, function or constant
Wording
the sphere of n (from the name)
English
Let $n$ be a natural number. Then the sphere of $n$ is a topological category defined as the disk boundary of $n + 1$.

Mathlib.Topology.Category.TopCat.ULift

TopCat.uliftFunctordefMathlib.Topology.Category.TopCat.ULift, function or constant
Wording
the lift functor (from the name)
English
The lift functor is a functor of the set of topological categories and the set of topological categories.
TopCat.uliftFunctorCompForgetIsodefMathlib.Topology.Category.TopCat.ULift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorCompForgetIso}$ is an isomorphism of the composition of the lift functor and the forgetful functor of the set of topological categories and the composition of the forgetful functor of the set of topological categories and the functor embedding defined as the identity of the composition of the lift functor and the forgetful functor of the set of topological categories.
TopCat.uliftFunctorFullyFaithfuldefMathlib.Topology.Category.TopCat.ULift, function or constant
Wording
no wording
English
$\operatorname{uliftFunctorFullyFaithful}$ is an element of $\operatorname{FullyFaithful}$ applied to the lift functor.
TopCat.uliftFunctorObjHomeodefMathlib.Topology.Category.TopCat.ULift, function or constant
Wording
the lift functor object homeomorphism of X (from the name)
English
Let $X$ be a topological category. Then the lift functor object homeomorphism of $X$ is a homeomorphism of the set of carriers of $X$ and the set of carriers of the action of the lift functor and $X$ defined as the inverse of the lift.

Mathlib.Topology.Category.TopCat.Yoneda

ContinuousMap.yonedaPresheafdefMathlib.Topology.Category.TopCat.Yoneda, function or constant
Wording
the Yoneda presheaf of F and Y (from the name)
English
Let $F$ be a functor of $C$ and the set of topological categories. Let $Y$ be a set. Then the Yoneda presheaf of $F$ and $Y$ is a functor of the set of opposites of $C$ and the set of sets.
ContinuousMap.yonedaPresheaf'defMathlib.Topology.Category.TopCat.Yoneda, function or constant
Wording
the Yoneda presheaf of Y (from the name)
English
Let $Y$ be a set. Then the Yoneda presheaf of $Y$ is a functor of the set of opposites of the set of topological categories and the set of sets.

Mathlib.Topology.Category.TopCommRingCat

TopCommRingCatstructureMathlib.Topology.Category.TopCommRingCat, type
Wording
top commutative ring category (from the name)
English
The top commutative ring categories are a basic type.
TopCommRingCat.αdefMathlib.Topology.Category.TopCommRingCat, type
Wording
no wording
English
Let $\mathrm{self}$ be a top commutative ring category. Then an element of $\mathrm{TopCommRingCat\_\_\_u3b1\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

‹ previous next ›