ConvexConestructureMathlib.Geometry.Convex.Cone.Basic, typeWording
convex cone of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the convex cones of $R$ and $M$ are a basic type.
ConvexCone.BluntdefMathlib.Geometry.Convex.Cone.Basic, predicateEnglish
Let $C$ be a convex cone of $R$ and $M$. Then $\operatorname{Blunt}$ holds for $C$, if $0$ is not an element of $C$.
ConvexCone.FlatdefMathlib.Geometry.Convex.Cone.Basic, predicateWording
C is flat (from the docstring)
English
Let $C$ be a convex cone of $R$ and $G$. Then $C$ is flat, if there exists an element $x_{4}$ of $G$, such that $x_{4}$ is an element of $C$, $x_{4} \neq 0$ and $\MembershipmemMACRoT {C}{\operatorname{neg} (x_{4})}$.
ConvexCone.IsReproducingdefMathlib.Geometry.Convex.Cone.Basic, predicateEnglish
Let $C$ be a convex cone of $R$ and $M$. Then $\operatorname{IsReproducing}$ holds for $C$, if $C - C$ is equal to the universal set.
ConvexCone.PointeddefMathlib.Geometry.Convex.Cone.Basic, predicateWording
C is pointed (from the docstring)
English
Let $C$ be a convex cone of $R$ and $M$. Then $C$ is pointed, if $0$ is an element of $C$.
ConvexCone.SalientdefMathlib.Geometry.Convex.Cone.Basic, predicateEnglish
Let $C$ be a convex cone of $R$ and $G$. Then $\operatorname{Salient}$ holds for $C$, if for all elements $x_{4}$ of $G$, if $x_{4}$ is an element of $C$, then if $x_{4} \neq 0$, then $\operatorname{neg}$ applied to $x_{4}$ is not an element of $C$.
ConvexCone.carrierdefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a convex cone of $R$ and $M$. Then the carrier of $\mathrm{self}$ is an element of $\wp M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ConvexCone.comapdefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the preimage of f and C (from the docstring)
English
Let $f$ be a linear map of $M$ and $N$. Let $C$ be a convex cone of $R$ and $N$. Then the preimage of $f$ and $C$ is a convex cone of $R$ and $M$.
ConvexCone.copydefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the copy of C and s (from the name)
English
Let $C$ be a convex cone of $R$ and $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{C}$. Then the copy of $C$ and $s$ is a convex cone of $R$ and $M$.
ConvexCone.gidefMathlib.Geometry.Convex.Cone.Basic, function or constantEnglish
$\operatorname{gi}$ is a Galois insertion of $\operatorname{hull}$ applied to $R$ and $\operatorname{instSetLike}$.
ConvexCone.hulldefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the cone hull of R and s (from the docstring)
English
Let $R$ be a set. Let $s$ be an element of $\wp M$. Then the cone hull of $R$ and $s$ is a convex cone of $R$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $C$ to $\mathrm{Leq} (s , C)$.
ConvexCone.mapdefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the map of f and C (from the name)
English
Let $f$ be a linear map of $M$ and $N$. Let $C$ be a convex cone of $R$ and $M$. Then the map of $f$ and $C$ is a convex cone of $R$ and $N$.
ConvexCone.positivedefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the positive cone of R and M (from the docstring)
English
Let $R$ and $M$ be sets. Then the positive cone of $R$ and $M$ is a convex cone of $R$ and $M$.
ConvexCone.strictlyPositivedefMathlib.Geometry.Convex.Cone.Basic, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{strictlyPositive}$ applied to $R$ and $M$ is a convex cone of $R$ and $M$.
Submodule.toConvexConedefMathlib.Geometry.Convex.Cone.Basic, function or constantWording
the convex cone of C (from the name)
English
Let $C$ be a submodule of $R$ and $M$. Then the convex cone of $C$ is a convex cone of $R$ and $M$ defined as $\operatorname{mk}$ applied to $C$, the function that maps $c$, $h$, $x_{4}$ and $\mathrm{hx}$ to $\mathrm{Submodule\_\_smul\_mem}$ applied to $C$, $c$ and $\mathrm{hx}$ and the function that maps $x_{5}$, $\mathrm{hx1}$, $x_{6}$ and $\mathrm{hy}$ to $\mathrm{Submodule\_\_add\_mem}$ applied to $C$, $\mathrm{hx1}$ and $\mathrm{hy}$.
PointedCone.dualdefMathlib.Geometry.Convex.Cone.Dual, function or constantWording
the dual cone of p and s (from the docstring)
English
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $s$ be an element of $\wp M$. Then the dual cone of $p$ and $s$ is a pointed cone of $R$ and $N$.
PointedCone.DualFGdefMathlib.Geometry.Convex.Cone.DualFinite, predicateEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $C$ be a pointed cone of $R$ and $N$. Then $\operatorname{DualFG}$ holds for $p$ and $C$, if there exists a finite set $s$ of $M$, such that the dual cone of $p$ and $s$ is equal to $C$.
PointedCone.IsFaceOfstructureMathlib.Geometry.Convex.Cone.Face.Basic, predicateEnglish
Let $F$ and $C$ be pointed cones of $R$ and $M$. Then we can say that $\operatorname{IsFaceOf}$ holds for $F$ and $C$.
PointedCone.FacestructureMathlib.Geometry.Convex.Cone.Face.Lattice, typeWording
face of C (from the name)
English
Let $C$ be a pointed cone of $R$ and $M$. Then the faces of $C$ are a basic type.
PointedCone.Face.fstdefMathlib.Geometry.Convex.Cone.Face.Lattice, function or constantWording
the first component of F (from the name)
English
Let $F$ be a face of the product of $x_{6}$ and $x_{7}$. Then the first component of $F$ is a face of $x_{6}$.
PointedCone.Face.proddefMathlib.Geometry.Convex.Cone.Face.Lattice, function or constantWording
the product of x8 and x9 (from the name)
English
Let $x_{8}$ be a face of $x_{6}$. Let $x_{9}$ be a face of $x_{7}$. Then the product of $x_{8}$ and $x_{9}$ is a face of the product of $x_{6}$ and $x_{7}$.
PointedCone.Face.prodOrderIsodefMathlib.Geometry.Convex.Cone.Face.Lattice, function or constantWording
the face lattice of the product of two cones of C and D (from the docstring)
English
Let $C$ be a pointed cone of $R$ and $M$. Let $D$ be a pointed cone of $R$ and $N$. Then the face lattice of the product of two cones of $C$ and $D$ is an order isomorphism of the set of faces of the product of $C$ and $D$ and $\mathrm{Prod}$ applied to the set of faces of $C$ and the set of faces of $D$.
PointedCone.Face.snddefMathlib.Geometry.Convex.Cone.Face.Lattice, function or constantWording
the second component of F (from the name)
English
Let $F$ be a face of the product of $x_{6}$ and $x_{7}$. Then the second component of $F$ is a face of $x_{7}$.
PointedCone.Face.toPointedConedefMathlib.Geometry.Convex.Cone.Face.Lattice, function or constantWording
the pointed cone of F (from the name)
English
Let $F$ be a face of $C$. Then the pointed cone of $F$ is a pointed cone of $R$ and $M$ defined as $\operatorname{toSubmodule}$ applied to $F$.
ConvexCone.toPointedConedefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the pointed cone of C and hC (from the name)
English
Let $C$ be a pointed convex cone of $R$ and $E$. Then the pointed cone of $C$ and $\mathrm{hC}$ is a pointed cone of $R$ and $E$.
PointedConedefMathlib.Geometry.Convex.Cone.Pointed, typeWording
pointed cone of R and E (from the name)
English
Let $R$ and $E$ be sets. Then a pointed cone of $R$ and $E$ is an element of the function that maps $R$ and $E$ to the set of submodules of $\mathrm{Nonneg}$ applied to $R$ and $E$.
PointedCone.comapdefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the preimage of f and C (from the docstring)
English
Let $f$ be a linear map of $E$ and $F$. Let $C$ be a pointed cone of $R$ and $F$. Then the preimage of $f$ and $C$ is a pointed cone of $R$ and $E$ defined as the preimage of $\operatorname{restrictScalars}$ applied to $\mathrm{Nonneg}$ applied to $R$ and $f$ and $C$.
PointedCone.hulldefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the cone hull of R and s (from the docstring)
English
Let $R$ be a set. Let $s$ be an element of $\wp E$. Then the cone hull of $R$ and $s$ is a pointed cone of $R$ and $E$ defined as the span of $\mathrm{Nonneg}$ applied to $R$ and $s$.
PointedCone.linealdefMathlib.Geometry.Convex.Cone.Pointed, function or constantEnglish
Let $C$ be a pointed cone of $R$ and $E$. Then $\operatorname{lineal}$ applied to $C$ is a submodule of $R$ and $E$.
PointedCone.mapdefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the map of f and C (from the name)
English
Let $f$ be a linear map of $E$ and $F$. Let $C$ be a pointed cone of $R$ and $E$. Then the map of $f$ and $C$ is a pointed cone of $R$ and $F$ defined as the map of $\operatorname{restrictScalars}$ applied to $\mathrm{Nonneg}$ applied to $R$ and $f$ and $C$.
PointedCone.ofConeCombdefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the pointed cone of C (from the name)
English
Let $C$ be an element of $\wp E$ such that $C$ is nonempty and for all elements $x_{4}$ of $E$, if $x_{4}$ is an element of $C$, then for all elements $y$ of $E$, if $y$ is an element of $C$, then for all elements $a$ of $R$, if $0 \leq a$, then for all elements $b$ of $R$, if $0 \leq b$, then $\HSMulhSMulMACRoAL {a}{x_{4}}+ \HSMulhSMulMACRoAL {b}{y}$ is an element of $C$. Then the pointed cone of $C$ is a pointed cone of $R$ and $E$.
PointedCone.ofSubmoduledefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the pointed cone of S (from the name)
English
Let $S$ be a submodule of $R$ and $E$. Then the pointed cone of $S$ is a pointed cone of $R$ and $E$ defined as $\operatorname{restrictScalars}$ applied to $\mathrm{Nonneg}$ applied to $R$ and $S$.
PointedCone.ofSubmoduleEmbeddingdefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the pointed cone (from the name)
English
The pointed cone is an order embedding of the set of submodules of $R$ and $E$ and the set of pointed cones of $R$ and $E$ defined as $\operatorname{restrictScalarsEmbedding}$ applied to $\mathrm{Nonneg}$ applied to $R$, $R$ and $E$.
PointedCone.ofSubmoduleLatticeHomdefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the pointed cone (from the name)
English
The pointed cone is a complete lattice homomorphism of the set of submodules of $R$ and $E$ and the set of pointed cones of $R$ and $E$ defined as $\operatorname{restrictScalarsLatticeHom}$ applied to $\mathrm{Nonneg}$ applied to $R$, $R$ and $E$.
PointedCone.positivedefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the positive cone of R and E (from the docstring)
English
Let $R$ and $E$ be sets. Then the positive cone of $R$ and $E$ is a pointed cone of $R$ and $E$.
PointedCone.toConvexConedefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the convex cone of C (from the name)
English
Let $C$ be a pointed cone of $R$ and $E$. Then the convex cone of $C$ is a convex cone of $R$ and $E$.
PointedCone.toSubmoduledefMathlib.Geometry.Convex.Cone.Pointed, function or constantWording
the submodule of hC (from the name)
English
Assume that $C$ is a self negation. Then the submodule of $\mathrm{hC}$ is a submodule of $R$ and $E$.
PointedCone.IsSimplicialdefMathlib.Geometry.Convex.Cone.Simplicial, predicateWording
C is simplicial (from the docstring)
English
Let $C$ be a pointed cone of $R$ and $M$. Then $C$ is simplicial, if there exists an element $s$ of $\wp M$, such that $s$ is finite, $\mathrm{LinearIndepOn}$ holds for $R$, $\mathrm{id}$ and $s$ and the cone hull of $R$ and $s$ is equal to $C$.
PointedCone.maxTensorProductdefMathlib.Geometry.Convex.Cone.TensorProduct, function or constantWording
the maximum tensor product of x6 and x7 (from the name)
English
Let $x_{6}$ be a pointed cone of $R$ and $G$. Let $x_{7}$ be a pointed cone of $R$ and $H$. Then the maximum tensor product of $x_{6}$ and $x_{7}$ is a pointed cone of $R$ and the set of tensor products of $G$ and $H$ defined as the dual cone of $\operatorname{dualDistrib}$ applied to $R$, $G$ and $H$ and the minimum tensor product of the dual cone of the evaluation of $R$ and $G$ and $x_{6}$ and the dual cone of the evaluation of $R$ and $H$ and $x_{7}$.
PointedCone.minTensorProductdefMathlib.Geometry.Convex.Cone.TensorProduct, function or constantWording
the minimum tensor product of x6 and x7 (from the name)
English
Let $x_{6}$ be a pointed cone of $R$ and $G$. Let $x_{7}$ be a pointed cone of $R$ and $H$. Then the minimum tensor product of $x_{6}$ and $x_{7}$ is a pointed cone of $R$ and the set of tensor products of $G$ and $H$ defined as the cone hull of $R$ and the image of $x_{6}$ and $x_{7}$.
Convexity.ConvexSpace.AffineMapstructureMathlib.Geometry.Convex.ConvexSpace.AffineMap, typeWording
affine map of X and Y (from the name)
English
Let $R$, $X$ and $Y$ be sets. Then the affine maps of $X$ and $Y$ are a basic type.
Convexity.ConvexSpace.AffineMap.compdefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an affine map of $Y$ and $Z$. Let $f$ be an affine map of $X$ and $Y$. Then the composition of $g$ and $f$ is an affine map of $X$ and $Z$.
Convexity.ConvexSpace.AffineMap.constdefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the constant of y (from the name)
English
Let $y$ be an element of $Y$. Then the constant of $y$ is an affine map of $X$ and $Y$.
Convexity.ConvexSpace.AffineMap.iddefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the identity of X (from the name)
English
Let $X$ be a set. Then the identity of $X$ is an affine map of $X$ and $X$.
Convexity.ConvexSpace.AffineMap.toFundefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the underlying map of self and x4 (from the docstring)
English
Let $\mathrm{self}$ be an affine map of $X$ and $Y$. Let $x_{4}$ be an element of $X$. Then the underlying map of $\mathrm{self}$ and $x_{4}$ is an element of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
Convexity.StdSimplex.affineMapdefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the affine map of f (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Then the affine map of $f$ is an affine map of $\operatorname{StdSimplex}$ applied to $R$ and $M$ and $\operatorname{StdSimplex}$ applied to $R$ and $N$.
Convexity.StdSimplex.affineMapMkdefMathlib.Geometry.Convex.ConvexSpace.AffineMap, function or constantWording
the affine map of f (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $X$. Then the affine map of $f$ is an affine map of $\operatorname{StdSimplex}$ applied to $R$ and $M$ and $X$.
Convexity.ConvexSpace.AffineMap.conedefMathlib.Geometry.Convex.ConvexSpace.AffineMapCone, function or constantWording
the cone of s and y (from the docstring)
English
Let $s$ be an affine map of $\operatorname{StdSimplex}$ applied to $R$ and $\mathrm{Fin}$ applied to $n$ and $Y$. Let $y$ be an element of $Y$. Then the cone of $s$ and $y$ is an affine map of $\operatorname{StdSimplex}$ applied to $R$ and $\mathrm{Fin}$ applied to $n + 1$ and $Y$ defined as the affine map of the function that maps $i$ to $\operatorname{cases}$ applied to $y$, the function that maps $i_{1}$ to $s$ applied to $\operatorname{single}$ applied to $i_{1}$ and $i$.
AddTorsor.convexCombinationdefMathlib.Geometry.Convex.ConvexSpace.AffineSpace, function or constantWording
the convex combination of s (from the name)
English
Let $s$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $P$. Then the convex combination of $s$ is an element of $P$ defined as $\operatorname{affineCombination}$ applied to $R$, $\FinsuppsupportMACRoR {\operatorname{weights} (s)}$, $\mathrm{id}$ and $\operatorname{coe}$ applied to $\operatorname{weights}$ applied to $s$.
Convexity.IsAffineConvexSpaceclassMathlib.Geometry.Convex.ConvexSpace.AffineSpace, predicateEnglish
Let $R$, $V$ and $P$ be sets. Then we can say that $\operatorname{IsAffineConvexSpace}$ holds for $R$, $V$ and $P$.
Convexity.StdSimplex.barycenterdefMathlib.Geometry.Convex.ConvexSpace.Barycenter, function or constantWording
the barycenter of the standard simplex (from the docstring)
English
The barycenter of the standard simplex is an element of $\operatorname{StdSimplex}$ applied to $K$ and $M$.
Convexity.StdSimplex.subBarycenterdefMathlib.Geometry.Convex.ConvexSpace.Barycenter, function or constantWording
the difference barycenter of S and hS (from the name)
English
Let $S$ be a nonempty finite set of $M$. Then the difference barycenter of $S$ and $\mathrm{hS}$ is an element of $\operatorname{StdSimplex}$ applied to $K$ and $M$.
Convexity.ConvexSpaceclassMathlib.Geometry.Convex.ConvexSpace.Defs, predicateEnglish
Let $R$ and $X$ be sets. Then we can say that $\operatorname{ConvexSpace}$ holds for $R$ and $X$.
Convexity.ConvexSpace.sConvexCombdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the convex comb of f (from the name)
English
Let $f$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$. Then the convex comb of $f$ is an element of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $f$.
Convexity.IsAffineMapstructureMathlib.Geometry.Convex.ConvexSpace.Defs, predicateWording
R is affine (from the docstring)
English
Let $R$ be a set. Let $f$ be a function from elements of $X$ to elements of $Y$. Then we can say that $R$ is affine.
Convexity.IsConvexCombCommclassMathlib.Geometry.Convex.ConvexSpace.Defs, predicateWording
X is a convex comb commutative with respect to S (from the name)
English
Let $R$, $S$ and $X$ be sets. Then we can say that $X$ is a convex comb commutative with respect to $S$.
Convexity.StdSimplexstructureMathlib.Geometry.Convex.ConvexSpace.Defs, typeEnglish
Let $R$ and $X$ be sets. Then the elements of $\operatorname{StdSimplex}$ applied to $R$ and $X$ are a basic type.
Convexity.StdSimplex.dupledefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantEnglish
Let $x_{2}$ and $y$ be elements of $X$. Assume that $0 \leq s$. Assume that $0 \leq t$. Assume that $\EqtMACRoH {s + t}{1}$. Then $\operatorname{duple}$ applied to $x_{2}$, $y$, $\mathrm{hs}$, $\mathrm{ht}$ and $h_{1}$ is an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$.
Convexity.StdSimplex.equivIccdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the bijection between the one dimensional standard simplex and the interval (from the docstring)
English
The bijection between the one dimensional standard simplex and the interval is an equivalence from $\operatorname{StdSimplex}$ applied to $\mathrm{R'}$ and $\mathrm{Fin}$ applied to $2$ to the set of elements of $\SetIccMACRoP {0}{1}$.
Convexity.StdSimplex.joindefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the join of f (from the name)
English
Let $f$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $\operatorname{StdSimplex}$ applied to $R$ and $X$. Then the join of $f$ is an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$.
Convexity.StdSimplex.mapdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the map of g and f (from the name)
English
Let $g$ be a function from elements of $X$ to elements of $Y$. Let $f$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$. Then the map of $g$ and $f$ is an element of $\operatorname{StdSimplex}$ applied to $R$ and $Y$.
Convexity.StdSimplex.restrictdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantEnglish
Let $w$ be an element of $\operatorname{StdSimplex}$ applied to $K$ and $X$. Let $s$ be an element of $\wp X$ such that there exists an element $x_{2}$ of $X$, such that $x_{2}$ is an element of $s$ and $\operatorname{weights} (w , x_{2})\neq 0$. Then $\operatorname{restrict}$ applied to $w$, $s$ and $\mathrm{hs}$ is an element of $\operatorname{StdSimplex}$ applied to $K$ and $X$.
Convexity.StdSimplex.singledefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantEnglish
Let $x_{2}$ be an element of $X$. Then $\operatorname{single}$ applied to $x_{2}$ is an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$.
Convexity.StdSimplex.weightsdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $X$. Then $\operatorname{weights}$ applied to $\mathrm{self}$ is an element of $\FinsuppMACRoQ {X}{R}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Convexity.convexCombPairdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the convex comb pair of x3 and y (from the name)
English
Let $s$ and $t$ be elements of $R$ such that $0 \leq s$, $0 \leq t$ and $\EqtMACRoH {s + t}{1}$. Let $x_{3}$ and $y$ be elements of $X$. Then the convex comb pair of $x_{3}$ and $y$ is an element of $X$ defined as the convex comb of $\operatorname{duple}$ applied to $x_{3}$, $y$, $\mathrm{hs}$, $\mathrm{ht}$ and $\mathrm{hst}$.
Convexity.iConvexCombdefMathlib.Geometry.Convex.ConvexSpace.Defs, function or constantWording
the convex comb of s and f (from the name)
English
Let $s$ be an element of $\operatorname{StdSimplex}$ applied to $R$ and $I$. Let $f$ be a function from elements of $I$ to elements of $X$. Then the convex comb of $s$ and $f$ is an element of $X$ defined as the convex comb of the map of $f$ and $s$.
Convexity.IsModuleConvexSpaceclassMathlib.Geometry.Convex.ConvexSpace.Module, predicateEnglish
Let $R$ and $M$ be sets. Then we can say that $\operatorname{IsModuleConvexSpace}$ holds for $R$ and $M$.
Convexity.StdSimplex.homeomorphIdefMathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex, function or constantWording
the homeomorphism (from the name)
English
The homeomorphism is a homeomorphism of $\operatorname{StdSimplex}$ applied to $\Real$ and $\mathrm{Fin}$ applied to $2$ and the set of elements of the unit interval.
Convexity.convexHulldefMathlib.Geometry.Convex.Hull, function or constantWording
the convex hull of R (from the docstring)
English
Let $R$ be a set. Then the convex hull of $R$ is a closure operator of $\wp X$ defined as the closure operator of the proposition that $\operatorname{IsConvexSet}$ and the function that maps $x_{3}$ to $\operatorname{sInter}$.
Convexity.IsConvexSetdefMathlib.Geometry.Convex.Set, predicateWording
s is a convex set (from the name)
English
Let $R$ be a set. Let $s$ be an element of $\wp X$. Then $s$ is a convex set, if for all elements $w$ of $\operatorname{StdSimplex}$ applied to $R$ and $X$, if $\FinsuppsupportMACRoR {\operatorname{weights} (w)}\leq s$, then the convex comb of $w$ is an element of $s$.
Convexity.IsStarConvexSetdefMathlib.Geometry.Convex.Star, predicateEnglish
Let $R$ be a set. Let $x_{3}$ be an element of $X$. Let $s$ be an element of $\wp X$. Then $\operatorname{IsStarConvexSet}$ holds for $R$, $x_{3}$ and $s$, if for all elements $y$ of $X$, if $y$ is an element of $s$, then for all elements $a$ and $b$ of $R$, for all elements $\mathrm{ha}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (0 , a)$, for all elements $\mathrm{hb}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (0 , b)$, for all elements $\mathrm{hab}$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {(a + b)}{1}$, the convex comb pair of $x_{3}$ and $y$ is an element of $s$.
DiffeologicalSpaceclassMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $X$ be a set. Then we can say that $\mathrm{DiffeologicalSpace}$ holds for $X$.
DiffeologicalSpace.CorePlotsOnstructureMathlib.Geometry.Diffeology.Basic, typeEnglish
Let $X$ be a set. Then the elements of $\operatorname{CorePlotsOn}$ applied to $X$ are a basic type.
DiffeologicalSpace.CorePlotsOn.isPlotdefMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $\mathrm{self}$ be an element of $\operatorname{CorePlotsOn}$ applied to $X$. Let $x$ be a function from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$. Then $\operatorname{isPlot}$ holds for $\mathrm{self}$ and $x$, if $\operatorname{proj2}$ holds for $\mathrm{self}$ and $x$.
DiffeologicalSpace.CorePlotsOn.isPlotOndefMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $\mathrm{self}$ be an element of $\operatorname{CorePlotsOn}$ applied to $X$. Assume that $u$ is open. Let $x$ be a function from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$. Then $\operatorname{isPlotOn}$ holds for $\mathrm{self}$, $\mathrm{hu}$ and $x$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $\mathrm{hu}$ and $x$.
DiffeologicalSpace.giGenerateFromdefMathlib.Geometry.Diffeology.Basic, function or constantEnglish
Let $X$ be a set. Then $\operatorname{giGenerateFrom}$ applied to $X$ is a Galois insertion of $\operatorname{generateFrom}$ and $\operatorname{toPlots}$.
DiffeologicalSpace.plotsdefMathlib.Geometry.Diffeology.Basic, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{plots}$ applied to $n$ is an element of the power set of the set of functions from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.
DiffeologicalSpace.toPlotsdefMathlib.Geometry.Diffeology.Basic, function or constantEnglish
Assume that $\mathrm{DiffeologicalSpace}$ holds for $X$. Then $\operatorname{toPlots}$ applied to $x$ is an element of the power set of $\Sigma$ applied to the function that maps $n$ to the set of functions from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\operatorname{IsPlot}$ applied to $\operatorname{snd}$ applied to $p$.
Diffeology.DSmoothdefMathlib.Geometry.Diffeology.Basic, predicateWording
f is smooth (from the name)
English
Let $f$ be a function from elements of $X$ to elements of $Y$. Then $f$ is smooth, if for all natural numbers $n$, for all functions $p$ from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$, if $\operatorname{IsPlot}$ holds for $p$, then $\operatorname{IsPlot}$ holds for $\operatorname{comp}$ applied to $f$ and $p$.
Diffeology.IsContDiffCompatibleclassMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $X$ be a set. Then we can say that $\operatorname{IsContDiffCompatible}$ holds for $X$.
Diffeology.IsDTopologyCompatibleclassMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $X$ be a set. Then we can say that $\operatorname{IsDTopologyCompatible}$ holds for $X$.
Diffeology.IsPlotdefMathlib.Geometry.Diffeology.Basic, predicateEnglish
Let $p$ be a function from Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ to elements of $X$. Then $\operatorname{IsPlot}$ holds for $p$, if $\MembershipmemMACRoT {\operatorname{plots} (n)}{p}$.
Affine.Simplex.altitudedefMathlib.Geometry.Euclidean.Altitude, function or constantWording
the altitude of s and i (from the name)
English
Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the altitude of $s$ and $i$ is an affine subspace of $\Real$ and $P$ defined as the minimum of $\operatorname{mk'}$ applied to the point of $s$ and $i$ and $\operatorname{orthogonal}$ applied to the direction of the affine span of $\Real$ and the image of $\operatorname{points}$ applied to $s$ and the complement of $\operatorname{singleton}$ applied to $i$ and the affine span of $\Real$ and the range of $\operatorname{points}$ applied to $s$.
Affine.Simplex.evalHeightdefMathlib.Geometry.Euclidean.Altitude, function or constantWording
the evaluation height (from the name)
English
The evaluation height is an element of $\operatorname{PositivityExt}$.
Affine.Simplex.heightdefMathlib.Geometry.Euclidean.Altitude, function or constantWording
the height of s and i (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the height of $s$ and $i$ is a real number defined as the distance of the point of $s$ and $i$ and $\operatorname{altitudeFoot}$ applied to $s$ and $i$.
EuclideanGeometry.odefMathlib.Geometry.Euclidean.Angle.Oriented.Affine, function or constantEnglish
$\operatorname{o}$ is an orientation of $M$ and $x_{4}$ defined as the positive orientation.
EuclideanGeometry.oangledefMathlib.Geometry.Euclidean.Angle.Oriented.Affine, function or constantEnglish
Let $x_{5}$, $x_{6}$ and $x_{7}$ be elements of $P$. Then $\operatorname{oangle}$ applied to $x_{5}$, $x_{6}$ and $x_{7}$ is an angle defined as $\operatorname{oangle}$ applied to $\operatorname{o}$, the vector difference of $x_{5}$ and $x_{6}$ and the vector difference of $x_{7}$ and $x_{6}$.
Orientation.oangledefMathlib.Geometry.Euclidean.Angle.Oriented.Basic, function or constantEnglish
Let $o$ be an orientation of $V$ and $\mathrm{Fin}$ applied to $2$. Let $x_{2}$ and $y$ be elements of $V$. Then $\operatorname{oangle}$ applied to $o$, $x_{2}$ and $y$ is an angle defined as the coercion of $\operatorname{arg}$ applied to $\operatorname{coe}$ applied to $\operatorname{kahler}$ applied to $o$, $x_{2}$ and $y$.
Orientation.rotationdefMathlib.Geometry.Euclidean.Angle.Oriented.Rotation, function or constantWording
the rotation of o and x2 (from the name)
English
Let $o$ be an orientation of $V$ and $\mathrm{Fin}$ applied to $2$. Let $x_{2}$ be an angle. Then the rotation of $o$ and $x_{2}$ is a linear isometry equivalence of $V$ and $V$.
EuclideanGeometry.angledefMathlib.Geometry.Euclidean.Angle.Unoriented.Affine, function or constantWording
the undirected angle at x4 (from the docstring)
English
Let $x_{4}$, $x_{5}$ and $x_{6}$ be elements of $P$. Then the undirected angle at $x_{4}$ is a real number defined as the angle of the vector difference of $x_{4}$ and $x_{5}$ and the vector difference of $x_{6}$ and $x_{5}$.
InnerProductGeometry.angledefMathlib.Geometry.Euclidean.Angle.Unoriented.Basic, function or constantWording
the angle of x2 and y (from the name)
English
Let $x_{2}$ and $y$ be elements of $V$. Then the angle of $x_{2}$ and $y$ is a real number defined as $\operatorname{arccos}$ applied to the quotient of $\operatorname{inner}$ applied to $\Real$, $x_{2}$ and $y$ and the product of the norm of $x_{2}$ and the norm of $y$.
Affine.Simplex.PointsWithCircumcenterIndexinductiveMathlib.Geometry.Euclidean.Circumcenter, typeWording
point with circumcenter index of n (from the name)
English
Let $n$ be a natural number. Then the point with circumcenter indexes of $n$ are a basic type.
Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndexconstructorMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the circumcenter index (from the name)
English
The circumcenter index is a point with circumcenter index of $n$.
Affine.Simplex.PointsWithCircumcenterIndex.ctorElimTypedefMathlib.Geometry.Euclidean.Circumcenter, typeEnglish
Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $\mathrm{motive}$ applied to the point index of $x$ and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the circumcenter index.
Affine.Simplex.PointsWithCircumcenterIndex.pointIndexconstructorMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the point index of x (from the name)
English
Let $x$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the point index of $x$ is a point with circumcenter index of $n$.
Affine.Simplex.PointsWithCircumcenterIndex.proxyTypedefMathlib.Geometry.Euclidean.Circumcenter, typeEnglish
Let $n$ be a natural number. Then an element of $\operatorname{proxyType}$ applied to $n$ is an element of the function that maps $n$ to $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Unit}$.
Affine.Simplex.PointsWithCircumcenterIndex.proxyTypeEquivdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{proxyTypeEquiv}$ applied to $n$ is an equivalence from $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Unit}$ to the set of point with circumcenter indexes of $n$.
Affine.Simplex.centroidWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $\mathrm{fs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $x$ be a point with circumcenter index of $n$. Then $\operatorname{centroidWeightsWithCircumcenter}$ applied to $\mathrm{fs}$ and $x$ is a real number.
Affine.Simplex.circumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the circumcenter of s (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then the circumcenter of $s$ is an element of $P$ defined as the center of the circumsphere of $s$.
Affine.Simplex.circumcenterWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $n$ be a natural number. Let $x$ be a point with circumcenter index of $n$. Then $\operatorname{circumcenterWeightsWithCircumcenter}$ applied to $n$ and $x$ is a real number.
Affine.Simplex.circumradiusdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{circumradius}$ applied to $s$ is a real number defined as the radius of the circumsphere of $s$.
Affine.Simplex.circumspheredefMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the circumsphere of s (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then the circumsphere of $s$ is a sphere of $P$.
Affine.Simplex.pointIndexEmbeddingdefMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the point index embedding of n (from the name)
English
Let $n$ be a natural number. Then the point index embedding of $n$ is an embedding of $\mathrm{Fin}$ applied to $n + 1$ and the set of point with circumcenter indexes of $n$.
Affine.Simplex.pointWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $x$ be a point with circumcenter index of $n$. Then $\operatorname{pointWeightsWithCircumcenter}$ applied to $i$ and $x$ is a real number.
Affine.Simplex.pointsWithCircumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantWording
the point with circumcenter of s and x4 (from the name)
English
Let $s$ be a simplex of $P$ and $n$. Let $x_{4}$ be a point with circumcenter index of $n$. Then the point with circumcenter of $s$ and $x_{4}$ is an element of $P$.
Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.Circumcenter, function or constantEnglish
Let $x$ and $x_{1}$ be elements of $\mathrm{Fin}$ applied to $n + 1$. Let $x_{2}$ be a point with circumcenter index of $n$. Then $\operatorname{reflectionCircumcenterWeightsWithCircumcenter}$ applied to $x$, $x_{1}$ and $x_{2}$ is a real number.
Affine.Simplex.ExcenterExistsdefMathlib.Geometry.Euclidean.Incenter.Basic, predicateEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{ExcenterExists}$ holds for $s$ and $\mathrm{signs}$, if $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{excenterWeightsUnnorm} (s , \mathrm{signs} , i)}\neq 0$.
Affine.Simplex.excenterdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantWording
the excenter of s and signs (from the name)
English
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Then the excenter of $s$ and $\mathrm{signs}$ is an element of $P$ defined as the center of $\operatorname{exsphere}$ applied to $s$ and $\mathrm{signs}$.
Affine.Simplex.excenterWeightsdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{excenterWeights}$ applied to $s$, $\mathrm{signs}$ and $x_{4}$ is a real number defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{excenterWeightsUnnorm} (s , \mathrm{signs} , i)})}{\operatorname{excenterWeightsUnnorm} (s , \mathrm{signs})}$.
Affine.Simplex.excenterWeightsUnnormdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{excenterWeightsUnnorm}$ applied to $s$, $\mathrm{signs}$ and $i$ is a real number defined as the product of $\iteMACRoG {(\MembershipmemMACRoT {\mathrm{signs}}{i})}{\operatorname{neg} (1)}{1}$ and $\operatorname{inv}$ applied to the height of $s$ and $i$.
Affine.Simplex.exradiusdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{exradius}$ applied to $s$ and $\mathrm{signs}$ is a real number defined as the radius of $\operatorname{exsphere}$ applied to $s$ and $\mathrm{signs}$.
Affine.Simplex.exspheredefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{exsphere}$ applied to $s$ and $\mathrm{signs}$ is a sphere of $P$ defined as $\operatorname{mk}$ applied to $\operatorname{affineCombination}$ applied to $\Real$, the universal set, $\operatorname{points}$ applied to $s$ and $\operatorname{excenterWeights}$ applied to $s$ and $\mathrm{signs}$ and the absolute value of $\operatorname{inv}$ applied to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{excenterWeightsUnnorm} (s , \mathrm{signs} , i)}$.
Affine.Simplex.incenterdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantWording
the incenter of s (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then the incenter of $s$ is an element of $P$ defined as the center of $\operatorname{exsphere}$ applied to $s$ and $\operatorname{emptyCollection}$.
Affine.Simplex.inradiusdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{inradius}$ applied to $s$ is a real number defined as the radius of $\operatorname{exsphere}$ applied to $s$ and $\operatorname{emptyCollection}$.
Affine.Simplex.inspheredefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{insphere}$ applied to $s$ is a sphere of $P$ defined as $\operatorname{exsphere}$ applied to $s$ and $\operatorname{emptyCollection}$.
Affine.Simplex.touchpointdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{touchpoint}$ applied to $s$, $\mathrm{signs}$ and $i$ is an element of $P$ defined as $\operatorname{orthogonalProjectionSpan}$ applied to the face of $s$ and $i$ and the excenter of $s$ and $\mathrm{signs}$.
Affine.Simplex.touchpointWeightsdefMathlib.Geometry.Euclidean.Incenter.Basic, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $i$ and $x_{4}$ be elements of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{touchpointWeights}$ applied to $s$, $\mathrm{signs}$, $i$ and $x_{4}$ is a real number.
Affine.Simplex.nsPoledefMathlib.Geometry.Euclidean.Incenter.SouthPole, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $\mathrm{signs}$ be a finite set of $\mathrm{Fin}$ applied to $n + 1$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{nsPole}$ applied to $s$, $\mathrm{signs}$ and $i$ is an element of $P$ defined as the second intersection of the point of $s$ and $i$ and the vector difference of the excenter of $s$ and $\mathrm{signs}$ and the point of $s$ and $i$.
Affine.Simplex.southPoledefMathlib.Geometry.Euclidean.Incenter.SouthPole, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{southPole}$ applied to $s$ and $i$ is an element of $P$ defined as the second intersection of the point of $s$ and $i$ and the vector difference of the incenter of $s$ and the point of $s$ and $i$.
Affine.Triangle.northPoledefMathlib.Geometry.Euclidean.Incenter.SouthPole, function or constantEnglish
Let $t$ be a triangle of $\Real$ and $P$. Let $i$ be an element of $\mathrm{Fin}$ applied to $3$. Then $\operatorname{northPole}$ applied to $t$ and $i$ is an element of $P$ defined as $\operatorname{nsPole}$ applied to $t$, $\operatorname{singleton}$ applied to $i + 1$ and $i$.
EuclideanGeometry.inversiondefMathlib.Geometry.Euclidean.Inversion.Basic, function or constantWording
the inversion of R and x4 (from the name)
English
Let $c$ and $x_{4}$ be elements of $P$. Let $R$ be an element of $\Real$. Then the inversion of $R$ and $x_{4}$ is an element of $P$ defined as the sum of $\HSMulhSMulMACRoAL {((\frac{ R}{\operatorname{dist} (x_{4} , c)})^ {2})}{\operatorname{vsub} (x_{4} , c)}$ and $c$.
Affine.Simplex.mongePlanedefMathlib.Geometry.Euclidean.MongePoint, function or constantEnglish
Let $s$ be a simplex of $P$ and $n + 2$. Let $x_{4}$ and $x_{5}$ be elements of $\mathrm{Fin}$ applied to $n + 3$. Then $\operatorname{mongePlane}$ applied to $s$, $x_{4}$ and $x_{5}$ is an affine subspace of $\Real$ and $P$ defined as the minimum of $\operatorname{mk'}$ applied to the centroid of the complement of $\operatorname{insert}$ applied to $x_{4}$ and $\operatorname{singleton}$ applied to $x_{5}$ and $\operatorname{points}$ applied to $s$ and $\operatorname{orthogonal}$ applied to the span of $\Real$ and $\operatorname{singleton}$ applied to the vector difference of the point of $s$ and $x_{4}$ and the point of $s$ and $x_{5}$ and the affine span of $\Real$ and the range of $\operatorname{points}$ applied to $s$.
Affine.Simplex.mongePointdefMathlib.Geometry.Euclidean.MongePoint, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{mongePoint}$ applied to $s$ is an element of $P$ defined as the sum of $\HSMulhSMulMACRoAL {(\frac{ n + 1}{n - 1})}{\operatorname{vsub} (\operatorname{centroid} (\FinsetunivMACRoAC , \operatorname{points} (s)), \operatorname{circumcenter} (s))}$ and the circumcenter of $s$.
Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.MongePoint, function or constantEnglish
Let $x$ and $x_{1}$ be elements of $\mathrm{Fin}$ applied to $n + 3$. Let $x_{2}$ be a point with circumcenter index of $n + 2$. Then $\operatorname{mongePointVSubFaceCentroidWeightsWithCircumcenter}$ applied to $x$, $x_{1}$ and $x_{2}$ is a real number.
Affine.Simplex.mongePointWeightsWithCircumcenterdefMathlib.Geometry.Euclidean.MongePoint, function or constantEnglish
Let $n$ be a natural number. Let $x$ be a point with circumcenter index of $n + 2$. Then $\operatorname{mongePointWeightsWithCircumcenter}$ applied to $n$ and $x$ is a real number.
Affine.Triangle.orthocenterdefMathlib.Geometry.Euclidean.MongePoint, function or constantWording
the orthocenter of t (from the docstring)
English
Let $t$ be a triangle of $\Real$ and $P$. Then the orthocenter of $t$ is an element of $P$ defined as $\operatorname{mongePoint}$ applied to $t$.
EuclideanGeometry.OrthocentricSystemdefMathlib.Geometry.Euclidean.MongePoint, predicateWording
s is a orthocentric system (from the name)
English
Let $s$ be an element of $\wp P$. Then $s$ is an orthocentric system, if there exists a triangle $t$ of $\Real$ and $P$, such that the orthocenter of $t$ is not an element of the range of $\operatorname{points}$ applied to $t$ and $s$ is equal to $\operatorname{insert}$ applied to the orthocenter of $t$ and the range of $\operatorname{points}$ applied to $t$.
Affine.Simplex.eulerPointdefMathlib.Geometry.Euclidean.NinePointCircle, function or constantWording
the Euler point of s and i (from the name)
English
Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the Euler point of $s$ and $i$ is an element of $P$ defined as the sum of $\HSMulhSMulMACRoAL {\operatorname{inv} (n)}{\operatorname{vsub} (\operatorname{points} (s , i), \operatorname{mongePoint} (s))}$ and $\operatorname{mongePoint}$ applied to $s$.
Affine.Simplex.ninePointCircledefMathlib.Geometry.Euclidean.NinePointCircle, function or constantEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{ninePointCircle}$ applied to $s$ is a sphere of $P$ defined as $\operatorname{mk}$ applied to the sum of $\HSMulhSMulMACRoAL {(\frac{ n + 1}{n})}{\operatorname{vsub} (\operatorname{centroid} (s), \operatorname{circumcenter} (s))}$ and the circumcenter of $s$ and $\frac{ \operatorname{circumradius} (s)}{n}$.
AffineSubspace.perpBisectordefMathlib.Geometry.Euclidean.PerpBisector, function or constantEnglish
Let $x_{4}$ and $x_{5}$ be elements of $P$. Then $\operatorname{perpBisector}$ applied to $x_{4}$ and $x_{5}$ is an affine subspace of $\Real$ and $P$ defined as $\operatorname{mk'}$ applied to the midpoint of $x_{4}$ and $x_{5}$ and the kernel of $\mathrm{inner\_u209b\_\_u2097\_\_\_app}$ applied to $\Real$ and the vector difference of $x_{5}$ and $x_{4}$.
Affine.Simplex.orthogonalProjectionSpandefMathlib.Geometry.Euclidean.Projection, function or constantWording
the orthogonal projection of s (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then the orthogonal projection of $s$ is a continuous affine map of $P$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{affineSpan} (x , \operatorname{range} (\operatorname{points} (s)))}{x_{6}})}$ defined as the orthogonal projection of the affine span of $x$ and the range of $\operatorname{points}$ applied to $s$.
EuclideanGeometry.orthogonalProjectiondefMathlib.Geometry.Euclidean.Projection, function or constantWording
the orthogonal projection of s (from the docstring)
English
Let $s$ be an affine subspace of $x$ and $P$. Then the orthogonal projection of $s$ is a continuous affine map of $P$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ defined as the composition of the composition of the continuous affine map of the continuous affine equivalence of the vector sum constant of $x$ and $\operatorname{arbitrary}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and the continuous affine map of the orthogonal projection onto a subspace of the direction of $s$ and the continuous affine map of the continuous affine equivalence of the inverse of the vector sum constant of $x$ and $\operatorname{arbitrary}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {s}{x_{7}})}$.
EuclideanGeometry.reflectiondefMathlib.Geometry.Euclidean.Projection, function or constantWording
the reflection of s (from the name)
English
Let $s$ be an affine subspace of $x$ and $P$. Then the reflection of $s$ is an affine isometry equivalence of $P$ and $P$ defined as the composition of the composition of the inverse of the vector sum constant of $x$ and $\operatorname{arbitrary}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and the affine isometry equivalence of the reflection of the direction of $s$ and the vector sum constant of $x$ and $\operatorname{arbitrary}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {s}{x_{7}})}$.
Affine.Simplex.signedInfDistdefMathlib.Geometry.Euclidean.SignedDist, function or constantWording
the signed infimum distance of s and i (from the name)
English
Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the signed infimum distance of $s$ and $i$ is a continuous affine map of $P$ and $\Real$ defined as the signed infimum distance of the affine span of $\Real$ and the image of $\operatorname{points}$ applied to $s$ and the complement of $\operatorname{singleton}$ applied to $i$ and the point of $s$ and $i$.
AffineSubspace.signedInfDistdefMathlib.Geometry.Euclidean.SignedDist, function or constantWording
the signed infimum distance of s and p (from the name)
English
Let $s$ be an affine subspace of $\Real$ and $P$. Let $p$ be an element of $P$. Then the signed infimum distance of $s$ and $p$ is a continuous affine map of $P$ and $\Real$ defined as $\operatorname{signedDist}$ applied to the vector difference of $p$ and $\operatorname{orthogonalProjection}$ applied to $s$ and $p$ and $\operatorname{ofNonempty}$.
signedDistdefMathlib.Geometry.Euclidean.SignedDist, function or constantWording
the signed distance of v (from the name)
English
Let $v$ be an element of $V$. Then the signed distance of $v$ is a continuous affine map of $P$ and the set of continuous affine maps of $P$ and $\Real$.
Affine.Simplex.AcuteAngleddefMathlib.Geometry.Euclidean.Simplex, predicateEnglish
Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{AcuteAngled}$ holds for $s$, if for all elements $x_{4}$, $x_{5}$ and $x_{6}$ of $\mathrm{Fin}$ applied to $n + 1$, if $x_{4} \neq x_{5}$, then if $x_{4} \neq x_{6}$, then if $x_{5} \neq x_{6}$, then the undirected angle at the point of $s$ and $x_{4}$ is less than the quotient of the product and $2$.
EuclideanGeometry.ConcyclicstructureMathlib.Geometry.Euclidean.Sphere.Basic, predicateEnglish
Let $\mathrm{ps}$ be an element of $\wp P$. Then we can say that $\operatorname{Concyclic}$ holds for $\mathrm{ps}$.
EuclideanGeometry.CosphericaldefMathlib.Geometry.Euclidean.Sphere.Basic, predicateEnglish
Let $\mathrm{ps}$ be an element of $\wp P$. Then $\operatorname{Cospherical}$ holds for $\mathrm{ps}$, if there exists an element $\mathrm{center}$ of $P$, such that there exists a real number $\mathrm{radius}$, such that for all elements $p$ of $P$, if $p$ is an element of $\mathrm{ps}$, then the distance of $p$ and $\mathrm{center}$ is equal to $\mathrm{radius}$.
EuclideanGeometry.SpherestructureMathlib.Geometry.Euclidean.Sphere.Basic, typeWording
sphere of P (from the name)
English
Let $P$ be a set. Then the spheres of $P$ are a basic type.
EuclideanGeometry.Sphere.IsDiameterstructureMathlib.Geometry.Euclidean.Sphere.Basic, predicateEnglish
Let $s$ be a sphere of $P$. Let $x_{4}$ and $x_{5}$ be elements of $P$. Then we can say that $\operatorname{IsDiameter}$ holds for $s$, $x_{4}$ and $x_{5}$.
EuclideanGeometry.Sphere.centerdefMathlib.Geometry.Euclidean.Sphere.Basic, function or constantWording
the center of self (from the name)
English
Let $\mathrm{self}$ be a sphere of $P$. Then the center of $\mathrm{self}$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
EuclideanGeometry.Sphere.ofDiameterdefMathlib.Geometry.Euclidean.Sphere.Basic, function or constantWording
the sphere of x4 and x5 (from the name)
English
Let $x_{4}$ and $x_{5}$ be elements of $P$. Then the sphere of $x_{4}$ and $x_{5}$ is a sphere of $P$ defined as $\operatorname{mk}$ applied to the midpoint of $x_{4}$ and $x_{5}$ and the quotient of the distance of $x_{4}$ and $x_{5}$ and $2$.
EuclideanGeometry.Sphere.radiusdefMathlib.Geometry.Euclidean.Sphere.Basic, function or constantWording
the radius of self (from the name)
English
Let $\mathrm{self}$ be a sphere of $P$. Then the radius of $\mathrm{self}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
EuclideanGeometry.Sphere.orthRadiusdefMathlib.Geometry.Euclidean.Sphere.OrthRadius, function or constantEnglish
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Then $\operatorname{orthRadius}$ applied to $s$ and $p$ is an affine subspace of $\Real$ and $P$ defined as $\operatorname{mk'}$ applied to $p$ and $\operatorname{orthogonal}$ applied to the span of $\Real$ and $\operatorname{singleton}$ applied to the vector difference of $p$ and the center of $s$.
EuclideanGeometry.Sphere.polardefMathlib.Geometry.Euclidean.Sphere.PolePolar, function or constantEnglish
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Then $\operatorname{polar}$ applied to $s$ and $p$ is an affine subspace of $\Real$ and $P$ defined as $\operatorname{orthRadius}$ applied to $s$ and the inversion of the radius of $s$ and $p$.
EuclideanGeometry.Sphere.poledefMathlib.Geometry.Euclidean.Sphere.PolePolar, function or constantWording
the pole of s and as (from the docstring)
English
Let $s$ be a sphere of $P$. Let $\mathrm{as}$ be an affine subspace of $\Real$ and $P$. Then the pole of $s$ and $\mathrm{as}$ is an element of $P$ defined as the inversion of the radius of $s$ and $\operatorname{orthogonalProjection}$ applied to $\mathrm{as}$ and the center of $s$.
EuclideanGeometry.Sphere.powerdefMathlib.Geometry.Euclidean.Sphere.Power, function or constantWording
the power of s and p (from the docstring)
English
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Then the power of $s$ and $p$ is a real number defined as the difference between the exponentiation of the distance of $p$ and the center of $s$ to $2$ and the exponentiation of the radius of $s$ to $2$.
EuclideanGeometry.Sphere.secondInterdefMathlib.Geometry.Euclidean.Sphere.SecondInter, function or constantWording
the second intersection of p and v (from the name)
English
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Let $v$ be an element of $V$. Then the second intersection of $p$ and $v$ is an element of $P$ defined as the sum of $\HSMulhSMulMACRoAL {(\frac{ \operatorname{neg} (2)\times \operatorname{inner} (\Real , v , \operatorname{vsub} (p , \operatorname{center} (s)))}{\operatorname{inner} (\Real , v , v)})}{v}$ and $p$.
EuclideanGeometry.Sphere.IsExtTangentdefMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Then $\operatorname{IsExtTangent}$ holds for $x_{4}$ and $x_{5}$, if there exists an element $p$ of $P$, such that $\operatorname{IsExtTangentAt}$ holds for $x_{4}$, $x_{5}$ and $p$.
EuclideanGeometry.Sphere.IsExtTangentAtstructureMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Let $p$ be an element of $P$. Then we can say that $\operatorname{IsExtTangentAt}$ holds for $x_{4}$, $x_{5}$ and $p$.
EuclideanGeometry.Sphere.IsIntTangentdefMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Then $\operatorname{IsIntTangent}$ holds for $x_{4}$ and $x_{5}$, if there exists an element $p$ of $P$, such that $\operatorname{IsIntTangentAt}$ holds for $x_{4}$, $x_{5}$ and $p$.
EuclideanGeometry.Sphere.IsIntTangentAtstructureMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Let $p$ be an element of $P$. Then we can say that $\operatorname{IsIntTangentAt}$ holds for $x_{4}$, $x_{5}$ and $p$.
EuclideanGeometry.Sphere.IsTangentdefMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $s$ be a sphere of $P$. Let $\mathrm{as}$ be an affine subspace of $\Real$ and $P$. Then $\operatorname{IsTangent}$ holds for $s$ and $\mathrm{as}$, if there exists an element $p$ of $P$, such that $\operatorname{IsTangentAt}$ holds for $s$, $p$ and $\mathrm{as}$.
EuclideanGeometry.Sphere.IsTangentAtstructureMathlib.Geometry.Euclidean.Sphere.Tangent, predicateEnglish
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Let $\mathrm{as}$ be an affine subspace of $\Real$ and $P$. Then we can say that $\operatorname{IsTangentAt}$ holds for $s$, $p$ and $\mathrm{as}$.
EuclideanGeometry.Sphere.commonExtTangentsdefMathlib.Geometry.Euclidean.Sphere.Tangent, function or constantEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Then $\operatorname{commonExtTangents}$ applied to $x_{4}$ and $x_{5}$ is an element of the power set of the set of affine subspaces of $\Real$ and $P$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{as}$ to the proposition that $\mathrm{as}$ is an element of the set of all maximal common tangent spaces to the spheres of $x_{4}$ and $x_{5}$ and for all elements $p$ of $P$, if $p$ is an element of $\mathrm{as}$, then it is not the case that $\mathrm{Sbtw}$ holds for $\Real$, the center of $x_{4}$, $p$ and the center of $x_{5}$.
EuclideanGeometry.Sphere.commonIntTangentsdefMathlib.Geometry.Euclidean.Sphere.Tangent, function or constantEnglish
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Then $\operatorname{commonIntTangents}$ applied to $x_{4}$ and $x_{5}$ is an element of the power set of the set of affine subspaces of $\Real$ and $P$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{as}$ to the proposition that $\mathrm{as}$ is an element of the set of all maximal common tangent spaces to the spheres of $x_{4}$ and $x_{5}$ and there exists an element $p$ of $P$ such that $p$ is an element of $\mathrm{as}$ and $\mathrm{Wbtw}$ holds for $\Real$, the center of $x_{4}$, $p$ and the center of $x_{5}$.
EuclideanGeometry.Sphere.commonTangentsdefMathlib.Geometry.Euclidean.Sphere.Tangent, function or constantWording
the set of all maximal common tangent spaces to the spheres of x4 and x5 (from the docstring)
English
Let $x_{4}$ and $x_{5}$ be spheres of $P$. Then the set of all maximal common tangent spaces to the spheres of $x_{4}$ and $x_{5}$ is an element of the power set of the set of affine subspaces of $\Real$ and $P$ defined as $\operatorname{inter}$ applied to the tangent set of $x_{4}$ and the tangent set of $x_{5}$.
EuclideanGeometry.Sphere.tangentSetdefMathlib.Geometry.Euclidean.Sphere.Tangent, function or constantWording
the tangent set of s (from the name)
English
Let $s$ be a sphere of $P$. Then the tangent set of $s$ is an element of the power set of the set of affine subspaces of $\Real$ and $P$ defined as the image of $\operatorname{orthRadius}$ applied to $s$ and the sphere of the center of $s$ and the radius of $s$.
EuclideanGeometry.Sphere.tangentsFromdefMathlib.Geometry.Euclidean.Sphere.Tangent, function or constantEnglish
Let $s$ be a sphere of $P$. Let $p$ be an element of $P$. Then $\operatorname{tangentsFrom}$ applied to $s$ and $p$ is an element of the power set of the set of affine subspaces of $\Real$ and $P$ defined as $\operatorname{ofPred}$ applied to the function that maps $\mathrm{as}$ to the proposition that $\mathrm{as}$ is an element of the tangent set of $s$ and $p$ is an element of $\mathrm{as}$.
Affine.Simplex.evalVolumedefMathlib.Geometry.Euclidean.Volume.Basic, function or constantWording
the evaluation volume (from the name)
English
The evaluation volume is an element of $\operatorname{PositivityExt}$.
Affine.Simplex.volumedefMathlib.Geometry.Euclidean.Volume.Def, function or constantWording
the volume of s (from the docstring)
English
Let $s$ be a simplex of $P$ and $n$. Then the volume of $s$ is a real number defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{Affine\_\_Simplex\_\_volume\_\_\_f}$ and $s$.
MeasureTheory.Measure.euclideanHausdorffMeasuredefMathlib.Geometry.Euclidean.Volume.Measure, function or constantWording
the Euclidean Hausdorff measure of d (from the name)
English
Let $d$ be an element of $\Natural$. Then the Euclidean Hausdorff measure of $d$ is a measure of $X$ defined as $\HSMulhSMulMACRoAL {\operatorname{addHaarScalarFactor} (\operatorname{volume} , \operatorname{hausdorffMeasure} (d))}{\operatorname{hausdorffMeasure} (d)}$.
Submodule.measurableEquivProddefMathlib.Geometry.Euclidean.Volume.Measure, function or constantWording
the measurable equivalence product of s and p (from the name)
English
Let $s$ be a submodule of $\Real$ and $V$. Let $p$ be an element of $P$. Then the measurable equivalence product of $s$ and $p$ is a measurable equivalence of $P$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (s)}{x_{7}})}$ defined as the composition of the inverse of the measurable equivalence of the homeomorphism of the vector sum constant of $p$ and the composition of the measurable equivalence of the homeomorphism of the orthogonal decomposition of $s$ and the inverse of $\operatorname{toLp}$ applied to $2$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (s)}{x_{7}})}$.
Group.Generators.IsGeodesicdefMathlib.Geometry.Group.WordMetric, predicateEnglish
Let $P$ be a generator of $G$ and $x$. Let $l$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then $\operatorname{IsGeodesic}$ holds for $P$ and $l$, if the word length of $P$ and the canonical map of $P$ and $l$ is equal to $\operatorname{length}$ applied to $l$.
Group.Generators.groupNormdefMathlib.Geometry.Group.WordMetric, function or constantWording
the group norm of P (from the name)
English
Let $P$ be a generator of $G$ and $x$. Then the group norm of $P$ is a group norm of $G$.
Group.Generators.wordLengthdefMathlib.Geometry.Group.WordMetric, function or constantWording
the word length of P and g (from the name)
English
Let $P$ be a generator of $G$ and $x$. Let $g$ be an element of $G$. Then the word length of $P$ and $g$ is a natural number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that there exists a list $l$ of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$, such that the canonical map of $P$ and $l$ is equal to $g$ and $\operatorname{length} (l)= n$.
Group.Generators.wordProddefMathlib.Geometry.Group.WordProd, function or constantWording
the canonical map of P and l (from the docstring)
English
Let $P$ be a generator of $G$ and $x$. Let $l$ be a list of elements of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Bool}$. Then the canonical map of $P$ and $l$ is an element of $G$ defined as $\operatorname{lift}$ applied to $P$ and $\operatorname{mk}$ applied to $l$.
LeftInvariantDerivationstructureMathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation, typeWording
left invariant derivation of I and G (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $G$ be a set. Then the left invariant derivations of $I$ and $G$ are a basic type.
LeftInvariantDerivation.coeFnAddMonoidHomdefMathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation, function or constantWording
the coercion to function of I and G (from the docstring)
English
Let $I$ be a model with corner of $E$ and $H$. Let $G$ be a set. Then the coercion to function of $I$ and $G$ is an additive monoid homomorphism of the set of left invariant derivations of $I$ and $G$ and the set of functions from continuous difference maps of $x$ and $\operatorname{some}$ applied to the top to continuous difference maps of $x$ and $\operatorname{some}$ applied to the top defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{LeftInvariantDerivation\_\_coe\_zero}$ and $\mathrm{LeftInvariantDerivation\_\_coe\_add}$.
LeftInvariantDerivation.evalAtdefMathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation, function or constantEnglish
Let $g$ be an element of $G$. Then $\operatorname{evalAt}$ applied to $g$ is a linear map of the set of left invariant derivations of $I$ and $G$ and the set of point derivations of $I$ and $g$.
ContMDiffInvâ‚€classMathlib.Geometry.Manifold.Algebra.LieGroup, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ be a set. Then we can say that $\mathrm{ContMDiffInv\_u2080\_}$ holds for $I$, $n$ and $G$.
LieAddGroupclassMathlib.Geometry.Manifold.Algebra.LieGroup, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ be a set. Then we can say that $\mathrm{LieAddGroup}$ holds for $I$, $n$ and $G$.
LieGroupclassMathlib.Geometry.Manifold.Algebra.LieGroup, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ be a set. Then we can say that $\mathrm{LieGroup}$ holds for $I$, $n$ and $G$.
ContMDiffAddclassMathlib.Geometry.Manifold.Algebra.Monoid, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ be a set. Then we can say that $\mathrm{ContMDiffAdd}$ holds for $I$, $n$ and $G$.
ContMDiffAddMonoidMorphismstructureMathlib.Geometry.Manifold.Algebra.Monoid, typeWording
continuous difference additive monoid morphism of #4 and #5 (from the name)
English
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ and $\mathrm{G'}$ be sets. Then the continuous difference additive monoid morphisms of $G$ and $\mathrm{G'}$ are a basic type.
ContMDiffMonoidMorphismstructureMathlib.Geometry.Manifold.Algebra.Monoid, typeWording
continuous difference monoid morphism of #4 and #5 (from the name)
English
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ and $\mathrm{G'}$ be sets. Then the continuous difference monoid morphisms of $G$ and $\mathrm{G'}$ are a basic type.
ContMDiffMulclassMathlib.Geometry.Manifold.Algebra.Monoid, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ be a set. Then we can say that $\mathrm{ContMDiffMul}$ holds for $I$, $n$ and $G$.
LibraryNote.Design_choices_about_smooth_algebraic_structuresdefMathlib.Geometry.Manifold.Algebra.Monoid, function or constantEnglish
$\mathrm{LibraryNote\_\_Design\_choices\_about\_smooth\_algebraic\_structures}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.
smoothLeftMuldefMathlib.Geometry.Manifold.Algebra.Monoid, function or constantWording
the smooth left product of I and g (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $g$ be an element of $G$. Then the smooth left product of $I$ and $g$ is a continuous difference map of $G$ and $\operatorname{some}$ applied to the top defined as the function that maps $x_{8}$ to $g \times x_{8}$.
smoothRightMuldefMathlib.Geometry.Manifold.Algebra.Monoid, function or constantWording
the smooth right product of I and g (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $g$ be an element of $G$. Then the smooth right product of $I$ and $g$ is a continuous difference map of $G$ and $\operatorname{some}$ applied to the top defined as the function that maps $x_{8}$ to $x_{8} \times g$.
ContMDiffConstSMulclassMathlib.Geometry.Manifold.Algebra.SMul, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $x_{5}$ and $M$ be sets. Then we can say that $\mathrm{ContMDiffConstSMul}$ holds for $I$, $n$, $x_{5}$ and $M$.
ContMDiffConstVAddclassMathlib.Geometry.Manifold.Algebra.SMul, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $x_{5}$ and $M$ be sets. Then we can say that $\mathrm{ContMDiffConstVAdd}$ holds for $I$, $n$, $x_{5}$ and $M$.
ContMDiffSMulclassMathlib.Geometry.Manifold.Algebra.SMul, predicateEnglish
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ and $M$ be sets. Then we can say that $\mathrm{ContMDiffSMul}$ holds for $I$, $\mathrm{I'}$, $n$, $G$ and $M$.
ContMDiffVAddclassMathlib.Geometry.Manifold.Algebra.SMul, predicateEnglish
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $G$ and $M$ be sets. Then we can say that $\mathrm{ContMDiffVAdd}$ holds for $I$, $\mathrm{I'}$, $n$, $G$ and $M$.
Diffeomorph.smuldefMathlib.Geometry.Manifold.Algebra.SMul, function or constantWording
the scalar multiple of g and #4 (from the name)
English
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $g$ be an element of $G$. Then the scalar multiple of $n$ and $g$ is a diffeomorphism of $M$ and $n$.
Diffeomorph.vadddefMathlib.Geometry.Manifold.Algebra.SMul, function or constantWording
the vector sum of g and #4 (from the name)
English
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $g$ be an element of $G$. Then the vector sum of $n$ and $g$ is a diffeomorphism of $M$ and $n$.
ContMDiffMap.CdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantEnglish
$\operatorname{C}$ is a ring homomorphism of $x$ and the set of continuous difference maps of $A$ and $n$.
ContMDiffMap.coeFnAddMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the coercion function additive monoid homomorphism (from the name)
English
The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of continuous difference maps of $G$ and $n$ and the set of functions from elements of $N$ to elements of $G$.
ContMDiffMap.coeFnAlgHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the coercion function algebra homomorphism (from the name)
English
The coercion function algebra homomorphism is an algebra homomorphism of the set of continuous difference maps of $A$ and $n$ and the set of functions from elements of $N$ to elements of $A$.
ContMDiffMap.coeFnLinearMapdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the coercion function linear map (from the name)
English
The coercion function linear map is a linear map of the set of continuous difference maps of $V$ and $n$ and the set of functions from elements of $N$ to elements of $V$.
ContMDiffMap.coeFnMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the coercion function monoid homomorphism (from the name)
English
The coercion function monoid homomorphism is a monoid homomorphism of the set of continuous difference maps of $G$ and $n$ and the set of functions from elements of $N$ to elements of $G$.
ContMDiffMap.coeFnRingHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the coercion function ring homomorphism (from the name)
English
The coercion function ring homomorphism is a ring homomorphism of the set of continuous difference maps of $R$ and $n$ and the set of functions from elements of $N$ to elements of $R$.
ContMDiffMap.compLeftAddMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the composition left additive monoid homomorphism of I and x19 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{19}$ be an additive monoid homomorphism of $\mathrm{G'}$ and $\mathrm{G''}$ such that $\mathrm{ContMDiff}$ holds for $\mathrm{I'}$, $\mathrm{I''}$, $n$ and $\operatorname{coe}$ applied to $x_{19}$. Then the composition left additive monoid homomorphism of $I$ and $x_{19}$ is an additive monoid homomorphism of the set of continuous difference maps of $\mathrm{G'}$ and $n$ and the set of continuous difference maps of $\mathrm{G''}$ and $n$.
ContMDiffMap.compLeftMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the composition left monoid homomorphism of I and x19 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{19}$ be a monoid homomorphism of $\mathrm{G'}$ and $\mathrm{G''}$ such that $\mathrm{ContMDiff}$ holds for $\mathrm{I'}$, $\mathrm{I''}$, $n$ and $\operatorname{coe}$ applied to $x_{19}$. Then the composition left monoid homomorphism of $I$ and $x_{19}$ is a monoid homomorphism of the set of continuous difference maps of $\mathrm{G'}$ and $n$ and the set of continuous difference maps of $\mathrm{G''}$ and $n$.
ContMDiffMap.compLeftRingHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the composition left ring homomorphism of I and x19 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $N$ be a set. Let $x_{19}$ be a ring homomorphism of $\mathrm{R'}$ and $\mathrm{R''}$ such that $\mathrm{ContMDiff}$ holds for $\mathrm{I'}$, $\mathrm{I''}$, $n$ and $\operatorname{coe}$ applied to $x_{19}$. Then the composition left ring homomorphism of $I$ and $x_{19}$ is a ring homomorphism of the set of continuous difference maps of $\mathrm{R'}$ and $n$ and the set of continuous difference maps of $\mathrm{R''}$ and $n$.
ContMDiffMap.evalRingHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantWording
the evaluation ring homomorphism of m (from the name)
English
Let $m$ be an element of $N$. Then the evaluation ring homomorphism of $m$ is a ring homomorphism of the set of continuous difference maps of $R$ and $n$ and $R$ defined as the composition of the evaluation ring homomorphism of the function that maps $x_{13}$ to $R$ and $m$ and the coercion function ring homomorphism.
ContMDiffMap.restrictAddMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantEnglish
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 $G$ be a set. Assume that $U \leq V$. Then $\operatorname{restrictAddMonoidHom}$ applied to $I$, $\mathrm{I'}$, $G$ and $h_{1}$ is an additive monoid homomorphism of the set of continuous difference maps of $G$ and $n$ and the set of continuous difference maps of $G$ and $n$.
ContMDiffMap.restrictMonoidHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantEnglish
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 $G$ be a set. Assume that $U \leq V$. Then $\operatorname{restrictMonoidHom}$ applied to $I$, $\mathrm{I'}$, $G$ and $h_{1}$ is a monoid homomorphism of the set of continuous difference maps of $G$ and $n$ and the set of continuous difference maps of $G$ and $n$.
ContMDiffMap.restrictRingHomdefMathlib.Geometry.Manifold.Algebra.SmoothFunctions, function or constantEnglish
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 $R$ be a set. Assume that $U \leq V$. Then $\operatorname{restrictRingHom}$ applied to $I$, $\mathrm{I'}$, $R$ and $h_{1}$ is a ring homomorphism of the set of continuous difference maps of $R$ and $n$ and the set of continuous difference maps of $R$ and $n$.
ContMDiffRingclassMathlib.Geometry.Manifold.Algebra.Structures, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $R$ be a set. Then we can say that $\mathrm{ContMDiffRing}$ holds for $I$, $n$ and $R$.
SingularManifoldstructureMathlib.Geometry.Manifold.Bordism, typeWording
singular manifold of k and I (from the name)
English
Let $X$ be a set. Let $k$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $I$ be a model with corner of $E$ and $H$. Then the singular manifolds of $k$ and $I$ are a basic type.
SingularManifold.MdefMathlib.Geometry.Manifold.Bordism, typeEnglish
Let $\mathrm{self}$ be a singular manifold of $k$ and $I$. Then an element of $\operatorname{M}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
SingularManifold.comapdefMathlib.Geometry.Manifold.Bordism, function or constantWording
the preimage of s and h4 (from the name)
English
Let $s$ be a singular manifold of $k$ and $I$. Assume that $x_{6}$ is continuous. Then the preimage of $s$ and $h_{4}$ is a singular manifold of $k$ and $I$.
SingularManifold.emptydefMathlib.Geometry.Manifold.Bordism, function or constantEnglish
Let $X$ and $M$ be sets. Let $I$ be a model with corner of $E$ and $H$. Then $\operatorname{empty}$ applied to $X$, $M$ and $I$ is a singular manifold of $k$ and $I$.
SingularManifold.fdefMathlib.Geometry.Manifold.Bordism, function or constantEnglish
Let $\mathrm{self}$ be a singular manifold of $k$ and $I$. Let $x_{4}$ be an element of $\operatorname{M}$ applied to $\mathrm{self}$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $X$ defined as $\operatorname{proj6}$ applied to $\mathrm{self}$ and $x_{4}$.
SingularManifold.mapdefMathlib.Geometry.Manifold.Bordism, function or constantWording
the map of s and h1 (from the name)
English
Let $s$ be a singular manifold of $k$ and $I$. Assume that $x_{5}$ is continuous. Then the map of $s$ and $h_{1}$ is a singular manifold of $k$ and $I$.
SingularManifold.proddefMathlib.Geometry.Manifold.Bordism, function or constantWording
the product of s and t (from the docstring)
English
Let $s$ be a singular manifold of $k$ and $I$. Let $t$ be a singular manifold of $k$ and $\mathrm{I'}$. Then the product of $s$ and $t$ is a singular manifold of $k$ and the product of $I$ and $\mathrm{I'}$.
SingularManifold.refldefMathlib.Geometry.Manifold.Bordism, function or constantWording
the identity of M and I (from the name)
English
Let $M$ be a set. Let $I$ be a model with corner of $E$ and $H$. Then the identity of $M$ and $I$ is a singular manifold of $k$ and $I$ defined as $\operatorname{mk}$ applied to $M$, $\mathrm{id}$ and $\mathrm{continuous\_id}$.
SingularManifold.sumdefMathlib.Geometry.Manifold.Bordism, function or constantWording
the sum of s and t (from the name)
English
Let $s$ and $t$ be singular manifolds of $k$ and $I$. Then the sum of $s$ and $t$ is a singular manifold of $k$ and $I$.
SingularManifold.toPUnitdefMathlib.Geometry.Manifold.Bordism, function or constantWording
the unit of M and I (from the name)
English
Let $M$ be a set. Let $I$ be a model with corner of $E$ and $H$. Then the unit of $M$ and $I$ is a singular manifold of $k$ and $I$ defined as $\operatorname{mk}$ applied to $M$, the function that maps $x_{5}$ to $\operatorname{unit}$ and $\mathrm{continuous\_const}$.
SmoothBumpFunctionstructureMathlib.Geometry.Manifold.BumpFunction, typeWording
smooth bump function of I and c (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $c$ be an element of $M$. Then the smooth bump functions of $I$ and $c$ are a basic type.
SmoothBumpFunction.toFundefMathlib.Geometry.Manifold.BumpFunction, function or constantWording
the smooth bump function of f and x5 (from the name)
English
Let $f$ be a smooth bump function of $I$ and $c$. Let $x_{5}$ be an element of $M$. Then the smooth bump function of $f$ and $x_{5}$ is a real number defined as the indicator of $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toContDiffBump}$ applied to $f$ and $\operatorname{toFun}$ applied to $\mathrm{extChartAt}$ applied to $I$ and $c$ and $x_{5}$.
SmoothBumpFunction.updateRIndefMathlib.Geometry.Manifold.BumpFunction, function or constantEnglish
Let $f$ be a smooth bump function of $I$ and $c$. Let $r$ be a real number such that $r$ is an element of the open interval of $0$ and $\operatorname{rOut}$ applied to $\operatorname{toContDiffBump}$ applied to $f$. Then $\operatorname{updateRIn}$ applied to $f$, $r$ and $\mathrm{hr}$ is a smooth bump function of $I$ and $c$.
ModelWithCorners.MfldCatstructureMathlib.Geometry.Manifold.Category.MfldCat.OfModel, typeEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the elements of $\operatorname{MfldCat}$ applied to $I$ and $n$ are a basic type.
ModelWithCorners.MfldCat.HomstructureMathlib.Geometry.Manifold.Category.MfldCat.OfModel, typeWording
homomorphism of M and N (from the name)
English
Let $M$ and $N$ be elements of $\operatorname{MfldCat}$ applied to $I$ and $n$. Then the homomorphisms of $M$ and $N$ are a basic type.
ModelWithCorners.MfldCat.Hom.homdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $M$ and $N$. Then the homomorphism of $f$ is a continuous difference map of the set of carriers of $N$ and $n$ defined as the homomorphism of $f$.
ModelWithCorners.MfldCat.Hom.hom'defMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $M$ and $N$. Then the homomorphism of $\mathrm{self}$ is a continuous difference map of the set of carriers of $N$ and $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ModelWithCorners.MfldCat.carrierdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{MfldCat}$ applied to $I$ and $n$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
ModelWithCorners.MfldCat.diffeomorphOfIsodefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantWording
the diffeomorphism of i (from the name)
English
Let $i$ be an isomorphism of $M$ and $N$. Then the diffeomorphism of $i$ is a diffeomorphism of the set of carriers of $N$ and $n$.
ModelWithCorners.MfldCat.isoEquivDiffeomorphdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantWording
the isomorphism equivalence diffeomorphism (from the name)
English
The isomorphism equivalence diffeomorphism is an equivalence from the set of isomorphisms of $M$ and $N$ to the set of diffeomorphisms of the set of carriers of $N$ and $n$.
ModelWithCorners.MfldCat.isoOfDiffeomorphdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantWording
the isomorphism of e (from the name)
English
Let $e$ be a diffeomorphism of the set of carriers of $N$ and $n$. Then the isomorphism of $e$ is an isomorphism of $M$ and $N$.
ModelWithCorners.MfldCat.ofdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\operatorname{MfldCat}$ applied to $I$ and $n$ defined as $\mathrm{ModelWithCorners\_\_MfldCat\_\_\_mkInternal}$ applied to $X$.
ModelWithCorners.MfldCat.ofHomdefMathlib.Geometry.Manifold.Category.MfldCat.OfModel, function or constantEnglish
Let $f$ be a continuous difference map of $Y$ and $n$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
ChartedSpaceclassMathlib.Geometry.Manifold.ChartedSpace, predicateEnglish
Let $H$ and $M$ be sets. Then we can say that $\mathrm{ChartedSpace}$ holds for $H$ and $M$.
ChartedSpace.atlasdefMathlib.Geometry.Manifold.ChartedSpace, function or constantWording
the atlas (from the name)
English
The atlas is an element of the power set of the set of open partial homeomorphisms of $M$ and $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ChartedSpace.chartAtdefMathlib.Geometry.Manifold.ChartedSpace, function or constantEnglish
Let $x_{2}$ be an element of $M$. Then $\operatorname{chartAt}$ applied to $x_{2}$ is an open partial homeomorphism of $M$ and $H$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
ChartedSpaceCorestructureMathlib.Geometry.Manifold.ChartedSpace, typeWording
charted space of H and M (from the name)
English
Let $H$ and $M$ be sets. Then the charted spaces of $H$ and $M$ are a basic type.
ChartedSpaceCore.atlasdefMathlib.Geometry.Manifold.ChartedSpace, function or constantWording
the atlas of self (from the name)
English
Let $\mathrm{self}$ be a charted space of $H$ and $M$. Then the atlas of $\mathrm{self}$ is an element of the power set of the set of partial equivalences of $M$ and $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
ChartedSpaceCore.chartAtdefMathlib.Geometry.Manifold.ChartedSpace, function or constantEnglish
Let $\mathrm{self}$ be a charted space of $H$ and $M$. Let $x_{1}$ be an element of $M$. Then $\operatorname{chartAt}$ applied to $\mathrm{self}$ and $x_{1}$ is a partial equivalence of $M$ and $H$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.
ChartedSpaceCore.openPartialHomeomorphdefMathlib.Geometry.Manifold.ChartedSpace, function or constantWording
the open partial homeomorphism of c and e (from the name)
English
Let $c$ be a charted space of $H$ and $M$. Let $e$ be a partial equivalence of $M$ and $H$ such that $e$ is an element of the atlas of $c$. Then the open partial homeomorphism of $c$ and $e$ is an open partial homeomorphism of $M$ and $H$.
ModelPidefMathlib.Geometry.Manifold.ChartedSpace, typeWording
model product of H (from the name)
English
Let $H$ be a function from elements of $x$ to sets. Then a model product of $H$ is an element of the function that maps $H$ to the set of functions from elements $i$ of $x$ to elements of $H$ applied to $i$.
ModelProddefMathlib.Geometry.Manifold.ChartedSpace, typeWording
model product of H and #2 (from the name)
English
Let $H$ and $\mathrm{H'}$ be sets. Then a model product of $H$ and $\mathrm{H'}$ is an element of the function that maps $H$ and $\mathrm{H'}$ to $\mathrm{Prod}$ applied to $H$ and $\mathrm{H'}$.
achartdefMathlib.Geometry.Manifold.ChartedSpace, function or constantEnglish
Let $H$ be a set. Let $x_{3}$ be an element of $M$. Then $\mathrm{achart}$ applied to $H$ and $x_{3}$ is an element of the atlas of $H$ and $M$ defined as $\mathrm{chartAt}$ applied to $H$ and $x_{3}$.
atlasdefMathlib.Geometry.Manifold.ChartedSpace, function or constantWording
the atlas of H and M (from the name)
English
Let $H$ and $M$ be sets. Then the atlas of $H$ and $M$ is an element of the power set of the set of open partial homeomorphisms of $M$ and $H$ defined as the atlas.
chartAtdefMathlib.Geometry.Manifold.ChartedSpace, function or constantEnglish
Let $H$ be a set. Let $x_{3}$ be an element of $M$. Then $\mathrm{chartAt}$ applied to $H$ and $x_{3}$ is an open partial homeomorphism of $M$ and $H$ defined as $\operatorname{chartAt}$ applied to $x_{3}$.
ContDiffWithinAtPropdefMathlib.Geometry.Manifold.ContMDiff.Defs, predicateEnglish
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 $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $f$ be a function from elements of $H$ to elements of $\mathrm{H'}$. Let $s$ be an element of $\wp H$. Let $x_{8}$ be an element of $H$. Then $\mathrm{ContDiffWithinAtProp}$ holds for $I$, $\mathrm{I'}$, $n$, $f$, $s$ and $x_{8}$, if $\mathrm{ContDiffWithinAt}$ holds for $x$, $n$, $\operatorname{comp}$ applied to $\operatorname{toFun'}$ applied to $\mathrm{I'}$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{toFun}$ applied to the inverse of $I$, $\operatorname{inter}$ applied to the preimage of $\operatorname{toFun}$ applied to the inverse of $I$ and $s$ and the range of $\operatorname{toFun'}$ applied to $I$ and the function of $I$ and $x_{8}$.
ContMDiffdefMathlib.Geometry.Manifold.ContMDiff.Defs, predicateEnglish
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 $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 $\mathrm{M'}$. Then $\mathrm{ContMDiff}$ holds for $I$, $\mathrm{I'}$, $n$ and $f$, if for all elements $x_{12}$ of $M$, $\mathrm{ContMDiffAt}$ holds for $I$, $\mathrm{I'}$, $n$, $f$ and $x_{12}$.
ContMDiffAtdefMathlib.Geometry.Manifold.ContMDiff.Defs, predicateEnglish
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 $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 $\mathrm{M'}$. Let $x_{12}$ be an element of $M$. Then $\mathrm{ContMDiffAt}$ holds for $I$, $\mathrm{I'}$, $n$, $f$ and $x_{12}$, if $\mathrm{ContMDiffWithinAt}$ holds for $I$, $\mathrm{I'}$, $n$, $f$, the universal set and $x_{12}$.
ContMDiffOndefMathlib.Geometry.Manifold.ContMDiff.Defs, predicateEnglish
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 $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 $\mathrm{M'}$. Let $s$ be an element of $\wp M$. Then $\mathrm{ContMDiffOn}$ holds for $I$, $\mathrm{I'}$, $n$, $f$ and $s$, if for all elements $x_{12}$ of $M$, if $x_{12}$ is an element of $s$, then $\mathrm{ContMDiffWithinAt}$ holds for $I$, $\mathrm{I'}$, $n$, $f$, $s$ and $x_{12}$.
ContMDiffWithinAtdefMathlib.Geometry.Manifold.ContMDiff.Defs, predicateEnglish
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 $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 $\mathrm{M'}$. Let $s$ be an element of $\wp M$. Let $x_{12}$ be an element of $M$. Then $\mathrm{ContMDiffWithinAt}$ holds for $I$, $\mathrm{I'}$, $n$, $f$, $s$ and $x_{12}$, if $\operatorname{LiftPropWithinAt}$ holds for $\mathrm{ContDiffWithinAtProp}$ applied to $I$, $\mathrm{I'}$ and $n$, $f$, $s$ and $x_{12}$.
equivTangentBundleProddefMathlib.Geometry.Manifold.ContMDiffMFDeriv, function or constantWording
the equivalence tangent bundle product of I and #3 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $\mathrm{M'}$ be sets. Let $\mathrm{I'}$ be a model with corner of $\mathrm{E'}$ and $\mathrm{H'}$. Then the equivalence tangent bundle product of $I$ and $\mathrm{I'}$ is an equivalence from the set of tangent bundles of the product of $I$ and $\mathrm{I'}$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ to $\mathrm{Prod}$ applied to the set of tangent bundles of $I$ and $M$ and the set of tangent bundles of $\mathrm{I'}$ and $\mathrm{M'}$.
ContMDiffMapdefMathlib.Geometry.Manifold.ContMDiffMap, typeWording
continuous difference map of #4 and #5 (from the name)
English
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 $M$ and $\mathrm{M'}$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then a continuous difference map of $\mathrm{M'}$ and $n$ is an element of the function that maps $I$, $\mathrm{I'}$, $M$, $\mathrm{M'}$ and $n$ to $\SubtypeSet {f}{\mathrm{ContMDiff} (I , \mathrm{I'} , n , f)}$.
ContMDiffMap.compdefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a continuous difference map of $\mathrm{M''}$ and $n$. Let $g$ be a continuous difference map of $\mathrm{M'}$ and $n$. Then the composition of $f$ and $g$ is a continuous difference map of $\mathrm{M''}$ and $n$ defined as the function that maps $a$ to $f$ applied to $g$ applied to $a$.
ContMDiffMap.constdefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the constant of y (from the name)
English
Let $y$ be an element of $\mathrm{M'}$. Then the constant of $y$ is a continuous difference map of $\mathrm{M'}$ and $n$ defined as the function that maps $x_{12}$ to $y$.
ContMDiffMap.fstdefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the first projection (from the docstring)
English
The first projection is a continuous difference map of $M$ and $n$ defined as $\ProdfstMACRoZ$.
ContMDiffMap.iddefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the identity (from the docstring)
English
The identity is a continuous difference map of $M$ and $n$ defined as $\mathrm{id}$.
ContMDiffMap.prodMkdefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the product of f and g (from the name)
English
Let $f$ be a continuous difference map of $M$ and $n$. Let $g$ be a continuous difference map of $\mathrm{M'}$ and $n$. Then the product of $f$ and $g$ is a continuous difference map of $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ and $n$ defined as the function that maps $x_{17}$ to $\ProdmkMACRoU {f (x_{17})}{g (x_{17})}$.
ContMDiffMap.snddefMathlib.Geometry.Manifold.ContMDiffMap, function or constantWording
the second projection (from the docstring)
English
The second projection is a continuous difference map of $\mathrm{M'}$ and $n$ defined as $\ProdsndMACRoAA$.
ContMDiffFunction.evalAtdefMathlib.Geometry.Manifold.DerivationBundle, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then $\operatorname{evalAt}$ applied to $I$ and $x_{7}$ is a linear map of the set of continuous difference maps of $x$ and $\operatorname{some}$ applied to the top and $x$ defined as the linear map of the evaluation of $x_{7}$.
Derivation.evalAtdefMathlib.Geometry.Manifold.DerivationBundle, function or constantWording
the evaluation at a point of x7 (from the docstring)
English
Let $x_{7}$ be an element of $M$. Then the evaluation at a point of $x_{7}$ is a linear map of the set of derivations of the set of continuous difference maps of $x$ and $\operatorname{some}$ applied to the top and the set of continuous difference maps of $x$ and $\operatorname{some}$ applied to the top and the set of point derivations of $I$ and $x_{7}$ defined as $\operatorname{compDer}$ applied to $\operatorname{evalAt}$ applied to $I$ and $x_{7}$.
PointDerivationdefMathlib.Geometry.Manifold.DerivationBundle, typeWording
point derivation of I and x7 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then a point derivation of $I$ and $x_{7}$ is an element of the function that maps $I$ and $x_{7}$ to the set of derivations of the set of pointed continuous difference maps of $\operatorname{some}$ applied to the top and $x_{7}$ and $x$.
PointedContMDiffMapdefMathlib.Geometry.Manifold.DerivationBundle, typeWording
pointed continuous difference map of n and x7 (from the name)
English
Let $x$ and $M$ be sets. Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $x_{7}$ be an element of $M$. Then a pointed continuous difference map of $n$ and $x_{7}$ is an element of the function that maps $x$, $I$, $M$, $n$ and $x_{7}$ to the set of continuous difference maps of $x$ and $n$.
PointedContMDiffMap.evaldefMathlib.Geometry.Manifold.DerivationBundle, function or constantWording
the evaluation of x7 (from the name)
English
Let $x_{7}$ be an element of $M$. Then the evaluation of $x_{7}$ is an algebra homomorphism of the set of continuous difference maps of $x$ and $\operatorname{some}$ applied to the top and $x$ defined as the algebra of the set of pointed continuous difference maps of $\operatorname{some}$ applied to the top and $x_{7}$ and $x$.
fdifferentialdefMathlib.Geometry.Manifold.DerivationBundle, function or constantEnglish
Let $f$ be a continuous difference map of $\mathrm{M'}$ and $\operatorname{some}$ applied to the top. Let $x_{12}$ be an element of $M$. Then $\mathrm{fdifferential}$ applied to $f$ and $x_{12}$ is a linear map of the set of point derivations of $I$ and $x_{12}$ and the set of point derivations of $\mathrm{I'}$ and $f$ applied to $x_{12}$.
hfdifferentialdefMathlib.Geometry.Manifold.DerivationBundle, function or constantEnglish
Assume that $\EqtMACRoH {f (x_{12})}{y}$. Then $\mathrm{hfdifferential}$ applied to $h$ is a linear map of the set of point derivations of $I$ and $x_{12}$ and the set of point derivations of $\mathrm{I'}$ and $y$.
ContinuousLinearEquiv.toDiffeomorphdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the diffeomorphism of e (from the name)
English
Let $e$ be a continuous linear equivalence of $E$ and $\mathrm{E'}$. Then the diffeomorphism of $e$ is a diffeomorphism of $\mathrm{E'}$ and $\operatorname{some}$ applied to the top.
ContinuousLinearEquiv.toTransContinuousLinearEquivdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the composition continuous linear equivalence of I and e (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Let $e$ be a continuous linear equivalence of $E$ and $F$. Then the composition continuous linear equivalence of $I$ and $e$ is a diffeomorphism of $M$ and $n$.
DiffeomorphstructureMathlib.Geometry.Manifold.Diffeomorph, typeWording
diffeomorphism of #4 and #5 (from the name)
English
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 $M$ and $\mathrm{M'}$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the diffeomorphisms of $\mathrm{M'}$ and $n$ are a basic type.
Diffeomorph.emptydefMathlib.Geometry.Manifold.Diffeomorph, function or constantEnglish
$\operatorname{empty}$ is a diffeomorphism of $\mathrm{M'}$ and $n$.
Diffeomorph.prodAssocdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the product associator of M and #7 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $F$ and $G$. Let $\mathrm{J'}$ be a model with corner of $F$ and $\mathrm{G'}$. Let $M$, $N$ and $\mathrm{N'}$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the product associator of $\mathrm{J'}$ and $n$ is a diffeomorphism of $\mathrm{Prod}$ applied to $M$ and $\mathrm{Prod}$ applied to $N$ and $\mathrm{N'}$ and $n$.
Diffeomorph.prodCommdefMathlib.Geometry.Manifold.Diffeomorph, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $F$ and $G$. Let $M$ and $N$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then $\operatorname{prodComm}$ applied to $I$, $J$, $M$, $N$ and $n$ is a diffeomorphism of $\mathrm{Prod}$ applied to $N$ and $M$ and $n$.
Diffeomorph.prodCongrdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the product congruence of x20 and x21 (from the name)
English
Let $x_{20}$ be a diffeomorphism of $\mathrm{M'}$ and $n$. Let $x_{21}$ be a diffeomorphism of $\mathrm{N'}$ and $n$. Then the product congruence of $x_{20}$ and $x_{21}$ is a diffeomorphism of $\mathrm{Prod}$ applied to $\mathrm{M'}$ and $\mathrm{N'}$ and $n$.
Diffeomorph.refldefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the identity of I and n (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the identity of $I$ and $n$ is a diffeomorphism of $M$ and $n$ defined as $\operatorname{mk}$ applied to the identity of $M$, $\mathrm{contMDiff\_id}$ and $\mathrm{contMDiff\_id}$.
Diffeomorph.sumAssocdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the sum associator of I and n (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $M$, $\mathrm{M'}$ and $\mathrm{M''}$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the sum associator of $I$ and $n$ is a diffeomorphism of $\mathrm{Sum}$ applied to $M$ and $\mathrm{Sum}$ applied to $\mathrm{M'}$ and $\mathrm{M''}$ and $n$.
Diffeomorph.sumCommdefMathlib.Geometry.Manifold.Diffeomorph, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $M$ and $\mathrm{M'}$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then $\operatorname{sumComm}$ applied to $I$, $M$, $n$ and $\mathrm{M'}$ is a diffeomorphism of $\mathrm{Sum}$ applied to $\mathrm{M'}$ and $M$ and $n$ defined as $\operatorname{mk}$ applied to $\operatorname{sumComm}$ applied to $M$ and $\mathrm{M'}$, $\operatorname{swap}$ and $\operatorname{swap}$.
Diffeomorph.sumCongrdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the sum congruence of x15 and x16 (from the name)
English
Let $x_{15}$ be a diffeomorphism of $N$ and $n$. Let $x_{16}$ be a diffeomorphism of $\mathrm{N'}$ and $n$. Then the sum congruence of $x_{15}$ and $x_{16}$ is a diffeomorphism of $\mathrm{Sum}$ applied to $N$ and $\mathrm{N'}$ and $n$.
Diffeomorph.sumEmptydefMathlib.Geometry.Manifold.Diffeomorph, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then $\operatorname{sumEmpty}$ applied to $I$, $M$ and $n$ is a diffeomorphism of $M$ and $n$.
Diffeomorph.symmdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the inverse of h (from the name)
English
Let $h$ be a diffeomorphism of $N$ and $n$. Then the inverse of $h$ is a diffeomorphism of $M$ and $n$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toEquiv}$ applied to $h$, $\mathrm{Diffeomorph\_\_contMDiff\_invFun}$ applied to $h$ and $\mathrm{Diffeomorph\_\_contMDiff\_toFun}$ applied to $h$.
Diffeomorph.toContMDiffMapdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the continuous difference map of x12 (from the name)
English
Let $x_{12}$ be a diffeomorphism of $\mathrm{M'}$ and $n$. Then the continuous difference map of $x_{12}$ is a continuous difference map of $\mathrm{M'}$ and $n$ defined as $\operatorname{coe}$ applied to $x_{12}$.
Diffeomorph.toHomeomorphdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the homeomorphism of h (from the name)
English
Let $h$ be a diffeomorphism of $N$ and $n$. Then the homeomorphism of $h$ is a homeomorphism of $M$ and $N$.
Diffeomorph.transdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the composition of x17 and x18 (from the name)
English
Let $x_{17}$ be a diffeomorphism of $\mathrm{M'}$ and $n$. Let $x_{18}$ be a diffeomorphism of $N$ and $n$. Then the composition of $x_{17}$ and $x_{18}$ is a diffeomorphism of $N$ and $n$.
ModelWithCorners.transContinuousLinearEquivdefMathlib.Geometry.Manifold.Diffeomorph, function or constantWording
the composition continuous linear equivalence of I and e (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $e$ be a continuous linear equivalence of $E$ and $\mathrm{E'}$. Then the composition continuous linear equivalence of $I$ and $e$ is a model with corner of $\mathrm{E'}$ and $H$.
AddGroupLieAlgebradefMathlib.Geometry.Manifold.GroupLieAlgebra, typeWording
additive group Lie algebra of I and G (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $G$ be a set. Then an additive group Lie algebra of $I$ and $G$ is an element of the function that maps $I$ and $G$ to the set of tangent spaces of $I$ and $0$.
GroupLieAlgebradefMathlib.Geometry.Manifold.GroupLieAlgebra, typeWording
group Lie algebra of I and G (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $G$ be a set. Then a group Lie algebra of $I$ and $G$ is an element of the function that maps $I$ and $G$ to the set of tangent spaces of $I$ and $1$.
addInvariantVectorFielddefMathlib.Geometry.Manifold.GroupLieAlgebra, function or constantWording
the additive invariant vector field of v and g (from the name)
English
Let $v$ be an additive group Lie algebra of $I$ and $G$. Let $g$ be an element of $G$. Then the additive invariant vector field of $v$ and $g$ is a tangent space of $I$ and $g$ defined as $\operatorname{mfderiv}$ applied to $I$, $I$, the function that maps $x_{9}$ to $g + x_{9}$, $0$ and $v$.
mulInvariantVectorFielddefMathlib.Geometry.Manifold.GroupLieAlgebra, function or constantWording
the multiplicative invariant vector field of v and g (from the name)
English
Let $v$ be a group Lie algebra of $I$ and $G$. Let $g$ be an element of $G$. Then the multiplicative invariant vector field of $v$ and $g$ is a tangent space of $I$ and $g$ defined as $\operatorname{mfderiv}$ applied to $I$, $I$, the function that maps $x_{9}$ to $g \times x_{9}$, $1$ and $v$.
HasGroupoidclassMathlib.Geometry.Manifold.HasGroupoid, predicateWording
G has groupoids (from the name)
English
Let $M$ be a set. Let $G$ be a structure groupoid of $H$. Then we can say that $G$ has groupoids.
OpenPartialHomeomorph.toStructomorphdefMathlib.Geometry.Manifold.HasGroupoid, function or constantEnglish
Assume that $\MembershipmemMACRoT {\mathrm{atlas} (H , M)}{e}$. Then $\operatorname{toStructomorph}$ applied to $\mathrm{he}$ is an element of $\mathrm{Structomorph}$ applied to $G$, $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{mk} (\operatorname{source} (\operatorname{toPartialEquiv} (\operatorname{toPartialHomeomorph} (e))), \mathrm{OpenPartialHomeomorph\_\_open\_source} (e))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{mk} (\operatorname{target} (\operatorname{toPartialEquiv} (\operatorname{toPartialHomeomorph} (e))), \mathrm{OpenPartialHomeomorph\_\_open\_target} (e))}{x_{4}})}$.
StructomorphstructureMathlib.Geometry.Manifold.HasGroupoid, typeEnglish
Let $G$ be a structure groupoid of $H$. Let $M$ and $\mathrm{M'}$ be sets. Then the elements of $\mathrm{Structomorph}$ applied to $G$, $M$ and $\mathrm{M'}$ are a basic type.
Structomorph.refldefMathlib.Geometry.Manifold.HasGroupoid, function or constantWording
the identity of M (from the docstring)
English
Let $M$ be a set. Then the identity of $M$ is an element of $\mathrm{Structomorph}$ applied to $G$, $M$ and $M$.
Structomorph.symmdefMathlib.Geometry.Manifold.HasGroupoid, function or constantWording
the inverse of e (from the docstring)
English
Let $e$ be an element of $\mathrm{Structomorph}$ applied to $G$, $M$ and $\mathrm{M'}$. Then the inverse of $e$ is an element of $\mathrm{Structomorph}$ applied to $G$, $\mathrm{M'}$ and $M$.
Structomorph.transdefMathlib.Geometry.Manifold.HasGroupoid, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be an element of $\mathrm{Structomorph}$ applied to $G$, $M$ and $\mathrm{M'}$. Let $\mathrm{e'}$ be an element of $\mathrm{Structomorph}$ applied to $G$, $\mathrm{M'}$ and $\mathrm{M''}$. Then the composition of $e$ and $\mathrm{e'}$ is an element of $\mathrm{Structomorph}$ applied to $G$, $M$ and $\mathrm{M''}$.
StructureGroupoid.maximalAtlasdefMathlib.Geometry.Manifold.HasGroupoid, function or constantWording
the maximal atlas of M and G (from the name)
English
Let $M$ be a set. Let $G$ be a structure groupoid of $H$. Then the maximal atlas of $M$ and $G$ is an element of the power set of the set of open partial homeomorphisms of $M$ and $H$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that for all open partial homeomorphisms $\mathrm{e'}$ of $M$ and $H$, if $\mathrm{e'}$ is an element of the atlas of $H$ and $M$, then the composition of the inverse of $e$ and $\mathrm{e'}$ is an element of $G$ and the composition of the inverse of $\mathrm{e'}$ and $e$ is an element of $G$.
Manifold.ImmersionAtPropdefMathlib.Geometry.Manifold.Immersion, predicateEnglish
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{ImmersionAtProp}$ holds for $F$, $I$, $J$, $M$, $N$, $x_{12}$, $x_{13}$ and $x_{14}$, if there exists a continuous linear equivalence $\mathrm{equiv}$ of $\mathrm{Prod}$ applied to $E$ and $F$ and $\mathrm{E''}$, 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 $\operatorname{coe}$ applied to $\mathrm{equiv}$ and the function that maps $x_{15}$ to $\ProdmkMACRoU {x_{15}}{0}$ and the target of $\operatorname{extend}$ applied to $x_{13}$ and $I$.
Manifold.IsImmersiondefMathlib.Geometry.Manifold.Immersion, predicateEnglish
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{IsImmersion}$ 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{IsImmersionOfComplement}$ holds for $F$, $I$, $J$, $n$ and $f$.
Manifold.IsImmersion.complementdefMathlib.Geometry.Manifold.Immersion, typeWording
complement of h (from the name)
English
Assume that $\operatorname{IsImmersion}$ 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$.
Manifold.IsImmersionAtdefMathlib.Geometry.Manifold.Immersion, predicateEnglish
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{IsImmersionAt}$ 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{IsImmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{12}$.
Manifold.IsImmersionAt.codChartdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the codomain chart of h (from the name)
English
Assume that $\operatorname{IsImmersionAt}$ 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\_\_IsImmersionAt\_\_isImmersionAtOfComplement\_complement}$ applied to $h$.
Manifold.IsImmersionAt.complementdefMathlib.Geometry.Manifold.Immersion, typeWording
complement of h (from the name)
English
Assume that $\operatorname{IsImmersionAt}$ 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$.
Manifold.IsImmersionAt.domChartdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the domain chart of h (from the name)
English
Assume that $\operatorname{IsImmersionAt}$ 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\_\_IsImmersionAt\_\_isImmersionAtOfComplement\_complement}$ applied to $h$.
Manifold.IsImmersionAt.equivdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the equivalence of h (from the name)
English
Assume that $\operatorname{IsImmersionAt}$ holds for $I$, $J$, $n$, $f$ and $x_{12}$. Then the equivalence of $h$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $E$ and the set of complements of $h$ and $\mathrm{E''}$ defined as the equivalence of $\mathrm{Manifold\_\_IsImmersionAt\_\_isImmersionAtOfComplement\_complement}$ applied to $h$.
Manifold.IsImmersionAtOfComplementdefMathlib.Geometry.Manifold.Immersion, predicateEnglish
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{IsImmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$, if $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{14}$ and $\operatorname{ImmersionAtProp}$ applied to $F$, $I$, $J$, $M$ and $N$.
Manifold.IsImmersionAtOfComplement.codChartdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the codomain chart of h (from the name)
English
Assume that $\operatorname{IsImmersionAtOfComplement}$ 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$.
Manifold.IsImmersionAtOfComplement.domChartdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the domain chart of h (from the name)
English
Assume that $\operatorname{IsImmersionAtOfComplement}$ 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$.
Manifold.IsImmersionAtOfComplement.equivdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the equivalence of h (from the name)
English
Assume that $\operatorname{IsImmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$. Then the equivalence of $h$ is a continuous linear equivalence of $\mathrm{Prod}$ applied to $E$ and $F$ and $\mathrm{E''}$.
Manifold.IsImmersionAtOfComplement.smallComplementdefMathlib.Geometry.Manifold.Immersion, typeWording
small complement of hf (from the name)
English
Assume that $\operatorname{IsImmersionAtOfComplement}$ 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$.
Manifold.IsImmersionAtOfComplement.smallEquivdefMathlib.Geometry.Manifold.Immersion, function or constantWording
the small equivalence of hf (from the name)
English
Assume that $\operatorname{IsImmersionAtOfComplement}$ 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.
Manifold.IsImmersionOfComplementdefMathlib.Geometry.Manifold.Immersion, predicateEnglish
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{IsImmersionOfComplement}$ holds for $F$, $I$, $J$, $n$ and $f$, if for all elements $x_{14}$ of $M$, $\operatorname{IsImmersionAtOfComplement}$ holds for $F$, $I$, $J$, $n$, $f$ and $x_{14}$.
IsDiffImmersionAtdefMathlib.Geometry.Manifold.ImmersionDiff, predicateEnglish
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 $x_{12}$ be an element of $M$. Then $\mathrm{IsDiffImmersionAt}$ holds for $I$, $\mathrm{I'}$, $f$ and $x_{12}$, if $\mathrm{mfderiv}$ applied to $I$, $\mathrm{I'}$, $f$ and $x_{12}$ has left inverses.
oneTangentSpaceIccdefMathlib.Geometry.Manifold.Instances.Icc, function or constantWording
the one tangent space closed interval of z (from the name)
English
Let $z$ be an element of $\SetIccMACRoP {x}{y}$. Then the one tangent space closed interval of $z$ is a tangent space of the model with corner Euclidean half space of $1$ and $z$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_Geometry\_\_Manifold\_\_Instances\_\_Icc\_\_824482695\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $z$.
EuclideanHalfSpacedefMathlib.Geometry.Manifold.Instances.Real, typeWording
Euclidean half space of n (from the name)
English
Let $n$ be a natural number. Then a Euclidean half space of $n$ is an element of the function that maps $n$ to $\SubtypeSet {x}{\mathrm{Leq} (0 , \operatorname{ofLp} (x , 0))}$.
EuclideanQuadrantdefMathlib.Geometry.Manifold.Instances.Real, typeWording
quadrant in n (from the docstring)
English
Let $n$ be a natural number. Then a quadrant in $n$ is an element of the function that maps $n$ to $\SubtypeSet {x}{\mathrm{forall} (\mathrm{Fin} (n), \lambda i . \mathrm{Leq} (0 , \operatorname{ofLp} (x , i)))}$.
IccLeftChartdefMathlib.Geometry.Manifold.Instances.Real, function or constantWording
the left chart for the topological space of x and y (from the docstring)
English
Let $x$ and $y$ be real numbers. Then the left chart for the topological space of $x$ and $y$ is an open partial homeomorphism of the set of elements of $\SetIccMACRoP {x}{y}$ and the set of Euclidean half spaces of $1$.
IccRightChartdefMathlib.Geometry.Manifold.Instances.Real, function or constantWording
the right chart for the topological space of x and y (from the docstring)
English
Let $x$ and $y$ be real numbers. Then the right chart for the topological space of $x$ and $y$ is an open partial homeomorphism of the set of elements of $\SetIccMACRoP {x}{y}$ and the set of Euclidean half spaces of $1$.
modelWithCornersEuclideanHalfSpacedefMathlib.Geometry.Manifold.Instances.Real, function or constantWording
the model with corner Euclidean half space of n (from the name)
English
Let $n$ be a natural number. Then the model with corner Euclidean half space of $n$ is a model with corner of the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ and the set of Euclidean half spaces of $n$.
modelWithCornersEuclideanQuadrantdefMathlib.Geometry.Manifold.Instances.Real, function or constantWording
the model with corner Euclidean quadrant of n (from the name)
English
Let $n$ be a natural number. Then the model with corner Euclidean quadrant of $n$ is a model with corner of the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$ and the set of quadrants in $n$.
stereoInvFundefMathlib.Geometry.Manifold.Instances.Sphere, function or constantEnglish
Assume that $\operatorname{norm} (v)= 1$. Let $w$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (\Real , \operatorname{singleton} (v)))}{x_{2}})}$. Then $\mathrm{stereoInvFun}$ applied to $\mathrm{hv}$ and $w$ is an element of the sphere of $0$ and $1$ defined as $\mathrm{stereoInvFunAux}$ applied to $v$ and $w$.
stereoToFundefMathlib.Geometry.Manifold.Instances.Sphere, function or constantEnglish
Let $v$ and $x_{2}$ be elements of $E$. Then $\mathrm{stereoToFun}$ applied to $v$ and $x_{2}$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (\Real , \operatorname{singleton} (v)))}{x_{3}})}$ defined as $\HSMulhSMulMACRoAL {(\frac{ 2}{1 - \operatorname{coe} (\mathrm{innerSL} (\Real), v , x_{2})})}{\operatorname{orthogonalProjectionOnto} (\operatorname{orthogonal} (\operatorname{span} (\Real , \operatorname{singleton} (v))), x_{2})}$.
stereographicdefMathlib.Geometry.Manifold.Instances.Sphere, function or constantEnglish
Assume that $\operatorname{norm} (v)= 1$. Then $\mathrm{stereographic}$ applied to $\mathrm{hv}$ is an open partial homeomorphism of the set of elements of the sphere of $0$ and $1$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{orthogonal} (\operatorname{span} (\Real , \operatorname{singleton} (v)))}{x_{2}})}$.
stereographic'defMathlib.Geometry.Manifold.Instances.Sphere, function or constantEnglish
Let $n$ be a natural number. Let $v$ be an element of the sphere of $0$ and $1$. Then $\mathrm{stereographic'}$ applied to $n$ and $v$ is an open partial homeomorphism of the set of elements of the sphere of $0$ and $1$ and the set of Euclidean spaces of $\Real$ and $\mathrm{Fin}$ applied to $n$.
IsMIntegralCurvedefMathlib.Geometry.Manifold.IntegralCurve.Basic, predicateEnglish
Let $x_{5}$ be a function from real numbers to elements of $M$. Let $v$ be a function from elements $x_{6}$ of $M$ to tangent spaces of $I$ and $x_{6}$. Then $\mathrm{IsMIntegralCurve}$ holds for $x_{5}$, $x_{6}$ and $v$, if for all real numbers $t$, $\mathrm{HasMFDerivAt}$ holds for the model with corner self of $\Real$ and $\Real$, $I$, $x_{5}$, $t$ and the right scalar multiple of $1$ and $x_{6}$ applied to $x_{5}$ applied to $t$.
IsMIntegralCurveAtdefMathlib.Geometry.Manifold.IntegralCurve.Basic, predicateEnglish
Let $x_{5}$ be a function from real numbers to elements of $M$. Let $v$ be a function from elements $x_{7}$ of $M$ to tangent spaces of $I$ and $x_{7}$. Let $x_{6}$ be a real number. Then $\mathrm{IsMIntegralCurveAt}$ holds for $x_{5}$, $x_{7}$, $v$ and $x_{6}$, if $\operatorname{Eventually}$ holds for the function that maps $t$ to $\mathrm{HasMFDerivAt}$ applied to the model with corner self of $\Real$ and $\Real$, $I$, $x_{5}$, $t$ and the right scalar multiple of $1$ and $x_{7}$ applied to $x_{5}$ applied to $t$, the neighbourhood filter of $v$ and $x_{6}$.
IsMIntegralCurveOndefMathlib.Geometry.Manifold.IntegralCurve.Basic, predicateEnglish
Let $x_{5}$ be a function from real numbers to elements of $M$. Let $v$ be a function from elements $x_{6}$ of $M$ to tangent spaces of $I$ and $x_{6}$. Let $s$ be an element of $\wp \Real$. Then $\mathrm{IsMIntegralCurveOn}$ holds for $x_{5}$, $x_{6}$, $v$ and $s$, if for all real numbers $t$, if $t$ is an element of $v$, then $\mathrm{HasMFDerivWithinAt}$ holds for the model with corner self of $\Real$ and $\Real$, $I$, $x_{5}$, $v$, $t$ and the right scalar multiple of $1$ and $x_{6}$ applied to $x_{5}$ applied to $t$.
ENat.LEInftyclassMathlib.Geometry.Manifold.IsManifold.Basic, predicateEnglish
Let $m$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then we can say that $\operatorname{LEInfty}$ holds for $m$.
IsManifoldclassMathlib.Geometry.Manifold.IsManifold.Basic, predicateWording
n is a manifold with respect to I (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $M$ be a set. Then we can say that $n$ is a manifold with respect to $I$.
IsManifold.maximalAtlasdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the maximal atlas of I and n (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $M$ be a set. Then the maximal atlas of $I$ and $n$ is an element of the power set of the set of open partial homeomorphisms of $M$ and $H$ defined as the maximal atlas of $M$ and the continuous difference groupoid of $n$ and $I$.
ModelWithCornersstructureMathlib.Geometry.Manifold.IsManifold.Basic, typeWording
model with corner of E and H (from the name)
English
Let $x$, $E$ and $H$ be sets. Then the models with corner of $E$ and $H$ are a basic type.
ModelWithCorners.BoundarylessclassMathlib.Geometry.Manifold.IsManifold.Basic, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Then we can say that $\operatorname{Boundaryless}$ holds for $I$.
ModelWithCorners.ofConvexRangedefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the model with corner of x3 (from the name)
English
Let $x_{3}$ be a partial equivalence of $H$ and $E$ such that the source of $x_{3}$ is equal to the universal set, the target of $x_{3}$ is convex, $\operatorname{toFun}$ applied to $x_{3}$ and $\operatorname{toFun}$ applied to the inverse of $x_{3}$ are continuous and the interior of the target of $x_{3}$ is nonempty. Then the model with corner of $x_{3}$ is a model with corner of $E$ and $H$.
ModelWithCorners.ofTargetUnivdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the model with corner of x5 (from the name)
English
Let $x$ be a set. Let $x_{5}$ be a partial equivalence of $H$ and $E$ such that the source of $x_{5}$ is equal to the universal set, the target of $x_{5}$ is equal to the universal set and $\operatorname{toFun}$ applied to $x_{5}$ and $\operatorname{toFun}$ applied to the inverse of $x_{5}$ are continuous. Then the model with corner of $x_{5}$ is a model with corner of $E$ and $H$.
ModelWithCorners.pidefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the product of I (from the name)
English
Let $I$ be a function from elements $i_{1}$ of $x_{2}$ to models with corner of $E$ applied to $i_{1}$ and $H$ applied to $i_{1}$. Then the product of $i_{1}$ is a model with corner of the set of functions from elements $i$ of $x_{2}$ to elements of $E$ applied to $i$ and the set of model products of $H$.
ModelWithCorners.proddefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the product of I and #2 (from the name)
English
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'}$. Then the product of $I$ and $\mathrm{I'}$ is a model with corner of $\mathrm{Prod}$ applied to $E$ and $\mathrm{E'}$ and the set of model products of $H$ and $\mathrm{H'}$.
ModelWithCorners.symmdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the inverse of I (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Then the inverse of $I$ is a partial equivalence of $E$ and $H$ defined as the inverse of $\operatorname{toPartialEquiv}$ applied to $I$.
ModelWithCorners.tangentdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the tangent of I (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Then the tangent of $I$ is a model with corner of $\mathrm{Prod}$ applied to $E$ and $E$ and the set of model products of $H$ and $E$ defined as the product of $I$ and the model with corner self of $x$ and $E$.
ModelWithCorners.toFun'defMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the function of e and x5 (from the name)
English
Let $e$ be a model with corner of $E$ and $H$. Let $x_{5}$ be an element of $H$. Then the function of $e$ and $x_{5}$ is an element of $E$ defined as the partial equivalence of $\operatorname{toPartialEquiv}$ applied to $e$ and $x_{5}$.
ModelWithCorners.toHomeomorphdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the homeomorphism of I (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Then the homeomorphism of $I$ is a homeomorphism of $H$ and $E$.
NormedSpace.fromTangentSpacedefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantEnglish
Let $v$ be an element of $E$. Then $\operatorname{fromTangentSpace}$ applied to $v$ is a continuous linear equivalence of the set of tangent spaces of the model with corner self of $x$ and $E$ and $v$ and $E$ defined as the tangent space cast model of the model with corner self of $x$ and $E$ and $v$.
TangentBundledefMathlib.Geometry.Manifold.IsManifold.Basic, typeWording
tangent bundle of I and M (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Then a tangent bundle of $I$ and $M$ is an element of the function that maps $I$ and $M$ to the set of total spaces of $E$ and the set of elements of $\mathrm{TangentSpace}$ applied to $I$.
TangentSpacedefMathlib.Geometry.Manifold.IsManifold.Basic, typeWording
tangent space of I and _x (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $\mathrm{\_x}$ be an element of $M$. Then a tangent space of $I$ and $\mathrm{\_x}$ is an element of the function that maps $I$ and $\mathrm{\_x}$ to $E$.
contDiffGroupoiddefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the continuous difference groupoid of n and I (from the name)
English
Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $I$ be a model with corner of $E$ and $H$. Then the continuous difference groupoid of $n$ and $I$ is a structure groupoid of $H$ defined as the groupoid of $\mathrm{contDiffPregroupoid}$ applied to $n$ and $I$.
contDiffPregroupoiddefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantEnglish
Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Let $I$ be a model with corner of $E$ and $H$. Then $\mathrm{contDiffPregroupoid}$ applied to $n$ and $I$ is an element of $\mathrm{Pregroupoid}$ applied to $H$.
tangentSpaceCastdefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the tangent space cast of x7 and y (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ and $y$ be elements of $M$. Then the tangent space cast of $x_{7}$ and $y$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{7}$ and the set of tangent spaces of $I$ and $y$.
tangentSpaceCastModeldefMathlib.Geometry.Manifold.IsManifold.Basic, function or constantWording
the tangent space cast model of I and x7 (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then the tangent space cast model of $I$ and $x_{7}$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{7}$ and $E$.
ModelWithCorners.extendCoordChangedefMathlib.Geometry.Manifold.IsManifold.ExtChartAt, function or constantEnglish
Let $e$ and $\mathrm{e'}$ be open partial homeomorphisms of $M$ and $H$. Then $\operatorname{extendCoordChange}$ applied to $e$ and $\mathrm{e'}$ is a partial equivalence of $E$ and $E$ defined as the composition of the inverse of $\operatorname{extend}$ applied to $e$ and $I$ and $\operatorname{extend}$ applied to $\mathrm{e'}$ and $I$.
OpenPartialHomeomorph.extenddefMathlib.Geometry.Manifold.IsManifold.ExtChartAt, function or constantEnglish
Let $f$ be an open partial homeomorphism of $M$ and $H$. Let $I$ be a model with corner of $E$ and $H$. Then $\operatorname{extend}$ applied to $f$ and $I$ is a partial equivalence of $M$ and $E$ defined as the composition of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $f$ and $\operatorname{toPartialEquiv}$ applied to $I$.
extChartAtdefMathlib.Geometry.Manifold.IsManifold.ExtChartAt, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then $\mathrm{extChartAt}$ applied to $I$ and $x_{7}$ is a partial equivalence of $M$ and $E$ defined as $\operatorname{extend}$ applied to $\mathrm{chartAt}$ applied to $H$ and $x_{7}$ and $I$.
writtenInExtChartAtdefMathlib.Geometry.Manifold.IsManifold.ExtChartAt, function or constantEnglish
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 $x_{12}$ be an element of $M$. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $x_{13}$ be an element of $E$. Then $\mathrm{writtenInExtChartAt}$ applied to $I$, $\mathrm{I'}$, $x_{12}$, $f$ and $x_{13}$ is an element of $\mathrm{E'}$ defined as $\operatorname{comp}$ applied to $\operatorname{toFun}$ applied to $\mathrm{extChartAt}$ applied to $\mathrm{I'}$ and $f$ applied to $x_{12}$, $\operatorname{comp}$ applied to $f$ and $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $x_{12}$ and $x_{13}$.
BoundarylessManifoldclassMathlib.Geometry.Manifold.IsManifold.InteriorBoundary, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $M$ be a set. Then we can say that $\mathrm{BoundarylessManifold}$ holds for $I$ and $M$.
ModelWithCorners.IsBoundaryPointdefMathlib.Geometry.Manifold.IsManifold.InteriorBoundary, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then $\operatorname{IsBoundaryPoint}$ holds for $I$ and $x_{7}$, if the partial equivalence of $\mathrm{extChartAt}$ applied to $I$ and $x_{7}$ and $x_{7}$ is an element of the frontier of the range of $\operatorname{toFun'}$ applied to $I$.
ModelWithCorners.IsInteriorPointdefMathlib.Geometry.Manifold.IsManifold.InteriorBoundary, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $x_{7}$ be an element of $M$. Then $\operatorname{IsInteriorPoint}$ holds for $I$ and $x_{7}$, if the partial equivalence of $\mathrm{extChartAt}$ applied to $I$ and $x_{7}$ and $x_{7}$ is an element of the interior of the range of $\operatorname{toFun'}$ applied to $I$.
ModelWithCorners.boundarydefMathlib.Geometry.Manifold.IsManifold.InteriorBoundary, function or constantWording
the boundary of M (from the name)
English
Let $M$ be a set. Then the boundary of $M$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to $\operatorname{IsBoundaryPoint}$ applied to $I$ and $x_{7}$.
ModelWithCorners.interiordefMathlib.Geometry.Manifold.IsManifold.InteriorBoundary, function or constantWording
the interior of M (from the name)
English
Let $M$ be a set. Then the interior of $M$ is an element of $\wp M$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to $\operatorname{IsInteriorPoint}$ applied to $I$ and $x_{7}$.
Diffeomorph.mfderivToContinuousLinearEquivdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantEnglish
Let $x_{14}$ be a diffeomorphism of $N$ and $n$. Assume that $n \neq 0$. Let $x_{15}$ be an element of $M$. Then $\operatorname{mfderivToContinuousLinearEquiv}$ applied to $x_{14}$, $\mathrm{hn}$ and $x_{15}$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{15}$ and the set of tangent spaces of $J$ and $x_{14}$ applied to $x_{15}$ defined as $\operatorname{mfderivToContinuousLinearEquiv}$ applied to $\operatorname{isLocalDiffeomorph}$ applied to $x_{14}$ and $x_{15}$ and $\mathrm{hn}$.
Diffeomorph.toPartialDiffeomorphdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the partial diffeomorphism of h (from the name)
English
Let $h$ be a diffeomorphism of $N$ and $n$. Then the partial diffeomorphism of $h$ is a partial diffeomorphism of $N$ and $n$.
IsLocalDiffeomorphdefMathlib.Geometry.Manifold.LocalDiffeomorph, predicateEnglish
Let $I$ be a model with corner of $E$ and $x_{6}$. Let $J$ be a model with corner of $F$ and $x_{8}$. 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 $\mathrm{IsLocalDiffeomorph}$ holds for $I$, $J$, $n$ and $f$, if for all elements $x_{14}$ of $M$, $\mathrm{IsLocalDiffeomorphAt}$ holds for $I$, $J$, $n$, $f$ and $x_{14}$.
IsLocalDiffeomorph.diffeomorphOfBijectivedefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the diffeomorphism of hf and #2 (from the name)
English
Assume that $\mathrm{IsLocalDiffeomorph}$ holds for $I$, $J$, $n$ and $f$. Assume that $f$ is bijective. Then the diffeomorphism of $\mathrm{hf}$ and $\mathrm{hf'}$ is a diffeomorphism of $N$ and $n$.
IsLocalDiffeomorph.imagedefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the image of hf (from the docstring)
English
Assume that $\mathrm{IsLocalDiffeomorph}$ holds for $I$, $J$, $n$ and $f$. Then the image of $\mathrm{hf}$ is an open of $N$ defined as $\operatorname{mk}$ applied to the range of $f$ and $\mathrm{IsLocalDiffeomorph\_\_isOpen\_range}$ applied to $\mathrm{hf}$.
IsLocalDiffeomorph.mfderivToContinuousLinearEquivdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantEnglish
Assume that $\mathrm{IsLocalDiffeomorph}$ holds for $I$, $J$, $n$ and $f$. Assume that $n \neq 0$. Let $x_{14}$ be an element of $M$. Then $\operatorname{mfderivToContinuousLinearEquiv}$ applied to $\mathrm{hf}$, $\mathrm{hn}$ and $x_{14}$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{14}$ and the set of tangent spaces of $J$ and $f$ applied to $x_{14}$ defined as $\operatorname{mfderivToContinuousLinearEquiv}$ applied to $\mathrm{hf}$ applied to $x_{14}$ and $\mathrm{hn}$.
IsLocalDiffeomorphAtdefMathlib.Geometry.Manifold.LocalDiffeomorph, predicateEnglish
Let $I$ be a model with corner of $E$ and $x_{6}$. Let $J$ be a model with corner of $F$ and $x_{8}$. 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 $\mathrm{IsLocalDiffeomorphAt}$ holds for $I$, $J$, $n$, $f$ and $x_{14}$, if there exists a partial diffeomorphism $x_{15}$ of $N$ and $n$, such that $x_{14}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $x_{15}$ and $\operatorname{EqOn}$ holds for $f$, $\operatorname{toFun}$ applied to $\operatorname{toPartialEquiv}$ applied to $x_{15}$ and the source of $\operatorname{toPartialEquiv}$ applied to $x_{15}$.
IsLocalDiffeomorphAt.localInversedefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the local inverse of hf (from the name)
English
Assume that $\mathrm{IsLocalDiffeomorphAt}$ holds for $I$, $J$, $n$, $f$ and $x_{14}$. Then the local inverse of $\mathrm{hf}$ is a partial diffeomorphism of $M$ and $n$ defined as the inverse of $\operatorname{choose}$ applied to $\mathrm{hf}$.
IsLocalDiffeomorphAt.mfderivToContinuousLinearEquivdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantEnglish
Assume that $\mathrm{IsLocalDiffeomorphAt}$ holds for $I$, $J$, $n$, $f$ and $x_{14}$. Assume that $n \neq 0$. Then $\operatorname{mfderivToContinuousLinearEquiv}$ applied to $\mathrm{hf}$ and $\mathrm{hn}$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{14}$ and the set of tangent spaces of $J$ and $f$ applied to $x_{14}$.
IsLocalDiffeomorphOndefMathlib.Geometry.Manifold.LocalDiffeomorph, predicateEnglish
Let $I$ be a model with corner of $E$ and $x_{6}$. Let $J$ be a model with corner of $F$ and $x_{8}$. 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 $s$ be an element of $\wp M$. Then $\mathrm{IsLocalDiffeomorphOn}$ holds for $I$, $J$, $n$, $f$ and $s$, if for all elements $x_{14}$ of $s$, $\mathrm{IsLocalDiffeomorphAt}$ holds for $I$, $J$, $n$, $f$ and $x_{14}$.
PartialDiffeomorphstructureMathlib.Geometry.Manifold.LocalDiffeomorph, typeWording
partial diffeomorphism of N and n (from the name)
English
Let $I$ be a model with corner of $E$ and $x_{6}$. Let $J$ be a model with corner of $F$ and $x_{8}$. Let $M$ and $N$ be sets. Let $n$ be an element of $\mathrm{WithTop}$ applied to the set of natural numbers. Then the partial diffeomorphisms of $N$ and $n$ are a basic type.
PartialDiffeomorph.symmdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the inverse of x14 (from the docstring)
English
Let $x_{14}$ be a partial diffeomorphism of $N$ and $n$. Then the inverse of $x_{14}$ is a partial diffeomorphism of $M$ and $n$ defined as $\operatorname{mk}$ applied to the inverse of $\operatorname{toPartialEquiv}$ applied to $x_{14}$, $\mathrm{PartialDiffeomorph\_\_open\_target}$ applied to $x_{14}$, $\mathrm{PartialDiffeomorph\_\_open\_source}$ applied to $x_{14}$, $\mathrm{PartialDiffeomorph\_\_contMDiffOn\_invFun}$ applied to $x_{14}$ and $\mathrm{PartialDiffeomorph\_\_contMDiffOn\_toFun}$ applied to $x_{14}$.
PartialDiffeomorph.toOpenPartialHomeomorphdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the open partial homeomorphism of x14 (from the name)
English
Let $x_{14}$ be a partial diffeomorphism of $N$ and $n$. Then the open partial homeomorphism of $x_{14}$ is an open partial homeomorphism of $M$ and $N$.
PartialDiffeomorph.transdefMathlib.Geometry.Manifold.LocalDiffeomorph, function or constantWording
the composition of x20 and x21 (from the name)
English
Let $x_{20}$ be a partial diffeomorphism of $N$ and $n$. Let $x_{21}$ be a partial diffeomorphism of $P$ and $n$. Then the composition of $x_{20}$ and $x_{21}$ is a partial diffeomorphism of $P$ and $n$.
ChartedSpace.LiftPropdefMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $P$ be a function from functions from elements of $H$ to elements of $\mathrm{H'}$ and elements of $\wp H$ and elements of $H$ to propositions. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Then $\operatorname{LiftProp}$ holds for $P$ and $f$, if for all elements $x_{6}$ of $M$, $\operatorname{LiftPropAt}$ holds for $P$, $f$ and $x_{6}$.
ChartedSpace.LiftPropAtdefMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $P$ be a function from functions from elements of $H$ to elements of $\mathrm{H'}$ and elements of $\wp H$ and elements of $H$ to propositions. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $x_{6}$ be an element of $M$. Then $\operatorname{LiftPropAt}$ holds for $P$, $f$ and $x_{6}$, if $\operatorname{LiftPropWithinAt}$ holds for $P$, $f$, the universal set and $x_{6}$.
ChartedSpace.LiftPropOndefMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $P$ be a function from functions from elements of $H$ to elements of $\mathrm{H'}$ and elements of $\wp H$ and elements of $H$ to propositions. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $s$ be an element of $\wp M$. Then $\operatorname{LiftPropOn}$ holds for $P$, $f$ and $s$, if for all elements $x_{6}$ of $M$, if $x_{6}$ is an element of $s$, then $\operatorname{LiftPropWithinAt}$ holds for $P$, $f$, $s$ and $x_{6}$.
ChartedSpace.LiftPropWithinAtstructureMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $P$ be a function from functions from elements of $H$ to elements of $\mathrm{H'}$ and elements of $\wp H$ and elements of $H$ to propositions. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $s$ be an element of $\wp M$. Let $x_{6}$ be an element of $M$. Then we can say that $\operatorname{LiftPropWithinAt}$ holds for $P$, $f$, $s$ and $x_{6}$.
StructureGroupoid.IsLocalStructomorphWithinAtdefMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $G$ be a structure groupoid of $H$. Let $f$ be a function from elements of $H$ to elements of $H$. Let $s$ be an element of $\wp H$. Let $x_{1}$ be an element of $H$. Then $\operatorname{IsLocalStructomorphWithinAt}$ holds for $G$, $f$, $s$ and $x_{1}$, if if $x_{1}$ is an element of $s$, then there exists an open partial homeomorphism $e$ of $H$ and $H$, such that $e$ is an element of $G$, $\operatorname{EqOn}$ holds for $f$, $\operatorname{toFun}$ applied to $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $\operatorname{inter}$ applied to $s$ and the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$ and $x_{1}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$.
StructureGroupoid.LocalInvariantPropstructureMathlib.Geometry.Manifold.LocalInvariantProperties, predicateEnglish
Let $G$ be a structure groupoid of $H$. Let $\mathrm{G'}$ be a structure groupoid of $\mathrm{H'}$. Let $P$ be a function from functions from elements of $H$ to elements of $\mathrm{H'}$ and elements of $\wp H$ and elements of $H$ to propositions. Then we can say that $\operatorname{LocalInvariantProp}$ holds for $G$, $\mathrm{G'}$ and $P$.
Manifold.IsLocalSourceTargetPropertystructureMathlib.Geometry.Manifold.LocalSourceTargetProperty, predicateWording
P is a local source target property (from the name)
English
Let $P$ be a function from functions from elements of $M$ to elements of $N$ and open partial homeomorphisms of $M$ and $H$ and open partial homeomorphisms of $N$ and $G$ to propositions. Then we can say that $P$ is a local source target property.
Manifold.LiftSourceTargetPropertyAtdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $F$ 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$. Let $P$ be a function from functions from elements of $M$ to elements of $N$ and open partial homeomorphisms of $M$ and $H$ and open partial homeomorphisms of $N$ and $G$ to propositions. Then $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{12}$ and $P$, if $\mathrm{Nonempty}$ holds for $\operatorname{LocalPresentationAt}$ applied to $I$, $J$, $n$, $f$, $x_{12}$ and $P$.
Manifold.LiftSourceTargetPropertyAt.codChartdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, function or constantWording
the codomain chart of h (from the name)
English
Assume that $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{12}$ and $P$. Then the codomain chart of $h$ is an open partial homeomorphism of $N$ and $G$ defined as the codomain chart of $\operatorname{localPresentationAt}$ applied to $h$.
Manifold.LiftSourceTargetPropertyAt.domChartdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, function or constantWording
the domain chart of h (from the name)
English
Assume that $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{12}$ and $P$. Then the domain chart of $h$ is an open partial homeomorphism of $M$ and $H$ defined as the domain chart of $\operatorname{localPresentationAt}$ applied to $h$.
Manifold.LiftSourceTargetPropertyAt.localPresentationAtdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, function or constantEnglish
Assume that $\operatorname{LiftSourceTargetPropertyAt}$ holds for $I$, $J$, $n$, $f$, $x_{12}$ and $P$. Then $\operatorname{localPresentationAt}$ applied to $h$ is an element of $\operatorname{LocalPresentationAt}$ applied to $I$, $J$, $n$, $f$, $x_{12}$ and $P$ defined as $\operatorname{choice}$ applied to $h$.
Manifold.LocalPresentationAtstructureMathlib.Geometry.Manifold.LocalSourceTargetProperty, typeEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $J$ be a model with corner of $F$ 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$. Let $P$ be a function from functions from elements of $M$ to elements of $N$ and open partial homeomorphisms of $M$ and $H$ and open partial homeomorphisms of $N$ and $G$ to propositions. Then the elements of $\operatorname{LocalPresentationAt}$ applied to $I$, $J$, $n$, $f$, $x_{12}$ and $P$ are a basic type.
Manifold.LocalPresentationAt.codChartdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, function or constantWording
the codomain chart of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{LocalPresentationAt}$ applied to $I$, $J$, $n$, $f$, $x_{12}$ and $P$. Then the codomain chart of $\mathrm{self}$ is an open partial homeomorphism of $N$ and $G$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Manifold.LocalPresentationAt.domChartdefMathlib.Geometry.Manifold.LocalSourceTargetProperty, function or constantWording
the domain chart of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{LocalPresentationAt}$ applied to $I$, $J$, $n$, $f$, $x_{12}$ and $P$. Then the domain chart of $\mathrm{self}$ is an open partial homeomorphism of $M$ and $H$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
OpenPartialHomeomorph.MDifferentiable.mfderivdefMathlib.Geometry.Manifold.MFDeriv.Atlas, function or constantEnglish
Assume that $\operatorname{MDifferentiable}$ holds for $I$, $\mathrm{I'}$ and $e$. Assume that $x_{12}$ is an element of the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $e$. Then $\operatorname{mfderiv}$ applied to $\mathrm{he}$ and $\mathrm{hx}$ is a continuous linear equivalence of the set of tangent spaces of $I$ and $x_{12}$ and the set of tangent spaces of $\mathrm{I'}$ and the function of $e$ and $x_{12}$.
DifferentiableWithinAtPropdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $H$ to elements of $\mathrm{H'}$. Let $s$ be an element of $\wp H$. Let $x_{8}$ be an element of $H$. Then $\mathrm{DifferentiableWithinAtProp}$ holds for $I$, $\mathrm{I'}$, $f$, $s$ and $x_{8}$, if $\mathrm{DifferentiableWithinAt}$ holds for $x$, $\operatorname{comp}$ applied to $\operatorname{toFun'}$ applied to $\mathrm{I'}$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{toFun}$ applied to the inverse of $I$, $\operatorname{inter}$ applied to the preimage of $\operatorname{toFun}$ applied to the inverse of $I$ and $s$ and the range of $\operatorname{toFun'}$ applied to $I$ and the function of $I$ and $x_{8}$.
HasMFDerivAtdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $x_{12}$ be an element of $M$. Let $\mathrm{f'}$ be a continuous linear map of the set of tangent spaces of $I$ and $x_{12}$ and the set of tangent spaces of $\mathrm{I'}$ and $f$ applied to $x_{12}$. Then $\mathrm{HasMFDerivAt}$ holds for $I$, $\mathrm{I'}$, $f$, $x_{12}$ and $\mathrm{f'}$, if $\mathrm{ContinuousAt}$ holds for $f$ and $x_{12}$ and $\mathrm{HasFDerivWithinAt}$ holds for $\mathrm{writtenInExtChartAt}$ applied to $I$, $\mathrm{I'}$, $x_{12}$ and $f$, the composition of the continuous linear map of the tangent space cast model of $\mathrm{I'}$ and $f$ applied to $x_{12}$ and the composition of $\mathrm{f'}$ and the continuous linear map of the inverse of the tangent space cast model of $I$ and $x_{12}$, the range of $\operatorname{toFun'}$ applied to $I$ and the partial equivalence of $\mathrm{extChartAt}$ applied to $I$ and $x_{12}$ and $x_{12}$.
HasMFDerivWithinAtdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $s$ be an element of $\wp M$. Let $x_{12}$ be an element of $M$. Let $\mathrm{f'}$ be a continuous linear map of the set of tangent spaces of $I$ and $x_{12}$ and the set of tangent spaces of $\mathrm{I'}$ and $f$ applied to $x_{12}$. Then $\mathrm{HasMFDerivWithinAt}$ holds for $I$, $\mathrm{I'}$, $f$, $s$, $x_{12}$ and $\mathrm{f'}$, if $\mathrm{ContinuousWithinAt}$ holds for $f$, $s$ and $x_{12}$ and $\mathrm{HasFDerivWithinAt}$ holds for $\mathrm{writtenInExtChartAt}$ applied to $I$, $\mathrm{I'}$, $x_{12}$ and $f$, the composition of the continuous linear map of the tangent space cast model of $\mathrm{I'}$ and $f$ applied to $x_{12}$ and the composition of $\mathrm{f'}$ and the continuous linear map of the inverse of the tangent space cast model of $I$ and $x_{12}$, $\operatorname{inter}$ applied to the preimage of $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $x_{12}$ and $s$ and the range of $\operatorname{toFun'}$ applied to $I$ and the partial equivalence of $\mathrm{extChartAt}$ applied to $I$ and $x_{12}$ and $x_{12}$.
MDifferentiabledefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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'}$. Then $\mathrm{MDifferentiable}$ holds for $I$, $\mathrm{I'}$ and $f$, if for all elements $x_{12}$ of $M$, $\mathrm{MDifferentiableAt}$ holds for $I$, $\mathrm{I'}$, $f$ and $x_{12}$.
MDifferentiableAtdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $x_{12}$ be an element of $M$. Then $\mathrm{MDifferentiableAt}$ holds for $I$, $\mathrm{I'}$, $f$ and $x_{12}$, if $\operatorname{LiftPropAt}$ holds for $\mathrm{DifferentiableWithinAtProp}$ applied to $I$ and $\mathrm{I'}$, $f$ and $x_{12}$.
MDifferentiableOndefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $s$ be an element of $\wp M$. Then $\mathrm{MDifferentiableOn}$ holds for $I$, $\mathrm{I'}$, $f$ and $s$, if for all elements $x_{12}$ of $M$, if $x_{12}$ is an element of $s$, then $\mathrm{MDifferentiableWithinAt}$ holds for $I$, $\mathrm{I'}$, $f$, $s$ and $x_{12}$.
MDifferentiableWithinAtdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 $s$ be an element of $\wp M$. Let $x_{12}$ be an element of $M$. Then $\mathrm{MDifferentiableWithinAt}$ holds for $I$, $\mathrm{I'}$, $f$, $s$ and $x_{12}$, if $\operatorname{LiftPropWithinAt}$ holds for $\mathrm{DifferentiableWithinAtProp}$ applied to $I$ and $\mathrm{I'}$, $f$, $s$ and $x_{12}$.
OpenPartialHomeomorph.MDifferentiabledefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
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 an open partial homeomorphism of $M$ and $\mathrm{M'}$. Then $\operatorname{MDifferentiable}$ holds for $I$, $\mathrm{I'}$ and $f$, if $\mathrm{MDifferentiableOn}$ holds for $I$, $\mathrm{I'}$, $\operatorname{toFun'}$ applied to $f$ and the source of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $f$ and $\mathrm{MDifferentiableOn}$ holds for $\mathrm{I'}$, $I$, $\operatorname{toFun'}$ applied to the inverse of $f$ and the target of $\operatorname{toPartialEquiv}$ applied to $\operatorname{toPartialHomeomorph}$ applied to $f$.
UniqueMDiffOndefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $s$ be an element of $\wp M$. Then $\mathrm{UniqueMDiffOn}$ holds for $I$ and $s$, if for all elements $x_{7}$ of $M$, if $x_{7}$ is an element of $s$, then $\mathrm{UniqueMDiffWithinAt}$ holds for $I$, $s$ and $x_{7}$.
UniqueMDiffWithinAtdefMathlib.Geometry.Manifold.MFDeriv.Defs, predicateEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $s$ be an element of $\wp M$. Let $x_{7}$ be an element of $M$. Then $\mathrm{UniqueMDiffWithinAt}$ holds for $I$, $s$ and $x_{7}$, if $\mathrm{UniqueDiffWithinAt}$ holds for $x$, $\operatorname{inter}$ applied to the preimage of $\operatorname{toFun}$ applied to the inverse of $\mathrm{extChartAt}$ applied to $I$ and $x_{7}$ and $s$ and the range of $\operatorname{toFun'}$ applied to $I$ and the partial equivalence of $\mathrm{extChartAt}$ applied to $I$ and $x_{7}$ and $x_{7}$.
mfderivdefMathlib.Geometry.Manifold.MFDeriv.Defs, function or constantEnglish
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 $x_{12}$ be an element of $M$. Then $\mathrm{mfderiv}$ applied to $I$, $\mathrm{I'}$, $f$ and $x_{12}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{12}$ and the set of tangent spaces of $\mathrm{I'}$ and $f$ applied to $x_{12}$ defined as $\iteMACRoG {\mathrm{MDifferentiableAt} (I , \mathrm{I'} , f , x_{12})}{\operatorname{comp} (\operatorname{toContinuousLinearMap} (\operatorname{symm} (\mathrm{tangentSpaceCastModel} (\mathrm{I'} , f (x_{12})))), \operatorname{comp} (\mathrm{fderivWithin} (x , \mathrm{writtenInExtChartAt} (I , \mathrm{I'} , x_{12} , f), \operatorname{range} (\operatorname{toFun'} (I)), \operatorname{toFun} (\mathrm{extChartAt} (I , x_{12}), x_{12})), \operatorname{toContinuousLinearMap} (\mathrm{tangentSpaceCastModel} (I , x_{12}))))}{0}$.
mfderivWithindefMathlib.Geometry.Manifold.MFDeriv.Defs, function or constantEnglish
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 $s$ be an element of $\wp M$. Let $x_{12}$ be an element of $M$. Then $\mathrm{mfderivWithin}$ applied to $I$, $\mathrm{I'}$, $f$, $s$ and $x_{12}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{12}$ and the set of tangent spaces of $\mathrm{I'}$ and $f$ applied to $x_{12}$ defined as $\iteMACRoG {\mathrm{MDifferentiableWithinAt} (I , \mathrm{I'} , f , s , x_{12})}{\operatorname{comp} (\operatorname{toContinuousLinearMap} (\operatorname{symm} (\mathrm{tangentSpaceCastModel} (\mathrm{I'} , f (x_{12})))), \operatorname{comp} (\mathrm{fderivWithin} (x , \mathrm{writtenInExtChartAt} (I , \mathrm{I'} , x_{12} , f), \operatorname{inter} (\operatorname{preimage} (\operatorname{toFun} (\operatorname{symm} (\mathrm{extChartAt} (I , x_{12}))), s), \operatorname{range} (\operatorname{toFun'} (I))), \operatorname{toFun} (\mathrm{extChartAt} (I , x_{12}), x_{12})), \operatorname{toContinuousLinearMap} (\mathrm{tangentSpaceCastModel} (I , x_{12}))))}{0}$.
tangentMapdefMathlib.Geometry.Manifold.MFDeriv.Defs, function or constantWording
the tangent map of x12 and #4 (from the name)
English
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 $x_{12}$ be a tangent bundle of $I$ and $M$. Then the tangent map of $f$ and $x_{12}$ is a tangent bundle of $\mathrm{I'}$ and $\mathrm{M'}$ defined as $\operatorname{mk}$ applied to $f$ applied to the projection of $x_{12}$ and $\operatorname{mfderiv}$ applied to $I$, $\mathrm{I'}$, $f$, the projection of $x_{12}$ and the second component of $x_{12}$.
tangentMapWithindefMathlib.Geometry.Manifold.MFDeriv.Defs, function or constantEnglish
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 $s$ be an element of $\wp M$. Let $x_{12}$ be a tangent bundle of $I$ and $M$. Then $\mathrm{tangentMapWithin}$ applied to $I$, $\mathrm{I'}$, $f$, $s$ and $x_{12}$ is a tangent bundle of $\mathrm{I'}$ and $\mathrm{M'}$ defined as $\operatorname{mk}$ applied to $f$ applied to the projection of $x_{12}$ and $\operatorname{mfderivWithin}$ applied to $I$, $\mathrm{I'}$, $f$, $s$, the projection of $x_{12}$ and the second component of $x_{12}$.
mvfderivdefMathlib.Geometry.Manifold.MFDeriv.NormedSpace, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $g$ be a function from elements of $M$ to elements of $F$. Let $x_{9}$ be an element of $M$. Then $\mathrm{mvfderiv}$ applied to $I$, $g$ and $x_{9}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{9}$ and $F$ defined as the composition of the continuous linear map of $\operatorname{fromTangentSpace}$ applied to $g$ applied to $x_{9}$ and $\mathrm{mfderiv}$ applied to $I$, the model with corner self of $x$ and $F$, $g$ and $x_{9}$.
mvfderivWithindefMathlib.Geometry.Manifold.MFDeriv.NormedSpace, function or constantEnglish
Let $I$ be a model with corner of $E$ and $H$. Let $g$ be a function from elements of $M$ to elements of $F$. Let $s$ be an element of $\wp M$. Let $x_{9}$ be an element of $M$. Then $\mathrm{mvfderivWithin}$ applied to $I$, $g$, $s$ and $x_{9}$ is a continuous linear map of the set of tangent spaces of $I$ and $x_{9}$ and $F$ defined as the composition of the continuous linear map of $\operatorname{fromTangentSpace}$ applied to $g$ applied to $x_{9}$ and $\mathrm{mfderivWithin}$ applied to $I$, the model with corner self of $x$ and $F$, $g$, $s$ and $x_{9}$.
tangentBundleModelSpaceDiffeomorphdefMathlib.Geometry.Manifold.MFDeriv.Tangent, function or constantWording
the tangent bundle model space diffeomorphism of I and n (from the name)
English
Let $I$ be a model with corner of $E$ and $H$. Let $n$ be a natural number. Then the tangent bundle model space diffeomorphism of $I$ and $n$ is a diffeomorphism of the set of model products of $H$ and $E$ and $\operatorname{some}$ applied to $n$.