Definitions: Mathlib.Geometry, part 2 of 2

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

the model of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{FindModelResult}$. Then the model of $\mathrm{self}$ is an element of $\operatorname{Expr}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{FindModelResult}$. Then $\mathrm{Manifold\_\_Elab\_\_FindModelResult\_\_normedSpaceInfo?}$ applied to $\mathrm{self}$ is an element of $\mathrm{Option}$ applied to $\operatorname{NormedSpaceInfo}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

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

the base field of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{NormedSpaceInfo}$. Then the base field of $\mathrm{self}$ is an element of $\operatorname{Expr}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the normed space of self (from the name)

Let $\mathrm{self}$ be an element of $\operatorname{NormedSpaceInfo}$. Then the normed space of $\mathrm{self}$ is an element of $\operatorname{Expr}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $e$ be an element of $\operatorname{Expr}$. Then $\operatorname{TermElabM}$ holds for $\operatorname{Expr}$.

Let $e$ be an element of $\operatorname{Expr}$. Then $\operatorname{TermElabM}$ holds for $\mathrm{Option}$ applied to $\operatorname{FindModelResult}$.

Let $e$ be an element of $\operatorname{Expr}$. Let $\mathrm{es}$ be an element of $\mathrm{Option}$ applied to $\operatorname{Expr}$. Then $\operatorname{TermElabM}$ holds for $\mathrm{Prod}$ applied to $\operatorname{Expr}$ and $\operatorname{Expr}$.

Let $e$ be an element of $\operatorname{Expr}$. Then $\operatorname{TermElabM}$ holds for $\mathrm{Option}$ applied to $\operatorname{Expr}$.

the default (from the name)

The default is an element of $\operatorname{FindModelResult}$ defined as $\operatorname{mk}$ applied to $\operatorname{default}$ and $\operatorname{none}$.

the default (from the name)

The default is an element of $\operatorname{NormedSpaceInfo}$ defined as $\operatorname{mk}$ applied to $\operatorname{default}$ and $\operatorname{default}$.

the total space of e (from the name)

Let $e$ be an element of $\operatorname{Expr}$. Then the total space of $e$ is an element of $\operatorname{MetaM}$ applied to $\operatorname{Expr}$.

the smooth partition of f and hf (from the name)

Let $f$ be a bump covering of $M$ and $s$ such that for all elements $i$ of $x$, $\mathrm{ContMDiff}$ holds for $I$, the model with corner self of $\Real$ and $\Real$, $\operatorname{some}$ applied to the top and $\operatorname{coe}$ applied to $f$ applied to $i$. Then the smooth partition of $f$ and $\mathrm{hf}$ is a smooth partition of unity of $M$ and $s$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $\operatorname{coe}$ applied to $\operatorname{toPartitionOfUnity}$ applied to $f$ and $i$, $\operatorname{locallyFinite'}$ applied to the partition of $f$, $\operatorname{nonneg'}$ applied to the partition of $f$, $\mathrm{PartitionOfUnity\_\_sum\_eq\_one'}$ applied to the partition of $f$ and $\mathrm{PartitionOfUnity\_\_sum\_le\_one'}$ applied to the partition of $f$.

smooth bump covering of M and s (from the name)

Let $x$ and $M$ be sets. Let $I$ be a model with corner of $E$ and $H$. Let $s$ be an element of $\mathrm{optParam}$ applied to $\wp M$ and the universal set. Then the smooth bump coverings of $M$ and $s$ are a basic type.

f is subordinate to U (from the name)

Let $f$ be a smooth bump covering of $M$ and $s$. Let $U$ be a function from elements of $M$ to elements of $\wp M$. Then $f$ is subordinate to $U$, if for all elements $i$ of $x$, $\mathrm{tsupport}$ applied to $\operatorname{toFun}$ applied to the smooth bump covering of $f$ and $i$ is less than or equal to $U$ applied to $\operatorname{c}$ applied to $f$ and $i$.

Let $\mathrm{self}$ be a smooth bump covering of $M$ and $s$. Let $x_{6}$ be an element of $x$. Then $\operatorname{c}$ applied to $\mathrm{self}$ and $x_{6}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.

the ind of fs and x6 (from the name)

