OpenPartialHomeomorph.EqOnSourcedefMathlib.Topology.OpenPartialHomeomorph.IsImage, predicateEnglish
Let $e$ and $\mathrm{e'}$ be open partial homeomorphisms of $X$ and $Y$. Then $\operatorname{EqOnSource}$ holds for $e$ and $\mathrm{e'}$, if the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ is equal to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $\mathrm{e'}$ and $\operatorname{EqOn}$ holds for $\operatorname{toFun'}$ applied to $e$, $\operatorname{toFun'}$ applied to $\mathrm{e'}$ and the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$.
OpenPartialHomeomorph.IsImagedefMathlib.Topology.OpenPartialHomeomorph.IsImage, predicateEnglish
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $s$ be an element of $\wp X$. Let $t$ be an element of $\wp Y$. Then $\operatorname{IsImage}$ holds for $e$, $s$ and $t$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$, then the function of $e$ and $x_{2}$ is an element of $t$, if and only if $x_{2}$ is an element of $s$.
OpenPartialHomeomorph.IsImage.restrdefMathlib.Topology.OpenPartialHomeomorph.IsImage, function or constantWording
the restriction of h and hs (from the name)
English
Assume that $\operatorname{IsImage}$ holds for $e$, $s$ and $t$. Assume that $\operatorname{inter}$ applied to the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $s$ is open. Then the restriction of $h$ and $\mathrm{hs}$ is an open partial homeomorphism of $X$ and $Y$.
OpenPartialHomeomorph.ofSetdefMathlib.Topology.OpenPartialHomeomorph.IsImage, function or constantWording
the open partial homeomorphism of s and hs (from the name)
English
Let $s$ be an open element of $\wp X$. Then the open partial homeomorphism of $s$ and $\mathrm{hs}$ is an open partial homeomorphism of $X$ and $X$.
OpenPartialHomeomorph.restrdefMathlib.Topology.OpenPartialHomeomorph.IsImage, function or constantWording
the restriction of e and s (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $s$ be an element of $\wp X$. Then the restriction of $e$ and $s$ is an open partial homeomorphism of $X$ and $Y$ defined as the restriction open of $e$ and the interior of $s$.
OpenPartialHomeomorph.restrOpendefMathlib.Topology.OpenPartialHomeomorph.IsImage, function or constantWording
the restriction open of e and s (from the name)
English
Let $e$ be an open partial homeomorphism of $X$ and $Y$. Let $s$ be an open element of $\wp X$. Then the restriction open of $e$ and $s$ is an open partial homeomorphism of $X$ and $Y$.
DiscreteTopologyclassMathlib.Topology.Order, predicateWording
x is discrete (from the docstring)
English
Let $x$ be a set. Then we can say that $x$ is discrete.
IndiscreteTopologyclassMathlib.Topology.Order, predicateWording
x is indiscrete (from the docstring)
English
Let $x$ be a set. Then we can say that $x$ is indiscrete.
NontrivialTopologyclassMathlib.Topology.Order, predicateWording
x is nontrivial (from the docstring)
English
Let $x$ be a set. Then we can say that $x$ is nontrivial.
TopologicalSpace.GenerateOpeninductiveMathlib.Topology.Order, predicateEnglish
Let $g$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{GenerateOpen}$ holds for $g$ and $x_{1}$.
TopologicalSpace.GenerateOpen.belowinductiveMathlib.Topology.Order, predicateEnglish
Assume that $\operatorname{GenerateOpen}$ holds for $g$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
TopologicalSpace.gciGenerateFromdefMathlib.Topology.Order, function or constantEnglish
Let $x$ be a set. Then $\operatorname{gciGenerateFrom}$ applied to $x$ is a Galois coinsertion of the function that maps $t$ to $\operatorname{toDual}$ applied to $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is open and $\operatorname{comp}$ applied to $\operatorname{generateFrom}$ and $\operatorname{coe}$ applied to the order dual.
WithDiscreteTopologydefMathlib.Topology.Order, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{WithDiscreteTopology}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{WithTopology}$ applied to $x$ and the bottom.
OrderTopologyclassMathlib.Topology.Order.Basic, predicateWording
x is a order topology (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order topology.
IsOrderBornologyclassMathlib.Topology.Order.Bornology, predicateWording
x is a order bornology (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order bornology.
IsCadlagstructureMathlib.Topology.Order.Cadlag, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $\mathrm{IsCadlag}$ holds for $f$.
IsCagladstructureMathlib.Topology.Order.Cadlag, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $\mathrm{IsCaglad}$ holds for $f$.
IsLeftContinuousdefMathlib.Topology.Order.Cadlag, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{IsLeftContinuous}$ holds for $f$, if for all elements $a$ of $X$, $\mathrm{ContinuousWithinAt}$ holds for $f$, $\operatorname{Iio}$ applied to $a$ and $a$.
IsRightContinuousdefMathlib.Topology.Order.Cadlag, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $\mathrm{IsRightContinuous}$ holds for $f$, if for all elements $a$ of $X$, $\mathrm{ContinuousWithinAt}$ holds for $f$, $\operatorname{Ioi}$ applied to $a$ and $a$.
AlexDiscstructureMathlib.Topology.Order.Category.AlexDisc, typeEnglish
The elements of $\mathrm{AlexDisc}$ are a basic type.
AlexDisc.Iso.mkdefMathlib.Topology.Order.Category.AlexDisc, function or constantEnglish
Let $e$ be a homeomorphism of the set of carriers of $\operatorname{toTopCat}$ applied to $x$ and the set of carriers of $\operatorname{toTopCat}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
AlexDisc.ofdefMathlib.Topology.Order.Category.AlexDisc, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{AlexDisc}$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$.
alexDiscEquivPreorddefMathlib.Topology.Order.Category.AlexDisc, function or constantEnglish
$\mathrm{alexDiscEquivPreord}$ is an equivalence of $\mathrm{AlexDisc}$ and $\mathrm{Preord}$.
Locale.PTdefMathlib.Topology.Order.Category.FrameAdjunction, typeEnglish
Let $L$ be a set. Then an element of $\operatorname{PT}$ applied to $L$ is an element of the function that maps $L$ to the set of frame homomorphisms of $L$ and the set of propositions.
Locale.adjunctionTopToLocalePTdefMathlib.Topology.Order.Category.FrameAdjunction, function or constantEnglish
$\operatorname{adjunctionTopToLocalePT}$ is an adjunction of the top to locale and $\operatorname{pt}$.
Locale.counitAppContdefMathlib.Topology.Order.Category.FrameAdjunction, function or constantWording
the counit of L (from the docstring)
English
Let $L$ be a locale. Then the counit of $L$ is a frame homomorphism of the set of carriers of the opposite of $L$ and the set of opens of $\operatorname{PT}$ applied to the set of carriers of the opposite of $L$.
Locale.localePointOfSpacePointdefMathlib.Topology.Order.Category.FrameAdjunction, function or constantWording
the locale point of X and x1 (from the name)
English
Let $X$ be a set. Let $x_{1}$ be an element of $X$. Then the locale point of $X$ and $x_{1}$ is an element of $\operatorname{PT}$ applied to the set of opens of $X$.
Locale.openOfElementHomdefMathlib.Topology.Order.Category.FrameAdjunction, function or constantWording
the open of L (from the name)
English
Let $L$ be a set. Then the open of $L$ is a frame homomorphism of $L$ and $\wp \operatorname{PT} (L)$.
Locale.ptdefMathlib.Topology.Order.Category.FrameAdjunction, function or constantEnglish
$\operatorname{pt}$ is a functor of the set of locales and the set of topological categories.
CompactIccSpaceclassMathlib.Topology.Order.Compact, predicateWording
x is a compact closed interval space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a compact closed interval space.
Order.FilldefMathlib.Topology.Order.Completion, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{Fill}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {x_{2}}{\mathrm{and} (\mathrm{if} (\operatorname{IsSuccPrelimit} (\ProdfstMACRoZ {\operatorname{ofLex} (x_{2})}), \mathrm{Leq} (0 , \ProdsndMACRoAA {\operatorname{ofLex} (x_{2})})), \mathrm{if} (\operatorname{IsPredPrelimit} (\ProdfstMACRoZ {\operatorname{ofLex} (x_{2})}), \mathrm{Leq} (\ProdsndMACRoAA {\operatorname{ofLex} (x_{2})}, 0)))}$.
Order.Fill.somedefMathlib.Topology.Order.Completion, function or constantEnglish
$\operatorname{some}$ is an order embedding of $x$ and $\operatorname{Fill}$ applied to $x$.
ContinuousOrderHomstructureMathlib.Topology.Order.Hom.Basic, typeWording
continuous order homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the continuous order homomorphisms of $x$ and $x_{1}$ are a basic type.
ContinuousOrderHom.compdefMathlib.Topology.Order.Hom.Basic, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a continuous order homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a continuous order homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a continuous order homomorphism of $x$ and $x_{2}$.
ContinuousOrderHom.copydefMathlib.Topology.Order.Hom.Basic, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a continuous order homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a continuous order homomorphism of $x$ and $x_{1}$.
ContinuousOrderHom.iddefMathlib.Topology.Order.Hom.Basic, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a continuous order homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to the identity function and $\mathrm{continuous\_id}$.
ContinuousOrderHom.toContinuousMapdefMathlib.Topology.Order.Hom.Basic, function or constantWording
the continuous map of f (from the name)
English
Let $f$ be a continuous order homomorphism of $x$ and $x_{1}$. Then the continuous map of $f$ is a continuous map of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOrderHom}$ applied to $f$ and $\mathrm{ContinuousOrderHom\_\_continuous\_toFun}$ applied to $f$.
ContinuousOrderHomClassclassMathlib.Topology.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{ContinuousOrderHomClass}$ holds for $F$, $x$ and $x_{1}$.
ContinuousOrderHomClass.toContinuousOrderHomdefMathlib.Topology.Order.Hom.Basic, function or constantWording
the continuous order homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the continuous order homomorphism of $f$ is a continuous order homomorphism of $x$ and $x_{1}$.
EsakiaHomstructureMathlib.Topology.Order.Hom.Esakia, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{1}$ are a basic type.
EsakiaHom.compdefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an element of $\mathrm{EsakiaHom}$ applied to $x_{1}$ and $x_{2}$. Let $f$ be an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{1}$. Then the composition of $g$ and $f$ is an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{2}$.
EsakiaHom.copydefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{1}$.
EsakiaHom.iddefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x$.
EsakiaHom.toPseudoEpimorphismdefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the pseudo epimorphism of f (from the name)
English
Let $f$ be an element of $\mathrm{EsakiaHom}$ applied to $x$ and $x_{1}$. Then the pseudo epimorphism of $f$ is a pseudo epimorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toOrderHom}$ applied to $\operatorname{toContinuousOrderHom}$ applied to $f$ and $\mathrm{EsakiaHom\_\_exists\_map\_eq\_of\_map\_le'}$ applied to $f$.
EsakiaHomClassclassMathlib.Topology.Order.Hom.Esakia, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{EsakiaHomClass}$ holds for $F$, $x$ and $x_{1}$.
PseudoEpimorphismstructureMathlib.Topology.Order.Hom.Esakia, typeWording
pseudo epimorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the pseudo epimorphisms of $x$ and $x_{1}$ are a basic type.
PseudoEpimorphism.compdefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a pseudo epimorphism of $x_{1}$ and $x_{2}$. Let $f$ be a pseudo epimorphism of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is a pseudo epimorphism of $x$ and $x_{2}$.
PseudoEpimorphism.copydefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a pseudo epimorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a pseudo epimorphism of $x$ and $x_{1}$.
PseudoEpimorphism.iddefMathlib.Topology.Order.Hom.Esakia, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a pseudo epimorphism of $x$ and $x$.
PseudoEpimorphismClassclassMathlib.Topology.Order.Hom.Esakia, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{PseudoEpimorphismClass}$ holds for $F$, $x$ and $x_{1}$.
PrimitiveSpectrum.OrderGeneratesdefMathlib.Topology.Order.HullKernel, predicateEnglish
Let $T$ be an element of $\wp x$. Then $\operatorname{OrderGenerates}$ holds for $T$, if for all elements $a$ of $x$, there exists an element $S$ of the power set of the set of elements of $T$, such that $a$ is equal to the kernel of $S$.
PrimitiveSpectrum.gidefMathlib.Topology.Order.HullKernel, function or constantEnglish
Assume that $\operatorname{OrderGenerates}$ holds for $T$. Then $\operatorname{gi}$ applied to $\mathrm{hG}$ is a Galois insertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{kernel}$ and $\operatorname{comp}$ applied to $\operatorname{hull}$ applied to $T$ and $\operatorname{coe}$ applied to the order dual.
PrimitiveSpectrum.hulldefMathlib.Topology.Order.HullKernel, function or constantWording
the hull of T and a (from the name)
English
Let $T$ be an element of $\wp x$. Let $a$ be an element of $x$. Then the hull of $T$ and $a$ is an element of the power set of the set of elements of $T$ defined as the preimage of the function that maps $x_{2}$ to $\MembershipmemMACRoT {T}{x_{2}}$ and $\operatorname{Ici}$ applied to $a$.
PrimitiveSpectrum.kerneldefMathlib.Topology.Order.HullKernel, function or constantWording
the kernel of S (from the name)
English
Let $S$ be an element of the power set of the set of elements of $T$. Then the kernel of $S$ is an element of $x$ defined as the infimum of the image of the function that maps $x_{2}$ to $\MembershipmemMACRoT {T}{x_{2}}$ and $S$.
ContinuousInfclassMathlib.Topology.Order.Lattice, predicateWording
L is a continuous infimum (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a continuous infimum.
ContinuousSupclassMathlib.Topology.Order.Lattice, predicateWording
L is a continuous supremum (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a continuous supremum.
TopologicalLatticeclassMathlib.Topology.Order.Lattice, predicateWording
L is a topological lattice (from the name)
English
Let $L$ be a set. Then we can say that $L$ is a topological lattice.
Topology.IsLawsonclassMathlib.Topology.Order.LawsonTopology, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{IsLawson}$ holds for $x$.
Topology.IsLawson.lawsonBasisdefMathlib.Topology.Order.LawsonTopology, function or constantEnglish
Let $x$ be a set. Then $\operatorname{lawsonBasis}$ applied to $x$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exists an element $t$ of $\wp x$, such that $t$ is finite and there exists an element $u$ of $\wp x$ such that $u$ is open and $\operatorname{sdiff}$ applied to $u$ and the upper closure of $t$ is equal to $s$.
Topology.WithLawsondefMathlib.Topology.Order.LawsonTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithLawson}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithLawson.homeomorphdefMathlib.Topology.Order.LawsonTopology, function or constantWording
the homeomorphism (from the name)
English
The homeomorphism is a homeomorphism of $\operatorname{WithLawson}$ applied to $x$ and $x$.
Topology.WithLawson.ofLawsondefMathlib.Topology.Order.LawsonTopology, function or constantEnglish
$\operatorname{ofLawson}$ is an element of $\EquivMACRoAE {\operatorname{WithLawson} (x)}{x}$ defined as the identity of $\operatorname{WithLawson}$ applied to $x$.
Topology.WithLawson.toLawsondefMathlib.Topology.Order.LawsonTopology, function or constantEnglish
$\operatorname{toLawson}$ is an element of $\EquivMACRoAE {x}{\operatorname{WithLawson} (x)}$ defined as the identity of $x$.
Function.leftLimdefMathlib.Topology.Order.LeftRightLim, function or constantWording
the left limit of f and a (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then the left limit of $f$ and $a$ is an element of $x_{1}$ defined as $\iteMACRoG {\mathrm{or} (\EqtMACRoH {\mathrm{nhdsWithin} (a , \operatorname{Iio} (a))}{\operatorname{bot}}, \mathrm{not} (\mathrm{exists} (x_{1} , \lambda y . \operatorname{Tendsto} (f , \mathrm{nhdsWithin} (a , \operatorname{Iio} (a)), \mathrm{nhds} (y)))))}{f (a)}{\operatorname{limUnder} (\mathrm{nhdsWithin} (a , \operatorname{Iio} (a)), f)}$.
Function.rightLimdefMathlib.Topology.Order.LeftRightLim, function or constantWording
the right limit of f and a (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then the right limit of $f$ and $a$ is an element of $x_{1}$ defined as $\iteMACRoG {\mathrm{or} (\EqtMACRoH {\mathrm{nhdsWithin} (a , \operatorname{Ioi} (a))}{\operatorname{bot}}, \mathrm{not} (\mathrm{exists} (x_{1} , \lambda y . \operatorname{Tendsto} (f , \mathrm{nhdsWithin} (a , \operatorname{Ioi} (a)), \mathrm{nhds} (y)))))}{f (a)}{\operatorname{limUnder} (\mathrm{nhdsWithin} (a , \operatorname{Ioi} (a)), f)}$.
BoundedGENhdsClassclassMathlib.Topology.Order.LiminfLimsup, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{BoundedGENhdsClass}$ holds for $x$.
BoundedLENhdsClassclassMathlib.Topology.Order.LiminfLimsup, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{BoundedLENhdsClass}$ holds for $x$.
IsLocalExtrdefMathlib.Topology.Order.LocalExtr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then $\mathrm{IsLocalExtr}$ holds for $f$ and $a$, if $\mathrm{IsExtrFilter}$ holds for $f$, the neighbourhood filter of $a$ and $a$.
IsLocalExtrOndefMathlib.Topology.Order.LocalExtr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsLocalExtrOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsExtrFilter}$ holds for $f$, $\mathrm{nhdsWithin}$ applied to $a$ and $s$ and $a$.
IsLocalMaxdefMathlib.Topology.Order.LocalExtr, predicateWording
f is a local maximum with respect to a (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then $f$ is a local maximum with respect to $a$, if $\mathrm{IsMaxFilter}$ holds for $f$, the neighbourhood filter of $a$ and $a$.
IsLocalMaxOndefMathlib.Topology.Order.LocalExtr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsLocalMaxOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsMaxFilter}$ holds for $f$, $\mathrm{nhdsWithin}$ applied to $a$ and $s$ and $a$.
IsLocalMindefMathlib.Topology.Order.LocalExtr, predicateWording
f is a local minimum with respect to a (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $a$ be an element of $x$. Then $f$ is a local minimum with respect to $a$, if $\mathrm{IsMinFilter}$ holds for $f$, the neighbourhood filter of $a$ and $a$.
IsLocalMinOndefMathlib.Topology.Order.LocalExtr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsLocalMinOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsMinFilter}$ holds for $f$, $\mathrm{nhdsWithin}$ applied to $a$ and $s$ and $a$.
Topology.IsLowerclassMathlib.Topology.Order.LowerUpperTopology, predicateWording
x is lower (from the name)
English
Let $x$ be a set. Then we can say that $x$ is lower.
Topology.IsLower.lowerBasisdefMathlib.Topology.Order.LowerUpperTopology, function or constantWording
the lower basis of x (from the name)
English
Let $x$ be a set. Then the lower basis of $x$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exists an element $t$ of $\wp x$, such that $t$ is finite and the complement of the upper closure of $t$ is equal to $s$.
Topology.IsLower.withLowerHomeomorphdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{withLowerHomeomorph}$ is a homeomorphism of $\operatorname{WithLower}$ applied to $x$ and $x$.
Topology.IsUpperclassMathlib.Topology.Order.LowerUpperTopology, predicateWording
x is upper (from the name)
English
Let $x$ be a set. Then we can say that $x$ is upper.
Topology.IsUpper.upperBasisdefMathlib.Topology.Order.LowerUpperTopology, function or constantWording
the upper basis of x (from the name)
English
Let $x$ be a set. Then the upper basis of $x$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exists an element $t$ of $\wp x$, such that $t$ is finite and the complement of the lower closure of $t$ is equal to $s$.
Topology.IsUpper.withUpperHomeomorphdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{withUpperHomeomorph}$ is a homeomorphism of $\operatorname{WithUpper}$ applied to $x$ and $x$.
Topology.WithLowerdefMathlib.Topology.Order.LowerUpperTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithLower}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithLower.ofLowerdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{ofLower}$ is an element of $\EquivMACRoAE {\operatorname{WithLower} (x)}{x}$ defined as the identity of $\operatorname{WithLower}$ applied to $x$.
Topology.WithLower.toDualHomeomorphdefMathlib.Topology.Order.LowerUpperTopology, function or constantWording
the dual homeomorphism (from the name)
English
The dual homeomorphism is a homeomorphism of $\operatorname{WithLower}$ applied to $x$ and $\operatorname{WithUpper}$ applied to the set of order duals of $x$.
Topology.WithLower.toLowerdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{toLower}$ is an element of $\EquivMACRoAE {x}{\operatorname{WithLower} (x)}$ defined as the identity of $x$.
Topology.WithUpperdefMathlib.Topology.Order.LowerUpperTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithUpper}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithUpper.ofUpperdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{ofUpper}$ is an element of $\EquivMACRoAE {\operatorname{WithUpper} (x)}{x}$ defined as the identity of $\operatorname{WithUpper}$ applied to $x$.
Topology.WithUpper.toUpperdefMathlib.Topology.Order.LowerUpperTopology, function or constantEnglish
$\operatorname{toUpper}$ is an element of $\EquivMACRoAE {x}{\operatorname{WithUpper} (x)}$ defined as the identity of $x$.
OrderIso.toHomeomorphdefMathlib.Topology.Order.MonotoneContinuity, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the homeomorphism of $e$ is a homeomorphism of $x$ and $x_{1}$ defined as the homeomorphism of $e$.
InfConvergenceClassclassMathlib.Topology.Order.MonotoneConvergence, predicateWording
x is a infimum convergence class (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an infimum convergence class.
SupConvergenceClassclassMathlib.Topology.Order.MonotoneConvergence, predicateWording
x is a supremum convergence class (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a supremum convergence class.
ClosedIciTopologyclassMathlib.Topology.Order.OrderClosed, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{ClosedIciTopology}$ holds for $x$.
ClosedIicTopologyclassMathlib.Topology.Order.OrderClosed, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{ClosedIicTopology}$ holds for $x$.
OrderClosedTopologyclassMathlib.Topology.Order.OrderClosed, predicateWording
x is a order closed topology (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order closed topology.
PriestleySpaceclassMathlib.Topology.Order.Priestley, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{PriestleySpace}$ holds for $x$.
Topology.IsScottclassMathlib.Topology.Order.ScottTopology, predicateEnglish
Let $x$ be a set. Let $D$ be an element of $\wp (\wp x)$. Then we can say that $\operatorname{IsScott}$ holds for $x$ and $D$.
Topology.IsScott.withScottHomeomorphdefMathlib.Topology.Order.ScottTopology, function or constantEnglish
$\operatorname{withScottHomeomorph}$ is a homeomorphism of $\operatorname{WithScott}$ applied to $x$ and $x$.
Topology.IsScottHausdorffclassMathlib.Topology.Order.ScottTopology, predicateEnglish
Let $x$ be a set. Let $D$ be an element of $\wp (\wp x)$. Then we can say that $\operatorname{IsScottHausdorff}$ holds for $x$ and $D$.
Topology.WithScottdefMathlib.Topology.Order.ScottTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithScott}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithScott.ofScottdefMathlib.Topology.Order.ScottTopology, function or constantEnglish
$\operatorname{ofScott}$ is an element of $\EquivMACRoAE {\operatorname{WithScott} (x)}{x}$ defined as the identity of $\operatorname{WithScott}$ applied to $x$.
Topology.WithScott.toScottdefMathlib.Topology.Order.ScottTopology, function or constantEnglish
$\operatorname{toScott}$ is an element of $\EquivMACRoAE {x}{\operatorname{WithScott} (x)}$ defined as the identity of $x$.
Topology.IsLowerSetclassMathlib.Topology.Order.UpperLowerSetTopology, predicateWording
x is a lower set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a lower set.
Topology.IsLowerSet.WithLowerSetHomeomorphdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{WithLowerSetHomeomorph}$ is a homeomorphism of $\operatorname{WithLowerSet}$ applied to $x$ and $x$.
Topology.IsUpperSetclassMathlib.Topology.Order.UpperLowerSetTopology, predicateWording
x is a upper set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a upper set.
Topology.IsUpperSet.WithUpperSetHomeomorphdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{WithUpperSetHomeomorph}$ is a homeomorphism of $\operatorname{WithUpperSet}$ applied to $x$ and $x$.
Topology.WithLowerSetdefMathlib.Topology.Order.UpperLowerSetTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithLowerSet}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithLowerSet.mapdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the map of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the map of $f$ is a continuous map of $\operatorname{WithLowerSet}$ applied to $x$ and $\operatorname{WithLowerSet}$ applied to $x_{1}$.
Topology.WithLowerSet.ofLowerSetdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{ofLowerSet}$ is an element of $\EquivMACRoAE {\operatorname{WithLowerSet} (x)}{x}$ defined as the identity of $\operatorname{WithLowerSet}$ applied to $x$.
Topology.WithLowerSet.ofLowerSetOrderIsodefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{ofLowerSetOrderIso}$ is an order isomorphism of $\operatorname{WithLowerSet}$ applied to $x$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ofLowerSet}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Topology\_\_WithLowerSet\_\_ofLowerSet\_le\_iff}$.
Topology.WithLowerSet.toLowerSetdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the lower set (from the name)
English
The lower set is an element of $\EquivMACRoAE {x}{\operatorname{WithLowerSet} (x)}$ defined as the identity of $x$.
Topology.WithLowerSet.toLowerSetOrderIsodefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the lower set order isomorphism (from the name)
English
The lower set order isomorphism is an order isomorphism of $x$ and $\operatorname{WithLowerSet}$ applied to $x$ defined as $\operatorname{mk}$ applied to the lower set and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Topology\_\_WithLowerSet\_\_toLowerSet\_le\_iff}$.
Topology.WithUpperSetdefMathlib.Topology.Order.UpperLowerSetTopology, typeEnglish
Let $x$ be a set. Then an element of $\operatorname{WithUpperSet}$ applied to $x$ is an element of the function that maps $x$ to $x$.
Topology.WithUpperSet.mapdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the map of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the map of $f$ is a continuous map of $\operatorname{WithUpperSet}$ applied to $x$ and $\operatorname{WithUpperSet}$ applied to $x_{1}$.
Topology.WithUpperSet.ofUpperSetdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{ofUpperSet}$ is an element of $\EquivMACRoAE {\operatorname{WithUpperSet} (x)}{x}$ defined as the identity of $\operatorname{WithUpperSet}$ applied to $x$.
Topology.WithUpperSet.ofUpperSetOrderIsodefMathlib.Topology.Order.UpperLowerSetTopology, function or constantEnglish
$\operatorname{ofUpperSetOrderIso}$ is an order isomorphism of $\operatorname{WithUpperSet}$ applied to $x$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ofUpperSet}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Topology\_\_WithUpperSet\_\_ofUpperSet\_le\_iff}$.
Topology.WithUpperSet.toDualHomeomorphdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the dual homeomorphism (from the name)
English
The dual homeomorphism is a homeomorphism of $\operatorname{WithUpperSet}$ applied to $x$ and $\operatorname{WithLowerSet}$ applied to the set of order duals of $x$.
Topology.WithUpperSet.toUpperSetdefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the upper set (from the name)
English
The upper set is an element of $\EquivMACRoAE {x}{\operatorname{WithUpperSet} (x)}$ defined as the identity of $x$.
Topology.WithUpperSet.toUpperSetOrderIsodefMathlib.Topology.Order.UpperLowerSetTopology, function or constantWording
the upper set order isomorphism (from the name)
English
The upper set order isomorphism is an order isomorphism of $x$ and $\operatorname{WithUpperSet}$ applied to $x$ defined as $\operatorname{mk}$ applied to the upper set and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Topology\_\_WithUpperSet\_\_toUpperSet\_le\_iff}$.
WithBot.neBotHomeomorphdefMathlib.Topology.Order.WithTop, function or constantEnglish
Let $x$ be a set. Then $\operatorname{neBotHomeomorph}$ applied to $x$ is a homeomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is distinct from the bottom and $x$.
WithBot.sumHomeomorphdefMathlib.Topology.Order.WithTop, function or constantWording
the sum homeomorphism of x (from the name)
English
Let $x$ be a set. Then the sum homeomorphism of $x$ is a homeomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Unit}$.
WithTop.neTopHomeomorphdefMathlib.Topology.Order.WithTop, function or constantEnglish
Let $x$ be a set. Then $\operatorname{neTopHomeomorph}$ applied to $x$ is a homeomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is distinct from the top and $x$.
WithTop.sumHomeomorphdefMathlib.Topology.Order.WithTop, function or constantWording
the sum homeomorphism of x (from the name)
English
Let $x$ be a set. Then the sum homeomorphism of $x$ is a homeomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Unit}$.
PContinuousdefMathlib.Topology.Partial, predicateWording
f is continuous (from the name)
English
Let $f$ be a function of $X$ and $Y$. Then $f$ is continuous, if for all elements $s$ of $\wp Y$, if $s$ is open, then the preimage of $f$ and $s$ is open.
PartialHomeomorph.homeomorphOfImageSubsetSourcedefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be a partial homeomorphism of $X$ and $Y$ such that $s$ is less than or equal to the source of $\operatorname{toPartialEquiv}$ applied to $e$ and the image of $\operatorname{toFun'}$ applied to $e$ and $s$ is equal to $t$. Then the homeomorphism of $e$ is a homeomorphism of the set of elements of $s$ and the set of elements of $t$.
PartialHomeomorph.ofContinuousOpendefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the partial homeomorphism of e (from the name)
English
Let $e$ be a partial equivalence of $X$ and $Y$ such that $\mathrm{ContinuousOn}$ holds for $\operatorname{toFun}$ applied to $e$ and the source of $e$, $\operatorname{toFun}$ applied to $e$ is an open map and the source of $e$ is open. Then the partial homeomorphism of $e$ is a partial homeomorphism of $X$ and $Y$.
PartialHomeomorph.ofContinuousOpenRestrictdefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the partial homeomorphism of e (from the name)
English
Let $e$ be a partial equivalence of $X$ and $Y$ such that $\mathrm{ContinuousOn}$ holds for $\operatorname{toFun}$ applied to $e$ and the source of $e$ and $\operatorname{domRestrict}$ applied to the source of $e$ and $\operatorname{toFun}$ applied to $e$ is an open map. Then the partial homeomorphism of $e$ is a partial homeomorphism of $X$ and $Y$.
PartialHomeomorph.ofIsHomeomorphToEquivdefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the partial homeomorphism of f and h (from the name)
English
Let $f$ be a partial equivalence of $X$ and $Y$ such that $\operatorname{coe}$ applied to the equivalence of $f$ is a homeomorphism. Then the partial homeomorphism of $f$ and $h$ is a partial homeomorphism of $X$ and $Y$.
PartialHomeomorph.refldefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the identity on the whole space of X (from the docstring)
English
Let $X$ be a set. Then the identity on the whole space of $X$ is a partial homeomorphism of $X$ and $X$ defined as the partial homeomorphism of the identity of $X$.
PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUnivdefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the homeomorphism of e (from the name)
English
Let $e$ be a partial homeomorphism of $X$ and $Y$ such that the source of $\operatorname{toPartialEquiv}$ applied to $e$ is equal to the universal set and the target of $\operatorname{toPartialEquiv}$ applied to $e$ is equal to the universal set. Then the homeomorphism of $e$ is a homeomorphism of $X$ and $Y$.
PartialHomeomorph.toHomeomorphSourceTargetdefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the homeomorphism source target of e (from the name)
English
Let $e$ be a partial homeomorphism of $X$ and $Y$. Then the homeomorphism source target of $e$ is a homeomorphism of the set of elements of the source of $\operatorname{toPartialEquiv}$ applied to $e$ and the set of elements of the target of $\operatorname{toPartialEquiv}$ applied to $e$.
Set.partialHomeomorphSubtypeCoedefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the partial homeomorphism subtype coercion of s and hs (from the name)
English
Let $s$ be an element of $\wp X$ such that $\mathrm{Nonempty}$ holds for the set of elements of $s$. Then the partial homeomorphism subtype coercion of $s$ and $\mathrm{hs}$ is a partial homeomorphism of the set of elements of $s$ and $X$.
Topology.IsEmbedding.toPartialHomeomorphdefMathlib.Topology.PartialHomeomorph.Basic, function or constantWording
the partial homeomorphism of f and h (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$ such that $f$ is an embedding. Then the partial homeomorphism of $f$ and $h$ is a partial homeomorphism of $X$ and $Y$.
Homeomorph.toPartialHomeomorphdefMathlib.Topology.PartialHomeomorph.Defs, function or constantWording
the partial homeomorphism of e (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Then the partial homeomorphism of $e$ is a partial homeomorphism of $X$ and $Y$.
Homeomorph.toPartialHomeomorphOfImageEqdefMathlib.Topology.PartialHomeomorph.Defs, function or constantWording
the partial homeomorphism of s and t (from the name)
English
Let $e$ be a homeomorphism of $X$ and $Y$. Let $s$ be an element of $\wp X$. Let $t$ be an element of $\wp Y$ such that the image of $\operatorname{coe}$ applied to $e$ and $s$ is equal to $t$. Then the partial homeomorphism of $s$ and $t$ is a partial homeomorphism of $X$ and $Y$.
PartialHomeomorphstructureMathlib.Topology.PartialHomeomorph.Defs, typeWording
partial homeomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be sets. Then the partial homeomorphisms of $X$ and $Y$ are a basic type.
PartialHomeomorph.replacePartialEquivdefMathlib.Topology.PartialHomeomorph.Defs, function or constantEnglish
Let $e$ be a partial homeomorphism of $X$ and $Y$. Let $\mathrm{e'}$ be a partial equivalence of $X$ and $Y$ such that $\EqtMACRoH {\operatorname{toPartialEquiv} (e)}{\mathrm{e'}}$. Then $\operatorname{replacePartialEquiv}$ applied to $e$, $\mathrm{e'}$ and $h$ is a partial homeomorphism of $X$ and $Y$.
PartialHomeomorph.symmdefMathlib.Topology.PartialHomeomorph.Defs, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be a partial homeomorphism of $X$ and $Y$. Then the inverse of $e$ is a partial homeomorphism of $Y$ and $X$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toPartialEquiv}$ applied to $e$, $\mathrm{PartialHomeomorph\_\_continuousOn\_invFun}$ applied to $e$ and $\mathrm{PartialHomeomorph\_\_continuousOn\_toFun}$ applied to $e$.
PartialHomeomorph.toFun'defMathlib.Topology.PartialHomeomorph.Defs, function or constantWording
the function of e and x2 (from the name)
English
Let $e$ be a partial homeomorphism of $X$ and $Y$. Let $x_{2}$ be an element of $X$. Then the function of $e$ and $x_{2}$ is an element of $Y$ defined as the partial equivalence of $\operatorname{toPartialEquiv}$ applied to $e$ and $x_{2}$.
BumpCoveringstructureMathlib.Topology.PartitionOfUnity, typeWording
bump covering of X and s (from the name)
English
Let $x$ and $X$ be sets. Let $s$ be an element of $\mathrm{optParam}$ applied to $\wp X$ and the universal set. Then the bump coverings of $X$ and $s$ are a basic type.
BumpCovering.IsSubordinatedefMathlib.Topology.PartitionOfUnity, predicateWording
f is subordinate to U (from the name)
English
Let $f$ be a bump covering of $X$ and $s$. Let $U$ be a function from elements of $x$ to elements of $\wp X$. Then $f$ is subordinate to $U$, if for all elements $i$ of $x$, $\mathrm{tsupport}$ applied to $\operatorname{coe}$ applied to $f$ applied to $i$ is less than or equal to $U$ applied to $i$.
BumpCovering.inddefMathlib.Topology.PartitionOfUnity, function or constantWording
the ind of f and x2 (from the name)
English
Let $f$ be a bump covering of $X$ and $s$. Let $x_{2}$ be an element of $X$ such that $x_{2}$ is an element of $s$. Then the ind of $f$ and $x_{2}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{BumpCovering\_\_eventuallyEq\_one'}$ applied to $f$, $x_{2}$ and $\mathrm{hx}$.
BumpCovering.singledefMathlib.Topology.PartitionOfUnity, function or constantEnglish
Let $i$ be an element of $x$. Let $s$ be an element of $\wp X$. Then $\operatorname{single}$ applied to $i$ and $s$ is a bump covering of $X$ and $s$.
BumpCovering.toFundefMathlib.Topology.PartitionOfUnity, function or constantWording
the bump covering of self and x2 (from the name)
English
Let $\mathrm{self}$ be a bump covering of $X$ and $s$. Let $x_{2}$ be an element of $x$. Then the bump covering of $\mathrm{self}$ and $x_{2}$ is a continuous map of $X$ and $\Real$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
BumpCovering.toPOUFundefMathlib.Topology.PartitionOfUnity, function or constantEnglish
Let $f$ be a bump covering of $X$ and $s$. Let $i$ be an element of $x$. Let $x_{2}$ be an element of $X$. Then $\operatorname{toPOUFun}$ applied to $f$, $i$ and $x_{2}$ is a real number defined as $\operatorname{coe} (f , i , x_{2})\times \mathrm{finprod} (\lambda j . \mathrm{finprod} (\lambda h . 1 - \operatorname{coe} (f , j , x_{2})))$.
BumpCovering.toPartitionOfUnitydefMathlib.Topology.PartitionOfUnity, function or constantWording
the partition of f (from the name)
English
Let $f$ be a bump covering of $X$ and $s$. Then the partition of $f$ is a partition of unity of $X$ and $s$.
PartitionOfUnitystructureMathlib.Topology.PartitionOfUnity, typeWording
partition of unity of X and s (from the name)
English
Let $x$ and $X$ be sets. Let $s$ be an element of $\mathrm{optParam}$ applied to $\wp X$ and the universal set. Then the partitions of unity of $X$ and $s$ are a basic type.
PartitionOfUnity.IsSubordinatedefMathlib.Topology.PartitionOfUnity, predicateWording
f is subordinate to U (from the name)
English
Let $f$ be a partition of unity of $X$ and $s$. Let $U$ be a function from elements of $x$ to elements of $\wp X$. Then $f$ is subordinate to $U$, if for all elements $i$ of $x$, $\mathrm{tsupport}$ applied to $\operatorname{coe}$ applied to $f$ applied to $i$ is less than or equal to $U$ applied to $i$.
PartitionOfUnity.finsupportdefMathlib.Topology.PartitionOfUnity, function or constantEnglish
Let $x_{2}$ be a partition of unity of $X$ and $s$. Let $x_{3}$ be an element of $X$. Then $\operatorname{finsupport}$ applied to $x_{2}$ and $x_{3}$ is a finite set of $x$.
PartitionOfUnity.fintsupportdefMathlib.Topology.PartitionOfUnity, function or constantEnglish
Let $x_{2}$ be a partition of unity of $X$ and $s$. Let $x_{3}$ be an element of $X$. Then $\operatorname{fintsupport}$ applied to $x_{2}$ and $x_{3}$ is a finite set of $x$ defined as the finite set of $\mathrm{PartitionOfUnity\_\_finite\_tsupport}$ applied to $x_{2}$ and $x_{3}$.
PartitionOfUnity.toFundefMathlib.Topology.PartitionOfUnity, function or constantWording
the partition of self and x2 (from the name)
English
Let $\mathrm{self}$ be a partition of unity of $X$ and $s$. Let $x_{2}$ be an element of $x$. Then the partition of $\mathrm{self}$ and $x_{2}$ is a continuous map of $X$ and $\Real$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
PathstructureMathlib.Topology.Path, typeWording
path of x1 and y (from the name)
English
Let $x_{1}$ and $y$ be elements of $X$. Then the paths of $x_{1}$ and $y$ are a basic type.
Path.adddefMathlib.Topology.Path, function or constantWording
the sum of x6 and x7 (from the name)
English
Let $x_{6}$ be a path of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a path of $x_{4}$ and $x_{5}$. Then the sum of $x_{6}$ and $x_{7}$ is a path of $x_{2} + x_{4}$ and $x_{3} + x_{5}$ defined as the map of the product of $x_{6}$ and $x_{7}$ and $\mathrm{continuous\_add}$.
Path.castdefMathlib.Topology.Path, function or constantWording
the cast of x2 (from the name)
English
Let $x_{2}$ be a path of $x_{1}$ and $y$. Assume that $\EqtMACRoH {\mathrm{x'}}{x_{1}}$. Assume that $\EqtMACRoH {\mathrm{y'}}{y}$. Then the cast of $x_{2}$ is a path of $\mathrm{x'}$ and $\mathrm{y'}$.
Path.extenddefMathlib.Topology.Path, function or constantEnglish
Let $x_{2}$ be a path of $x_{1}$ and $y$. Then $\operatorname{extend}$ applied to $x_{2}$ is a continuous map of $\Real$ and $X$.
Path.iddefMathlib.Topology.Path, function or constantWording
the identity (from the name)
English
The identity is a path of $0$ and $1$.
Path.invdefMathlib.Topology.Path, function or constantWording
the inverse of x2 (from the name)
English
Let $x_{2}$ be a path of $a$ and $b$. Then the inverse of $x_{2}$ is a path of $\operatorname{inv}$ applied to $a$ and $\operatorname{inv}$ applied to $b$ defined as the map of $x_{2}$ and $\mathrm{ContinuousInv\_\_continuous\_inv}$.
Path.mapdefMathlib.Topology.Path, function or constantWording
the map of x3 and h (from the name)
English
Let $x_{3}$ be a path of $x_{2}$ and $y$. Assume that $f$ is continuous. Then the map of $x_{3}$ and $h$ is a path of $f$ applied to $x_{2}$ and $f$ applied to $y$.
Path.map'defMathlib.Topology.Path, function or constantWording
the map of x3 and h (from the name)
English
Let $x_{3}$ be a path of $x_{2}$ and $y$ such that $\mathrm{ContinuousOn}$ holds for $f$ and the range of $\operatorname{coe}$ applied to $x_{3}$. Then the map of $x_{3}$ and $h$ is a path of $f$ applied to $x_{2}$ and $f$ applied to $y$.
Path.muldefMathlib.Topology.Path, function or constantWording
the product of x6 and x7 (from the name)
English
Let $x_{6}$ be a path of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a path of $x_{4}$ and $x_{5}$. Then the product of $x_{6}$ and $x_{7}$ is a path of $x_{2} \times x_{4}$ and $x_{3} \times x_{5}$ defined as the map of the product of $x_{6}$ and $x_{7}$ and $\mathrm{continuous\_mul}$.
Path.negdefMathlib.Topology.Path, function or constantWording
the negation of x2 (from the name)
English
Let $x_{2}$ be a path of $a$ and $b$. Then the negation of $x_{2}$ is a path of $\operatorname{neg}$ applied to $a$ and $\operatorname{neg}$ applied to $b$ defined as the map of $x_{2}$ and $\mathrm{ContinuousNeg\_\_continuous\_neg}$.
Path.ofLinedefMathlib.Topology.Path, function or constantWording
the path of h and h1 (from the name)
English
Assume that $\mathrm{ContinuousOn}$ holds for $f$ and the unit interval. Assume that $\EqtMACRoH {f (0)}{x_{1}}$. Assume that $\EqtMACRoH {f (1)}{y}$. Then the path of $h$ and $h_{1}$ is a path of $x_{1}$ and $y$.
Path.pidefMathlib.Topology.Path, function or constantWording
the product of x3 (from the name)
English
Let $x_{3}$ be a function from elements $i$ of $x$ to paths of $\mathrm{as}$ applied to $i$ and $\mathrm{bs}$ applied to $i$. Then the product of $i$ is a path of $\mathrm{as}$ and $\mathrm{bs}$.
Path.proddefMathlib.Topology.Path, function or constantWording
the product of x6 and x7 (from the name)
English
Let $x_{6}$ be a path of $x_{2}$ and $x_{3}$. Let $x_{7}$ be a path of $x_{4}$ and $x_{5}$. Then the product of $x_{6}$ and $x_{7}$ is a path of $\ProdmkMACRoU {x_{2}}{x_{4}}$ and $\ProdmkMACRoU {x_{3}}{x_{5}}$.
Path.refldefMathlib.Topology.Path, function or constantWording
the identity of x1 (from the name)
English
Let $x_{1}$ be an element of $X$. Then the identity of $x_{1}$ is a path of $x_{1}$ and $x_{1}$.
Path.reparamdefMathlib.Topology.Path, function or constantEnglish
Let $x_{2}$ be a path of $x_{1}$ and $y$. Let $f$ be a function from elements of the unit interval to elements of the unit interval such that $f$ is continuous, $\EqtMACRoH {f (0)}{0}$ and $\EqtMACRoH {f (1)}{1}$. Then $\operatorname{reparam}$ applied to $x_{2}$, $f$, $\mathrm{hfcont}$, $h$ and $h_{1}$ is a path of $x_{1}$ and $y$.
Path.simps.applydefMathlib.Topology.Path, function or constantEnglish
Let $x_{2}$ be a path of $x_{1}$ and $y$. Let $x_{3}$ be an element of the unit interval. Then $\operatorname{apply}$ applied to $x_{2}$ and $x_{3}$ is an element of $X$ defined as the coercion of $x_{2}$ and $x_{3}$.
Path.symmdefMathlib.Topology.Path, function or constantWording
the inverse of x2 (from the name)
English
Let $x_{2}$ be a path of $x_{1}$ and $y$. Then the inverse of $x_{2}$ is a path of $y$ and $x_{1}$.
Path.transdefMathlib.Topology.Path, function or constantWording
the composition of x2 and x3 (from the name)
English
Let $x_{2}$ be a path of $x_{1}$ and $y$. Let $x_{3}$ be a path of $y$ and $z$. Then the composition of $x_{2}$ and $x_{3}$ is a path of $x_{1}$ and $z$.
Path.truncatedefMathlib.Topology.Path, function or constantEnglish
Let $x_{1}$ be a path of $a$ and $b$. Let $x_{2}$ and $x_{3}$ be real numbers. Then $\operatorname{truncate}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is a path of $\operatorname{extend}$ applied to $x_{1}$ and $\MinminMACRoAG {x_{2}}{x_{3}}$ and $\operatorname{extend}$ applied to $x_{1}$ and $x_{3}$.
Path.truncateOfLEdefMathlib.Topology.Path, function or constantEnglish
Let $x_{1}$ be a path of $a$ and $b$. Assume that $x_{2} \leq x_{3}$. Then $\operatorname{truncateOfLE}$ applied to $x_{1}$ and $h$ is a path of $\operatorname{extend}$ applied to $x_{1}$ and $x_{2}$ and $\operatorname{extend}$ applied to $x_{1}$ and $x_{3}$.
PerfectstructureMathlib.Topology.Perfect, predicateWording
C is perfect (from the name)
English
Let $C$ be an element of $\wp x$. Then we can say that $C$ is perfect.
PerfectSpaceclassMathlib.Topology.Perfect, predicateWording
x is a perfect space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a perfect space.
PreperfectdefMathlib.Topology.Perfect, predicateEnglish
Let $C$ be an element of $\wp x$. Then $\mathrm{Preperfect}$ holds for $C$, if for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of $C$, then $\mathrm{AccPt}$ holds for $x_{2}$ and the principal filter of $C$.
IsQuasiSeparateddefMathlib.Topology.QuasiSeparated, predicateEnglish
Let $s$ be an element of $\wp x$. Then $\mathrm{IsQuasiSeparated}$ holds for $s$, if for all elements $U$ and $V$ of $\wp x$, if $U \leq s$, then if $U$ is open, then if $U$ is compact, then if $V \leq s$, then if $V$ is open, then if $V$ is compact, then $\operatorname{inter}$ applied to $U$ and $V$ is compact.
QuasiSeparatedSpaceclassMathlib.Topology.QuasiSeparated, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{QuasiSeparatedSpace}$ holds for $x$.
HasOpenCGraphdefMathlib.Topology.Semicontinuity.Defs, predicateWording
f has open graphs (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Then $f$ has open graphs, if $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to $\MembershipmemMACRoT {f (\ProdfstMACRoZ {x_{4}})}{\ProdsndMACRoAA {x_{4}}}$ is open.
HasOpenLowerSectionsdefMathlib.Topology.Semicontinuity.Defs, predicateWording
f has open lower sections (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Then $f$ has open lower sections, if the function that maps $x_{3}$ and $b$ to $\MembershipmemMACRoT {f (x_{3})}{b}$ is semicontinuous.
HasOpenLowerSectionsOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{HasOpenLowerSectionsOn}$ holds for $f$ and $s$, if $\mathrm{SemicontinuousOn}$ holds for the function that maps $x_{3}$ and $b$ to $\MembershipmemMACRoT {f (x_{3})}{b}$ and $s$.
LowerHemicontinuousdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Then $\mathrm{LowerHemicontinuous}$ holds for $f$, if the function that maps $x_{4}$ and $t$ to the proposition that $t$ is open and $\operatorname{inter}$ applied to $f$ applied to $x_{4}$ and $t$ is nonempty is semicontinuous.
LowerHemicontinuousAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $x_{4}$ be an element of $x$. Then $\mathrm{LowerHemicontinuousAt}$ holds for $f$ and $x_{4}$, if $\mathrm{SemicontinuousAt}$ holds for the function that maps $x_{5}$ and $t$ to the proposition that $t$ is open and $\operatorname{inter}$ applied to $f$ applied to $x_{5}$ and $t$ is nonempty and $x_{4}$.
LowerHemicontinuousOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{LowerHemicontinuousOn}$ holds for $f$ and $s$, if $\mathrm{SemicontinuousOn}$ holds for the function that maps $x_{4}$ and $t$ to the proposition that $t$ is open and $\operatorname{inter}$ applied to $f$ applied to $x_{4}$ and $t$ is nonempty and $s$.
LowerHemicontinuousWithinAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $x$. Then $\mathrm{LowerHemicontinuousWithinAt}$ holds for $f$, $s$ and $x_{4}$, if $\mathrm{SemicontinuousWithinAt}$ holds for the function that maps $x_{5}$ and $t$ to the proposition that $t$ is open and $\operatorname{inter}$ applied to $f$ applied to $x_{5}$ and $t$ is nonempty, $s$ and $x_{4}$.
LowerSemicontinuousdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{LowerSemicontinuous}$ holds for $f$, if the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Gt} (f (x_{4}), x_{5})$ is semicontinuous.
LowerSemicontinuousAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\mathrm{LowerSemicontinuousAt}$ holds for $f$ and $x_{4}$, if $\mathrm{SemicontinuousAt}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Gt} (f (x_{5}), x_{6})$ and $x_{4}$.
LowerSemicontinuousOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{LowerSemicontinuousOn}$ holds for $f$ and $s$, if $\mathrm{SemicontinuousOn}$ holds for the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Gt} (f (x_{4}), x_{5})$ and $s$.
LowerSemicontinuousWithinAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $x$. Then $\mathrm{LowerSemicontinuousWithinAt}$ holds for $f$, $s$ and $x_{4}$, if $\mathrm{SemicontinuousWithinAt}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Gt} (f (x_{5}), x_{6})$, $s$ and $x_{4}$.
SemicontinuousdefMathlib.Topology.Semicontinuity.Defs, predicateWording
r is semicontinuous (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $r$ is semicontinuous, if for all elements $x_{3}$ of $x$, $\mathrm{SemicontinuousAt}$ holds for $r$ and $x_{3}$.
SemicontinuousAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $x_{3}$ be an element of $x$. Then $\mathrm{SemicontinuousAt}$ holds for $r$ and $x_{3}$, if for all elements $y$ of $x_{1}$, if $r$ holds for $x_{3}$ and $y$, then $\operatorname{Eventually}$ holds for the function that maps $\mathrm{x'}$ to $r$ applied to $\mathrm{x'}$ and $y$ and the neighbourhood filter of $x_{3}$.
SemicontinuousOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{SemicontinuousOn}$ holds for $r$ and $s$, if for all elements $x_{3}$ of $x$, if $x_{3}$ is an element of $s$, then $\mathrm{SemicontinuousWithinAt}$ holds for $r$, $s$ and $x_{3}$.
SemicontinuousWithinAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$. Let $x_{3}$ be an element of $x$. Then $\mathrm{SemicontinuousWithinAt}$ holds for $r$, $s$ and $x_{3}$, if for all elements $y$ of $x_{1}$, if $r$ holds for $x_{3}$ and $y$, then $\operatorname{Eventually}$ holds for the function that maps $\mathrm{x'}$ to $r$ applied to $\mathrm{x'}$ and $y$ and $\mathrm{nhdsWithin}$ applied to $x_{3}$ and $s$.
UpperHemicontinuousdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Then $\mathrm{UpperHemicontinuous}$ holds for $f$, if the function that maps $x_{4}$ and $t$ to the proposition that $t$ is an element of the neighbourhood filter set of $f$ applied to $x_{4}$ is semicontinuous.
UpperHemicontinuousAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $x_{4}$ be an element of $x$. Then $\mathrm{UpperHemicontinuousAt}$ holds for $f$ and $x_{4}$, if $\mathrm{SemicontinuousAt}$ holds for the function that maps $x_{5}$ and $t$ to the proposition that $t$ is an element of the neighbourhood filter set of $f$ applied to $x_{5}$ and $x_{4}$.
UpperHemicontinuousOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{UpperHemicontinuousOn}$ holds for $f$ and $s$, if $\mathrm{SemicontinuousOn}$ holds for the function that maps $x_{4}$ and $t$ to the proposition that $t$ is an element of the neighbourhood filter set of $f$ applied to $x_{4}$ and $s$.
UpperHemicontinuousWithinAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $x$. Then $\mathrm{UpperHemicontinuousWithinAt}$ holds for $f$, $s$ and $x_{4}$, if $\mathrm{SemicontinuousWithinAt}$ holds for the function that maps $x_{5}$ and $t$ to the proposition that $t$ is an element of the neighbourhood filter set of $f$ applied to $x_{5}$, $s$ and $x_{4}$.
UpperSemicontinuousdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{UpperSemicontinuous}$ holds for $f$, if the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (f (x_{4}), x_{5})$ is semicontinuous.
UpperSemicontinuousAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\mathrm{UpperSemicontinuousAt}$ holds for $f$ and $x_{4}$, if $\mathrm{SemicontinuousAt}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (f (x_{5}), x_{6})$ and $x_{4}$.
UpperSemicontinuousOndefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{UpperSemicontinuousOn}$ holds for $f$ and $s$, if $\mathrm{SemicontinuousOn}$ holds for the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (f (x_{4}), x_{5})$ and $s$.
UpperSemicontinuousWithinAtdefMathlib.Topology.Semicontinuity.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $x$. Then $\mathrm{UpperSemicontinuousWithinAt}$ holds for $f$, $s$ and $x_{4}$, if $\mathrm{SemicontinuousWithinAt}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (f (x_{5}), x_{6})$, $s$ and $x_{4}$.
IsLocallyInjectivedefMathlib.Topology.SeparatedMap, predicateWording
f is locally injective (from the name)
English
generation took over the time limit
IsSeparatedMapdefMathlib.Topology.SeparatedMap, predicateWording
f is a separated map (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is a separated map, if for all elements $x_{1}$ and $x_{2}$ of $X$, if $\EqtMACRoH {f (x_{1})}{f (x_{2})}$, then if $x_{1} \neq x_{2}$, then there exist elements $x_{3}$ and $x_{4}$ of $\wp X$, such that $x_{3}$ and $x_{4}$ are open, $x_{1}$ is an element of $x_{3}$, $x_{2}$ is an element of $x_{4}$ and $x_{3}$ is disjoint to $x_{4}$.
R0SpaceclassMathlib.Topology.Separation.Basic, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
R1SpaceclassMathlib.Topology.Separation.Basic, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
T0SpaceclassMathlib.Topology.Separation.Basic, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
T1SpaceclassMathlib.Topology.Separation.Basic, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
CompletelyRegularSpaceclassMathlib.Topology.Separation.CompletelyRegular, predicateWording
X is completely regular (from the docstring)
English
generation took over the time limit
T35SpaceclassMathlib.Topology.Separation.CompletelyRegular, predicateEnglish
Let $X$ be a set. Then we can say that $\mathrm{T35Space}$ holds for $X$.
PerfectlyNormalSpaceclassMathlib.Topology.Separation.GDelta, predicateWording
X is a perfectly normal space (from the name)
English
generation took over the time limit
T6SpaceclassMathlib.Topology.Separation.GDelta, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
T2QuotientdefMathlib.Topology.Separation.Hausdorff, typeWording
quotient of X (from the name)
English
Let $X$ be a set. Then a quotient of $X$ is an element of the function that maps $X$ to $\mathrm{Quotient}$ applied to $\mathrm{t2Setoid}$ applied to $X$.
T2Quotient.liftdefMathlib.Topology.Separation.Hausdorff, function or constantWording
the lift of hf and x2 (from the name)
English
Assume that $f$ is continuous. Let $x_{2}$ be a quotient of $X$. Then the lift of $\mathrm{hf}$ and $x_{2}$ is an element of $Y$ defined as $\operatorname{lift}$ applied to $f$, $\operatorname{compatible}$ applied to $\mathrm{hf}$ and $x_{2}$.
T2Quotient.mkdefMathlib.Topology.Separation.Hausdorff, function or constantEnglish
Let $x_{1}$ be an element of $X$. Then $\operatorname{mk}$ applied to $x_{1}$ is a quotient of $X$ defined as $\operatorname{mk}$ applied to $\mathrm{t2Setoid}$ applied to $X$ and $x_{1}$.
T2SpaceclassMathlib.Topology.Separation.Hausdorff, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
CompletelyNormalSpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a completely normal space (from the name)
English
generation took over the time limit
NormalSpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a normal space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a normal space.
RegularSpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a regular space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a regular space.
T25SpaceclassMathlib.Topology.Separation.Regular, predicateEnglish
Let $X$ be a set. Then we can say that $\mathrm{T25Space}$ holds for $X$.
T3SpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
T4SpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
T5SpaceclassMathlib.Topology.Separation.Regular, predicateWording
X is a space (from the name)
English
Let $X$ be a set. Then we can say that $X$ is a space.
HasSeparatingCoverdefMathlib.Topology.Separation.SeparatedNhds, predicateEnglish
Let $x_{1}$ and $x_{2}$ be elements of $\wp X$. Then $\mathrm{HasSeparatingCover}$ holds for $x_{1}$ and $x_{2}$, if there exists a function $u$ from natural numbers to elements of $\wp X$, such that $x_{1}$ is less than or equal to the union of the function that maps $n$ to $u$ applied to $n$ and for all natural numbers $n_{1}$, $u$ applied to $n_{1}$ is open and the closure of $u$ applied to $n_{1}$ is disjoint to $x_{2}$.
SeparatedNhdsdefMathlib.Topology.Separation.SeparatedNhds, predicateEnglish
Let $x_{1}$ and $x_{2}$ be elements of $\wp X$. Then $\mathrm{SeparatedNhds}$ holds for $x_{1}$ and $x_{2}$, if there exist elements $U$ and $V$ of $\wp X$, such that $U$ and $V$ are open, $x_{1} \leq U$, $x_{2} \leq V$ and $U$ is disjoint to $V$.
TopologicalSpace.Compacts.baseChangeOpenNhdsdefMathlib.Topology.Sets.BaseChangeNhds, function or constantWording
the base change open neighbourhood filter of h and x2 (from the name)
English
Let $h$ be a homomorphism of $K$ and $L$. Let $x_{2}$ be an element of the open neighbourhood filter of $L$. Then the base change open neighbourhood filter of $h$ and $x_{2}$ is an element of the open neighbourhood filter of $K$.
TopologicalSpace.Compacts.isInitialBotOpensOpenNhdsBotdefMathlib.Topology.Sets.BaseChangeNhds, function or constantEnglish
$\operatorname{isInitialBotOpensOpenNhdsBot}$ is an element of $\operatorname{IsInitial}$ applied to the bottom.
TopologicalSpace.Opens.baseChangeCompactsInsidedefMathlib.Topology.Sets.BaseChangeNhds, function or constantEnglish
Let $h$ be a homomorphism of $U$ and $V$. Let $x_{2}$ be an element of $\operatorname{compactsInside}$ applied to $U$. Then $\operatorname{baseChangeCompactsInside}$ applied to $h$ and $x_{2}$ is an element of $\operatorname{compactsInside}$ applied to $V$.
TopologicalSpace.ClopensstructureMathlib.Topology.Sets.Closeds, typeWording
clopen of x (from the name)
English
Let $x$ be a set. Then the clopens of $x$ are a basic type.
TopologicalSpace.Clopens.carrierdefMathlib.Topology.Sets.Closeds, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a clopen of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopologicalSpace.Clopens.toClosedsdefMathlib.Topology.Sets.Closeds, function or constantEnglish
Let $s$ be a clopen of $x$. Then $\operatorname{toCloseds}$ applied to $s$ is an element of $\operatorname{Closeds}$ applied to $x$ defined as $\operatorname{mk}$ applied to $s$ and $\operatorname{isClosed}$ applied to $s$.
TopologicalSpace.Clopens.toOpensdefMathlib.Topology.Sets.Closeds, function or constantWording
the open of s (from the name)
English
Let $s$ be a clopen of $x$. Then the open of $s$ is an open of $x$ defined as $\operatorname{mk}$ applied to $s$ and $\operatorname{isOpen}$ applied to $s$.
TopologicalSpace.ClosedsstructureMathlib.Topology.Sets.Closeds, typeEnglish
Let $x$ be a set. Then the elements of $\operatorname{Closeds}$ applied to $x$ are a basic type.
TopologicalSpace.Closeds.carrierdefMathlib.Topology.Sets.Closeds, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{Closeds}$ applied to $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopologicalSpace.Closeds.closuredefMathlib.Topology.Sets.Closeds, function or constantWording
the closure of s (from the docstring)
English
Let $s$ be an element of $\wp x$. Then the closure of $s$ is an element of $\operatorname{Closeds}$ applied to $x$ defined as $\operatorname{mk}$ applied to the closure of $s$ and $\mathrm{isClosed\_closure}$.
TopologicalSpace.Closeds.compldefMathlib.Topology.Sets.Closeds, function or constantWording
the complement of s (from the docstring)
English
Let $s$ be an element of $\operatorname{Closeds}$ applied to $x$. Then the complement of $s$ is an open of $x$.
TopologicalSpace.Closeds.complOrderIsodefMathlib.Topology.Sets.Closeds, function or constantWording
the complement order isomorphism of x (from the name)
English
Let $x$ be a set. Then the complement order isomorphism of $x$ is an order isomorphism of $\operatorname{Closeds}$ applied to $x$ and the set of order duals of the set of opens of $x$.
TopologicalSpace.Closeds.gidefMathlib.Topology.Sets.Closeds, function or constantEnglish
$\operatorname{gi}$ is a Galois insertion of $\operatorname{closure}$ and $\operatorname{instSetLike}$.
TopologicalSpace.Closeds.preimagedefMathlib.Topology.Sets.Closeds, function or constantWording
the preimage of s and hf (from the docstring)
English
Let $s$ be an element of $\operatorname{Closeds}$ applied to $x_{1}$. Assume that $f$ is continuous. Then the preimage of $s$ and $\mathrm{hf}$ is an element of $\operatorname{Closeds}$ applied to $x$.
TopologicalSpace.IrreducibleClosedsstructureMathlib.Topology.Sets.Closeds, typeEnglish
Let $x$ be a set. Then the elements of $\operatorname{IrreducibleCloseds}$ applied to $x$ are a basic type.
TopologicalSpace.IrreducibleCloseds.carrierdefMathlib.Topology.Sets.Closeds, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{IrreducibleCloseds}$ applied to $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopologicalSpace.IrreducibleCloseds.equivSubtypedefMathlib.Topology.Sets.Closeds, function or constantWording
the equivalence subtype (from the name)
English
The equivalence subtype is an element of $\EquivMACRoAE {\operatorname{IrreducibleCloseds} (x)}{(\SubtypeSet {x_{2}}{\mathrm{and} (\mathrm{IsIrreducible} (x_{2}), \mathrm{IsClosed} (x_{2}))})}$.
TopologicalSpace.IrreducibleCloseds.equivSubtype'defMathlib.Topology.Sets.Closeds, function or constantWording
the equivalence subtype (from the name)
English
The equivalence subtype is an element of $\EquivMACRoAE {\operatorname{IrreducibleCloseds} (x)}{(\SubtypeSet {x_{2}}{\mathrm{and} (\mathrm{IsClosed} (x_{2}), \mathrm{IsIrreducible} (x_{2}))})}$.
TopologicalSpace.IrreducibleCloseds.mapdefMathlib.Topology.Sets.Closeds, function or constantWording
the map of f and c (from the name)
English
Let $f$ be a continuous function from elements of $x_{1}$ to elements of $x$. Let $c$ be an element of $\operatorname{IrreducibleCloseds}$ applied to $x_{1}$. Then the map of $f$ and $c$ is an element of $\operatorname{IrreducibleCloseds}$ applied to $x$.
TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbeddingdefMathlib.Topology.Sets.Closeds, function or constantWording
the order isomorphism of f and h (from the name)
English
Let $f$ be a function from elements of $x_{1}$ to elements of $x$ such that $f$ is an open embedding. Then the order isomorphism of $f$ and $h$ is an order isomorphism of $\operatorname{IrreducibleCloseds}$ applied to $x_{1}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $V$ to the proposition that the preimage of $f$ and $V$ is nonempty.
TopologicalSpace.IrreducibleCloseds.orderIsoSubtypedefMathlib.Topology.Sets.Closeds, function or constantWording
the order isomorphism subtype of x (from the name)
English
Let $x$ be a set. Then the order isomorphism subtype of $x$ is an order isomorphism of $\operatorname{IrreducibleCloseds}$ applied to $x$ and $\SubtypeSet {x_{2}}{\mathrm{and} (\mathrm{IsIrreducible} (x_{2}), \mathrm{IsClosed} (x_{2}))}$ defined as the order isomorphism of the equivalence subtype.
TopologicalSpace.IrreducibleCloseds.orderIsoSubtype'defMathlib.Topology.Sets.Closeds, function or constantWording
the order isomorphism subtype of x (from the name)
English
Let $x$ be a set. Then the order isomorphism subtype of $x$ is an order isomorphism of $\operatorname{IrreducibleCloseds}$ applied to $x$ and $\SubtypeSet {x_{2}}{\mathrm{and} (\mathrm{IsClosed} (x_{2}), \mathrm{IsIrreducible} (x_{2}))}$ defined as the order isomorphism of the equivalence subtype.
TopologicalSpace.Opens.compldefMathlib.Topology.Sets.Closeds, function or constantWording
the complement of s (from the docstring)
English
Let $s$ be an open of $x$. Then the complement of $s$ is an element of $\operatorname{Closeds}$ applied to $x$.
TopologicalSpace.Opens.complOrderIsodefMathlib.Topology.Sets.Closeds, function or constantWording
the complement order isomorphism of x (from the name)
English
Let $x$ be a set. Then the complement order isomorphism of $x$ is an order isomorphism of the set of opens of $x$ and the set of order duals of $\operatorname{Closeds}$ applied to $x$.
IsCompactOpenCovereddefMathlib.Topology.Sets.CompactOpenCovered, predicateEnglish
Let $f$ be a function from elements $i$ of $x$ and elements of $X$ applied to $i$ to elements of $S$. Let $U$ be an element of $\wp S$. Then $\mathrm{IsCompactOpenCovered}$ holds for $i$, $f$ and $U$, if there exists an element $s$ of $\wp x$, such that there exists an element $h$ of $\operatorname{Finite}$ applied to $s$, such that there exists a function $V$ from elements $i_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i_{2}}$ to opens of $X$ applied to $i_{2}$, such that for all elements $i$ of $x$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{i}$, the carrier of $V$ applied to $i$ and $h_{1}$ is compact and the union of the function that maps $i_{1}$ to the union of the function that maps $h_{2}$ to the image of $i$ applied to $i_{1}$ and $V$ applied to $i_{1}$ and $h_{2}$ is equal to $f$.
TopologicalSpace.CompactOpensstructureMathlib.Topology.Sets.Compacts, typeWording
compact open of x (from the name)
English
Let $x$ be a set. Then the compact opens of $x$ are a basic type.
TopologicalSpace.CompactOpens.mapdefMathlib.Topology.Sets.Compacts, function or constantWording
the map of f and #4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is continuous and $f$ is an open map. Let $s$ be a compact open of $x$. Then the map of $f$ and $s$ is a compact open of $x_{1}$.
TopologicalSpace.CompactOpens.toClopensdefMathlib.Topology.Sets.Compacts, function or constantWording
the clopen of s (from the name)
English
Let $s$ be a compact open of $x$. Then the clopen of $s$ is a clopen of $x$.
TopologicalSpace.CompactOpens.toOpensdefMathlib.Topology.Sets.Compacts, function or constantWording
the open of s (from the name)
English
Let $s$ be a compact open of $x$. Then the open of $s$ is an open of $x$ defined as $\operatorname{mk}$ applied to $s$ and $\operatorname{isOpen}$ applied to $s$.
TopologicalSpace.CompactsstructureMathlib.Topology.Sets.Compacts, typeWording
compact of x (from the name)
English
Let $x$ be a set. Then the compacts of $x$ are a basic type.
TopologicalSpace.Compacts.carrierdefMathlib.Topology.Sets.Compacts, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a compact of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopologicalSpace.Compacts.compactNhdsdefMathlib.Topology.Sets.Compacts, function or constantWording
the compact neighbourhood filter of K (from the name)
English
Let $K$ be a compact of $x$. Then the compact neighbourhood filter of $K$ is an element of the power set of the set of compacts of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{K'}$ to the proposition that for all elements $x_{2}$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {K}{x_{3}})}$, $\mathrm{K'}$ is an element of the neighbourhood filter of $x_{2}$.
TopologicalSpace.Compacts.compactNhdsMkOfOpensdefMathlib.Topology.Sets.Compacts, function or constantWording
the compact neighbourhood filter of L and U (from the name)
English
Let $L$ be a compact of $x$. Let $U$ be an open of $x$ such that $K \leq U \leq L$. Then the compact neighbourhood filter of $L$ and $U$ is an element of the compact neighbourhood filter of $K$ defined as $L$.
TopologicalSpace.Compacts.compactsInsideOfOpenNhdsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $U$ be an element of the open neighbourhood filter of $K$. Then $\operatorname{compactsInsideOfOpenNhds}$ applied to $U$ is an element of $\operatorname{compactsInside}$ applied to $U$ defined as $K$.
TopologicalSpace.Compacts.equivdefMathlib.Topology.Sets.Compacts, function or constantWording
the equivalence of f (from the name)
English
Let $f$ be a homeomorphism of $x$ and $x_{1}$. Then the equivalence of $f$ is an equivalence from the set of compacts of $x$ to the set of compacts of $x_{1}$.
TopologicalSpace.Compacts.mapdefMathlib.Topology.Sets.Compacts, function or constantWording
the map of f and K (from the name)
English
Let $f$ be a continuous function from elements of $x$ to elements of $x_{1}$. Let $K$ be a compact of $x$. Then the map of $f$ and $K$ is a compact of $x_{1}$.
TopologicalSpace.Compacts.openNhdsdefMathlib.Topology.Sets.Compacts, function or constantWording
the open neighbourhood filter of K (from the name)
English
Let $K$ be a compact of $x$. Then the open neighbourhood filter of $K$ is an element of the power set of the set of opens of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $U$ to $\mathrm{Leq} (K , U)$.
TopologicalSpace.Compacts.openRcNhdsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $K$ be a compact of $x$. Then $\operatorname{openRcNhds}$ applied to $K$ is an element of the power set of the set of opens of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $U$ to the proposition that the closure of $U$ is compact and $K \leq U$.
TopologicalSpace.Compacts.openRcNhdsToCompactNhdsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $K$ be a compact of $x$. Let $x_{2}$ be an element of $\operatorname{openRcNhds}$ applied to $K$. Then $\operatorname{openRcNhdsToCompactNhds}$ applied to $K$ and $x_{2}$ is an element of the compact neighbourhood filter of $K$.
TopologicalSpace.Compacts.openRcNhdsToOpenNhdsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $K$ be a compact of $x$. Let $x_{2}$ be an element of $\operatorname{openRcNhds}$ applied to $K$. Then $\operatorname{openRcNhdsToOpenNhds}$ applied to $K$ and $x_{2}$ is an element of the open neighbourhood filter of $K$ defined as $x_{2}$.
TopologicalSpace.Compacts.toClosedsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $s$ be a compact of $x$. Then $\operatorname{toCloseds}$ applied to $s$ is an element of $\operatorname{Closeds}$ applied to $x$.
TopologicalSpace.NonemptyCompactsstructureMathlib.Topology.Sets.Compacts, typeWording
nonempty compact of x (from the name)
English
Let $x$ be a set. Then the nonempty compacts of $x$ are a basic type.
TopologicalSpace.NonemptyCompacts.mapdefMathlib.Topology.Sets.Compacts, function or constantWording
the map of f and K (from the name)
English
Let $f$ be a continuous function from elements of $x$ to elements of $x_{1}$. Let $K$ be a nonempty compact of $x$. Then the map of $f$ and $K$ is a nonempty compact of $x_{1}$.
TopologicalSpace.NonemptyCompacts.toClosedsdefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $s$ be a nonempty compact of $x$. Then $\operatorname{toCloseds}$ applied to $s$ is an element of $\operatorname{Closeds}$ applied to $x$.
TopologicalSpace.NonemptyCompacts.toCompactsOrderEmbeddingdefMathlib.Topology.Sets.Compacts, function or constantWording
the compact order embedding (from the name)
English
The compact order embedding is an order embedding of the set of nonempty compacts of $x$ and the set of compacts of $x$.
TopologicalSpace.Opens.compactsInsidedefMathlib.Topology.Sets.Compacts, function or constantEnglish
Let $U$ be an open of $x$. Then $\operatorname{compactsInside}$ applied to $U$ is an element of the power set of the set of compacts of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $K$ to $\mathrm{Leq} (K , U)$.
TopologicalSpace.Opens.openNhdsOfCompactsInsidedefMathlib.Topology.Sets.Compacts, function or constantWording
the open neighbourhood filter of K (from the name)
English
Let $K$ be an element of $\operatorname{compactsInside}$ applied to $U$. Then the open neighbourhood filter of $K$ is an element of the open neighbourhood filter of $K$ defined as $U$.
TopologicalSpace.PositiveCompactsstructureMathlib.Topology.Sets.Compacts, typeWording
positive compact of x (from the name)
English
Let $x$ be a set. Then the positive compacts of $x$ are a basic type.
TopologicalSpace.PositiveCompacts.mapdefMathlib.Topology.Sets.Compacts, function or constantWording
the map of f and #4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $f$ is continuous and $f$ is an open map. Let $K$ be a positive compact of $x$. Then the map of $f$ and $K$ is a positive compact of $x_{1}$.
TopologicalSpace.PositiveCompacts.toNonemptyCompactsdefMathlib.Topology.Sets.Compacts, function or constantWording
the nonempty compact of s (from the name)
English
Let $s$ be a positive compact of $x$. Then the nonempty compact of $s$ is a nonempty compact of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{toCompacts}$ applied to $s$ and $\operatorname{nonempty}$ applied to $s$.
TopologicalSpace.IsOpenCoverdefMathlib.Topology.Sets.OpenCover, predicateWording
u is a open cover (from the name)
English
Let $u$ be a function from elements of $x$ to opens of $X$. Then $u$ is an open cover, if the supremum of $u$ is equal to the top.
Homeomorph.opensCongrdefMathlib.Topology.Sets.Opens, function or constantWording
the open congruence of f (from the name)
English
Let $f$ be a homeomorphism of $x$ and $x_{1}$. Then the open congruence of $f$ is an order isomorphism of the set of opens of $x$ and the set of opens of $x_{1}$.
TopologicalSpace.OpenNhdsOfstructureMathlib.Topology.Sets.Opens, typeEnglish
Let $x_{2}$ be an element of $x$. Then the elements of $\operatorname{OpenNhdsOf}$ applied to $x_{2}$ are a basic type.
TopologicalSpace.OpenNhdsOf.comapdefMathlib.Topology.Sets.Opens, function or constantWording
the preimage of f and x4 (from the name)
English
Let $f$ be a continuous map of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the preimage of $f$ and $x_{4}$ is a lattice homomorphism of $\operatorname{OpenNhdsOf}$ applied to $f$ applied to $x_{4}$ and $\operatorname{OpenNhdsOf}$ applied to $x_{4}$.
TopologicalSpace.OpensstructureMathlib.Topology.Sets.Opens, typeWording
open of x (from the name)
English
Let $x$ be a set. Then the opens of $x$ are a basic type.
TopologicalSpace.Opens.IsBasisdefMathlib.Topology.Sets.Opens, predicateWording
B is a basis (from the name)
English
Let $B$ be an element of the power set of the set of opens of $x$. Then $B$ is a basis, if the image of $\operatorname{instSetLike}$ and $B$ is a topological basis.
TopologicalSpace.Opens.carrierdefMathlib.Topology.Sets.Opens, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be an open of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopologicalSpace.Opens.comapdefMathlib.Topology.Sets.Opens, function or constantWording
the preimage of f (from the docstring)
English
Let $f$ be a continuous map of $x$ and $x_{1}$. Then the preimage of $f$ is a frame homomorphism of the set of opens of $x_{1}$ and the set of opens of $x$.
TopologicalSpace.Opens.frameHomdefMathlib.Topology.Sets.Opens, function or constantWording
the frame homomorphism (from the name)
English
The frame homomorphism is a frame homomorphism of the set of opens of $x$ and $\wp x$.
TopologicalSpace.Opens.gidefMathlib.Topology.Sets.Opens, function or constantEnglish
$\operatorname{gi}$ is a Galois coinsertion of $\operatorname{instSetLike}$ and $\operatorname{interior}$.
TopologicalSpace.Opens.inclusiondefMathlib.Topology.Sets.Opens, function or constantWording
the inclusion of h and x2 (from the name)
English
Assume that $U \leq V$. Let $x_{2}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$. Then the inclusion of $h$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {V}{x_{3}})}$ defined as the inclusion of $h$ and $x_{2}$.
TopologicalSpace.Opens.interiordefMathlib.Topology.Sets.Opens, function or constantWording
the interior of s (from the docstring)
English
Let $s$ be an element of $\wp x$. Then the interior of $s$ is an open of $x$ defined as $\operatorname{mk}$ applied to the interior of $s$ and $\mathrm{isOpen\_interior}$.
ClopenUpperSetstructureMathlib.Topology.Sets.Order, typeWording
clopen upper set of x (from the name)
English
Let $x$ be a set. Then the clopen upper sets of $x$ are a basic type.
ClopenUpperSet.toUpperSetdefMathlib.Topology.Sets.Order, function or constantWording
the upper set of s (from the name)
English
Let $s$ be a clopen upper set of $x$. Then the upper set of $s$ is a upper set of $x$ defined as $\operatorname{mk}$ applied to $s$ and $\operatorname{upper}$ applied to $s$.
Alexandrov.generatordefMathlib.Topology.Sheaves.Alexandrov, function or constantWording
the generator of U (from the name)
English
Let $U$ be an open of $X$. Then the generator of $U$ is a functor of the set of structured arrows of $\operatorname{op}$ applied to $U$ and $\operatorname{principals}$ applied to $X$ and $X$ defined as the projection of $\operatorname{op}$ applied to $U$ and $\operatorname{principals}$ applied to $X$.
Alexandrov.isLimitdefMathlib.Topology.Sheaves.Alexandrov, function or constantEnglish
Let $F$ be a functor of the set of carriers of $X$ and $C$. Let $x_{2}$ be a set. Let $\mathrm{Us}$ be a function from elements of $x_{2}$ to opens of the set of carriers of $X$. Then $\operatorname{isLimit}$ applied to $F$, $x_{2}$ and $\mathrm{Us}$ is an element of $\operatorname{IsLimit}$ applied to the map cone of the principal Kan extension of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $\mathrm{Us}$.
Alexandrov.lowerConedefMathlib.Topology.Sheaves.Alexandrov, function or constantWording
the lower cone of Us and S (from the name)
English
Let $\mathrm{Us}$ be a function from elements of $x_{3}$ to opens of $X$. Let $S$ be a cone of the composition of the opposite of the inclusion of the function that maps $V$ to the proposition that there exists an element $i$ of $x_{3}$, such that $V \leq \mathrm{Us} (i)$ and the principal Kan extension of $F$. Then the lower cone of $\mathrm{Us}$ and $S$ is a cone of the composition of the generator of the supremum of $\mathrm{Us}$ and $F$.
Alexandrov.principalOpendefMathlib.Topology.Sheaves.Alexandrov, function or constantWording
the principal open of x2 (from the name)
English
Let $x_{2}$ be an element of $X$. Then the principal open of $x_{2}$ is an open of $X$.
Alexandrov.principalsdefMathlib.Topology.Sheaves.Alexandrov, function or constantEnglish
Let $X$ be a set. Then $\operatorname{principals}$ applied to $X$ is a functor of $X$ and the set of opposites of the set of opens of $X$.
Alexandrov.principalsKanExtensiondefMathlib.Topology.Sheaves.Alexandrov, function or constantWording
the principal Kan extension of F (from the name)
English
Let $F$ be a functor of $X$ and $C$. Then the principal Kan extension of $F$ is a functor of the set of opposites of the set of opens of $X$ and $C$ defined as the pointwise right Kan extension of $\operatorname{principals}$ applied to $X$ and $F$.
Alexandrov.projSupdefMathlib.Topology.Sheaves.Alexandrov, function or constantWording
the projection supremum of Us (from the name)
English
Let $\mathrm{Us}$ be a function from elements of $x_{2}$ to opens of $X$. Then the projection supremum of $\mathrm{Us}$ is a functor of the set of structured arrows of $\operatorname{op}$ applied to the supremum of $\mathrm{Us}$ and $\operatorname{principals}$ applied to $X$ and the set of opposites of $\operatorname{OpensLeCover}$ applied to $\mathrm{Us}$.
TopCat.Presheaf.SubmonoidPresheafstructureMathlib.Topology.Sheaves.CommRingCat, typeWording
submonoid presheaf of F (from the name)
English
Let $F$ be a presheaf of the set of categories of commutative rings and $X$. Then the submonoid presheafs of $F$ are a basic type.
TopCat.Presheaf.SubmonoidPresheaf.localizationPresheafdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the localization of G (from the docstring)
English
Let $G$ be a submonoid presheaf of $F$. Then the localization of $G$ is a presheaf of the set of categories of commutative rings and $X$.
TopCat.Presheaf.SubmonoidPresheaf.objdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the object of self and U (from the name)
English
Let $\mathrm{self}$ be a submonoid presheaf of $F$. Let $U$ be an opposite of the set of opens of the set of carriers of $X$. Then the object of $\mathrm{self}$ and $U$ is a submonoid of the set of carriers of the action of $F$ and $U$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $U$.
TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheafdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the map into the localization presheaf of G (from the docstring)
English
Let $G$ be a submonoid presheaf of $F$. Then the map into the localization presheaf of $G$ is a homomorphism of $F$ and the localization of $G$.
TopCat.Presheaf.submonoidPresheafOfStalkdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the submonoid presheaf of F and S (from the name)
English
Let $F$ be a presheaf of the set of categories of commutative rings and $X$. Let $S$ be a function from carriers $x$ of $X$ to submonoids of the set of carriers of the stalk of $F$ and $x$. Then the submonoid presheaf of $F$ and $x$ is a submonoid presheaf of $F$.
TopCat.Presheaf.toTotalQuotientPresheafdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the map into the presheaf of total quotient rings of F (from the docstring)
English
Let $F$ be a presheaf of the set of categories of commutative rings and $X$. Then the map into the presheaf of total quotient rings of $F$ is a homomorphism of $F$ and the localization of $F$ defined as the map into the localization presheaf of the submonoid presheaf of $F$ and the function that maps $x$ to the non zero divisor of the set of carriers of the stalk of $F$ and $x$.
TopCat.Presheaf.totalQuotientPresheafdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the localization of F (from the docstring)
English
Let $F$ be a presheaf of the set of categories of commutative rings and $X$. Then the localization of $F$ is a presheaf of the set of categories of commutative rings and $X$ defined as the localization of the submonoid presheaf of $F$ and the function that maps $x$ to the non zero divisor of the set of carriers of the stalk of $F$ and $x$.
TopCat.Sheaf.objSupIsoProdEqLocusdefMathlib.Topology.Sheaves.CommRingCat, function or constantEnglish
Let $F$ be a sheaf of the set of categories of commutative rings and $X$. Let $U$ and $V$ be opens of the set of carriers of $X$. Then $\operatorname{objSupIsoProdEqLocus}$ applied to $F$, $U$ and $V$ is an isomorphism of the action of the object of $F$ and $\operatorname{op}$ applied to $\MaxmaxMACRoAF {U}{V}$ and $\operatorname{of}$ applied to $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{eqLocus} (\operatorname{comp} (\operatorname{hom} (\operatorname{map} (\operatorname{obj} (F), \operatorname{op} (\operatorname{homOfLE} (\mathrm{inf\_le\_left})))), \operatorname{fst} (\operatorname{carrier} (\operatorname{obj} (\operatorname{obj} (F), \operatorname{op} (U))), \operatorname{carrier} (\operatorname{obj} (\operatorname{obj} (F), \operatorname{op} (V))))), \operatorname{comp} (\operatorname{hom} (\operatorname{map} (\operatorname{obj} (F), \operatorname{op} (\operatorname{homOfLE} (\mathrm{inf\_le\_right})))), \operatorname{snd} (\operatorname{carrier} (\operatorname{obj} (\operatorname{obj} (F), \operatorname{op} (U))), \operatorname{carrier} (\operatorname{obj} (\operatorname{obj} (F), \operatorname{op} (V))))))}{x})}$.
TopCat.commRingYonedadefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the commutative ring Yoneda (from the name)
English
The commutative ring Yoneda is a functor of the set of top commutative ring categories and the set of functors of the set of opposites of the set of topological categories and the set of categories of commutative rings.
TopCat.continuousFunctionsdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the continuous function of X and R (from the name)
English
Let $X$ be an opposite of the set of topological categories. Let $R$ be a top commutative ring category. Then the continuous function of $X$ and $R$ is a category of commutative rings defined as $\operatorname{of}$ applied to the set of homomorphisms of the opposite of $X$ and the action of the forgetful functor of the set of top commutative ring categories and the set of topological categories and $R$.
TopCat.continuousFunctions.mapdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the map of X and x (from the name)
English
Let $X$ be an opposite of the set of topological categories. Let $x$ be a homomorphism of $R$ and $S$. Then the map of $X$ and $x$ is a homomorphism of the continuous function of $X$ and $R$ and the continuous function of $X$ and $S$.
TopCat.continuousFunctions.pullbackdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the pullback of f and R (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $R$ be a top commutative ring category. Then the pullback of $f$ and $R$ is a homomorphism of the continuous function of $X$ and $R$ and the continuous function of $Y$ and $R$.
TopCat.presheafToTopCommRingdefMathlib.Topology.Sheaves.CommRingCat, function or constantWording
the presheaf to top commutative ring of X and T (from the name)
English
Let $X$ be a topological category. Let $T$ be a top commutative ring category. Then the presheaf to top commutative ring of $X$ and $T$ is a presheaf of the set of categories of commutative rings and $X$ defined as the composition of the opposite of the topological category of $X$ and the action of the commutative ring Yoneda and $T$.
TopCat.Presheaf.EtaleSpacestructureMathlib.Topology.Sheaves.EtaleSpace, typeWording
etale space of F (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Then the etale spaces of $F$ are a basic type.
TopCat.Presheaf.EtaleSpace.basedefMathlib.Topology.Sheaves.EtaleSpace, function or constantWording
the base point of self (from the docstring)
English
Let $\mathrm{self}$ be an etale space of $F$. Then the base point of $\mathrm{self}$ is a carrier of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
TopCat.Presheaf.EtaleSpace.germdefMathlib.Topology.Sheaves.EtaleSpace, function or constantWording
the germ of self (from the name)
English
Let $\mathrm{self}$ be an etale space of $F$. Then the germ of $\mathrm{self}$ is a type of the stalk of $F$ and the base point of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
TopCat.Presheaf.EtaleSpace.homeomorphdefMathlib.Topology.Sheaves.EtaleSpace, function or constantWording
the homeomorphism of U and x3 (from the name)
English
Let $U$ be an open of the set of carriers of $X$ such that for all carriers $x_{5}$ of $X$, for all elements $\mathrm{hx1}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {U}{x_{5}}$, $\operatorname{coe}$ applied to the homomorphism of the germ of $U$ and $x_{5}$ is bijective. Let $x_{3}$ be a carrier of $X$ such that $x_{3}$ is an element of $U$. Then the homeomorphism of $U$ and $x_{3}$ is a homeomorphism of the set of elements of the preimage of $\operatorname{base}$ and $U$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {U}{x_{4}})}$ and $\mathrm{WithDiscreteTopology}$ applied to the set of types of the stalk of $F$ and $x_{3}$.
TopCat.Presheaf.IsFlasqueclassMathlib.Topology.Sheaves.Flasque, predicateEnglish
Let $F$ be a presheaf of $C$ and $X$. Then we can say that $\operatorname{IsFlasque}$ holds for $F$.
TopCat.Sheaf.IsFlasquedefMathlib.Topology.Sheaves.Flasque, predicateEnglish
Let $F$ be a sheaf of $C$ and $X$. Then $\operatorname{IsFlasque}$ holds for $F$, if $\operatorname{IsFlasque}$ holds for the object of $F$.
TopCat.Sheaf.IsFlasque.UnderdefMathlib.Topology.Sheaves.Flasque, typeEnglish
Let $g$ be a homomorphism of $F$ and $G$. Let $s$ be a carrier of the action of the object of $G$ and $\operatorname{op}$ applied to $U$. Then an element of $\operatorname{Under}$ applied to $g$ and $s$ is an element of the function that maps $g$ and $s$ to the set of structured arrows of the element of $\operatorname{op}$ applied to $U$ and $s$ and the map element of the right whisker of the homomorphism of $g$ and the forgetful functor of the set of additive commutative group categories.
TopCat.Sheaf.pullbackdefMathlib.Topology.Sheaves.Functors, function or constantWording
the pullback functor of A and f (from the docstring)
English
Let $A$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback functor of $A$ and $f$ is a functor of the set of sheaves of $A$ and $Y$ and the set of sheaves of $A$ and $X$ defined as the sheaf pullback of the Grothendieck topology of the set of carriers of $Y$ and the Grothendieck topology of the set of carriers of $X$.
TopCat.Sheaf.pullbackIsodefMathlib.Topology.Sheaves.Functors, function or constantWording
the pullback of A and f (from the docstring)
English
Let $A$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $A$ and $f$ is an isomorphism of the pullback functor of $A$ and $f$ and the composition of $\operatorname{forget}$ applied to $A$ and $Y$ and the composition of the pullback of $A$ and $f$ and the presheaf to sheaf of the Grothendieck topology of the set of carriers of $X$ and $A$ defined as the sheaf pullback isomorphism of the Grothendieck topology of the set of carriers of $Y$ and the Grothendieck topology of the set of carriers of $X$.
TopCat.Sheaf.pullbackPushforwardAdjunctiondefMathlib.Topology.Sheaves.Functors, function or constantWording
the pullback pushforward adjunction of A and f (from the name)
English
Let $A$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback pushforward adjunction of $A$ and $f$ is an adjunction of the pullback functor of $A$ and $f$ and the pushforward functor of $A$ and $f$ defined as $\operatorname{sheafAdjunctionContinuous}$ applied to the map of $f$, $A$, the Grothendieck topology of the set of carriers of $Y$ and the Grothendieck topology of the set of carriers of $X$.
TopCat.Sheaf.pushforwarddefMathlib.Topology.Sheaves.Functors, function or constantWording
the pushforward functor of C and f (from the docstring)
English
Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pushforward functor of $C$ and $f$ is a functor of the set of sheaves of $C$ and $X$ and the set of sheaves of $C$ and $Y$ defined as $\operatorname{sheafPushforwardContinuous}$ applied to the map of $f$, $C$, the Grothendieck topology of the set of carriers of $Y$ and the Grothendieck topology of the set of carriers of $X$.
TopCat.Sheaf.pushforwardForgetIsodefMathlib.Topology.Sheaves.Functors, function or constantEnglish
Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{pushforwardForgetIso}$ applied to $C$ and $f$ is an isomorphism of the composition of the pushforward functor of $C$ and $f$ and $\operatorname{forget}$ applied to $C$ and $Y$ and the composition of $\operatorname{forget}$ applied to $C$ and $X$ and the pushforward functor of $C$ and $f$ defined as the identity of the composition of the pushforward functor of $C$ and $f$ and $\operatorname{forget}$ applied to $C$ and $Y$.
Topology.IsOpenEmbedding.sheafPullbackdefMathlib.Topology.Sheaves.Functors, function or constantWording
the sheaf pullback of A and hf (from the name)
English
Let $A$ be a set. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the sheaf pullback of $A$ and $\mathrm{hf}$ is a functor of the set of sheaves of $A$ and $Y$ and the set of sheaves of $A$ and $X$ defined as $\operatorname{sheafPushforwardContinuous}$ applied to the functor of $\mathrm{hf}$, $A$, the Grothendieck topology of the set of carriers of $X$ and the Grothendieck topology of the set of carriers of $Y$.
Topology.IsOpenEmbedding.sheafPullbackIsodefMathlib.Topology.Sheaves.Functors, function or constantWording
the pullback of A and hf (from the docstring)
English
Let $A$ be a set. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the pullback of $A$ and $\mathrm{hf}$ is an isomorphism of the pullback functor of $A$ and $f$ and the sheaf pullback of $A$ and $\mathrm{hf}$.
TopCat.LocalPredicatestructureMathlib.Topology.Sheaves.LocalPredicate, typeWording
local predicate of T (from the name)
English
Let $T$ be a function from carriers of $X$ to sets. Then the local predicates of $T$ are a basic type.
TopCat.LocalPredicate.anddefMathlib.Topology.Sheaves.LocalPredicate, function or constantEnglish
Let $P$ and $Q$ be local predicates of $T$. Then $\operatorname{and}$ applied to $P$ and $Q$ is a local predicate of $T$.
TopCat.PrelocalPredicatestructureMathlib.Topology.Sheaves.LocalPredicate, typeWording
prelocal predicate of T (from the name)
English
Let $T$ be a function from carriers of $X$ to sets. Then the prelocal predicates of $T$ are a basic type.
TopCat.PrelocalPredicate.anddefMathlib.Topology.Sheaves.LocalPredicate, function or constantEnglish
Let $P$ and $Q$ be prelocal predicates of $T$. Then $\operatorname{and}$ applied to $P$ and $Q$ is a prelocal predicate of $T$.
TopCat.PrelocalPredicate.preddefMathlib.Topology.Sheaves.LocalPredicate, predicateEnglish
Let $\mathrm{self}$ be a prelocal predicate of $T$. Let $x$ be a function from elements $x_{1}$ of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {U}{x_{2}})}$ to elements of $T$ applied to $x_{1}$. Then $\operatorname{pred}$ holds for $\mathrm{self}$, $x_{1}$ and $x$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$ and $x$.
TopCat.PrelocalPredicate.sheafifydefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the sheafification of P (from the name)
English
Let $P$ be a prelocal predicate of $T$. Then the sheafification of $P$ is a local predicate of $T$.
TopCat.continuousLocaldefMathlib.Topology.Sheaves.LocalPredicate, function or constantEnglish
Let $X$ be a topological category. Let $T$ be a set. Then $\operatorname{continuousLocal}$ applied to $X$ and $T$ is a local predicate of the function that maps $x_{1}$ to $T$.
TopCat.continuousPrelocaldefMathlib.Topology.Sheaves.LocalPredicate, function or constantEnglish
Let $X$ be a topological category. Let $T$ be a set. Then $\operatorname{continuousPrelocal}$ applied to $X$ and $T$ is a prelocal predicate of the function that maps $x_{1}$ to $T$.
TopCat.isSectiondefMathlib.Topology.Sheaves.LocalPredicate, function or constantEnglish
Let $p$ be a function from elements of $T$ to carriers of $X$. Then $\operatorname{isSection}$ applied to $p$ is a local predicate of the function that maps $x$ to $T$.
TopCat.sheafToTopdefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the sheaf to top of T (from the name)
English
Let $T$ be a topological category. Then the sheaf to top of $T$ is a sheaf of the set of sets and $X$.
TopCat.stalkToFiberdefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the stalk to fiber of P and x (from the name)
English
Let $P$ be a local predicate of $T$. Let $x$ be a carrier of $X$. Then the stalk to fiber of $P$ and $x$ is a homomorphism of the stalk of the underlying presheaf of the subsheaf to type of $P$ and $x$ and $T$ applied to $x$ defined as $\operatorname{desc}$ applied to the composition of the opposite of the inclusion of $x$ and the subpresheaf to type of $\operatorname{toPrelocalPredicate}$ applied to $P$ and $\operatorname{cocone}$ applied to $P$ and $x$.
TopCat.subpresheafContinuousPrelocalIsoPresheafToTopdefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the subpresheaf continuous prelocal isomorphism presheaf to top of T (from the name)
English
Let $T$ be a topological category. Then the subpresheaf continuous prelocal isomorphism presheaf to top of $T$ is an isomorphism of the subpresheaf to type of $\operatorname{continuousPrelocal}$ applied to $X$ and the set of carriers of $T$ and the presheaf to top of $X$ and $T$.
TopCat.subpresheafToTypesdefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the subpresheaf to type of P (from the name)
English
Let $P$ be a prelocal predicate of $T$. Then the subpresheaf to type of $P$ is a presheaf of the set of sets and $X$.
TopCat.subpresheafToTypes.subtypedefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the subtype of P (from the name)
English
Let $P$ be a prelocal predicate of $T$. Then the subtype of $P$ is a homomorphism of the subpresheaf to type of $P$ and the presheaf to type of $X$ and $T$.
TopCat.subsheafToTypesdefMathlib.Topology.Sheaves.LocalPredicate, function or constantWording
the subsheaf to type of P (from the name)
English
Let $P$ be a local predicate of $T$. Then the subsheaf to type of $P$ is a sheaf of the set of sets and $X$ defined as $\operatorname{mk}$ applied to the subpresheaf to type of $\operatorname{toPrelocalPredicate}$ applied to $P$ and $\operatorname{isSheaf}$ applied to $P$.
TopCat.Presheaf.IsLocallySurjectivedefMathlib.Topology.Sheaves.LocallySurjective, predicateWording
T is locally surjective (from the name)
English
generation took over the time limit
Opens.mayerVietorisSquaredefMathlib.Topology.Sheaves.MayerVietoris, function or constantEnglish
Let $U$ and $V$ be opens of $T$. Then $\operatorname{mayerVietorisSquare}$ applied to $U$ and $V$ is an element of $\operatorname{MayerVietorisSquare}$ applied to the Grothendieck topology of $T$.
Opens.mayerVietorisSquare'defMathlib.Topology.Sheaves.MayerVietoris, function or constantEnglish
Let $\mathrm{sq}$ be a square of the set of opens of $T$ such that $\EqtMACRoH {\mathrm{CategoryTheory\_\_Square\_\_X\_u2084\_} (\mathrm{sq})}{\MaxmaxMACRoAF {\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_} (\mathrm{sq})}{\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_} (\mathrm{sq})}}$ and $\EqtMACRoH {\mathrm{CategoryTheory\_\_Square\_\_X\_u2081\_} (\mathrm{sq})}{\MinminMACRoAG {\mathrm{CategoryTheory\_\_Square\_\_X\_u2082\_} (\mathrm{sq})}{\mathrm{CategoryTheory\_\_Square\_\_X\_u2083\_} (\mathrm{sq})}}$. Then $\operatorname{mayerVietorisSquare'}$ applied to $\mathrm{sq}$, $h$ and $h_{1}$ is an element of $\operatorname{MayerVietorisSquare}$ applied to the Grothendieck topology of $T$.
TopologicalSpace.Opens.sheafOfModulesEquivOverdefMathlib.Topology.Sheaves.Module, function or constantWording
the sheaf of U and R (from the name)
English
Let $U$ be an open of the set of carriers of $X$. Let $R$ be a sheaf of the set of categories of rings and $X$. Then the sheaf of $U$ and $R$ is an equivalence of the set of sheaves of module of $\operatorname{over}$ applied to $R$ and $U$ and the set of sheaves of module of the action of the restriction functor of $U$ and $R$.
TopologicalSpace.Opens.sheafOfModulesEquivOverInverseUnitdefMathlib.Topology.Sheaves.Module, function or constantWording
the sheaf of U and R (from the name)
English
Let $U$ be an open of the set of carriers of $X$. Let $R$ be a sheaf of the set of categories of rings and $X$. Then the sheaf of $U$ and $R$ is an isomorphism of the action of the inverse of the sheaf of $U$ and $R$ and the unit of the action of the restriction functor of $U$ and $R$ and the unit of $\operatorname{over}$ applied to $R$ and $U$ defined as the composition of the map isomorphism of the inverse of the sheaf of $U$ and $R$ and the inverse of the sheaf of $U$ and $R$ and the inverse of the application of the unit isomorphism of the sheaf of $U$ and $R$ and the unit of $\operatorname{over}$ applied to $R$ and $U$.
TopologicalSpace.Opens.sheafOfModulesEquivOverUnitdefMathlib.Topology.Sheaves.Module, function or constantWording
the sheaf of U and R (from the name)
English
Let $U$ be an open of the set of carriers of $X$. Let $R$ be a sheaf of the set of categories of rings and $X$. Then the sheaf of $U$ and $R$ is an isomorphism of the action of the functor of the sheaf of $U$ and $R$ and the unit of $\operatorname{over}$ applied to $R$ and $U$ and the unit of the action of the restriction functor of $U$ and $R$ defined as the identity of the action of the functor of the sheaf of $U$ and $R$ and the unit of $\operatorname{over}$ applied to $R$ and $U$.
TopologicalSpace.Opens.overEquivalencedefMathlib.Topology.Sheaves.Over, function or constantEnglish
Let $U$ be an open of $X$. Then $\operatorname{overEquivalence}$ applied to $U$ is an equivalence of $\operatorname{Over}$ applied to $U$ and the set of opens of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {U}{x_{1}})}$.
TopologicalSpace.Opens.overPullbackSheafEquivOverdefMathlib.Topology.Sheaves.Over, function or constantEnglish
Let $U$ be an open of the set of carriers of $X$. Then $\operatorname{overPullbackSheafEquivOver}$ applied to $U$ is an isomorphism of the composition of $\operatorname{overPullback}$ applied to the Grothendieck topology of the set of carriers of $X$, $A$ and $U$ and the functor of $\operatorname{sheafEquivOver}$ applied to $U$ and the restriction functor of $U$ defined as the identity of the composition of $\operatorname{overPullback}$ applied to the Grothendieck topology of the set of carriers of $X$, $A$ and $U$ and the functor of $\operatorname{sheafEquivOver}$ applied to $U$.
TopologicalSpace.Opens.sheafEquivOverdefMathlib.Topology.Sheaves.Over, function or constantEnglish
Let $U$ be an open of $X$. Then $\operatorname{sheafEquivOver}$ applied to $U$ is an equivalence of the set of sheaves of $\operatorname{over}$ applied to the Grothendieck topology of $X$ and $U$ and $A$ and the set of sheaves of the Grothendieck topology of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {U}{x_{2}})}$ and $A$ defined as the sheaf congruence of the Grothendieck topology of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {U}{x_{2}})}$ and $\operatorname{overEquivalence}$ applied to $U$.
TopologicalSpace.Opens.sheafRestrictSheafEquivOverdefMathlib.Topology.Sheaves.Over, function or constantEnglish
Let $U$ be an open of the set of carriers of $X$. Then $\operatorname{sheafRestrictSheafEquivOver}$ applied to $U$ is an isomorphism of the composition of the restriction functor of $U$ and the inverse of $\operatorname{sheafEquivOver}$ applied to $U$ and $\operatorname{overPullback}$ applied to the Grothendieck topology of the set of carriers of $X$, $A$ and $U$ defined as the inverse of the isomorphism composition inverse of $\operatorname{overPullbackSheafEquivOver}$ applied to $U$.
Opens.pointGrothendieckTopologydefMathlib.Topology.Sheaves.Points, function or constantWording
the point Grothendieck topology of x1 (from the name)
English
Let $x_{1}$ be an element of $X$. Then the point Grothendieck topology of $x_{1}$ is a point of the Grothendieck topology of $X$.
Opens.pointGrothendieckTopologyHomEquivdefMathlib.Topology.Sheaves.Points, function or constantWording
the point Grothendieck topology homomorphism equivalence (from the name)
English
The point Grothendieck topology homomorphism equivalence is an equivalence from the set of homomorphisms of the point Grothendieck topology of $x_{1}$ and the point Grothendieck topology of $y$ to $\mathrm{Specializes}$ applied to $x_{1}$ and $y$.
Opens.pointsGrothendieckTopologydefMathlib.Topology.Sheaves.Points, function or constantWording
the point Grothendieck topology of X (from the name)
English
Let $X$ be a set. Then the point Grothendieck topology of $X$ is an object property of the set of points of the Grothendieck topology of $X$ defined as the object property of $\operatorname{pointGrothendieckTopology}$.
IsOpenMap.pullbackIsodefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback isomorphism of hf (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Then the pullback isomorphism of $\mathrm{hf}$ is an isomorphism of the pullback of $C$ and $f$ and the action of the left whiskering of the set of opposites of the set of opens of the set of carriers of $Y$ and $C$ and the opposite of the functor of $\mathrm{hf}$ defined as the natural isomorphism of $\operatorname{pullbackObjIso}$ applied to $\mathrm{hf}$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{IsOpenMap\_\_pullbackObjIso\_hom\_naturality}$ applied to $\mathrm{hf}$.
IsOpenMap.pullbackObjIsodefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback object isomorphism of hf and x1 (from the name)
English
Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open map. Let $x_{1}$ be a presheaf of $C$ and $Y$. Then the pullback object isomorphism of $\mathrm{hf}$ and $x_{1}$ is an isomorphism of the action of the pullback of $C$ and $f$ and $x_{1}$ and the composition of the opposite of the functor of $\mathrm{hf}$ and $x_{1}$.
TopCat.PresheafdefMathlib.Topology.Sheaves.Presheaf, typeWording
presheaf of C and X (from the name)
English
Let $C$ be a set. Let $X$ be a topological category. Then a presheaf of $C$ and $X$ is an element of the function that maps $C$ and $X$ to the set of functors of the set of opposites of the set of opens of the set of carriers of $X$ and $C$.
TopCat.Presheaf.Pushforward.compdefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the composition of g and x1 (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $x_{1}$ be a presheaf of $C$ and $X$. Then the composition of $g$ and $x_{1}$ is an isomorphism of the action of the pushforward functor of $C$ and the composition of $f$ and $g$ and $x_{1}$ and the action of the pushforward functor of $C$ and $g$ and the action of the pushforward functor of $C$ and $f$ and $x_{1}$ defined as the identity of the action of the pushforward functor of $C$ and the composition of $f$ and $g$ and $x_{1}$.
TopCat.Presheaf.Pushforward.iddefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the identity of x1 (from the name)
English
Let $x_{1}$ be a presheaf of $C$ and $X$. Then the identity of $x_{1}$ is an isomorphism of the action of the pushforward functor of $C$ and the identity morphism of $X$ and $x_{1}$ and $x_{1}$ defined as the identity of the action of the pushforward functor of $C$ and the identity morphism of $X$ and $x_{1}$.
TopCat.Presheaf.attrSheaf_restrictdefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
generation took over the time limit
TopCat.Presheaf.presheafEquivOfIsodefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the presheaf equivalence of C and H (from the name)
English
Let $C$ be a set. Let $H$ be an isomorphism of $X$ and $Y$. Then the presheaf equivalence of $C$ and $H$ is an equivalence of the set of presheafs of $C$ and $X$ and the set of presheafs of $C$ and $Y$ defined as the left congruence of the opposite of the inverse of the map map isomorphism of $H$.
TopCat.Presheaf.pullbackdefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback of C and f (from the name)
English
Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback of $C$ and $f$ is a functor of the set of presheafs of $C$ and $Y$ and the set of presheafs of $C$ and $X$ defined as $\operatorname{lan}$ applied to the opposite of the map of $f$.
TopCat.Presheaf.pullbackHomIsoPushforwardInvdefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback homomorphism isomorphism pushforward inverse of C and H (from the name)
English
Let $C$ be a set. Let $H$ be an isomorphism of $X$ and $Y$. Then the pullback homomorphism isomorphism pushforward inverse of $C$ and $H$ is an isomorphism of the pullback of $C$ and the homomorphism of $H$ and the pushforward functor of $C$ and the inverse of $H$ defined as $\operatorname{leftAdjointUniq}$ applied to the pullback pushforward adjunction of $C$ and the homomorphism of $H$ and the adjunction of the presheaf equivalence of $C$ and the inverse of $H$.
TopCat.Presheaf.pullbackInvIsoPushforwardHomdefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback inverse isomorphism pushforward homomorphism of C and H (from the name)
English
Let $C$ be a set. Let $H$ be an isomorphism of $X$ and $Y$. Then the pullback inverse isomorphism pushforward homomorphism of $C$ and $H$ is an isomorphism of the pullback of $C$ and the inverse of $H$ and the pushforward functor of $C$ and the homomorphism of $H$ defined as $\operatorname{leftAdjointUniq}$ applied to the pullback pushforward adjunction of $C$ and the inverse of $H$ and the adjunction of the presheaf equivalence of $C$ and $H$.
TopCat.Presheaf.pullbackObjObjOfImageOpendefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback object object of x1 and U (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Let $x_{1}$ be a presheaf of $C$ and $Y$. Let $U$ be an open of the set of carriers of $X$ such that the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $U$ is open. Then the pullback object object of $x_{1}$ and $U$ is an isomorphism of the action of the action of the pullback of $C$ and $f$ and $x_{1}$ and $\operatorname{op}$ applied to $U$ and the action of $x_{1}$ and $\operatorname{op}$ applied to $\operatorname{mk}$ applied to the image of $\operatorname{coe}$ applied to the homomorphism of $f$ and $U$ and $H$.
TopCat.Presheaf.pullbackPushforwardAdjunctiondefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pullback pushforward adjunction of C and f (from the name)
English
Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pullback pushforward adjunction of $C$ and $f$ is an adjunction of the pullback of $C$ and $f$ and the pushforward functor of $C$ and $f$ defined as $\operatorname{lanAdjunction}$ applied to the opposite of the map of $f$ and $C$.
TopCat.Presheaf.pushforwarddefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the pushforward functor of C and f (from the docstring)
English
Let $C$ be a set. Let $f$ be a homomorphism of $X$ and $Y$. Then the pushforward functor of $C$ and $f$ is a functor of the set of presheafs of $C$ and $X$ and the set of presheafs of $C$ and $Y$ defined as the action of the left whiskering of the set of opposites of the set of opens of the set of carriers of $X$ and $C$ and the opposite of the map of $f$.
TopCat.Presheaf.pushforwardEqdefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
Assume that $\EqtMACRoH {f}{g}$. Let $x_{1}$ be a presheaf of $C$ and $X$. Then $\operatorname{pushforwardEq}$ applied to $h$ and $x_{1}$ is an isomorphism of the action of the pushforward functor of $C$ and $f$ and $x_{1}$ and the action of the pushforward functor of $C$ and $g$ and $x_{1}$ defined as the right isomorphism whisker of the opposite of the inverse of the map isomorphism of $f$ and $g$ and $x_{1}$.
TopCat.Presheaf.pushforwardToOfIsodefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
Let $x_{1}$ be an isomorphism of $X$ and $Y$. Let $x_{4}$ be a homomorphism of $x_{2}$ and the action of the pushforward functor of $C$ and the homomorphism of $x_{1}$ and $x_{3}$. Then $\operatorname{pushforwardToOfIso}$ applied to $x_{1}$ and $x_{4}$ is a homomorphism of the action of the pushforward functor of $C$ and the inverse of $x_{1}$ and $x_{2}$ and $x_{3}$ defined as $\operatorname{symm}$ applied to the homomorphism equivalence of $x_{2}$ and $x_{3}$ and $x_{4}$.
TopCat.Presheaf.restrictdefMathlib.Topology.Sheaves.Presheaf, function or constantWording
the restriction of x3 and h (from the docstring)
English
Let $x_{3}$ be a type of the action of $F$ and $\operatorname{op}$ applied to $V$. Let $h$ be a homomorphism of $U$ and $V$. Then the restriction of $x_{3}$ and $h$ is a type of the action of $F$ and $\operatorname{op}$ applied to $U$ defined as $\operatorname{hom}$ applied to the map of $F$ and the opposite in $h$ and $x_{3}$.
TopCat.Presheaf.restrictOpendefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
Let $x_{3}$ be a type of the action of $F$ and $\operatorname{op}$ applied to $V$. Let $U$ be an open of the set of carriers of $X$ such that $\mathrm{autoParam}$ holds for $\mathrm{Leq} (U , V)$ and $\mathrm{TopCat\_\_Presheaf\_\_restrictOpen\_\_\_auto\_1}$. Then $\operatorname{restrictOpen}$ applied to $x_{3}$, $U$ and $e$ is a type of the action of $F$ and $\operatorname{op}$ applied to $U$ defined as the restriction of $x_{3}$ and the homomorphism of $e$.
TopCat.Presheaf.restrict_tacdefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
generation took over the time limit
TopCat.Presheaf.restrict_tac?defMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
generation took over the time limit
TopCat.Presheaf.toPushforwardOfIsodefMathlib.Topology.Sheaves.Presheaf, function or constantEnglish
Let $H$ be an isomorphism of $X$ and $Y$. Let $x_{3}$ be a homomorphism of the action of the pushforward functor of $C$ and the homomorphism of $H$ and $x_{1}$ and $x_{2}$. Then $\operatorname{toPushforwardOfIso}$ applied to $H$ and $x_{3}$ is a homomorphism of $x_{1}$ and the action of the pushforward functor of $C$ and the inverse of $H$ and $x_{2}$ defined as $\operatorname{homEquiv}$ applied to the adjunction of the presheaf equivalence of $C$ and $H$, $x_{1}$, $x_{2}$ and $x_{3}$.
TopCat.presheafToTopdefMathlib.Topology.Sheaves.PresheafOfFunctions, function or constantWording
the presheaf to top of X and T (from the name)
English
Let $X$ and $T$ be topological categories. Then the presheaf to top of $X$ and $T$ is a presheaf of the set of sets and $X$ defined as the composition of the opposite of the topological category of $X$ and the action of the Yoneda and $T$.
TopCat.presheafToTypedefMathlib.Topology.Sheaves.PresheafOfFunctions, function or constantWording
the presheaf to type of X and T (from the name)
English
Let $X$ be a topological category. Let $T$ be a set. Then the presheaf to type of $X$ and $T$ is a presheaf of the set of sets and $X$.
TopCat.presheafToTypesdefMathlib.Topology.Sheaves.PresheafOfFunctions, function or constantWording
the presheaf to type of X and T (from the name)
English
Let $X$ be a topological category. Let $T$ be a function from carriers of $X$ to sets. Then the presheaf to type of $X$ and $T$ is a presheaf of the set of sets and $X$.
TopCat.Presheaf.IsSheafdefMathlib.Topology.Sheaves.Sheaf, predicateWording
F is a sheaf (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Then $F$ is a sheaf, if $\operatorname{IsSheaf}$ holds for the Grothendieck topology of the set of carriers of $X$ and $F$.
TopCat.SheafdefMathlib.Topology.Sheaves.Sheaf, typeWording
sheaf of C and X (from the name)
English
Let $C$ be a set. Let $X$ be a topological category. Then a sheaf of $C$ and $X$ is an element of the function that maps $C$ and $X$ to the set of sheaves of the Grothendieck topology of the set of carriers of $X$ and $C$.
TopCat.Sheaf.forgetdefMathlib.Topology.Sheaves.Sheaf, function or constantEnglish
Let $C$ be a set. Let $X$ be a topological category. Then $\operatorname{forget}$ applied to $C$ and $X$ is a functor of the set of sheaves of $C$ and $X$ and the set of presheafs of $C$ and $X$ defined as the sheaf to presheaf of the Grothendieck topology of the set of carriers of $X$ and $C$.
TopCat.Sheaf.presheafdefMathlib.Topology.Sheaves.Sheaf, function or constantWording
the underlying presheaf of F (from the docstring)
English
Let $F$ be a sheaf of $C$ and $X$. Then the underlying presheaf of $F$ is a presheaf of $C$ and $X$ defined as the object of $F$.
TopCat.Presheaf.IsSheafEqualizerProductsdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, predicateEnglish
Let $F$ be a presheaf of $C$ and $X$. Then $\operatorname{IsSheafEqualizerProducts}$ holds for $F$, if for all sets $x_{1}$, for all functions $U$ from elements of $x_{1}$ to opens of the set of carriers of $X$, $\mathrm{Nonempty}$ holds for $\operatorname{IsLimit}$ applied to the fork of $F$ and $U$.
TopCat.Presheaf.SheafConditionEqualizerProducts.diagramdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the equalizer diagram for the sheaf condition of F and U (from the docstring)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the equalizer diagram for the sheaf condition of $F$ and $U$ is a functor of the set of walking parallel pairs and $C$ defined as the parallel pair of the left restriction of $F$ and $U$ and the right restriction of $F$ and $U$.
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIsodefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the isomorphism of U and x2 (from the name)
English
Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the isomorphism of $U$ and $x_{2}$ is an isomorphism of the equalizer diagram for the sheaf condition of $F$ and $U$ and the equalizer diagram for the sheaf condition of $G$ and $U$.
TopCat.Presheaf.SheafConditionEqualizerProducts.forkdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the fork of F and U (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the fork of $F$ and $U$ is a fork of the left restriction of $F$ and $U$ and the right restriction of $F$ and $U$ defined as the inclusion of the restriction of $F$ and $U$ and $\operatorname{w}$ applied to $F$ and $U$.
TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIsodefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the isomorphism of U and x2 (from the name)
English
Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the isomorphism of $U$ and $x_{2}$ is an isomorphism of the fork of $F$ and $U$ and the action of the postcomposition of the inverse of the isomorphism of $U$ and $x_{2}$ and the fork of $G$ and $U$.
TopCat.Presheaf.SheafConditionEqualizerProducts.leftResdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the left restriction of F and U (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the left restriction of $F$ and $U$ is a homomorphism of the product of the sections of $F$ and $U$ and the product of the sections of $F$ and $U$ defined as the lift of the function that maps $p$ to the composition of the projection of the function that maps $i$ to the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$ and $\ProdfstMACRoZ {p}$ and the map of $F$ and the opposite in $\operatorname{infLELeft}$ applied to $U$ applied to $\ProdfstMACRoZ {p}$ and $U$ applied to $\ProdsndMACRoAA {p}$.
TopCat.Presheaf.SheafConditionEqualizerProducts.piIntersdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the product of the sections of F and U (from the docstring)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the product of the sections of $F$ and $U$ is an element of $C$ defined as the product object of the function that maps $p$ to the action of $F$ and $\operatorname{op}$ applied to $\MinminMACRoAG {U (\ProdfstMACRoZ {p})}{U (\ProdsndMACRoAA {p})}$.
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIsodefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the isomorphism of U and x2 (from the name)
English
Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the isomorphism of $U$ and $x_{2}$ is an isomorphism of the product of the sections of $F$ and $U$ and the product of the sections of $G$ and $U$ defined as the map isomorphism of the function that maps $x_{3}$ to the application of $x_{2}$ and $\operatorname{op}$ applied to $\MinminMACRoAG {U (\ProdfstMACRoZ {x_{3}})}{U (\ProdsndMACRoAA {x_{3}})}$.
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpensdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the product of the sections of F and U (from the docstring)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the product of the sections of $F$ and $U$ is an element of $C$ defined as the product object of the function that maps $i$ to the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$.
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIsodefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the isomorphism of U and x2 (from the name)
English
Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $x_{2}$ be an isomorphism of $F$ and $G$. Then the isomorphism of $U$ and $x_{2}$ is an isomorphism of the product of the sections of $F$ and $U$ and the product of the sections of $G$ and $U$ defined as the map isomorphism of the function that maps $x_{3}$ to the application of $x_{2}$ and $\operatorname{op}$ applied to $U$ applied to $x_{3}$.
TopCat.Presheaf.SheafConditionEqualizerProducts.resdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the restriction of F and U (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the restriction of $F$ and $U$ is a homomorphism of the action of $F$ and $\operatorname{op}$ applied to the supremum of $U$ and the product of the sections of $F$ and $U$ defined as the lift of the function that maps $i$ to the map of $F$ and the opposite in $\operatorname{leSupr}$ applied to $U$ and $i$.
TopCat.Presheaf.SheafConditionEqualizerProducts.rightResdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the right restriction of F and U (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the right restriction of $F$ and $U$ is a homomorphism of the product of the sections of $F$ and $U$ and the product of the sections of $F$ and $U$ defined as the lift of the function that maps $p$ to the composition of the projection of the function that maps $i$ to the action of $F$ and $\operatorname{op}$ applied to $U$ applied to $i$ and $\ProdsndMACRoAA {p}$ and the map of $F$ and the opposite in $\operatorname{infLERight}$ applied to $U$ applied to $\ProdfstMACRoZ {p}$ and $U$ applied to $\ProdsndMACRoAA {p}$.
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantWording
the cone equivalence of F and U (from the name)
English
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Then the cone equivalence of $F$ and $U$ is an equivalence of the set of cones of the composition of the opposite of the diagram of $U$ and $F$ and the set of cones of the equalizer diagram for the sheaf condition of $F$ and $U$.
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionForkdefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantEnglish
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $P$ be an element of $\operatorname{IsLimit}$ applied to the fork of $F$ and $U$. Then $\operatorname{isLimitMapConeOfIsLimitSheafConditionFork}$ applied to $F$, $U$ and $P$ is an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of $U$.
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapConedefMathlib.Topology.Sheaves.SheafCondition.EqualizerProducts, function or constantEnglish
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$. Let $Q$ be an element of $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of $U$. Then $\operatorname{isLimitSheafConditionForkOfIsLimitMapCone}$ applied to $F$, $U$ and $Q$ is an element of $\operatorname{IsLimit}$ applied to the fork of $F$ and $U$.
TopCat.Presheaf.IsSheafOpensLeCoverdefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, predicateEnglish
Let $F$ be a presheaf of $C$ and $X$. Then $\operatorname{IsSheafOpensLeCover}$ holds for $F$, if for all sets $x_{1}$, for all functions $U$ from elements of $x_{1}$ to opens of the set of carriers of $X$, $\mathrm{Nonempty}$ holds for $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$.
TopCat.Presheaf.SheafCondition.OpensLeCoverdefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, typeEnglish
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then an element of $\operatorname{OpensLeCover}$ applied to $U$ is an element of the function that maps $U$ to the set of full subcategories of the function that maps $V$ to the proposition that there exists an element $i$ of $x$, such that $V \leq U (i)$.
TopCat.Presheaf.SheafCondition.OpensLeCover.homToIndexdefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantWording
the homomorphism to index of V (from the name)
English
Let $V$ be an element of $\operatorname{OpensLeCover}$ applied to $U$. Then the homomorphism to index of $V$ is a homomorphism of the object of $V$ and $U$ applied to the index of $V$.
TopCat.Presheaf.SheafCondition.OpensLeCover.indexdefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantWording
the index of V (from the name)
English
Let $V$ be an element of $\operatorname{OpensLeCover}$ applied to $U$. Then the index of $V$ is an element of $x$.
TopCat.Presheaf.SheafCondition.opensLeCoverCoconedefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then $\operatorname{opensLeCoverCocone}$ applied to $U$ is a cocone of the inclusion of the function that maps $V$ to the proposition that there exists an element $i$ of $x$, such that $V \leq U (i)$.
TopCat.Presheaf.generateEquivalenceOpensLedefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$ such that $Y$ is equal to the supremum of $U$. Then $\operatorname{generateEquivalenceOpensLe}$ applied to $U$ and $\mathrm{hY}$ is an equivalence of the set of full subcategories of the function that maps $f$ to the arrow of $\operatorname{generate}$ applied to $\operatorname{presieveOfCoveringAux}$ applied to $U$ and $Y$ and $\operatorname{OpensLeCover}$ applied to $U$.
TopCat.Presheaf.generateEquivalenceOpensLe_functor'defMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$. Then $\mathrm{TopCat\_\_Presheaf\_\_generateEquivalenceOpensLe\_functor'}$ applied to $U$ is a functor of the set of full subcategories of the function that maps $f$ to the arrow of $\operatorname{generate}$ applied to $\operatorname{presieveOfCoveringAux}$ applied to $U$ and $Y$ and $\operatorname{OpensLeCover}$ applied to $U$.
TopCat.Presheaf.generateEquivalenceOpensLe_inverse'defMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $U$ be a function from elements of $x$ to opens of the set of carriers of $X$ such that $Y$ is equal to the supremum of $U$. Then $\mathrm{TopCat\_\_Presheaf\_\_generateEquivalenceOpensLe\_inverse'}$ applied to $U$ and $\mathrm{hY}$ is a functor of $\operatorname{OpensLeCover}$ applied to $U$ and the set of full subcategories of the function that maps $f$ to the arrow of $\operatorname{generate}$ applied to $\operatorname{presieveOfCoveringAux}$ applied to $U$ and $Y$.
TopCat.Presheaf.isLimitOpensLeEquivGenerate₁defMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$ such that $Y$ is equal to the supremum of $U$. Then $\mathrm{TopCat\_\_Presheaf\_\_isLimitOpensLeEquivGenerate\_u2081\_}$ applied to $F$, $U$ and $\mathrm{hY}$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$ to $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of the arrow of $\operatorname{generate}$ applied to $\operatorname{presieveOfCoveringAux}$ applied to $U$ and $Y$ defined as the composition of the whisker equivalence equivalence of the opposite of $\operatorname{generateEquivalenceOpensLe}$ applied to $U$ and $\mathrm{hY}$ and the equivalence isomorphism limit of $\operatorname{whiskerIsoMapGenerateCocone}$ applied to $F$, $U$ and $\mathrm{hY}$.
TopCat.Presheaf.isLimitOpensLeEquivGenerate₂defMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $F$ be a presheaf of $C$ and $X$. Let $R$ be a presieve of $Y$ such that $\operatorname{generate}$ applied to $R$ is an element of $\operatorname{grothendieckTopology}$ applied to the set of carriers of $X$ and $Y$. Then $\mathrm{TopCat\_\_Presheaf\_\_isLimitOpensLeEquivGenerate\_u2082\_}$ applied to $F$, $R$ and $\mathrm{hR}$ is an equivalence from $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $\operatorname{coveringOfPresieve}$ applied to $R$ to $\operatorname{IsLimit}$ applied to the map cone of $F$ and the opposite of the cocone of the arrow of $\operatorname{generate}$ applied to $R$.
TopCat.Presheaf.whiskerIsoMapGenerateCoconedefMathlib.Topology.Sheaves.SheafCondition.OpensLeCover, function or constantEnglish
Let $F$ be a presheaf of $C$ and $X$. Let $U$ be a function from elements of $x_{1}$ to opens of the set of carriers of $X$ such that $Y$ is equal to the supremum of $U$. Then $\operatorname{whiskerIsoMapGenerateCocone}$ applied to $F$, $U$ and $\mathrm{hY}$ is an isomorphism of the whisker of the functor of the opposite of $\operatorname{generateEquivalenceOpensLe}$ applied to $U$ and $\mathrm{hY}$ and the map cone of $F$ and the opposite of $\operatorname{opensLeCoverCocone}$ applied to $U$ and the map cone of $F$ and the opposite of the cocone of the arrow of $\operatorname{generate}$ applied to $\operatorname{presieveOfCoveringAux}$ applied to $U$ and $Y$.