Let $\mathrm{fs}$ be a smooth bump covering of $M$ and $s$. Let $x_{6}$ be an element of $M$ such that $x_{6}$ is an element of $s$. Then the ind of $\mathrm{fs}$ and $x_{6}$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{SmoothBumpCovering\_\_eventuallyEq\_one'}$ applied to $\mathrm{fs}$, $x_{6}$ and $\mathrm{hx}$.

the bump covering of fs (from the name)

Let $\mathrm{fs}$ be a smooth bump covering of $M$ and $s$. Then the bump covering of $\mathrm{fs}$ is a bump covering of $M$ and $s$.

the smooth bump covering of self and i (from the name)

Let $\mathrm{self}$ be a smooth bump covering of $M$ and $s$. Let $i$ be an element of $x$. Then the smooth bump covering of $\mathrm{self}$ and $i$ is a smooth bump function of $I$ and $\operatorname{c}$ applied to $\mathrm{self}$ and $i$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $i$.

the smooth partition of fs (from the name)

Let $\mathrm{fs}$ be a smooth bump covering of $M$ and $s$. Then the smooth partition of $\mathrm{fs}$ is a smooth partition of unity of $M$ and $s$.

smooth partition of unity of M and s (from the name)

Let $x$ and $M$ be sets. Let $I$ be a model with corner of $E$ and $H$. Let $s$ be an element of $\mathrm{optParam}$ applied to $\wp M$ and the universal set. Then the smooth partitions of unity of $M$ and $s$ are a basic type.

f is subordinate to U (from the name)

Let $f$ be a smooth partition of unity of $M$ and $s$. Let $U$ be a function from elements of $x$ to elements of $\wp M$. 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$.

Let $x_{6}$ be a smooth partition of unity of $M$ and $s$. Let $x_{7}$ be an element of $M$. Then $\operatorname{finsupport}$ applied to $x_{6}$ and $x_{7}$ is a finite set of $x$ defined as $\operatorname{finsupport}$ applied to the partition of $x_{6}$ and $x_{7}$.

Let $x_{6}$ be a smooth partition of unity of $M$ and $s$. Let $x_{7}$ be an element of $M$. Then $\operatorname{fintsupport}$ applied to $x_{6}$ and $x_{7}$ is a finite set of $x$ defined as the finite set of $\mathrm{SmoothPartitionOfUnity\_\_finite\_tsupport}$ applied to $x_{6}$ and $x_{7}$.

Let $I$ be a model with corner of $E$ and $H$. Let $i$ be an element of $x$. Let $s$ be an element of $\wp M$. Then $\operatorname{single}$ applied to $I$, $i$ and $s$ is a smooth partition of unity of $M$ and $s$.

the smooth partition of self and x6 (from the name)

Let $\mathrm{self}$ be a smooth partition of unity of $M$ and $s$. Let $x_{6}$ be an element of $x$. Then the smooth partition of $\mathrm{self}$ and $x_{6}$ is a continuous difference map of $\Real$ and $\operatorname{some}$ applied to the top defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.

the partition of f (from the name)

Let $f$ be a smooth partition of unity of $M$ and $s$. Then the partition of $f$ is a partition of unity of $M$ and $s$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to the continuous map of $f$ applied to $i$, $\operatorname{locallyFinite'}$ applied to $f$, $\operatorname{nonneg'}$ applied to $f$, $\mathrm{SmoothPartitionOfUnity\_\_sum\_eq\_one'}$ applied to $f$ and $\mathrm{SmoothPartitionOfUnity\_\_sum\_le\_one'}$ applied to $f$.

n is a nonempty diffeomorphism sphere (from the name)

Let $M$ be a set. Let $n$ be a natural number. Then $n$ is a nonempty diffeomorphism sphere, if for all elements $x_{1}$ of $\mathrm{ChartedSpace}$ applied to the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ and $M$, if $\operatorname{some}$ applied to the top is a manifold with respect to the model with corner self of $\Real$ and the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$, then for all homotopy equivalences $x_{2}$ of $M$ and the set of elements of the sphere of $0$ and $1$, $\mathrm{Nonempty}$ holds for the set of diffeomorphisms of the set of elements of the sphere of $0$ and $1$ and $\operatorname{some}$ applied to the top.

Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Then we can say that $\mathrm{IsRiemannianManifold}$ holds for $I$ and $M$.

Let $F$ be a set. Then $\mathrm{riemannianMetricVectorSpace}$ applied to $F$ is an element of $\operatorname{ContMDiffRiemannianMetric}$ applied to the model with corner self of $\Real$ and $F$, the top, $F$ and the function that maps $x_{2}$ to the set of tangent spaces of the model with corner self of $\Real$ and $F$ and $x_{2}$.

the path length of a and b (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $x_{6}$ be a function from real numbers to elements of $M$. Let $a$ and $b$ be real numbers. Then the path length of $a$ and $b$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{Manifold\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Geometry\_\_Manifold\_\_Riemannian\_\_PathELength\_\_2732887573\_\_\_hygCtx\_\_\_hyg\_\_76}$, $I$, $x_{6}$, $a$ and $b$.

Let $I$ be a model with corner of $E$ and $H$. Let $x_{6}$ and $y$ be elements of $M$. Then $\operatorname{riemannianEDist}$ applied to $I$, $x_{6}$ and $y$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{Manifold\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Geometry\_\_Manifold\_\_Riemannian\_\_PathELength\_\_4077471356\_\_\_hygCtx\_\_\_hyg\_\_100}$, $I$, $x_{6}$ and $y$.

the local predicate of hG and #3 (from the name)

Let $M$ and $\mathrm{M'}$ be sets. Assume that $\operatorname{LocalInvariantProp}$ holds for $G$, $\mathrm{G'}$ and $P$. Then the local predicate of $\mathrm{M'}$ and $\mathrm{hG}$ is a local predicate of the function that maps $x_{6}$ to $\mathrm{M'}$.

the sheaf of hG and #3 (from the name)

Let $M$ and $\mathrm{M'}$ be sets. Assume that $\operatorname{LocalInvariantProp}$ holds for $G$, $\mathrm{G'}$ and $P$. Then the sheaf of $\mathrm{M'}$ and $\mathrm{hG}$ is a sheaf of the set of sets and $\operatorname{of}$ applied to $M$ defined as the subsheaf to type of the local predicate of $\mathrm{M'}$ and $\mathrm{hG}$.

the locally ringed space of IM and M (from the name)

the locally ringed space map of f and hf (from the name)

the smooth sheaf commutative ring homomorphism of IP and f (from the name)

Let $\mathrm{IP}$ be a model with corner of $\mathrm{EP}$ and $\mathrm{HP}$. Let $P$ be a set. Let $f$ be a function from elements of $M$ to elements of $P$ such that $\mathrm{ContMDiff}$ holds for $\mathrm{IM}$, $\mathrm{IP}$, $\operatorname{some}$ applied to the top and $f$. Then the smooth sheaf commutative ring homomorphism of $\mathrm{IP}$ and $f$ is a homomorphism of the smooth sheaf commutative ring of $\mathrm{IP}$ and $I$ and the action of the pushforward functor of the set of categories of commutative rings and the topological category of $\operatorname{mk}$ applied to $f$ and $\operatorname{continuous}$ applied to $\mathrm{hf}$ and the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$.

the smooth sheaf homomorphism of IP and f (from the name)

Let $\mathrm{IP}$ be a model with corner of $\mathrm{EP}$ and $\mathrm{HP}$. Let $P$ be a set. Let $f$ be a function from elements of $M$ to elements of $P$ such that $\mathrm{ContMDiff}$ holds for $\mathrm{IM}$, $\mathrm{IP}$, $\operatorname{some}$ applied to the top and $f$. Then the smooth sheaf homomorphism of $\mathrm{IP}$ and $f$ is a homomorphism of the smooth sheaf of $\mathrm{IP}$ and $I$ and the action of the pushforward functor of the set of sets and the topological category of $\operatorname{mk}$ applied to $f$ and $\operatorname{continuous}$ applied to $\mathrm{hf}$ and the smooth sheaf of $\mathrm{IM}$ and $I$.

the smooth presheaf additive commutative group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $A$ be sets. Then the smooth presheaf additive commutative group of $\mathrm{IM}$ and $I$ is a presheaf of the set of additive commutative group categories and $\operatorname{of}$ applied to $M$.

the smooth presheaf additive group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $G$ be sets. Then the smooth presheaf additive group of $\mathrm{IM}$ and $I$ is a presheaf of the set of additive group categories and $\operatorname{of}$ applied to $M$.

the smooth presheaf commutative group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $A$ be sets. Then the smooth presheaf commutative group of $\mathrm{IM}$ and $I$ is a presheaf of the set of commutative group categories and $\operatorname{of}$ applied to $M$.

the smooth presheaf commutative ring of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Then the smooth presheaf commutative ring of $\mathrm{IM}$ and $I$ is a presheaf of the set of categories of commutative rings and $\operatorname{of}$ applied to $M$.

the smooth presheaf group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $G$ be sets. Then the smooth presheaf group of $\mathrm{IM}$ and $I$ is a presheaf of the set of group categories and $\operatorname{of}$ applied to $M$.

the smooth presheaf ring of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Then the smooth presheaf ring of $\mathrm{IM}$ and $I$ is a presheaf of the set of categories of rings and $\operatorname{of}$ applied to $M$.

the smooth sheaf of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $N$ be sets. Then the smooth sheaf of $\mathrm{IM}$ and $I$ is a sheaf of the set of sets and $\operatorname{of}$ applied to $M$.

the evaluation of x12 and x13 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{12}$ be an element of $M$. Let $x_{13}$ be an element of the stalk of the underlying presheaf of the smooth sheaf of $\mathrm{IM}$ and $I$ and $x_{12}$. Then the evaluation of $x_{12}$ and $x_{13}$ is an element of $N$.

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{12}$ be a carrier of $\operatorname{of}$ applied to $M$. Let $U$ be an open neighbourhood filter of $x_{12}$. Let $i$ be an element of the action of the underlying presheaf of the smooth sheaf of $\mathrm{IM}$ and $I$ and $\operatorname{op}$ applied to $U$. Then $\operatorname{evalAt}$ applied to $\mathrm{IM}$, $I$, $N$, $x_{12}$, $U$ and $i$ is an element of $N$ defined as $x_{12}$.

the evaluation homomorphism of I and x12 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{12}$ be a carrier of $\operatorname{of}$ applied to $M$. Then the evaluation homomorphism of $I$ and $x_{12}$ is a homomorphism of the stalk of the underlying presheaf of the smooth sheaf of $\mathrm{IM}$ and $I$ and $x_{12}$ and $N$.

the smooth sheaf additive commutative group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $A$ be sets. Then the smooth sheaf additive commutative group of $\mathrm{IM}$ and $I$ is a sheaf of the set of additive commutative group categories and $\operatorname{of}$ applied to $M$.

the left composition of M and #7 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{I'}$ be a model with corner of $E$ and $\mathrm{H'}$. Let $M$, $A$ and $\mathrm{A'}$ be sets. Let $x_{17}$ be an additive monoid homomorphism of $A$ and $\mathrm{A'}$ such that $\mathrm{ContMDiff}$ holds for $I$, $\mathrm{I'}$, $\operatorname{some}$ applied to the top and $\operatorname{coe}$ applied to $x_{17}$. Then the left composition of $\mathrm{I'}$ and $x_{17}$ is a homomorphism of the smooth sheaf additive commutative group of $\mathrm{IM}$ and $I$ and the smooth sheaf additive commutative group of $\mathrm{IM}$ and $\mathrm{I'}$.

the smooth sheaf additive group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $G$ be sets. Then the smooth sheaf additive group of $\mathrm{IM}$ and $I$ is a sheaf of the set of additive group categories and $\operatorname{of}$ applied to $M$.

the smooth sheaf commutative group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $A$ be sets. Then the smooth sheaf commutative group of $\mathrm{IM}$ and $I$ is a sheaf of the set of commutative group categories and $\operatorname{of}$ applied to $M$.

the left composition of M and #7 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{I'}$ be a model with corner of $E$ and $\mathrm{H'}$. Let $M$, $A$ and $\mathrm{A'}$ be sets. Let $x_{17}$ be a monoid homomorphism of $A$ and $\mathrm{A'}$ such that $\mathrm{ContMDiff}$ holds for $I$, $\mathrm{I'}$, $\operatorname{some}$ applied to the top and $\operatorname{coe}$ applied to $x_{17}$. Then the left composition of $\mathrm{I'}$ and $x_{17}$ is a homomorphism of the smooth sheaf commutative group of $\mathrm{IM}$ and $I$ and the smooth sheaf commutative group of $\mathrm{IM}$ and $\mathrm{I'}$.

the smooth sheaf commutative ring of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Then the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$ is a sheaf of the set of categories of commutative rings and $\operatorname{of}$ applied to $M$.

the evaluation of I and x13 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Let $x_{13}$ be an element of $M$. Then the evaluation of $I$ and $x_{13}$ is a ring homomorphism of the set of carriers of the stalk of the underlying presheaf of the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$ and $x_{13}$ and $R$ defined as the underlying ring hom of the evaluation homomorphism of $I$ and $x_{13}$.

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Let $x_{13}$ be a carrier of $\operatorname{of}$ applied to $M$. Let $U$ be an open neighbourhood filter of $x_{13}$. Then $\operatorname{evalAt}$ applied to $\mathrm{IM}$, $I$, $M$, $R$, $x_{13}$ and $U$ is a homomorphism of the action of the underlying presheaf of the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$ and $\operatorname{op}$ applied to $U$ and $\operatorname{of}$ applied to $R$ defined as the commutative ring category of the evaluation ring homomorphism of $x_{13}$.

the evaluation homomorphism of I and x13 (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Let $x_{13}$ be a carrier of $\operatorname{of}$ applied to $M$. Then the evaluation homomorphism of $I$ and $x_{13}$ is a homomorphism of the stalk of the underlying presheaf of the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$ and $x_{13}$ and $\operatorname{of}$ applied to $R$.

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Let $x_{13}$ be a carrier of $\operatorname{of}$ applied to $M$. Then $\operatorname{forgetStalk}$ applied to $\mathrm{IM}$, $I$, $M$, $R$ and $x_{13}$ is an isomorphism of the set of carriers of the stalk of the underlying presheaf of the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$ and $x_{13}$ and the stalk of the underlying presheaf of the smooth sheaf of $\mathrm{IM}$ and $I$ and $x_{13}$ defined as $\operatorname{preservesColimitIso}$ applied to the forgetful functor of the set of categories of commutative rings and the action of the action of the left whiskering of the set of opposites of the set of opens of the set of carriers of $\operatorname{of}$ applied to $M$ and the set of categories of commutative rings and the opposite of the inclusion of $x_{13}$ and the underlying presheaf of the smooth sheaf commutative ring of $\mathrm{IM}$ and $I$.

the smooth sheaf group of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $G$ be sets. Then the smooth sheaf group of $\mathrm{IM}$ and $I$ is a sheaf of the set of group categories and $\operatorname{of}$ applied to $M$.

the smooth sheaf ring of IM and I (from the name)

Let $\mathrm{IM}$ be a model with corner of $\mathrm{EM}$ and $\mathrm{HM}$. Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $R$ be sets. Then the smooth sheaf ring of $\mathrm{IM}$ and $I$ is a sheaf of the set of categories of rings and $\operatorname{of}$ applied to $M$.

Let $I$ be a model with corner of $x_{2}$ and $H$. Let $J$ be a model with corner of $x_{3}$ and $G$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $M$ to elements of $N$. Then we can say that $\operatorname{IsSmoothEmbedding}$ holds for $I$, $J$, $n$ and $f$.

G is closed under restriction (from the docstring)

Let $G$ be a structure groupoid of $H$. Then we can say that $G$ is closed under restriction.

Let $H$ be a set. Then the elements of $\mathrm{Pregroupoid}$ applied to $H$ are a basic type.

the groupoid of PG (from the name)

Let $\mathrm{PG}$ be an element of $\mathrm{Pregroupoid}$ applied to $H$. Then the groupoid of $\mathrm{PG}$ is a structure groupoid of $H$.

Let $\mathrm{self}$ be an element of $\mathrm{Pregroupoid}$ applied to $H$. Let $x_{1}$ be a function from elements of $H$ to elements of $H$. Let $x_{2}$ be an element of $\wp H$. Then $\operatorname{property}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$.

structure groupoid of H (from the name)

Let $H$ be a set. Then the structure groupoids of $H$ are a basic type.

Let $\mathrm{self}$ be a structure groupoid of $H$. Then $\operatorname{members}$ applied to $\mathrm{self}$ is an element of the power set of the set of open partial homeomorphisms of $H$ and $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the continuous groupoid of H (from the name)

Let $H$ be a set. Then the continuous groupoid of $H$ is a structure groupoid of $H$ defined as the groupoid of $\mathrm{continuousPregroupoid}$ applied to $H$.

Let $H$ be a set. Then $\mathrm{continuousPregroupoid}$ applied to $H$ is an element of $\mathrm{Pregroupoid}$ applied to $H$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{True}$, the function that maps $x_{3}$, $x_{4}$, $x_{5}$, $x_{6}$, $h$, $h_{1}$, $h_{2}$, $h_{3}$ and $h_{4}$ to $\mathrm{trivial}$, $\mathrm{trivial}$, the function that maps $x_{7}$, $x_{8}$, $h_{5}$ and $h_{6}$ to $\mathrm{trivial}$ and the function that maps $x_{9}$, $x_{10}$, $x_{11}$, $h_{7}$, $h_{8}$ and $h_{9}$ to $\mathrm{trivial}$.

the identity groupoid of H (from the name)

Let $H$ be a set. Then the identity groupoid of $H$ is a structure groupoid of $H$.

the identity restriction groupoid (from the name)

The identity restriction groupoid is a structure groupoid of $H$.

Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $\mathrm{E''}$ and $G$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $M$ to elements of $N$. Then $\operatorname{IsSubmersion}$ holds for $I$, $J$, $n$ and $f$, if there exists a set $F$, such that there exists an element $x_{12}$ of $\mathrm{NormedAddCommGroup}$ applied to $F$, such that there exists an element $x_{13}$ of $\mathrm{NormedSpace}$ applied to $x$ and $F$, such that $\operatorname{IsSubmersionOfComplement}$ holds for $F$, $I$, $J$, $n$ and $f$.

complement of h (from the name)

Assume that $\operatorname{IsSubmersion}$ holds for $I$, $J$, $n$ and $f$. Then a complement of $h$ is an element of the function that maps $h$ to $\operatorname{choose}$ applied to $h$.

Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $\mathrm{E''}$ and $G$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{12}$ be an element of $M$. Then $\operatorname{IsSubmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$, if there exists a set $F$, such that there exists an element $x_{13}$ of $\mathrm{NormedAddCommGroup}$ applied to $F$, such that there exists an element $x_{14}$ of $\mathrm{NormedSpace}$ applied to $x$ and $F$, such that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{12}$.

the codomain chart of h (from the name)

Assume that $\operatorname{IsSubmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$. Then the codomain chart of $h$ is an open partial homeomorphism of $N$ and $G$ defined as the codomain chart of $\mathrm{Manifold\_\_IsSubmersionAt\_\_isSubmersionAtOfComplement\_complement}$ applied to $h$.

complement of h (from the name)

Assume that $\operatorname{IsSubmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$. Then a complement of $h$ is an element of the function that maps $h$ to $\operatorname{choose}$ applied to $h$.

the domain chart of h (from the name)

Assume that $\operatorname{IsSubmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$. Then the domain chart of $h$ is an open partial homeomorphism of $M$ and $H$ defined as the domain chart of $\mathrm{Manifold\_\_IsSubmersionAt\_\_isSubmersionAtOfComplement\_complement}$ applied to $h$.

the equivalence of h (from the name)

Assume that $\operatorname{IsSubmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$. Then the equivalence of $h$ is a continuous linear equivalence of $E$ and $\mathrm{Prod}$ applied to $\mathrm{E''}$ and the set of complements of $h$ defined as the equivalence of $\mathrm{Manifold\_\_IsSubmersionAt\_\_isSubmersionAtOfComplement\_complement}$ applied to $h$.

Let $F$ be a set. Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $\mathrm{E''}$ and $G$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{14}$ be an element of $M$. Then $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$, if $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{14}$ and $\operatorname{SubmersionAtProp}$ applied to $F$, $I$, $J$, $M$ and $N$.

the codomain chart of h (from the name)

Assume that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then the codomain chart of $h$ is an open partial homeomorphism of $N$ and $G$ defined as the codomain chart of $h$.

the domain chart of h (from the name)

Assume that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then the domain chart of $h$ is an open partial homeomorphism of $M$ and $H$ defined as the domain chart of $h$.

the equivalence of h (from the name)

Assume that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then the equivalence of $h$ is a continuous linear equivalence of $E$ and $\mathrm{Prod}$ applied to $\mathrm{E''}$ and $F$.

small complement of hf (from the name)

Assume that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then a small complement of $\mathrm{hf}$ is an element of the function that maps $\mathrm{hf}$ to the set of shrinks of $F$.

the small equivalence of hf (from the name)

Assume that $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then the small equivalence of $\mathrm{hf}$ is a continuous linear equivalence of $F$ and the set of small complements of $\mathrm{hf}$ defined as the inverse of the continuous linear equivalence of $x$ and the additive equivalence.

Let $F$ be a set. Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $\mathrm{E''}$ and $G$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $M$ to elements of $N$. Then $\operatorname{IsSubmersionOfComplement}$ holds for $F$, $I$, $J$, $n$ and $f$, if for all elements $x_{14}$ of $M$, $\operatorname{IsSubmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$.

Let $F$, $M$ and $N$ be sets. Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $\mathrm{E''}$ and $G$. Let $x_{12}$ be a function from elements of $M$ to elements of $N$. Let $x_{13}$ be an open partial homeomorphism of $M$ and $H$. Let $x_{14}$ be an open partial homeomorphism of $N$ and $G$. Then $\operatorname{SubmersionAtProp}$ holds for $F$, $I$, $J$, $M$, $N$, $x_{12}$, $x_{13}$ and $x_{14}$, if there exists a continuous linear equivalence $\mathrm{equiv}$ of $E$ and $\mathrm{Prod}$ applied to $\mathrm{E''}$ and $F$, such that $\operatorname{EqOn}$ holds for $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $\operatorname{extend}$ applied to $x_{14}$ and $J$ and $\operatorname{comp}$ applied to $x_{12}$ and $\operatorname{toFun}$ applied to the inverse of $\operatorname{extend}$ applied to $x_{13}$ and $I$, $\operatorname{comp}$ applied to $\ProdfstMACRoZ$ and $\operatorname{coe}$ applied to $\mathrm{equiv}$ and the target of $\operatorname{extend}$ applied to $x_{13}$ and $I$.

Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Then we can say that $\mathrm{ContMDiffVectorBundle}$ holds for $n$, $F$, $E$ and $\mathrm{IB}$.

Let $Z$ be a vector bundle of $F$ and $x_{9}$. Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then we can say that $\operatorname{IsContMDiff}$ holds for $Z$, $\mathrm{IB}$ and $n$.

n is a continuous difference with respect to a (from the name)

Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $a$ be an element of $\mathrm{VectorPrebundle}$ applied to $x$, $F$ and $E$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then we can say that $n$ is a continuous difference with respect to $a$.

the continuous difference coordinate change of a and #6 (from the name)

Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $a$ be an element of $\mathrm{VectorPrebundle}$ applied to $x$, $F$ and $E$ such that $e$ is an element of the pretrivialization atlas of $a$ and $\mathrm{e'}$ is an element of the pretrivialization atlas of $a$. Let $b$ be an element of $B$. Then the continuous difference coordinate change of $a$ and $b$ is a continuous linear map of $F$ and $F$ defined as $\operatorname{choose}$ applied to $\mathrm{VectorPrebundle\_\_IsContMDiff\_\_exists\_contMDiffCoordChange}$ applied to $e$, $\mathrm{he}$, $\mathrm{e'}$ and $\mathrm{he'}$ and $b$.

continuous difference section of n and V (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $F$ be a set. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $V$ be a function from elements of $M$ to sets. Then the continuous difference sections of $n$ and $V$ are a basic type.

the coercion additive homomorphism of n and V (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $F$ be a set. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $V$ be a function from elements of $M$ to sets. Then the coercion additive homomorphism of $n$ and $V$ is an additive monoid homomorphism of the set of continuous difference sections of $n$ and $V$ and the set of functions from elements $x_{14}$ of $M$ to elements of $V$ applied to $x_{14}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{ContMDiffSection\_\_coe\_zero}$ and $\mathrm{ContMDiffSection\_\_coe\_add}$.

the continuous difference section of self and x12 (from the name)

Let $\mathrm{self}$ be a continuous difference section of $n$ and $V$. Let $x_{12}$ be an element of $M$. Then the continuous difference section of $\mathrm{self}$ and $x_{12}$ is an element of $V$ applied to $x_{12}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{12}$.

Let $F$ be a set. Let $k$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $\mathrm{cov}$ be a function from functions from elements $x_{16}$ of $M$ to elements of $V$ applied to $x_{16}$ and elements $x_{15}$ of $M$ to continuous linear maps of the set of tangent spaces of $I$ and $x_{15}$ and $V$ applied to $x_{15}$. Let $u$ be an element of $\wp M$. Then we can say that $\mathrm{ContMDiffCovariantDerivativeOn}$ holds for $F$, $k$, $x_{15}$, $\mathrm{cov}$ and $u$.

covariant derivative of F and V (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $F$ be a set. Let $V$ be a function from elements of $M$ to sets. Then the covariant derivatives of $F$ and $V$ are a basic type.

Let $\mathrm{cov}$ be a covariant derivative of $F$ and $V$. Let $k$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then we can say that $\operatorname{ContMDiffCovariantDerivative}$ holds for $\mathrm{cov}$ and $k$.

the additive one form of cov and A (from the name)

Let $\mathrm{cov}$ be a covariant derivative of $F$ and $V$. Let $A$ be a function from elements $x_{14}$ of $M$ to continuous linear maps of $V$ applied to $x_{14}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{14}$ and $V$ applied to $x_{14}$. Then the additive one form of $\mathrm{cov}$ and $x_{14}$ is a covariant derivative of $F$ and $V$.

the affine combination of g and #3 (from the name)

Let $\mathrm{cov}$ and $\mathrm{cov'}$ be covariant derivatives of $F$ and $V$. Let $g$ be a function from elements of $M$ to elements of $x$. Then the affine combination of $\mathrm{cov'}$ and $g$ is a covariant derivative of $F$ and $V$.

the difference of x14 and #3 (from the name)

Let $\mathrm{cov}$ and $\mathrm{cov'}$ be covariant derivatives of $F$ and $V$. Let $x_{14}$ be an element of $M$. Then the difference of $\mathrm{cov'}$ and $x_{14}$ is a continuous linear map of $V$ applied to $x_{14}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{14}$ and $V$ applied to $x_{14}$ defined as the difference of $x_{14}$.

the finite affine combination of cov and hf (from the name)

Let $\mathrm{cov}$ be a function from elements of $x_{14}$ to covariant derivatives of $F$ and $V$. Assume that $\EqtMACRoH {\FinsetSum {s}{i}{x_{16}}{f (i , x_{16})}}{1}$. Then the finite affine combination of $\mathrm{cov}$ and $\mathrm{hf}$ is a covariant derivative of $F$ and $V$.

the covariant derivative of hcov and hs (from the name)

Assume that for all elements $i_{1}$ of $x_{14}$, $\mathrm{IsCovariantDerivativeOn}$ holds for $F$, $\mathrm{cov}$ and $s$ applied to $i_{1}$. Assume that the union of the function that maps $i$ to $s$ applied to $i$ is equal to the universal set. Then the covariant derivative of $\mathrm{hcov}$ and $\mathrm{hs}$ is a covariant derivative of $F$ and $V$.

the covariant derivative of x14 and x16 (from the name)

Let $\mathrm{self}$ be a covariant derivative of $F$ and $V$. Let $x_{14}$ be a function from elements $x_{16}$ of $M$ to elements of $V$ applied to $x_{16}$. Let $x_{15}$ be an element of $M$. Then the covariant derivative of $x_{16}$ and $x_{14}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{15}$ and $V$ applied to $x_{15}$ defined as the function that maps $x_{15}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{16}$, $x_{14}$ and $x_{15}$.

Let $F$ be a set. Let $\mathrm{cov}$ be a function from functions from elements $x_{16}$ of $M$ to elements of $V$ applied to $x_{16}$ and elements $x_{15}$ of $M$ to continuous linear maps of the set of tangent spaces of $I$ and $x_{15}$ and $V$ applied to $x_{15}$. Let $s$ be an element of $\mathrm{optParam}$ applied to $\wp M$ and the universal set. Then we can say that $\mathrm{IsCovariantDerivativeOn}$ holds for $F$, $x_{15}$, $\mathrm{cov}$ and $s$.

the difference of #3 (from the name)

Assume that $\mathrm{IsCovariantDerivativeOn}$ holds for $F$, $\mathrm{cov}$ and $s$. Assume that $\mathrm{IsCovariantDerivativeOn}$ holds for $F$, $\mathrm{cov'}$ and $s$. Let $x_{14}$ be an element of $M$. Then the difference of $x_{14}$ is a continuous linear map of $V$ applied to $x_{14}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{14}$ and $V$ applied to $x_{14}$.

Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{cov}$ be a covariant derivative of $E$ and the set of elements of $\mathrm{TangentSpace}$ applied to $I$. Then we can say that $\operatorname{IsLeviCivitaConnection}$ holds for $I$ and $\mathrm{cov}$.

Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Then $\operatorname{leviCivitaConnection}$ applied to $I$ and $M$ is a covariant derivative of $E$ and the set of elements of $\mathrm{TangentSpace}$ applied to $I$.

Let $\mathrm{cov}$ be a covariant derivative of $F$ and $V$. Then $\operatorname{IsMetricCompatible}$ holds for $\mathrm{cov}$, if $\operatorname{derivMetricTensor}$ applied to $\mathrm{cov}$ is equal to $0$.

the tensor of cov and x11 (from the docstring)

Let $\mathrm{cov}$ be a covariant derivative of $F$ and $V$. Let $x_{11}$ be an element of $M$. Then the tensor of $\mathrm{cov}$ and $x_{11}$ is a continuous linear map of $V$ applied to $x_{11}$ and the set of continuous linear maps of $V$ applied to $x_{11}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{11}$ and $\Real$.

the torsion tensor of cov and x7 (from the docstring)

Let $\mathrm{cov}$ be a covariant derivative of $E$ and the set of elements of $\mathrm{TangentSpace}$ applied to $I$. Let $x_{7}$ be an element of $M$. Then the torsion tensor of $\mathrm{cov}$ and $x_{7}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{7}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{7}$ and the set of tangent spaces of $I$ and $x_{7}$.

the torsion tensor of hcov and x7 (from the docstring)

Assume that $\mathrm{IsCovariantDerivativeOn}$ holds for $E$, $\mathrm{cov}$ and the universal set. Let $x_{7}$ be an element of $M$. Then the torsion tensor of $\mathrm{hcov}$ and $x_{7}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{7}$ and the set of continuous linear maps of the set of tangent spaces of $I$ and $x_{7}$ and the set of tangent spaces of $I$ and $x_{7}$.

the open partial homeomorphism of x5 (from the name)

Let $x_{5}$ be a function from elements of $B$ to continuous linear equivalences of $F$ and $F$. Assume that $U$ is open. Assume that $\mathrm{ContinuousOn}$ holds for the function that maps $x_{7}$ to the continuous linear map of $x_{5}$ applied to $x_{7}$ and $U$. Assume that $\mathrm{ContinuousOn}$ holds for the function that maps $x_{6}$ to the continuous linear map of the inverse of $x_{5}$ applied to $x_{6}$ and $U$. Then the open partial homeomorphism of $x_{5}$ is an open partial homeomorphism of $\mathrm{Prod}$ applied to $B$ and $F$ and $\mathrm{Prod}$ applied to $B$ and $F$.

Let $B$ and $F$ be sets. Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then $\mathrm{contMDiffFiberwiseLinear}$ applied to $B$, $F$, $\mathrm{IB}$ and $n$ is a structure groupoid of $\mathrm{Prod}$ applied to $B$ and $F$.

Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be a basis of $x$ and $F$. Assume that $x_{11}$ is an element of the base set of $e$. Then $\operatorname{basisAt}$ applied to $e$, $b$ and $\mathrm{hx}$ is a basis of $x$ and $V$ applied to $x_{11}$ defined as the map of $b$ and the inverse of $\operatorname{linearEquivAt}$ applied to $x$, $e$, $x_{11}$ and $\mathrm{hx}$.

the local frame of x11 and x12 (from the name)

Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be a basis of $x$ and $F$. Let $x_{11}$ be an element of $x_{10}$. Let $x_{12}$ be an element of $M$. Then the local frame of $x_{11}$ and $x_{12}$ is an element of $V$ applied to $x_{12}$ defined as $\mathrm{dite}$ applied to the proposition that $x_{12}$ is an element of the base set of $e$, the function that maps $\mathrm{hx}$ to $\operatorname{basisAt}$ applied to $e$, $b$, $\mathrm{hx}$ and $x_{11}$ and the function that maps $\mathrm{hx1}$ to $0$.

the local frame coefficient of i and x15 (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $e$ be a trivialization of $F$ and $\operatorname{proj}$. Let $b$ be a basis of $x$ and $F$. Let $i$ be an element of $x_{14}$. Let $x_{15}$ be an element of $M$. Then the local frame coefficient of $i$ and $x_{15}$ is a linear map of $V$ applied to $x_{15}$ and $x$.

Let $I$ be a model with corner of $E$ and $H$. Let $F$ be a set. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $s$ be a function from elements of $x_{14}$ and elements $x_{16}$ of $M$ to elements of $V$ applied to $x_{16}$. Let $u$ be an element of $\wp M$. Then we can say that $\mathrm{IsLocalFrameOn}$ holds for $I$, $F$, $n$, $x_{16}$, $s$ and $u$.

the coefficient of i and x15 (from the name)

Assume that $\mathrm{IsLocalFrameOn}$ holds for $I$, $F$, $n$, $s$ and $u$. Let $i$ be an element of $x_{14}$. Let $x_{15}$ be an element of $M$. Then the coefficient of $i$ and $x_{15}$ is a linear map of $V$ applied to $x_{15}$ and $x$ defined as $\mathrm{dite}$ applied to $\MembershipmemMACRoT {u}{x_{15}}$, the function that maps $\mathrm{hx}$ to the coordinate of $\operatorname{toBasisAt}$ applied to $\mathrm{hs}$ and $\mathrm{hx}$ and $i$ and the function that maps $\mathrm{hx1}$ to $0$.

Assume that $\mathrm{IsLocalFrameOn}$ holds for $I$, $F$, $n$, $s$ and $u$. Assume that $x_{15}$ is an element of $u$. Then $\operatorname{toBasisAt}$ applied to $\mathrm{hs}$ and $\mathrm{hx}$ is a basis of $x$ and $V$ applied to $x_{15}$ defined as $\operatorname{mk}$ applied to $\operatorname{linearIndependent}$ applied to $\mathrm{hs}$ and $\mathrm{hx}$ and $\operatorname{generating}$ applied to $\mathrm{hs}$ and $\mathrm{hx}$.

Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Then the elements of $\operatorname{ContMDiffRiemannianMetric}$ applied to $\mathrm{IB}$, $n$, $F$ and $E$ are a basic type.

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

Let $g$ be an element of $\operatorname{ContMDiffRiemannianMetric}$ applied to $\mathrm{IB}$, $n$, $F$ and $E$. Then $\operatorname{toContinuousRiemannianMetric}$ applied to $g$ is an element of $\operatorname{ContinuousRiemannianMetric}$ applied to $F$ and $E$.

Let $g$ be an element of $\operatorname{ContMDiffRiemannianMetric}$ applied to $\mathrm{IB}$, $n$, $F$ and $E$. Then $\operatorname{toRiemannianMetric}$ applied to $g$ is an element of $\operatorname{RiemannianMetric}$ applied to $E$ defined as $\operatorname{toRiemannianMetric}$ applied to $\operatorname{toContinuousRiemannianMetric}$ applied to $g$.

Let $\mathrm{IB}$ be a model with corner of $\mathrm{EB}$ and $\mathrm{HB}$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $F$ be a set. Let $E$ be a function from elements of $B$ to sets. Then we can say that $\mathrm{IsContMDiffRiemannianBundle}$ holds for $\mathrm{IB}$, $n$, $F$ and $E$.

Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{I'}$ be a model with corner of $\mathrm{E'}$ and $\mathrm{H'}$. Let $f$ be a function from elements of $N$ to elements of $M$. Let $g$ be a function from elements of $N$ to elements of $\mathrm{M'}$. Let $x_{12}$ be a function from elements $x_{15}$ of $N$ to continuous linear maps of the set of tangent spaces of $I$ and $f$ applied to $x_{15}$ and the set of tangent spaces of $\mathrm{I'}$ and $g$ applied to $x_{15}$. Let $x_{13}$ and $x_{14}$ be elements of $N$. Then $\mathrm{inTangentCoordinates}$ applied to $I$, $\mathrm{I'}$, $f$, $g$, $x_{15}$, $x_{12}$, $x_{13}$ and $x_{14}$ is a continuous linear map of $E$ and $\mathrm{E'}$ defined as the function that maps $x_{14}$ to $\operatorname{inCoordinates}$ applied to $E$, the set of elements of $\mathrm{TangentSpace}$ applied to $I$, $\mathrm{E'}$, the set of elements of $\mathrm{TangentSpace}$ applied to $\mathrm{I'}$, $f$ applied to $x_{12}$, $f$ applied to $x_{13}$, $g$ applied to $x_{12}$, $g$ applied to $x_{13}$, $x_{15}$ applied to $x_{13}$ and $x_{14}$.

the tangent bundle of I and M (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Then the tangent bundle of $I$ and $M$ is a vector bundle of $E$ and the set of elements of the atlas of $H$ and $M$.

the tangent bundle model space homeomorphism of I (from the name)

Let $I$ be a model with corner of $E$ and $H$. Then the tangent bundle model space homeomorphism of $I$ is a homeomorphism of the set of tangent bundles of $I$ and $H$ and the set of model products of $H$ and $E$.

the tangent coordinate change of y and x8 (from the name)

Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$, $y$ and $x_{8}$ be elements of $M$. Then the tangent coordinate change of $y$ and $x_{8}$ is a continuous linear map of $E$ and $E$ defined as the coordinate change of $\mathrm{achart}$ applied to $H$ and $y$ and $x_{8}$.

Let $I$ be a model with corner of $E$ and $H$. Let $F$ be a set. Let $x_{16}$ be a function from functions from elements $x_{19}$ of $M$ to elements of $V$ applied to $x_{19}$ to elements of $A$. Let $x_{17}$ be an element of $M$. Then we can say that $\mathrm{TensorialAt}$ holds for $I$, $F$, $x_{16}$ and $x_{17}$.

the homomorphism of x17 and x20 (from the name)

Let $x_{17}$ be a function from functions from elements $x_{20}$ of $M$ to elements of $V$ applied to $x_{20}$ to elements of $A$. Let $x_{18}$ be an element of $M$ such that $\mathrm{TensorialAt}$ holds for $I$, $F$, $x_{17}$ and $x_{18}$. Then the homomorphism of $x_{17}$ and $x_{18}$ is a continuous linear map of $V$ applied to $x_{18}$ and $A$.

the homomorphism of x24 and x36 (from the name)

Let $x_{24}$ be a function from functions from elements $x_{36}$ of $M$ to elements of $V$ applied to $x_{36}$ and functions from elements $x_{35}$ of $M$ to elements of $\mathrm{V'}$ applied to $x_{35}$ to elements of $A$. Let $x_{25}$ be an element of $M$ such that for all functions $x_{29}$ from elements $x_{32}$ of $M$ to elements of $\mathrm{V'}$ applied to $x_{32}$, if $\mathrm{MDifferentiableAt}$ holds for $I$, the product of $I$ and the model with corner self of $x$ and $\mathrm{F'}$, the function that maps $x_{31}$ to $\operatorname{mk'}$ applied to $\mathrm{F'}$, $x_{31}$ and $x_{29}$ applied to $x_{31}$ and $x_{25}$, then $\mathrm{TensorialAt}$ holds for $I$, $F$, the function that maps $x_{30}$ to $x_{24}$ applied to $x_{30}$ and $x_{29}$ and $x_{25}$ and for all functions $x_{26}$ from elements $x_{28}$ of $M$ to elements of $V$ applied to $x_{28}$, if $\mathrm{MDifferentiableAt}$ holds for $I$, the product of $I$ and the model with corner self of $x$ and $F$, the function that maps $x_{27}$ to $\operatorname{mk'}$ applied to $F$, $x_{27}$ and $x_{26}$ applied to $x_{27}$ and $x_{25}$, then $\mathrm{TensorialAt}$ holds for $I$, $\mathrm{F'}$, $x_{24}$ applied to $x_{26}$ and $x_{25}$. Then the homomorphism of $x_{24}$ and $x_{25}$ is a continuous linear map of $V$ applied to $x_{25}$ and the set of continuous linear maps of $\mathrm{V'}$ applied to $x_{25}$ and $A$.

Let $I$ be a model with corner of $E$ and $H$. Let $V$ be a function from elements $x_{9}$ of $M$ to tangent spaces of $I$ and $x_{9}$. Let $W$ be a function from elements $x_{8}$ of $M$ to tangent spaces of $I$ and $x_{8}$. Let $x_{7}$ be an element of $M$. Then $\operatorname{mlieBracket}$ applied to $I$, $x_{9}$, $V$, $x_{8}$, $W$ and $x_{7}$ is a tangent space of $I$ and $x_{7}$ defined as the function that maps $W$ and $x_{7}$ to $\operatorname{mlieBracketWithin}$ applied to $I$, $x_{9}$, $V$, the universal set, $x_{8}$, $W$ and $x_{7}$.

Let $I$ be a model with corner of $E$ and $H$. Let $V$ be a function from elements $x_{9}$ of $M$ to tangent spaces of $I$ and $x_{9}$. Let $W$ be a function from elements $x_{8}$ of $M$ to tangent spaces of $I$ and $x_{8}$. Let $s$ be an element of $\wp M$. Let $x_{7}$ be an element of $M$. Then $\operatorname{mlieBracketWithin}$ applied to $I$, $x_{9}$, $V$, $x_{8}$, $W$, $s$ and $x_{7}$ is a tangent space of $I$ and $x_{7}$ defined as the function that maps $s$ and $x_{7}$ to $\operatorname{mpullback}$ applied to $I$, the model with corner self of $x$ and $E$, $\operatorname{toFun}$ applied to $\mathrm{extChartAt}$ applied to $I$ and $W$, $\operatorname{lieBracketWithin}$ applied to $x$, $\operatorname{mpullbackWithin}$ applied to the model with corner self of $x$ and $E$, $I$, $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $W$, $x_{9}$ and the range of $\operatorname{toFun'}$ applied to $I$, $\operatorname{mpullbackWithin}$ applied to the model with corner self of $x$ and $E$, $I$, $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $W$, $V$ and the range of $\operatorname{toFun'}$ applied to $I$ and $\operatorname{inter}$ applied to the preimage of $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $W$ and $x_{8}$ and the range of $\operatorname{toFun'}$ applied to $I$, $W$, $s$ and $x_{7}$.

Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{I'}$ be a model with corner of $\mathrm{E'}$ and $\mathrm{H'}$. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $V$ be a function from elements $x_{13}$ of $\mathrm{M'}$ to tangent spaces of $\mathrm{I'}$ and $x_{13}$. Let $x_{12}$ be an element of $M$. Then $\operatorname{mpullback}$ applied to $I$, $\mathrm{I'}$, $f$, $x_{13}$, $V$ and $x_{12}$ is a tangent space of $I$ and $x_{12}$ defined as the function that maps $x_{12}$ to $\operatorname{inverse}$ applied to $\mathrm{mfderiv}$ applied to $I$, $\mathrm{I'}$, $f$ and $V$, $x_{13}$ applied to $f$ applied to $V$ and $x_{12}$.

Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{I'}$ be a model with corner of $\mathrm{E'}$ and $\mathrm{H'}$. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $V$ be a function from elements $x_{13}$ of $\mathrm{M'}$ to tangent spaces of $\mathrm{I'}$ and $x_{13}$. Let $s$ be an element of $\wp M$. Let $x_{12}$ be an element of $M$. Then $\operatorname{mpullbackWithin}$ applied to $I$, $\mathrm{I'}$, $f$, $x_{13}$, $V$, $s$ and $x_{12}$ is a tangent space of $I$ and $x_{12}$ defined as the function that maps $x_{12}$ to $\operatorname{inverse}$ applied to $\mathrm{mfderivWithin}$ applied to $I$, $\mathrm{I'}$, $f$, $V$ and $s$, $x_{13}$ applied to $f$ applied to $s$ and $x_{12}$.

the polygon (from the name)

The polygon is an embedding of the set of triangles of $R$ and $P$ and the set of polygons of $P$ and $3$.

polygon of P and n (from the name)

Let $P$ be a set. Let $n$ be a natural number. Then the polygons of $P$ and $n$ are a basic type.

poly has nondegenerate edges (from the name)

Let $\mathrm{poly}$ be a polygon of $P$ and $n$. Then $\mathrm{poly}$ has nondegenerate edges, if for all elements $i$ of $\mathrm{Fin}$ applied to $n$, the vertice of $\mathrm{poly}$ and $i$ is distinct from the vertice of $\mathrm{poly}$ and $\operatorname{finRotate}$ applied to $n$ and $i$.

poly has nondegenerate vertices (from the name)

Let $R$ be a set. Let $\mathrm{poly}$ be a polygon of $P$ and $n$. Then $\mathrm{poly}$ has nondegenerate vertices, if for all elements $i$ of $\mathrm{Fin}$ applied to $n$, $\mathrm{AffineIndependent}$ holds for $R$ and $\operatorname{vecCons}$ applied to the vertice of $\mathrm{poly}$ and $i$ and $\operatorname{vecCons}$ applied to the vertice of $\mathrm{poly}$ and $i + 1$ and $\operatorname{vecCons}$ applied to the vertice of $\mathrm{poly}$ and $i + 2$ and $\operatorname{vecEmpty}$.

the boundary of the polygon of R and poly (from the docstring)

Let $R$ be a set. Let $\mathrm{poly}$ be a polygon of $P$ and $n$. Then the boundary of the polygon of $R$ and $\mathrm{poly}$ is an element of $\wp P$ defined as the union of the function that maps $i$ to the edge set of $\mathrm{poly}$ and $i$.

the edge path of poly and i (from the name)

Let $R$ be a set. Let $\mathrm{poly}$ be a polygon of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the edge path of $\mathrm{poly}$ and $i$ is an affine map of $R$ and $P$ defined as the line map of the vertice of $\mathrm{poly}$ and $i$ and the vertice of $\mathrm{poly}$ and $\operatorname{finRotate}$ applied to $n$ and $i$.

the edge set of poly and i (from the name)

Let $R$ be a set. Let $\mathrm{poly}$ be a polygon of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the edge set of $\mathrm{poly}$ and $i$ is an element of $\wp P$ defined as the affine segment of the vertice of $\mathrm{poly}$ and $i$ and the vertice of $\mathrm{poly}$ and $\operatorname{finRotate}$ applied to $n$ and $i$.

the triangle of p (from the name)

Let $R$ be a set. Let $p$ be a polygon of $P$ and $3$ such that $p$ has nondegenerate vertices. Then the triangle of $p$ is a triangle of $R$ and $P$.

the vertice of self and x (from the name)

Let $\mathrm{self}$ be a polygon of $P$ and $n$. Let $x$ be an element of $\mathrm{Fin}$ applied to $n$. Then the vertice of $\mathrm{self}$ and $x$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

ringed space (from the name)

A ringed space is a sheafed space of the set of categories of commutative rings.

Let $X$ be a ringed space. Let $f$ be a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$. Then $\operatorname{basicOpen}$ applied to $X$ and $f$ is an open of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $X$.

the zero locus of X and s (from the docstring)

Let $X$ be a ringed space. Let $s$ be an element of the power set of the set of carriers of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$. Then the zero locus of $X$ and $s$ is an element of the power set of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $X$ defined as the intersection of the function that maps $f$ to the intersection of the function that maps $h$ to the complement of $\operatorname{basicOpen}$ applied to $X$ and $f$.

locally ringed space (from the name)

homomorphism of X and Y (from the name)

the stalk map of f and x (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of the underlying topological space of $X$. Then the stalk map of $f$ and $x$ is a homomorphism of the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $Y$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $f$ and $x$ and the stalk of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $X$ and $x$ defined as the stalk map of the homomorphism of $\operatorname{toShHom}$ applied to $f$ and $x$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{toShHom}$ applied to $f$ is a homomorphism of $\operatorname{toSheafedSpace}$ applied to $X$ and $\operatorname{toSheafedSpace}$ applied to $Y$ defined as the homomorphism of $\operatorname{toHom}$ applied to $f$.

the composition of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the composition of $f$ and $g$ is a homomorphism of $X$ and $Z$.

the empty locally ringed space (from the docstring)

the empty space (from the docstring)

The empty space is an element of $\operatorname{IsInitial}$ applied to $\operatorname{emptyCollection}$ defined as $\operatorname{ofUnique}$ applied to $\operatorname{emptyCollection}$.

the canonical map from the empty locally ringed space of X (from the docstring)

the homomorphism of f and h (from the name)

Let $f$ be a homomorphism of $\operatorname{toSheafedSpace}$ applied to $X$ and $\operatorname{toSheafedSpace}$ applied to $Y$ such that $\mathrm{autoParam}$ holds for the proposition that for all carriers $x$ of the underlying topological space of $X$, the underlying ring hom of the stalk map of the homomorphism of $f$ and $x$ is a local homomorphism and $\mathrm{AlgebraicGeometry\_\_LocallyRingedSpace\_\_homMk\_\_\_auto\_1}$. Then the homomorphism of $f$ and $h$ is a homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to the homomorphism of $f$ and $h$.

the homomorphism of f (from the name)

Let $f$ be a homomorphism of $\operatorname{toSheafedSpace}$ applied to $X$ and $\operatorname{toSheafedSpace}$ applied to $Y$. Then the homomorphism of $f$ is a homomorphism of $X$ and $Y$.

the identity morphism of X (from the docstring)

the isomorphism of f (from the name)

Let $f$ be an isomorphism of $\operatorname{toSheafedSpace}$ applied to $X$ and $\operatorname{toSheafedSpace}$ applied to $Y$. Then the isomorphism of $f$ is an isomorphism of $X$ and $Y$.

the canonical map from the restriction to the subspace of X and h (from the docstring)

the restriction of X and h (from the docstring)

the restriction of X (from the docstring)

the ringed space of X (from the name)

the underlying topological space of X (from the docstring)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to the coequalizer of $\operatorname{toShHom}$ applied to $f$ and $\operatorname{toShHom}$ applied to $g$. Let $s$ be a carrier of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to the coequalizer of $\operatorname{toShHom}$ applied to $f$ and $\operatorname{toShHom}$ applied to $g$ and $\operatorname{op}$ applied to $U$. Then $\operatorname{imageBasicOpen}$ applied to $f$, $g$, $U$ and $s$ is an open of the set of carriers of the underlying topological space of $Y$ defined as $\operatorname{basicOpen}$ applied to the ringed space of $Y$ and $\operatorname{hom}$ applied to the component of $\operatorname{c}$ applied to the homomorphism of the projection of $\operatorname{toShHom}$ applied to $f$ and $\operatorname{toShHom}$ applied to $g$ and $\operatorname{op}$ applied to $U$ and $s$.

the coequalizer of f and g (from the name)

the coequalizer cofork of f and g (from the name)

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the coequalizer cofork of $f$ and $g$ is a cofork of $f$ and $g$.

Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then $\operatorname{coequalizerCoforkIsColimit}$ applied to $f$ and $g$ is an element of $\operatorname{IsColimit}$ applied to the coequalizer cofork of $f$ and $g$.

the coproduct of F (from the name)

the coproduct cofan of F (from the name)

the evaluation of X and x (from the name)

the residue map from the stalk to the residue field of X and x (from the docstring)

the residue field of X and x (from the name)

the residue field map of f and x (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $x$ be a carrier of the underlying topological space of $X$. Then the residue field map of $f$ and $x$ is a homomorphism of the residue field of $Y$ and $\operatorname{hom}$ applied to the base of $\operatorname{toHom}$ applied to $f$ and $x$ and the residue field of $X$ and $x$ defined as the commutative ring category of the map of the underlying ring hom of the stalk map of $f$ and $x$.

the evaluation of X and x (from the name)

f is an open immersion (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ is an open immersion, if $\operatorname{toShHom}$ applied to $f$ is an open immersion.

the inverse application of f and U (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of the set of carriers of the underlying topological space of $X$. Then the inverse application of $f$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{toSheafedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the action of the functor of $f$ and $U$ defined as the inverse application of $\operatorname{toHom}$ applied to $f$ and $U$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isoRestrict}$ applied to $f$ is an isomorphism of $X$ and the restriction of $Y$ and $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_IsOpenImmersion\_\_base\_open}$ defined as the isomorphism of the unique isomorphism of $\operatorname{fullyFaithfulForgetToPresheafedSpace}$ and $\operatorname{isoRestrict}$ applied to $\operatorname{toHom}$ applied to $f$.

the lift of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $g$ is less than or equal to the range of $\operatorname{coe}$ applied to the homomorphism of the base of $\operatorname{toHom}$ applied to $f$. Then the lift of $f$ and $g$ is a homomorphism of $Y$ and $X$ defined as the composition of the inverse of the second projection of the pullback of $f$ and $g$ and the first projection of the pullback of $f$ and $g$.

the functor of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the functor of $f$ is a functor of the set of opens of the set of carriers of the underlying topological space of $X$ and the set of opens of the set of carriers of the underlying topological space of $Y$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$.

f is a open immersion (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Then we can say that $f$ is an open immersion.

the inverse application of f and U (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of the set of carriers of the carrier of $X$. Then the inverse application of $f$ and $U$ is a homomorphism of the action of the presheaf of $X$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $Y$ and $\operatorname{op}$ applied to the action of the functor of $f$ and $U$.

the isomorphism of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the range of $\operatorname{coe}$ applied to the homomorphism of the base of $f$ is equal to the range of $\operatorname{coe}$ applied to the homomorphism of the base of $g$. Then the isomorphism of $f$ and $g$ is an isomorphism of $X$ and $Y$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isoRestrict}$ applied to $f$ is an isomorphism of $X$ and the restriction of $Y$ and $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_IsOpenImmersion\_\_base\_open}$.

the lift of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$ such that the range of $\operatorname{coe}$ applied to the homomorphism of the base of $g$ is less than or equal to the range of $\operatorname{coe}$ applied to the homomorphism of the base of $f$. Then the lift of $f$ and $g$ is a homomorphism of $Y$ and $X$ defined as the composition of the inverse of the second projection of the pullback of $f$ and $g$ and the first projection of the pullback of $f$ and $g$.

the functor of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the functor of $f$ is a functor of the set of opens of the set of carriers of the carrier of $X$ and the set of opens of the set of carriers of the carrier of $Y$ defined as the functor of $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_IsOpenImmersion\_\_base\_open}$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is a pullback cone of $f$ and $g$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is a homomorphism of the restriction of $Y$ and $\mathrm{TopCat\_\_snd\_isOpenEmbedding\_of\_left}$ applied to $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_IsOpenImmersion\_\_base\_open}$ and the base of $g$ and $X$.

the pullback cone of f and g (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Then the pullback cone of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $f$ and $g$ defined as $\operatorname{isLimitAux'}$ applied to the pullback cone of $f$ and $g$ and the function that maps $s$ to the pullback cone of $g$ and $s$.

the pullback cone of g and s (from the name)

Let $f$ be a homomorphism of $X$ and $Z$. Let $g$ be a homomorphism of $Y$ and $Z$. Let $s$ be a pullback cone of $f$ and $g$. Then the pullback cone of $g$ and $s$ is a homomorphism of $\operatorname{pt}$ applied to $s$ and $\operatorname{pt}$ applied to the pullback cone of $f$ and $g$.

the locally ringed space of Y and f (from the name)

the locally ringed space homomorphism of Y and f (from the name)

the sheafed space of Y and f (from the name)

Let $Y$ be a sheafed space of $C$. Let $f$ be a homomorphism of $X$ and $\operatorname{toPresheafedSpace}$ applied to $Y$. Then the sheafed space of $Y$ and $f$ is a sheafed space of $C$.

the sheafed space homomorphism of Y and f (from the name)

Let $Y$ be a sheafed space of $C$. Let $f$ be a homomorphism of $X$ and $\operatorname{toPresheafedSpace}$ applied to $Y$. Then the sheafed space homomorphism of $Y$ and $f$ is a homomorphism of the sheafed space of $Y$ and $f$ and $Y$ defined as the homomorphism of $f$.

f is an open immersion (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then $f$ is an open immersion, if the homomorphism of $f$ is an open immersion.

the inverse application of f and U (from the name)

Let $f$ be a homomorphism of $X$ and $Y$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $X$. Then the inverse application of $f$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $X$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $\operatorname{toPresheafedSpace}$ applied to $Y$ and $\operatorname{op}$ applied to the action of the functor of $f$ and $U$ defined as the inverse application of the homomorphism of $f$ and $U$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{isoRestrict}$ applied to $f$ is an isomorphism of $X$ and the restriction of $Y$ and $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_IsOpenImmersion\_\_base\_open}$ defined as the isomorphism of $\operatorname{isoRestrict}$ applied to the homomorphism of $f$.

the functor of f (from the docstring)

Let $f$ be a homomorphism of $X$ and $Y$. Then the functor of $f$ is a functor of the set of opens of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $X$ and the set of opens of the set of carriers of the carrier of $\operatorname{toPresheafedSpace}$ applied to $Y$.

presheafed space of C (from the name)

Let $C$ be a set. Then the presheafed spaces of $C$ are a basic type.

homomorphism of X and Y (from the name)

Let $X$ and $Y$ be presheafed spaces of $C$. Then the homomorphisms of $X$ and $Y$ are a basic type.

the base of self (from the name)

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the base of $\mathrm{self}$ is a homomorphism of the carrier of $X$ and the carrier of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is a homomorphism of the presheaf of $Y$ and the action of the pushforward functor of $C$ and the base of $\mathrm{self}$ and the presheaf of $X$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $f$ be a homomorphism of $X$ and $Y$. Then $\operatorname{toPshHom}$ applied to $f$ is a homomorphism of $X$ and $Y$ defined as $f$.

the carrier of self (from the name)

Let $\mathrm{self}$ be a presheafed space of $C$. Then the carrier of $\mathrm{self}$ is a topological category defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

the composition of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $x_{2}$ be a homomorphism of $Y$ and $Z$. Then the composition of $x_{1}$ and $x_{2}$ is a homomorphism of $X$ and $Z$ defined as $\operatorname{mk}$ applied to the composition of the base of $x_{1}$ and the base of $x_{2}$ and the composition of $\operatorname{c}$ applied to $x_{2}$ and the map of the pushforward functor of $C$ and the base of $x_{2}$ and $\operatorname{c}$ applied to $x_{1}$.

the constant of X and Z (from the name)

Let $X$ be a topological category. Let $Z$ be an element of $C$. Then the constant of $X$ and $Z$ is a presheafed space of $C$ defined as $\operatorname{mk}$ applied to $X$ and the action of the constant of the set of opposites of the set of opens of the set of carriers of $X$ and $Z$.

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of the set of presheafed spaces of $C$ and the set of topological categories.

the identity morphism of X (from the docstring)

Let $X$ be a presheafed space of $C$. Then the identity morphism of $X$ is a homomorphism of $X$ and $X$ defined as $\operatorname{mk}$ applied to the identity morphism of the carrier of $X$ and the identity morphism of the presheaf of $X$.

the isomorphism of H and x1 (from the name)

Let $H$ be an isomorphism of the carrier of $X$ and the carrier of $Y$. Let $x_{1}$ be an isomorphism of the action of the pushforward functor of $C$ and the homomorphism of $H$ and the presheaf of $X$ and the presheaf of $Y$. Then the isomorphism of $H$ and $x_{1}$ is an isomorphism of $X$ and $Y$.

the map from the restriction of X and h (from the docstring)

Let $X$ be a presheafed space of $C$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the map from the restriction of $X$ and $h$ is a homomorphism of the restriction of $X$ and $h$ and $X$.

the presheaf of self (from the name)

Let $\mathrm{self}$ be a presheafed space of $C$. Then the presheaf of $\mathrm{self}$ is a presheaf of $C$ and the carrier of $\mathrm{self}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

the restriction of X and h (from the docstring)

Let $X$ be a presheafed space of $C$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the restriction of $X$ and $h$ is a presheafed space of $C$ defined as $\operatorname{mk}$ applied to $U$ and the composition of the opposite of the functor of $h$ and the presheaf of $X$.

the isomorphism from the restriction to the top subspace of X (from the docstring)

Let $X$ be a presheafed space of $C$. Then the isomorphism from the restriction to the top subspace of $X$ is an isomorphism of the restriction of $X$ and $\operatorname{isOpenEmbedding}$ applied to the top and $X$.

the sheaf isomorphism of H (from the name)

Let $H$ be an isomorphism of $X$ and $Y$. Then the sheaf isomorphism of $H$ is an isomorphism of the presheaf of $Y$ and the action of the pushforward functor of $C$ and the base of the homomorphism of $H$ and the presheaf of $X$.

the map to the restriction of X (from the docstring)

Let $X$ be a presheafed space of $C$. Then the map to the restriction of $X$ is a homomorphism of $X$ and the restriction of $X$ and $\operatorname{isOpenEmbedding}$ applied to the top defined as $\operatorname{mk}$ applied to the inverse of the inclusion top isomorphism of the carrier of $X$ and $\operatorname{eqToHom}$ applied to $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_restrict\_top\_presheaf}$ applied to $X$.

$\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_\_u393\_}$ is a functor of the set of opposites of the set of presheafed spaces of $C$ and $C$.

the map presheaf of F (from the name)

Let $F$ be a functor of $C$ and $D$. Then the map presheaf of $F$ is a functor of the set of presheafed spaces of $C$ and the set of presheafed spaces of $D$.

Let $x_{2}$ be a homomorphism of $F$ and $G$. Then $\operatorname{onPresheaf}$ applied to $x_{2}$ is a homomorphism of the map presheaf of $G$ and the map presheaf of $F$.

glue data (from the name)

The glue data are a basic type.

the isomorphism sheafed space of D (from the name)

Let $D$ be a glue data. Then the isomorphism sheafed space of $D$ is an isomorphism of $\operatorname{toSheafedSpace}$ applied to $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to the sheafed space glue data of $D$ defined as the glued isomorphism of $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{forgetToSheafedSpace}$.

the sheafed space glue data of D (from the name)

Let $D$ be a glue data. Then the sheafed space glue data of $D$ is a glue data of the set of categories of commutative rings defined as $\operatorname{mk}$ applied to the map glue data of $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{forgetToSheafedSpace}$ and $\mathrm{AlgebraicGeometry\_\_LocallyRingedSpace\_\_GlueData\_\_f\_open}$ applied to $D$.

Let $D$ be a glue data. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then $\operatorname{vPullbackConeIsLimit}$ applied to $D$, $i$ and $j$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $i$ and $j$ defined as $\operatorname{vPullbackConeIsLimitOfMap}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{forgetToSheafedSpace}$, $i$, $j$ and $\operatorname{vPullbackConeIsLimit}$ applied to the sheafed space glue data of $D$, $i$ and $j$.

glue data of C (from the name)

Let $C$ be a set. Then the glue data of $C$ are a basic type.

the diagram over open of D and U (from the name)

Let $D$ be a glue data of $C$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then the diagram over open of $D$ and $U$ is a functor of the set of opposites of the set of walking multispans of the product of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $C$ defined as the componentwise diagram of the multispan of the diagram of $\operatorname{toGlueData}$ applied to $D$ and the action of the functor of $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_GlueData\_\_\_u3b9\_\_isOpenEmbedding}$ applied to $D$ and $i$ and $U$.

the diagram over open projection of U and j (from the name)

Let $D$ be a glue data of $C$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Let $j$ be an element of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then the diagram over open projection of $U$ and $j$ is a homomorphism of the limit of the diagram over open of $D$ and $U$ and the action of the diagram over open of $D$ and $U$ and $\operatorname{op}$ applied to the right of $j$ defined as the projection from the limit object to a value of the functor of the diagram over open of $D$ and $U$ and $\operatorname{op}$ applied to the right of $j$.

the open image preimage map of j and U (from the name)

Let $D$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then the open image preimage map of $j$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and $\operatorname{op}$ applied to $U$ and the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $j$ and $\operatorname{op}$ applied to the action of the map of the base of the inclusion of $\operatorname{toGlueData}$ applied to $D$ and $j$ and the action of the functor of $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_GlueData\_\_\_u3b9\_\_isOpenEmbedding}$ applied to $D$ and $i$ and $U$ defined as the composition of the component of $\operatorname{c}$ applied to $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $i$ and $j$ and $\operatorname{op}$ applied to $U$ and the composition of the component of $\operatorname{c}$ applied to $\operatorname{t}$ applied to $\operatorname{toGlueData}$ applied to $D$, $j$ and $i$ and the action of the opposite of the map of the base of $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $i$ and $j$ and $\operatorname{op}$ applied to $U$ and the composition of the inverse application of $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $j$ and $i$ and the opposite of $\operatorname{op}$ applied to $\operatorname{proj0}$ applied to the map of the base of $\operatorname{t}$ applied to $\operatorname{toGlueData}$ applied to $D$, $j$ and $i$ and the opposite of the action of the opposite of the map of the base of $\operatorname{f}$ applied to $\operatorname{toGlueData}$ applied to $D$, $i$ and $j$ and $\operatorname{op}$ applied to $U$ and the map of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $j$ and the opposite in $\operatorname{eqToHom}$ applied to $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_GlueData\_\_\_u3b9\_\_image\_preimage\_eq}$ applied to $D$, $i$, $j$ and $U$.

the top glue data of D (from the name)

Let $D$ be a glue data of $C$. Then the top glue data of $D$ is a glue data.

Let $D$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then $\operatorname{vPullbackConeIsLimit}$ applied to $D$, $i$ and $j$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $i$ and $j$.

the inclusion inverse application of D and U (from the name)

Let $D$ be a glue data of $C$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then the inclusion inverse application of $D$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and $\operatorname{op}$ applied to $U$ and the limit of the diagram over open of $D$ and $U$.

the inclusion inverse application projection application of U and j (from the name)

Let $D$ be a glue data of $C$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Let $j$ be a walking multispan of the product of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then the inclusion inverse application projection application of $U$ and $j$ is a homomorphism of the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and $\operatorname{op}$ applied to $U$ and the action of the diagram over open of $D$ and $U$ and $\operatorname{op}$ applied to $j$.

Let $D$ be a glue data of $C$. Let $U$ be an open of the set of carriers of the carrier of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$. Then $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_GlueData\_\_\_u3b9\_InvApp\_u3c0\_EqMap}$ applied to $D$ and $U$ is a homomorphism of the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and $\operatorname{op}$ applied to the action of the map of the base of the inclusion of the multispan of the diagram of $\operatorname{toGlueData}$ applied to $D$ and the opposite of $\operatorname{op}$ applied to the right of $i$ and the action of the functor of $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_GlueData\_\_\_u3b9\_\_isOpenEmbedding}$ applied to $D$ and $i$ and $U$ and the action of the presheaf of $\operatorname{U}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $i$ and $\operatorname{op}$ applied to $U$.

glue data of C (from the name)

Let $C$ be a set. Then the glue data of $C$ are a basic type.

the isomorphism presheafed space of D (from the name)

Let $D$ be a glue data of $C$. Then the isomorphism presheafed space of $D$ is an isomorphism of $\operatorname{toPresheafedSpace}$ applied to $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{glued}$ applied to $\operatorname{toGlueData}$ applied to the presheafed space glue data of $D$ defined as the glued isomorphism of $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{forgetToPresheafedSpace}$.

the presheafed space glue data of D (from the name)

Let $D$ be a glue data of $C$. Then the presheafed space glue data of $D$ is a glue data of $C$ defined as $\operatorname{mk}$ applied to the map glue data of $\operatorname{toGlueData}$ applied to $D$ and $\operatorname{forgetToPresheafedSpace}$ and $\mathrm{AlgebraicGeometry\_\_SheafedSpace\_\_GlueData\_\_f\_open}$ applied to $D$.

Let $D$ be a glue data of $C$. Let $i$ and $j$ be elements of $\operatorname{J}$ applied to $\operatorname{toGlueData}$ applied to $D$. Then $\operatorname{vPullbackConeIsLimit}$ applied to $D$, $i$ and $j$ is an element of $\operatorname{IsLimit}$ applied to the pullback cone of $i$ and $j$ defined as $\operatorname{vPullbackConeIsLimitOfMap}$ applied to $\operatorname{toGlueData}$ applied to $D$, $\operatorname{forgetToPresheafedSpace}$, $i$, $j$ and $\operatorname{vPullbackConeIsLimit}$ applied to the presheafed space glue data of $D$, $i$ and $j$.

the colimit presheaf object isomorphism componentwise limit of F and U (from the name)

Let $F$ be a functor of $J$ and the set of presheafed spaces of $C$. Let $U$ be an open of the set of carriers of the carrier of the colimit of $F$. Then the colimit presheaf object isomorphism componentwise limit of $F$ and $U$ is an isomorphism of the action of the presheaf of the colimit of $F$ and $\operatorname{op}$ applied to $U$ and the limit of the componentwise diagram of $F$ and $U$.

the componentwise diagram of F and U (from the name)

Let $F$ be a functor of $J$ and the set of presheafed spaces of $C$. Let $U$ be an open of the set of carriers of the carrier of the colimit of $F$. Then the componentwise diagram of $F$ and $U$ is a functor of the set of opposites of $J$ and $C$.

the pushforward diagram to colimit of F (from the name)

Let $F$ be a functor of $J$ and the set of presheafed spaces of $C$. Then the pushforward diagram to colimit of $F$ is a functor of $J$ and the set of opposites of the set of presheafs of $C$ and the colimit of the composition of $F$ and $\operatorname{forget}$ applied to $C$.

sheafed space of C (from the name)

Let $C$ be a set. Then the sheafed spaces of $C$ are a basic type.

Let $C$ be a set. Then $\operatorname{forget}$ applied to $C$ is a functor of the set of sheafed spaces of $C$ and the set of topological categories.

$\operatorname{forgetToPresheafedSpace}$ is a functor of the set of sheafed spaces of $C$ and the set of presheafed spaces of $C$ defined as the induced functor of $\operatorname{toPresheafedSpace}$.

$\operatorname{fullyFaithfulForgetToPresheafedSpace}$ is an element of $\operatorname{FullyFaithful}$ applied to $\operatorname{forgetToPresheafedSpace}$.

the isomorphism of e (from the name)

Let $e$ be an isomorphism of $\operatorname{toPresheafedSpace}$ applied to $X$ and $\operatorname{toPresheafedSpace}$ applied to $Y$. Then the isomorphism of $e$ is an isomorphism of $X$ and $Y$.

the map from the restriction of X and h (from the docstring)

Let $X$ be a sheafed space of $C$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the map from the restriction of $X$ and $h$ is a homomorphism of the restriction of $X$ and $h$ and $X$ defined as the homomorphism of the map from the restriction of $\operatorname{toPresheafedSpace}$ applied to $X$ and $h$.

the restriction of X and h (from the docstring)

Let $X$ be a sheafed space of $C$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Then the restriction of $X$ and $h$ is a sheafed space of $C$.

the restriction of X (from the docstring)

Let $X$ be a sheafed space of $C$. Then the restriction of $X$ is an isomorphism of the restriction of $X$ and $\operatorname{isOpenEmbedding}$ applied to the top and $X$ defined as the isomorphism of the isomorphism from the restriction to the top subspace of $\operatorname{toPresheafedSpace}$ applied to $X$.

the sheaf of X (from the name)

Let $X$ be a sheafed space of $C$. Then the sheaf of $X$ is a sheaf of $C$ and the carrier of $\operatorname{toPresheafedSpace}$ applied to $X$ defined as $\operatorname{mk}$ applied to the presheaf of $\operatorname{toPresheafedSpace}$ applied to $X$ and $\operatorname{IsSheaf}$ applied to $X$.

the unit of X (from the name)

Let $X$ be a topological category. Then the unit of $X$ is a sheafed space of $\operatorname{Discrete}$ applied to $\mathrm{Unit}$.

$\mathrm{AlgebraicGeometry\_\_SheafedSpace\_\_\_u393\_}$ is a functor of the set of opposites of the set of sheafed spaces of $C$ and $C$ defined as the composition of the opposite of $\operatorname{forgetToPresheafedSpace}$ and $\mathrm{AlgebraicGeometry\_\_PresheafedSpace\_\_\_u393\_}$.

the stalk map of x1 and x2 (from the name)

Let $x_{1}$ be a homomorphism of $X$ and $Y$. Let $x_{2}$ be a carrier of the carrier of $X$. Then the stalk map of $x_{1}$ and $x_{2}$ is a homomorphism of the stalk of the presheaf of $Y$ and $\operatorname{hom}$ applied to the base of $x_{1}$ and $x_{2}$ and the stalk of the presheaf of $X$ and $x_{2}$ defined as the composition of the map of the stalk functor of $C$ and $\operatorname{hom}$ applied to the base of $x_{1}$ and $x_{2}$ and $\operatorname{c}$ applied to $x_{1}$ and $\operatorname{stalkPushforward}$ applied to $C$, the base of $x_{1}$, the presheaf of $X$ and $x_{2}$.

Let $X$ be a presheafed space of $C$. Assume that $\operatorname{coe}$ applied to the homomorphism of $f$ is an open embedding. Let $x_{1}$ be a carrier of $U$. Then $\operatorname{restrictStalkIso}$ applied to $X$, $h_{1}$ and $x_{1}$ is an isomorphism of the stalk of the presheaf of the restriction of $X$ and $h_{1}$ and $x_{1}$ and the stalk of the presheaf of $X$ and $\operatorname{hom}$ applied to $f$ and $x_{1}$ defined as the colimit isomorphism of the opposite of the functor neighbourhood filter of $h_{1}$ and $x_{1}$ and the composition of the opposite of the inclusion of $\operatorname{hom}$ applied to $f$ and $x_{1}$ and the presheaf of $X$.

the stalk isomorphism of x1 and x2 (from the name)

Let $x_{1}$ be an isomorphism of $X$ and $Y$. Let $x_{2}$ be a carrier of the carrier of $X$. Then the stalk isomorphism of $x_{1}$ and $x_{2}$ is an isomorphism of the stalk of the presheaf of $Y$ and $\operatorname{hom}$ applied to the base of the homomorphism of $x_{1}$ and $x_{2}$ and the stalk of the presheaf of $X$ and $x_{2}$ defined as $\operatorname{asIso}$ applied to the stalk map of the homomorphism of $x_{1}$ and $x_{2}$.