IsEquivclassMathlib.Order.Defs.Unbundled, predicateWording
r is an equivalence relation (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is an equivalence relation.
IsLinearOrderclassMathlib.Order.Defs.Unbundled, predicateWording
r is a linear order (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is a linear order.
IsLowerSetdefMathlib.Order.Defs.Unbundled, predicateWording
s is a lower set (by hand)
English
Let $s$ be an element of $\wp x$. Then $s$ is a lower set, if for all elements $a$ and $b$ of $x$, if $b \leq a$, then if $a$ is an element of $s$, then $b$ is an element of $s$.
IsPartialOrderclassMathlib.Order.Defs.Unbundled, predicateWording
r is a partial order (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is a partial order.
IsPreorderclassMathlib.Order.Defs.Unbundled, predicateWording
r is a preorder (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is a preorder.
IsRelLowerSetdefMathlib.Order.Defs.Unbundled, predicateWording
s is a relative lower set with respect to P (from the name)
English
Let $s$ be an element of $\wp x$. Let $P$ be a function from elements of $x$ to propositions. Then $s$ is a relative lower set with respect to $P$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $P$ holds for $a$ and for all elements $b$ of $x$, if $b \leq a$, then if $P$ holds for $b$, then $b$ is an element of $s$.
IsRelUpperSetdefMathlib.Order.Defs.Unbundled, predicateWording
s is a relative upper set with respect to P (from the name)
English
Let $s$ be an element of $\wp x$. Let $P$ be a function from elements of $x$ to propositions. Then $s$ is a relative upper set with respect to $P$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $P$ holds for $a$ and for all elements $b$ of $x$, if $a \leq b$, then if $P$ holds for $b$, then $b$ is an element of $s$.
IsStrictOrderclassMathlib.Order.Defs.Unbundled, predicateWording
r is a strict order (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is a strict order.
IsStrictTotalOrderclassMathlib.Order.Defs.Unbundled, predicateWording
lt is a strict total order (by hand)
English
Let $x$ be a set. Let $\mathrm{lt}$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $\mathrm{lt}$ is a strict total order.
IsStrictWeakOrderclassMathlib.Order.Defs.Unbundled, predicateWording
lt is a strict weak order (by hand)
English
Let $x$ be a set. Let $\mathrm{lt}$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $\mathrm{lt}$ is a strict weak order.
IsTransclassMathlib.Order.Defs.Unbundled, predicateWording
r is transitive (by hand)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is transitive.
IsUpperSetdefMathlib.Order.Defs.Unbundled, predicateWording
s is an upper set (by hand)
English
Let $s$ be an element of $\wp x$. Then $s$ is a upper set, if for all elements $a$ and $b$ of $x$, if $a \leq b$, then if $a$ is an element of $s$, then $b$ is an element of $s$.
LowerSetstructureMathlib.Order.Defs.Unbundled, typeWording
lower set of x (by hand)
English
Let $x$ be a set. Then the lower sets of $x$ are a basic type.
LowerSet.carrierdefMathlib.Order.Defs.Unbundled, function or constantWording
the carrier of self (from the docstring)
English
Let $\mathrm{self}$ be a lower set of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
MaximaldefMathlib.Order.Defs.Unbundled, predicateWording
x2 is maximal with respect to P (by hand)
English
Let $P$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $x$. Then $x_{2}$ is maximal with respect to $P$, if $P$ holds for $x_{2}$ and for all elements $y$ of $x$, if $P$ holds for $y$, then if $x_{2} \leq y$, then $y \leq x_{2}$.
MaximalFordefMathlib.Order.Defs.Unbundled, predicateEnglish
Let $P$ be a function from elements of $x$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $i$ be an element of $x$. Then $\mathrm{MaximalFor}$ holds for $P$, $f$ and $i$, if $P$ holds for $i$ and for all elements $j$ of $x$, if $P$ holds for $j$, then if $f (i)\leq f (j)$, then $f (j)\leq f (i)$.
MinimaldefMathlib.Order.Defs.Unbundled, predicateWording
x2 is minimal with respect to P (by hand)
English
Let $P$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $x$. Then $x_{2}$ is minimal with respect to $P$, if $P$ holds for $x_{2}$ and for all elements $y$ of $x$, if $P$ holds for $y$, then if $y \leq x_{2}$, then $x_{2} \leq y$.
MinimalFordefMathlib.Order.Defs.Unbundled, predicateEnglish
Let $P$ be a function from elements of $x$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $i$ be an element of $x$. Then $\mathrm{MinimalFor}$ holds for $P$, $f$ and $i$, if $P$ holds for $i$ and for all elements $j$ of $x$, if $P$ holds for $j$, then if $f (j)\leq f (i)$, then $f (i)\leq f (j)$.
RelLowerSetstructureMathlib.Order.Defs.Unbundled, typeWording
relative lower set of P (from the name)
English
Let $P$ be a function from elements of $x$ to propositions. Then the relative lower sets of $P$ are a basic type.
RelLowerSet.carrierdefMathlib.Order.Defs.Unbundled, function or constantWording
the carrier of self (from the docstring)
English
Let $\mathrm{self}$ be a relative lower set of $P$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RelUpperSetstructureMathlib.Order.Defs.Unbundled, typeWording
relative upper set of P (from the name)
English
Let $P$ be a function from elements of $x$ to propositions. Then the relative upper sets of $P$ are a basic type.
RelUpperSet.carrierdefMathlib.Order.Defs.Unbundled, function or constantWording
the carrier of self (from the docstring)
English
Let $\mathrm{self}$ be a relative upper set of $P$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
UpperSetstructureMathlib.Order.Defs.Unbundled, typeWording
upper set of x (by hand)
English
Let $x$ be a set. Then the upper sets of $x$ are a basic type.
UpperSet.carrierdefMathlib.Order.Defs.Unbundled, function or constantWording
the carrier of self (from the docstring)
English
Let $\mathrm{self}$ be a upper set of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
DirSupCloseddefMathlib.Order.DirSupClosed, predicateEnglish
Let $s$ be an element of $\wp x$. Then $\mathrm{DirSupClosed}$ holds for $s$, if for all elements $d$ of $\wp x$, if $d \leq s$, then if $d$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then $a$ is an element of $s$.
DirSupClosedOndefMathlib.Order.DirSupClosed, predicateEnglish
Let $D$ be an element of $\wp (\wp x)$. Let $s$ be an element of $\wp x$. Then $\mathrm{DirSupClosedOn}$ holds for $D$ and $s$, if for all elements $d$ of $\wp x$, if $d$ is an element of $D$, then if $d \leq s$, then if $d$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then $a$ is an element of $s$.
DirSupInaccdefMathlib.Order.DirSupClosed, predicateEnglish
Let $s$ be an element of $\wp x$. Then $\mathrm{DirSupInacc}$ holds for $s$, if for all elements $d$ of $\wp x$, if $d$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then if $a$ is an element of $s$, then $\operatorname{inter}$ applied to $d$ and $s$ is nonempty.
DirSupInaccOndefMathlib.Order.DirSupClosed, predicateEnglish
Let $D$ be an element of $\wp (\wp x)$. Let $s$ be an element of $\wp x$. Then $\mathrm{DirSupInaccOn}$ holds for $D$ and $s$, if for all elements $d$ of $\wp x$, if $d$ is an element of $D$, then if $d$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then if $a$ is an element of $s$, then $\operatorname{inter}$ applied to $d$ and $s$ is nonempty.
DirecteddefMathlib.Order.Directed, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{Directed}$ holds for $r$ and $f$, if for all elements $x_{2}$ and $y$ of $x_{1}$, there exists an element $z$ of $x_{1}$, such that $r$ holds for $f$ applied to $x_{2}$ and $f$ applied to $z$ and $r$ holds for $f$ applied to $y$ and $f$ applied to $z$.
DirectedOndefMathlib.Order.Directed, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{DirectedOn}$ holds for $r$ and $s$, if for all elements $x_{1}$ of $x$, if $x_{1}$ is an element of $s$, then for all elements $y$ of $x$, if $y$ is an element of $s$, then there exists an element $z$ of $x$, such that $z$ is an element of $s$, $r$ holds for $x_{1}$ and $z$ and $r$ holds for $y$ and $z$.
IsCodirectedOrderdefMathlib.Order.Directed, predicateEnglish
Let $x$ be a set. Then $\mathrm{IsCodirectedOrder}$ holds for $x$, if the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{3} , x_{2})$ is directed.
IsDirectedclassMathlib.Order.Directed, predicateWording
r is directed (from the name)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $r$ is directed.
IsDirectedOrderdefMathlib.Order.Directed, predicateWording
x is a directed order (from the name)
English
Let $x$ be a set. Then $x$ is a directed order, if the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ is directed.
DirectLimitdefMathlib.Order.DirectedInverseSystem, typeWording
direct limit of F and f (from the name)
English
Let $F$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements $h_{2}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to elements of $T$ applied to $i$, $j$ and $h_{2}$. Then a direct limit of $F$ and $i$ is an element of the function that maps $F$, $f$, $j$, $h_{2}$ and $f$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $i$, $j$, $h_{2}$ and $f$.
DirectLimit.liftdefMathlib.Order.DirectedInverseSystem, function or constantWording
the lift of i2 and h3 (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements $h_{3}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to elements of $T$ applied to $i_{2}$, $j_{1}$ and $h_{3}$. Let $\mathrm{ih}$ be a function from elements $i_{1}$ of $x$ and elements of $F$ applied to $i_{1}$ to elements of $C$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{2}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{3}$ of $F$ applied to $i$, $\EqtMACRoH {\mathrm{ih} (i , x_{3})}{\mathrm{ih} (j , f (i , j , h_{2} , x_{3}))}$. Let $z$ be a direct limit of $F$ and $f$. Then the lift of $j_{1}$ and $f$ is an element of $C$.
DirectLimit.lift₂defMathlib.Order.DirectedInverseSystem, function or constantWording
the lift of x8 and i2 (from the name)
English
Let $x_{5}$ be a function from elements $i_{3}$ of $x$ and elements $j_{2}$ of $x$ and elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{3} , j_{2})$ to elements of $x_{4}$ applied to $i_{3}$, $j_{2}$ and $h_{5}$. Let $x_{8}$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to elements of $x_{7}$ applied to $i_{2}$, $j_{1}$ and $h_{4}$. Let $\mathrm{ih}$ be a function from elements $i_{1}$ of $x$ and elements of $x_{2}$ applied to $i_{1}$ and elements of $x_{3}$ applied to $i_{1}$ to elements of $C$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{3}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{10}$ of $x_{2}$ applied to $i$, for all elements $y$ of $x_{3}$ applied to $i$, $\EqtMACRoH {\mathrm{ih} (i , x_{10} , y)}{\mathrm{ih} (j , x_{5} (i , j , h_{3} , x_{10}), x_{8} (i , j , h_{3} , y))}$. Let $z$ be a direct limit of $x_{2}$ and $x_{5}$. Let $w$ be a direct limit of $x_{3}$ and $x_{8}$. Then the lift of $i_{2}$ and $j_{1}$ is an element of $C$.
DirectLimit.mapdefMathlib.Order.DirectedInverseSystem, function or constantWording
the map of j2 and x8 (from the name)
English
Let $x_{5}$ be a function from elements $i_{3}$ of $x$ and elements $j_{2}$ of $x$ and elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{3} , j_{2})$ to elements of $x_{4}$ applied to $i_{3}$, $j_{2}$ and $h_{5}$. Let $x_{8}$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to elements of $x_{7}$ applied to $i_{2}$, $j_{1}$ and $h_{4}$. Let $\mathrm{ih}$ be a function from elements $i_{1}$ of $x$ and elements of $x_{2}$ applied to $i_{1}$ to elements of $x_{3}$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{3}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{10}$ of $x_{2}$ applied to $i$, $\EqtMACRoH {x_{8} (i , j , h_{3} , \mathrm{ih} (i , x_{10}))}{\mathrm{ih} (j , x_{5} (i , j , h_{3} , x_{10}))}$. Let $z$ be a direct limit of $x_{2}$ and $x_{5}$. Then the map of $h_{5}$ and $i_{2}$ is a direct limit of $x_{3}$ and $x_{8}$.
DirectLimit.map₀defMathlib.Order.DirectedInverseSystem, function or constantWording
the map of f and i1 (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements $h_{3}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ to elements of $T$ applied to $i_{1}$, $j$ and $h_{3}$. Let $\mathrm{ih}$ be a function from elements $i$ of $x$ to elements of $F$ applied to $i$. Then the map of $i_{1}$ and $j$ is a direct limit of $F$ and $f$ defined as the function that maps $h_{3}$, $f$, $i$ and $\mathrm{ih}$ to $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $i_{1}$, $\operatorname{mk}$ applied to $\operatorname{arbitrary}$ applied to $x$ and $j$ applied to $\operatorname{arbitrary}$ applied to $x$, $h_{3}$, $f$, $i$ and $\mathrm{ih}$.
DirectLimit.map₂defMathlib.Order.DirectedInverseSystem, function or constantWording
the map of i3 and j2 (from the name)
English
Let $x_{5}$ be a function from elements $i_{4}$ of $x$ and elements $j_{3}$ of $x$ and elements $h_{7}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{4} , j_{3})$ to elements of $x_{4}$ applied to $i_{4}$, $j_{3}$ and $h_{7}$. Let $x_{8}$ be a function from elements $i_{3}$ of $x$ and elements $j_{2}$ of $x$ and elements $h_{6}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{3} , j_{2})$ to elements of $x_{7}$ applied to $i_{3}$, $j_{2}$ and $h_{6}$. Let $f$ be a function from elements $i_{2}$ of $x$ and elements $j_{1}$ of $x$ and elements $h_{5}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{2} , j_{1})$ to elements of $T$ applied to $i_{2}$, $j_{1}$ and $h_{5}$. Let $\mathrm{ih}$ be a function from elements $i_{1}$ of $x$ and elements of $x_{2}$ applied to $i_{1}$ and elements of $x_{3}$ applied to $i_{1}$ to elements of $F$ applied to $i_{1}$ such that for all elements $i$ and $j$ of $x$, for all elements $h_{4}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$, for all elements $x_{13}$ of $x_{2}$ applied to $i$, for all elements $y$ of $x_{3}$ applied to $i$, $\EqtMACRoH {f (i , j , h_{4} , \mathrm{ih} (i , x_{13} , y))}{\mathrm{ih} (j , x_{5} (i , j , h_{4} , x_{13}), x_{8} (i , j , h_{4} , y))}$. Let $x_{11}$ be a direct limit of $x_{2}$ and $x_{5}$. Let $x_{12}$ be a direct limit of $x_{3}$ and $x_{8}$. Then the map of $j_{2}$ and $h_{6}$ is a direct limit of $F$ and $f$.
DirectedSystemclassMathlib.Order.DirectedInverseSystem, predicateEnglish
Let $F$ be a function from elements of $x$ to sets. Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ and elements of $F$ applied to $i$ to elements of $F$ applied to $j$. Then we can say that $\mathrm{DirectedSystem}$ holds for $F$, $i$, $j$ and $f$.
InverseSystemclassMathlib.Order.DirectedInverseSystem, predicateWording
f is a inverse system (from the name)
English
Let $f$ be a function from elements $i$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ and elements of $F$ applied to $j$ to elements of $F$ applied to $i$. Then we can say that $i$ is an inverse system.
InverseSystem.IsNatEquivdefMathlib.Order.DirectedInverseSystem, predicateEnglish
Let $f$ be a function from elements $i$ of $x$ and elements $j_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j_{1})$ and elements of $F$ applied to $j_{1}$ to elements of $F$ applied to $i$. Let $\mathrm{equiv}$ be a function from elements $j$ of $s$ to elements of $\EquivMACRoAE {F (j)}{\operatorname{piLT} (X , j)}$. Then $\operatorname{IsNatEquiv}$ holds for $i$, $j_{1}$, $f$, $j$ and $\mathrm{equiv}$, if for all elements $j$ and $k$ of $x$, for all elements $\mathrm{hj}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{j}$, for all elements $\mathrm{hk}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {s}{k}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (k , j)$, for all elements $x_{2}$ of $F$ applied to $j$, $\EqtMACRoH {j_{1} (k , i (k , j , h , x_{2}))}{\operatorname{piLTProj} (h , j_{1} (j , x_{2}))}$.
InverseSystem.PEquivOnstructureMathlib.Order.DirectedInverseSystem, typeEnglish
Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ and elements of $F$ applied to $j$ to elements of $F$ applied to $i_{1}$. Let $\mathrm{equivSucc}$ be a function from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $i$ is not a maximum to equivalences from $F$ applied to the successor of $i$ to $\mathrm{Prod}$ applied to $F$ applied to $i$ and $X$ applied to $i$. Let $s$ be an element of $\wp x$. Then the elements of $\operatorname{PEquivOn}$ applied to $i_{1}$, $j$, $f$, $i$, $\mathrm{equivSucc}$ and $s$ are a basic type.
InverseSystem.PEquivOn.equivdefMathlib.Order.DirectedInverseSystem, function or constantWording
the equivalence of self and i (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $s$. Let $i$ be an element of $s$. Then the equivalence of $\mathrm{self}$ and $i$ is an element of $\EquivMACRoAE {F (i)}{\operatorname{piLT} (X , i)}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.
InverseSystem.PEquivOn.restrictdefMathlib.Order.DirectedInverseSystem, function or constantEnglish
Let $e$ be an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $t$. Assume that $s \leq t$. Then $\operatorname{restrict}$ applied to $e$ and $h$ is an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $s$.
InverseSystem.globalEquivdefMathlib.Order.DirectedInverseSystem, function or constantWording
the global equivalence of i2 and equivLim (from the name)
English
Let $\mathrm{equivSucc}$ be a function from elements $i_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $i_{2}$ is not a maximum to elements of $\SubtypeSet {e_{1}}{\mathrm{forall} (F (\operatorname{succ} (i_{2})), \lambda x_{4} . \EqtMACRoH {\ProdfstMACRoZ {e_{1} (x_{4})}}{f (i_{2} , \operatorname{succ} (i_{2}), \mathrm{Order\_\_le\_succ} (i_{2}), x_{4})})}$. Let $\mathrm{equivLim}$ be a function from elements $i_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{IsSuccPrelimit}$ applied to $i_{1}$ to elements of $\SubtypeSet {e}{\mathrm{forall} (F (i_{1}), \lambda x_{3} . \mathrm{forall} (\operatorname{Elem} (\operatorname{Iio} (i_{1})), \lambda l . \EqtMACRoH {l}{f (l , i_{1} , \operatorname{le} (\operatorname{property} (l)), x_{3})}))}$. Let $i$ be an element of $x$. Then the global equivalence of $\mathrm{equivSucc}$ and $i_{1}$ is an element of $\EquivMACRoAE {F (i)}{\operatorname{piLT} (X , i)}$.
InverseSystem.invLimEquivdefMathlib.Order.DirectedInverseSystem, function or constantWording
the inverse limit equivalence of nat (from the name)
English
Assume that $\operatorname{IsNatEquiv}$ holds for $f$ and $\mathrm{equiv}$. Then the inverse limit equivalence of $\mathrm{nat}$ is an equivalence from the set of elements of the inverse limit of $f$ and $i$ to the set of elements of the inverse limit of $\operatorname{piLTProj}$ and $i$.
InverseSystem.limitdefMathlib.Order.DirectedInverseSystem, function or constantWording
the inverse limit of f and i1 (from the docstring)
English
Let $f$ be a function from elements $i_{1}$ of $x$ and elements $j$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i_{1} , j)$ and elements of $F$ applied to $j$ to elements of $F$ applied to $i_{1}$. Let $i$ be an element of $x$. Then the inverse limit of $i_{1}$ and $j$ is an element of the power set of the set of functions from elements $l$ of $\operatorname{Iio}$ applied to $i$ to elements of $F$ applied to $l$ defined as the function that maps $f$ and $i$ to $\operatorname{ofPred}$ applied to the function that maps $F_{1}$ to the proposition that for all elements $j$ and $k$ of $\operatorname{Iio}$ applied to $j$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (j , k)$, $\EqtMACRoH {i_{1} (j , k , h , F_{1} (k))}{F_{1} (j)}$, $f$ and $i$.
InverseSystem.pEquivOnGluedefMathlib.Order.DirectedInverseSystem, function or constantWording
the equivalence on glue of hi and e (from the name)
English
Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Let $e$ be a function from elements $j$ of $\operatorname{Iio}$ applied to $i$ to elements of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iic}$ applied to $j$. Then the equivalence on glue of $\mathrm{hi}$ and $j$ is an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iio}$ applied to $i$.
InverseSystem.pEquivOnLimdefMathlib.Order.DirectedInverseSystem, function or constantWording
the equivalence on limit of e and j (from the name)
English
Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Let $e$ be a function from elements $j$ of $\operatorname{Iio}$ applied to $i$ to elements of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iic}$ applied to $j$. Let $\mathrm{equivLim}$ be an equivalence from $F$ applied to $i$ to the set of elements of the inverse limit of $f$ and $i$. Assume that for all elements $x_{3}$ of $F$ applied to $i$, for all elements $l$ of $\operatorname{Iio}$ applied to $i$, $\EqtMACRoH {l}{f (l , i , \operatorname{le} (\operatorname{property} (l)), x_{3})}$. Then the equivalence on limit of $j$ and $e$ is an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iic}$ applied to $i$.
InverseSystem.pEquivOnSuccdefMathlib.Order.DirectedInverseSystem, function or constantWording
the equivalence on successor of e (from the name)
English
Assume that $i$ is not a maximum. Let $e$ be an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iic}$ applied to $i$. Assume that for all elements $i_{1}$ of $x$, for all elements $\mathrm{hi1}$ of $\mathrm{Proof}$ applied to the proposition that $i_{1}$ is not a maximum, for all elements $x_{3}$ of $F$ applied to the successor of $i_{1}$, $\ProdfstMACRoZ {\mathrm{equivSucc} (i_{1} , \mathrm{hi1} , x_{3})}$ is equal to $f$ applied to $i_{1}$, the successor of $i_{1}$, $\mathrm{Order\_\_le\_succ}$ applied to $i_{1}$ and $x_{3}$. Then the equivalence on successor of $e$ is an element of $\operatorname{PEquivOn}$ applied to $f$, $\mathrm{equivSucc}$ and $\operatorname{Iic}$ applied to the successor of $i$.
InverseSystem.piEquivLimdefMathlib.Order.DirectedInverseSystem, function or constantWording
the product equivalence limit of equivLim and j (from the name)
English
Assume that $\operatorname{IsNatEquiv}$ holds for $f$ and $\mathrm{equiv}$. Let $\mathrm{equivLim}$ be an element of $\EquivMACRoAE {F (i)}{\operatorname{Elem} (\operatorname{limit} (f , i))}$. Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Let $j$ be an element of $\operatorname{Iic}$ applied to $i$. Then the product equivalence limit of $\mathrm{equivLim}$ and $j$ is an element of $\EquivMACRoAE {F (j)}{\operatorname{piLT} (X , j)}$ defined as $\operatorname{piSplitLE}$ applied to $\ProdmkMACRoU {\mathrm{equiv}}{\operatorname{trans} (\mathrm{equivLim} , \operatorname{trans} (\operatorname{invLimEquiv} (\mathrm{nat}), \operatorname{symm} (\operatorname{piLTLim} (\mathrm{hi}))))}$ and $j$.
InverseSystem.piEquivSuccdefMathlib.Order.DirectedInverseSystem, function or constantWording
the product equivalence successor of j1 and hi (from the name)
English
Let $\mathrm{equiv}$ be a function from elements $j_{1}$ of $\operatorname{Iic}$ applied to $i$ to elements of $\EquivMACRoAE {F (j_{1})}{\operatorname{piLT} (X , j_{1})}$. Let $e$ be an equivalence from $F$ applied to the successor of $i$ to $\mathrm{Prod}$ applied to $F$ applied to $i$ and $X$ applied to $i$. Assume that $i$ is not a maximum. Let $j$ be an element of $\operatorname{Iic}$ applied to the successor of $i$. Then the product equivalence successor of $\mathrm{equiv}$ and $\mathrm{hi}$ is an element of $\EquivMACRoAE {F (j)}{\operatorname{piLT} (X , j)}$.
InverseSystem.piLTdefMathlib.Order.DirectedInverseSystem, typeEnglish
Let $X$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then an element of $\operatorname{piLT}$ applied to $X$ and $i$ is an element of the function that maps $X$ and $i$ to the set of functions from elements $l$ of $\operatorname{Iio}$ applied to $i$ to elements of $X$ applied to $l$.
InverseSystem.piLTLimdefMathlib.Order.DirectedInverseSystem, function or constantEnglish
Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Then $\operatorname{piLTLim}$ applied to $\mathrm{hi}$ is an equivalence from $\operatorname{piLT}$ applied to $X$ and $i$ to the set of elements of the inverse limit of $\operatorname{piLTProj}$ and $i$.
InverseSystem.piLTProjdefMathlib.Order.DirectedInverseSystem, function or constantEnglish
Assume that $i \leq j$. Let $f$ be an element of $\operatorname{piLT}$ applied to $X$ and $j$. Then $\operatorname{piLT}$ holds for $X$ and $i$. Proof. Let $h$ be arbitrary. Let $f$ be arbitrary. Let $l$ be arbitrary. By l. By f.
InverseSystem.piSplitLEdefMathlib.Order.DirectedInverseSystem, function or constantEnglish
$\operatorname{piSplitLE}$ is an equivalence from $\mathrm{Prod}$ applied to $\operatorname{piLT}$ applied to $X$ and $i$ and $X$ applied to $i$ to the set of functions from elements $j$ of $\operatorname{Iic}$ applied to $i$ to elements of $X$ applied to $j$.
CodisjointdefMathlib.Order.Disjoint, predicateEnglish
Let $a$ and $b$ be elements of $x$. Then $\mathrm{Codisjoint}$ holds for $a$ and $b$, if for all elements $x_{3}$ of $x$, if $a \leq x_{3}$, then if $b \leq x_{3}$, then the top is less than or equal to $x_{3}$.
ComplementedLatticeclassMathlib.Order.Disjoint, predicateWording
x is a complemented lattice (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complemented lattice.
ComplementedsdefMathlib.Order.Disjoint, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{Complementeds}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {a}{\mathrm{IsComplemented} (a)}$.
DisjointdefMathlib.Order.Disjoint, predicateWording
a is disjoint to b (from the name)
English
Let $a$ and $b$ be elements of $x$. Then $a$ is disjoint to $b$, if for all elements $x_{3}$ of $x$, if $x_{3} \leq a$, then if $x_{3} \leq b$, then $x_{3}$ is less than or equal to the bottom.
IsComplstructureMathlib.Order.Disjoint, predicateEnglish
Let $x_{3}$ and $y$ be elements of $x$. Then we can say that $\mathrm{IsCompl}$ holds for $x_{3}$ and $y$.
IsComplementeddefMathlib.Order.Disjoint, predicateWording
a is complemented (from the docstring)
English
Let $a$ be an element of $x$. Then $a$ is complemented, if there exists an element $b$ of $x$, such that $\mathrm{IsCompl}$ holds for $a$ and $b$.
disjointeddefMathlib.Order.Disjointed, function or constantEnglish
Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $i$ be an element of $x_{1}$. Then $\mathrm{disjointed}$ applied to $f$ and $i$ is an element of $x$ defined as $\operatorname{sdiff}$ applied to $f$ applied to $i$ and the supremum of $\FinsetIioMACRoAK {i}$ and $f$.
LinearExtensiondefMathlib.Order.Extension.Linear, typeWording
linear extension of x (from the name)
English
Let $x$ be a set. Then a linear extension of $x$ is an element of the function that maps $x$ to $x$.
toLinearExtensiondefMathlib.Order.Extension.Linear, function or constantWording
the linear extension (from the name)
English
The linear extension is an order homomorphism of $x$ and the set of linear extensions of $x$.
WellOrderExtensiondefMathlib.Order.Extension.Well, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{WellOrderExtension}$ applied to $x$ is an element of the function that maps $x$ to $x$.
toWellOrderExtensiondefMathlib.Order.Extension.Well, function or constantEnglish
$\mathrm{toWellOrderExtension}$ is an element of $\EquivMACRoAE {x}{\mathrm{WellOrderExtension} (x)}$ defined as the identity of $x$.
Filter.atBotdefMathlib.Order.Filter.AtTopBot.Defs, function or constantEnglish
$\operatorname{atBot}$ is a filter of $x$ defined as the infimum of the function that maps $a$ to the principal filter of $\operatorname{Iic}$ applied to $a$.
Filter.atTopdefMathlib.Order.Filter.AtTopBot.Defs, function or constantEnglish
$\operatorname{atTop}$ is a filter of $x$ defined as the infimum of the function that maps $a$ to the principal filter of $\operatorname{Ici}$ applied to $a$.
Filter.HasAntitoneBasisstructureMathlib.Order.Filter.Bases.Basic, predicateEnglish
Let $l$ be a filter of $x$. Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{HasAntitoneBasis}$ holds for $l$ and $s$.
Filter.HasBasisstructureMathlib.Order.Filter.Bases.Basic, predicateEnglish
Let $l$ be a filter of $x$. Let $p$ be a function from elements of $x_{1}$ to propositions. Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{HasBasis}$ holds for $l$, $p$ and $s$.
Filter.HasBasis.indexdefMathlib.Order.Filter.Bases.Basic, function or constantWording
the index of t (from the name)
English
Assume that $\operatorname{HasBasis}$ holds for $l$, $p$ and $s$. Let $t$ be an element of $\wp x$ such that $t$ is an element of $l$. Then the index of $t$ is an element of $\SubtypeSet {i}{p (i)}$.
Filter.IsAntitoneBasisstructureMathlib.Order.Filter.Bases.Basic, predicateWording
#1 is a antitone basis (from the name)
English
Let $\mathrm{s''}$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\mathrm{s''}$ is an antitone basis.
Filter.IsBasisstructureMathlib.Order.Filter.Bases.Basic, predicateEnglish
Let $p$ be a function from elements of $x_{1}$ to propositions. Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{IsBasis}$ holds for $p$ and $s$.
Filter.IsBasis.filterdefMathlib.Order.Filter.Bases.Basic, function or constantWording
the filter of h (from the name)
English
Assume that $\operatorname{IsBasis}$ holds for $p$ and $s$. Then the filter of $h$ is a filter of $x$ defined as the filter of the filter basis of $h$.
Filter.IsBasis.filterBasisdefMathlib.Order.Filter.Bases.Basic, function or constantWording
the filter basis of h (from the name)
English
Assume that $\operatorname{IsBasis}$ holds for $p$ and $s$. Then the filter basis of $h$ is a filter basis of $x$.
Filter.asBasisdefMathlib.Order.Filter.Bases.Basic, function or constantEnglish
Let $f$ be a filter of $x$. Then $\operatorname{asBasis}$ applied to $f$ is a filter basis of $x$.
FilterBasisstructureMathlib.Order.Filter.Bases.Basic, typeWording
filter basis of x (from the name)
English
Let $x$ be a set. Then the filter bases of $x$ are a basic type.
FilterBasis.filterdefMathlib.Order.Filter.Bases.Basic, function or constantWording
the filter of B (from the name)
English
Let $B$ be a filter basis of $x$. Then the filter of $B$ is a filter of $x$.
FilterBasis.setsdefMathlib.Order.Filter.Bases.Basic, function or constantWording
the set of self (from the name)
English
Let $\mathrm{self}$ be a filter basis of $x$. Then the set of $\mathrm{self}$ is an element of $\wp (\wp x)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Filter.FilterBasis.ofSetsdefMathlib.Order.Filter.Bases.Finite, function or constantWording
the filter basis of s (from the name)
English
Let $s$ be an element of $\wp (\wp x)$. Then the filter basis of $s$ is a filter basis of $x$.
Filter.GenerateSetsinductiveMathlib.Order.Filter.Basic, predicateEnglish
Let $g$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{GenerateSets}$ holds for $g$ and $x_{1}$.
Filter.GenerateSets.belowinductiveMathlib.Order.Filter.Basic, predicateEnglish
Assume that $\operatorname{GenerateSets}$ holds for $g$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
Filter.generatedefMathlib.Order.Filter.Basic, function or constantEnglish
Let $g$ be an element of $\wp (\wp x)$. Then $\operatorname{generate}$ applied to $g$ is a filter of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{GenerateSets}$ applied to $g$ and $s$, $\operatorname{univ}$, the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{superset}$ and the function that maps $x_{3}$ and $x_{4}$ to $\operatorname{inter}$.
Filter.giGeneratedefMathlib.Order.Filter.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{giGenerate}$ applied to $x$ is a Galois insertion of $\operatorname{generate}$ and $\operatorname{sets}$.
Filter.mkOfClosuredefMathlib.Order.Filter.Basic, function or constantEnglish
Let $s$ be an element of $\wp (\wp x)$ such that the set of $\operatorname{generate}$ applied to $s$ is equal to $s$. Then $\operatorname{mkOfClosure}$ applied to $s$ and $\mathrm{hs}$ is a filter of $x$.
CardinalInterFilterclassMathlib.Order.Filter.CardinalInter, predicateWording
l is a cardinal intersection filter with respect to c (from the name)
English
Let $l$ be a filter of $x$. Let $c$ be a cardinal. Then we can say that $l$ is a cardinal intersection filter with respect to $c$.
Filter.CardinalGenerateSetsinductiveMathlib.Order.Filter.CardinalInter, predicateEnglish
Let $g$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{CardinalGenerateSets}$ holds for $g$ and $x_{1}$.
Filter.CardinalGenerateSets.belowinductiveMathlib.Order.Filter.CardinalInter, predicateEnglish
Assume that $\operatorname{CardinalGenerateSets}$ holds for $g$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
Filter.cardinalGeneratedefMathlib.Order.Filter.CardinalInter, function or constantEnglish
Let $g$ be an element of $\wp (\wp x)$. Assume that $2 < c$. Then $\operatorname{cardinalGenerate}$ applied to $g$ and $\mathrm{hc}$ is a filter of $x$ defined as the filter of $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{CardinalGenerateSets}$ applied to $g$ and $s$.
Filter.ofCardinalInterdefMathlib.Order.Filter.CardinalInter, function or constantWording
the filter of l (from the name)
English
Let $l$ be an element of $\wp (\wp x)$. Assume that $2 < c$. Assume that for all elements $S$ of $\wp (\wp x)$, if $\operatorname{mk}$ applied to the set of elements of $S$ is less than $c$, then if $S \leq l$, then the intersection of $S$ is an element of $l$. Assume that for all elements $s$ and $t$ of $\wp x$, if $\MembershipmemMACRoT {l}{s}$, then if $s \leq t$, then $\MembershipmemMACRoT {l}{t}$. Then the filter of $l$ is a filter of $x$.
Filter.ofCardinalUniondefMathlib.Order.Filter.CardinalInter, function or constantWording
the filter of l (from the name)
English
Let $l$ be an element of $\wp (\wp x)$. Assume that $2 < c$. Assume that for all elements $S$ of $\wp (\wp x)$, if $\operatorname{mk}$ applied to the set of elements of $S$ is less than $c$, then if for all elements $s_{1}$ of $\wp x$, if $\MembershipmemMACRoT {S}{s_{1}}$, then $\MembershipmemMACRoT {l}{s_{1}}$, then the union of $S$ is an element of $l$. Assume that for all elements $t$ of $\wp x$, if $\MembershipmemMACRoT {l}{t}$, then for all elements $s$ of $\wp x$, if $s \leq t$, then $\MembershipmemMACRoT {l}{s}$. Then the filter of $l$ is a filter of $x$.
Filter.cocardinaldefMathlib.Order.Filter.Cocardinal, function or constantEnglish
Let $x$ be a set. Assume that $c$ is regular. Then $\operatorname{cocardinal}$ applied to $x$ and $\mathrm{hreg}$ is a filter of $x$.
Filter.cocountabledefMathlib.Order.Filter.Cocardinal, function or constantEnglish
$\operatorname{cocountable}$ is a filter of $x$ defined as $\operatorname{cocardinal}$ applied to $x$ and $\mathrm{Cardinal\_\_isRegular\_aleph\_one}$.
Filter.cofinitedefMathlib.Order.Filter.Cofinite, function or constantWording
the cofinite filter (from the docstring)
English
The cofinite filter is a filter of $x$ defined as $\operatorname{comk}$ applied to the proposition that $\operatorname{Finite}$, $\mathrm{Set\_\_finite\_empty}$, the function that maps $\mathrm{\_t}$, $\mathrm{ht}$, $\mathrm{\_s}$ and $\mathrm{hsub}$ to $\operatorname{subset}$ applied to $\mathrm{ht}$ and $\mathrm{hsub}$ and the function that maps $x_{1}$, $h$ and $x_{2}$ to $\operatorname{union}$ applied to $h$.
CountableInterFilterclassMathlib.Order.Filter.CountableInter, predicateWording
l is a countable intersection filter (from the name)
English
Let $l$ be a filter of $x$. Then we can say that $l$ is a countable intersection filter.
Filter.CountableGenerateSetsinductiveMathlib.Order.Filter.CountableInter, predicateEnglish
Let $g$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{CountableGenerateSets}$ holds for $g$ and $x_{1}$.
Filter.CountableGenerateSets.belowinductiveMathlib.Order.Filter.CountableInter, predicateEnglish
Assume that $\operatorname{CountableGenerateSets}$ holds for $g$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
Filter.countableGeneratedefMathlib.Order.Filter.CountableInter, function or constantEnglish
Let $g$ be an element of $\wp (\wp x)$. Then $\operatorname{countableGenerate}$ applied to $g$ is a filter of $x$ defined as the filter of $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{CountableGenerateSets}$ applied to $g$ and $s$.
Filter.ofCountableInterdefMathlib.Order.Filter.CountableInter, function or constantWording
the filter of l (from the name)
English
Let $l$ be an element of $\wp (\wp x)$ such that for all elements $S$ of $\wp (\wp x)$, if $S$ is countable, then if $S \leq l$, then the intersection of $S$ is an element of $l$ and for all elements $s$ of $\wp x$, for all elements $t$ of $\wp x$, if $\MembershipmemMACRoT {l}{s}$, then if $s \leq t$, then $\MembershipmemMACRoT {l}{t}$. Then the filter of $l$ is a filter of $x$.
Filter.ofCountableUniondefMathlib.Order.Filter.CountableInter, function or constantWording
the filter of l (from the name)
English
Let $l$ be an element of $\wp (\wp x)$ such that for all elements $S$ of $\wp (\wp x)$, if $S$ is countable, then if for all elements $s_{1}$ of $\wp x$, if $\MembershipmemMACRoT {S}{s_{1}}$, then $\MembershipmemMACRoT {l}{s_{1}}$, then the union of $S$ is an element of $l$ and for all elements $t$ of $\wp x$, if $\MembershipmemMACRoT {l}{t}$, then for all elements $s$ of $\wp x$, if $s \leq t$, then $\MembershipmemMACRoT {l}{s}$. Then the filter of $l$ is a filter of $x$.
HasCountableSeparatingOnclassMathlib.Order.Filter.CountableSeparatingOn, predicateEnglish
Let $x$ be a set. Let $p$ be a function from elements of $\wp x$ to propositions. Let $t$ be an element of $\wp x$. Then we can say that $\mathrm{HasCountableSeparatingOn}$ holds for $x$, $p$ and $t$.
Filter.CountableFilterBasisstructureMathlib.Order.Filter.CountablyGenerated, typeWording
countable filter basis of x (from the name)
English
Let $x$ be a set. Then the countable filter bases of $x$ are a basic type.
Filter.HasCountableBasisstructureMathlib.Order.Filter.CountablyGenerated, predicateEnglish
Let $l$ be a filter of $x$. Let $p$ be a function from elements of $x_{1}$ to propositions. Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{HasCountableBasis}$ holds for $l$, $p$ and $s$.
Filter.IsCountableBasisstructureMathlib.Order.Filter.CountablyGenerated, predicateEnglish
Let $p$ be a function from elements of $x_{1}$ to propositions. Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{IsCountableBasis}$ holds for $p$ and $s$.
Filter.IsCountablyGeneratedclassMathlib.Order.Filter.CountablyGenerated, predicateEnglish
Let $f$ be a filter of $x$. Then we can say that $\operatorname{IsCountablyGenerated}$ holds for $f$.
FilterstructureMathlib.Order.Filter.Defs, typeWording
filter of x (from the name)
English
Let $x$ be a set. Then the filters of $x$ are a basic type.
Filter.EventuallydefMathlib.Order.Filter.Defs, predicateEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $f$ be a filter of $x$. Then $\operatorname{Eventually}$ holds for $p$ and $f$, if $\MembershipmemMACRoT {f}{\operatorname{ofPred} (\lambda x_{1} . p (x_{1}))}$.
Filter.EventuallyEqdefMathlib.Order.Filter.Defs, predicateEnglish
Let $l$ be a filter of $x$. Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Then $\operatorname{EventuallyEq}$ holds for $l$, $f$ and $g$, if $\operatorname{Eventually}$ holds for the function that maps $x_{2}$ to $\EqtMACRoH {f (x_{2})}{g (x_{2})}$ and $l$.
Filter.EventuallyEqSetdefMathlib.Order.Filter.Defs, predicateEnglish
Let $l$ be a filter of $x$. Let $s$ and $t$ be elements of $\wp x$. Then $\operatorname{EventuallyEqSet}$ holds for $l$, $s$ and $t$, if $\operatorname{EventuallyEq}$ holds for $l$, the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {t}{x_{2}}$.
Filter.EventuallyLEdefMathlib.Order.Filter.Defs, predicateEnglish
Let $l$ be a filter of $x$. Let $f$ and $g$ be functions from elements of $x$ to elements of $x_{1}$. Then $\operatorname{EventuallyLE}$ holds for $l$, $f$ and $g$, if $\operatorname{Eventually}$ holds for the function that maps $x_{3}$ to $\mathrm{Leq} (f (x_{3}), g (x_{3}))$ and $l$.
Filter.EventuallySubsetdefMathlib.Order.Filter.Defs, predicateEnglish
Let $l$ be a filter of $x$. Let $s$ and $t$ be elements of $\wp x$. Then $\operatorname{EventuallySubset}$ holds for $l$, $s$ and $t$, if $\operatorname{EventuallyLE}$ holds for $l$, the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {t}{x_{2}}$.
Filter.FrequentlydefMathlib.Order.Filter.Defs, predicateEnglish
Let $p$ be a function from elements of $x$ to propositions. Let $f$ be a filter of $x$. Then $\operatorname{Frequently}$ holds for $p$ and $f$, if it is not the case that $\operatorname{Eventually}$ holds for the function that maps $x_{1}$ to the proposition that it is not the case that $p$ holds for $x_{1}$ and $f$.
Filter.IsBoundeddefMathlib.Order.Filter.Defs, predicateWording
f is bounded with respect to r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a filter of $x$. Then $f$ is bounded with respect to $r$, if there exists an element $b$ of $x$, such that $\operatorname{Eventually}$ holds for the function that maps $x_{1}$ to $r$ applied to $x_{1}$ and $b$ and $f$.
Filter.IsBoundedUnderdefMathlib.Order.Filter.Defs, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a filter of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then $\operatorname{IsBoundedUnder}$ holds for $r$, $f$ and $u$, if the forward map of $u$ and $f$ is bounded with respect to $r$.
Filter.IsCoboundeddefMathlib.Order.Filter.Defs, predicateWording
r is cobounded with respect to f (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a filter of $x$. Then $r$ is cobounded with respect to $f$, if there exists an element $b$ of $x$, such that for all elements $a$ of $x$, if $\operatorname{Eventually}$ holds for the function that maps $x_{1}$ to $r$ applied to $x_{1}$ and $a$ and $f$, then $r$ holds for $b$ and $a$.
Filter.IsCoboundedUnderdefMathlib.Order.Filter.Defs, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a filter of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then $\operatorname{IsCoboundedUnder}$ holds for $r$, $f$ and $u$, if $r$ is cobounded with respect to the forward map of $u$ and $f$.
Filter.NeBotclassMathlib.Order.Filter.Defs, predicateEnglish
Let $f$ be a filter of $x$. Then we can say that $\operatorname{NeBot}$ holds for $f$.
Filter.TendstodefMathlib.Order.Filter.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a filter of $x$. Let $x_{3}$ be a filter of $x_{1}$. Then $\operatorname{Tendsto}$ holds for $f$, $x_{2}$ and $x_{3}$, if the forward map of $f$ and $x_{2}$ is less than or equal to $x_{3}$.
Filter.binddefMathlib.Order.Filter.Defs, function or constantEnglish
Let $f$ be a filter of $x$. Let $m$ be a function from elements of $x$ to filters of $x_{1}$. Then $\operatorname{bind}$ applied to $f$ and $m$ is a filter of $x_{1}$ defined as the join of the forward map of $m$ and $f$.
Filter.comapdefMathlib.Order.Filter.Defs, function or constantWording
the preimage of m and f (from the name)
English
Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be a filter of $x_{1}$. Then the preimage of $m$ and $f$ is a filter of $x$.
Filter.comkdefMathlib.Order.Filter.Defs, function or constantEnglish
Let $p$ be a function from elements of $\wp x$ to propositions such that $p$ holds for $\operatorname{emptyCollection}$, for all elements $t_{1}$ of $\wp x$, if $p$ holds for $t_{1}$, then for all elements $s_{1}$ of $\wp x$, if $s_{1} \leq t_{1}$, then $p$ holds for $s_{1}$ and for all elements $s$ of $\wp x$, if $p$ holds for $s$, then for all elements $t$ of $\wp x$, if $p$ holds for $t$, then $p$ holds for $\UnionunionMACRoAB {s}{t}$. Then $\operatorname{comk}$ applied to $p$, $\mathrm{he}$, $\mathrm{hmono}$ and $\mathrm{hunion}$ is a filter of $x$.
Filter.coproddefMathlib.Order.Filter.Defs, function or constantWording
the coproduct of f and g (from the name)
English
Let $f$ be a filter of $x$. Let $g$ be a filter of $x_{1}$. Then the coproduct of $f$ and $g$ is a filter of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as the maximum of the preimage of $\ProdfstMACRoZ$ and $f$ and the preimage of $\ProdsndMACRoAA$ and $g$.
Filter.copydefMathlib.Order.Filter.Defs, function or constantWording
the copy of f and S (from the name)
English
Let $f$ be a filter of $x$. Let $S$ be an element of $\wp (\wp x)$ such that for all elements $s$ of $\wp x$, $s$ is an element of $S$, if and only if $s$ is an element of $f$. Then the copy of $f$ and $S$ is a filter of $x$.
Filter.currydefMathlib.Order.Filter.Defs, function or constantWording
the curry of f and g (from the name)
English
Let $f$ be a filter of $x$. Let $g$ be a filter of $x_{1}$. Then the curry of $f$ and $g$ is a filter of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{bind}$ applied to $f$ and the function that maps $a$ to the forward map of the function that maps $x_{2}$ to $\ProdmkMACRoU {a}{x_{2}}$ and $g$.
Filter.elabEventuallyEqdefMathlib.Order.Filter.Defs, function or constantEnglish
$\operatorname{TermElab}$.
Filter.elabEventuallyLEdefMathlib.Order.Filter.Defs, function or constantEnglish
$\operatorname{TermElab}$.
Filter.elabEventuallyRelSidesdefMathlib.Order.Filter.Defs, function or constantEnglish
Let $x$ and $y$ be elements of $\operatorname{Term}$. Then $\operatorname{TermElabM}$ holds for $\mathrm{Prod}$ applied to $\operatorname{Term}$ and $\mathrm{Prod}$ applied to $\operatorname{Term}$ and $\mathrm{Bool}$.
Filter.eventuallyEqStxdefMathlib.Order.Filter.Defs, function or constantEnglish
generation took over the time limit
Filter.eventuallyLEStxdefMathlib.Order.Filter.Defs, function or constantEnglish
generation took over the time limit
Filter.joindefMathlib.Order.Filter.Defs, function or constantWording
the join of f (from the docstring)
English
Let $f$ be a filter of the set of filters of $x$. Then the join of $f$ is a filter of $x$.
Filter.kerdefMathlib.Order.Filter.Defs, function or constantWording
the kernel of f (from the name)
English
Let $f$ be a filter of $x$. Then the kernel of $f$ is an element of $\wp x$ defined as the intersection of the set of $f$.
Filter.liftdefMathlib.Order.Filter.Defs, function or constantWording
the lift of f and g (from the name)
English
Let $f$ be a filter of $x$. Let $g$ be a function from elements of $\wp x$ to filters of $x_{1}$. Then the lift of $f$ and $g$ is a filter of $x_{1}$ defined as the infimum of the function that maps $s$ to the infimum of the function that maps $h$ to $g$ applied to $s$.
Filter.lift'defMathlib.Order.Filter.Defs, function or constantWording
the lift of f and h (from the name)
English
Let $f$ be a filter of $x$. Let $h$ be a function from elements of $\wp x$ to elements of $\wp x_{1}$. Then the lift of $f$ and $h$ is a filter of $x_{1}$ defined as the lift of $f$ and $\operatorname{comp}$ applied to $\operatorname{principal}$ and $h$.
Filter.mapdefMathlib.Order.Filter.Defs, function or constantWording
the forward map of m and f (from the docstring)
English
Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be a filter of $x$. Then the forward map of $m$ and $f$ is a filter of $x_{1}$.
Filter.pidefMathlib.Order.Filter.Defs, function or constantWording
the product of f (from the docstring)
English
Let $f$ be a function from elements $i_{1}$ of $x$ to filters of $x_{1}$ applied to $i_{1}$. Then the product of $i_{1}$ is a filter of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ defined as the function that maps $f$ to the infimum of the function that maps $i$ to the preimage of $\operatorname{eval}$ applied to $i$ and $i_{1}$ applied to $i$.
Filter.precheckEventuallyEqdefMathlib.Order.Filter.Defs, function or constantEnglish
generation took over the time limit
Filter.precheckEventuallyLEdefMathlib.Order.Filter.Defs, function or constantEnglish
generation took over the time limit
Filter.principaldefMathlib.Order.Filter.Defs, function or constantWording
the principal filter of s (from the docstring)
English
Let $s$ be an element of $\wp x$. Then the principal filter of $s$ is a filter of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ofPred}$ applied to the function that maps $t$ to $\mathrm{Leq} (s , t)$, $\mathrm{Set\_\_subset\_univ}$ applied to $s$, the function that maps $x_{1}$, $x_{2}$ and $\mathrm{hx}$ to $\operatorname{trans}$ applied to $\mathrm{hx}$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Set\_\_subset\_inter}$.
Filter.sInfdefMathlib.Order.Filter.Defs, function or constantWording
the infimum of s (from the name)
English
Let $s$ be an element of the power set of the set of filters of $x$. Then the infimum of $s$ is a filter of $x$ defined as the supremum of the lower bound of $s$.
Filter.seqdefMathlib.Order.Filter.Defs, function or constantWording
the sequence of f and g (from the name)
English
Let $f$ be a filter of the set of functions from elements of $x$ to elements of $x_{1}$. Let $g$ be a filter of $x$. Then the sequence of $f$ and $g$ is a filter of $x_{1}$.
Filter.setsdefMathlib.Order.Filter.Defs, function or constantWording
the set of self (from the name)
English
Let $\mathrm{self}$ be a filter of $x$. Then the set of $\mathrm{self}$ is an element of $\wp (\wp x)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Filter.EventuallyConstdefMathlib.Order.Filter.EventuallyConst, predicateWording
f is eventually constant with respect to l (from the name)
English
generation took over the time limit
Filter.EventuallyEmptyOrUnivdefMathlib.Order.Filter.EventuallyConst, predicateWording
s is a eventually empty or universal set with respect to l (from the name)
English
generation took over the time limit
IsExtrFilterdefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a filter of $x$. Let $a$ be an element of $x$. Then $\mathrm{IsExtrFilter}$ holds for $f$, $l$ and $a$, if $\mathrm{IsMinFilter}$ holds for $f$, $l$ and $a$ or $\mathrm{IsMaxFilter}$ holds for $f$, $l$ and $a$.
IsExtrOndefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsExtrOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsExtrFilter}$ holds for $f$, the principal filter of $s$ and $a$.
IsMaxFilterdefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a filter of $x$. Let $a$ be an element of $x$. Then $\mathrm{IsMaxFilter}$ holds for $f$, $l$ and $a$, if $\operatorname{Eventually}$ holds for the function that maps $x_{3}$ to $\mathrm{Leq} (f (x_{3}), f (a))$ and $l$.
IsMaxOndefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsMaxOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsMaxFilter}$ holds for $f$, the principal filter of $s$ and $a$.
IsMinFilterdefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a filter of $x$. Let $a$ be an element of $x$. Then $\mathrm{IsMinFilter}$ holds for $f$, $l$ and $a$, if $\operatorname{Eventually}$ holds for the function that maps $x_{3}$ to $\mathrm{Leq} (f (a), f (x_{3}))$ and $l$.
IsMinOndefMathlib.Order.Filter.Extr, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsMinOn}$ holds for $f$, $s$ and $a$, if $\mathrm{IsMinFilter}$ holds for $f$, the principal filter of $s$ and $a$.
Filter.GermdefMathlib.Order.Filter.Germ.Basic, typeWording
germ of l and x1 (from the name)
English
Let $l$ be a filter of $x$. Let $x_{1}$ be a set. Then a germ of $l$ and $x_{1}$ is an element of the function that maps $l$ and $x_{1}$ to $\mathrm{Quotient}$ applied to $\operatorname{germSetoid}$ applied to $l$ and $x_{1}$.
Filter.Germ.IsConstantdefMathlib.Order.Filter.Germ.Basic, predicateWording
P is constant (from the name)
English
Let $P$ be a germ of $l$ and $x_{1}$. Then we can say that $P$ is constant.
Filter.Germ.LiftPreddefMathlib.Order.Filter.Germ.Basic, predicateEnglish
Let $p$ be a function from elements of $x_{1}$ to propositions. Let $f$ be a germ of $l$ and $x_{1}$. Then we can say that $\operatorname{LiftPred}$ holds for $p$ and $f$.
Filter.Germ.LiftReldefMathlib.Order.Filter.Germ.Basic, predicateEnglish
Let $r$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to propositions. Let $f$ be a germ of $l$ and $x_{1}$. Let $g$ be a germ of $l$ and $x_{2}$. Then we can say that $\operatorname{LiftRel}$ holds for $r$, $f$ and $g$.
Filter.Germ.TendstodefMathlib.Order.Filter.Germ.Basic, predicateEnglish
Let $f$ be a germ of $l$ and $x_{1}$. Let $\mathrm{lb}$ be a filter of $x_{1}$. Then we can say that $\operatorname{Tendsto}$ holds for $f$ and $\mathrm{lb}$.
Filter.Germ.coeAddHomdefMathlib.Order.Filter.Germ.Basic, function or constantWording
the coercion additive homomorphism of l (from the name)
English
Let $l$ be a filter of $x$. Then the coercion additive homomorphism of $l$ is an additive monoid homomorphism of the set of functions from elements of $x$ to elements of $M$ and the set of germs of $l$ and $M$.
Filter.Germ.coeMulHomdefMathlib.Order.Filter.Germ.Basic, function or constantWording
the coercion multiplicative homomorphism of l (from the name)
English
Let $l$ be a filter of $x$. Then the coercion multiplicative homomorphism of $l$ is a monoid homomorphism of the set of functions from elements of $x$ to elements of $M$ and the set of germs of $l$ and $M$.
Filter.Germ.coeRingHomdefMathlib.Order.Filter.Germ.Basic, function or constantWording
the coercion ring homomorphism of l (from the name)
English
Let $l$ be a filter of $x$. Then the coercion ring homomorphism of $l$ is a ring homomorphism of the set of functions from elements of $x$ to elements of $R$ and the set of germs of $l$ and $R$.
Filter.Germ.compTendstodefMathlib.Order.Filter.Germ.Basic, function or constantWording
the composition limit of f and g (from the name)
English
Let $f$ be a germ of $l$ and $x_{1}$. Let $g$ be a function from elements of $x_{2}$ to elements of $x$ such that $\operatorname{Tendsto}$ holds for $g$, $\mathrm{lc}$ and $l$. Then the composition limit of $f$ and $g$ is a germ of $\mathrm{lc}$ and $x_{1}$ defined as the composition limit of $f$ and the germ corresponding to a global function of $g$.
Filter.Germ.compTendsto'defMathlib.Order.Filter.Germ.Basic, function or constantWording
the composition limit of f and g (from the name)
English
Let $f$ be a germ of $l$ and $x_{1}$. Let $g$ be a germ of $\mathrm{lc}$ and $x$ such that $\operatorname{Tendsto}$ holds for $g$ and $l$. Then the composition limit of $f$ and $g$ is a germ of $\mathrm{lc}$ and $x_{1}$.
Filter.Germ.constdefMathlib.Order.Filter.Germ.Basic, function or constantWording
the constant of b (from the name)
English
Let $b$ be an element of $x_{1}$. Then the constant of $b$ is a germ of $l$ and $x_{1}$ defined as the germ corresponding to a global function of the function that maps $x_{2}$ to $b$.
Filter.Germ.liftOndefMathlib.Order.Filter.Germ.Basic, function or constantEnglish
Let $f$ be a germ of $l$ and $x_{1}$. Let $F$ be a function from functions from elements of $x$ to elements of $x_{1}$ to elements of $x_{2}$ such that $\operatorname{LiftFun}$ holds for $\operatorname{EventuallyEq}$ applied to $l$, the function that maps $x_{3}$ and $x_{4}$ to $\EqtMACRoH {x_{3}}{x_{4}}$, $F$ and $F$. Then $\operatorname{liftOn}$ applied to $f$, $F$ and $\mathrm{hF}$ is an element of $x_{2}$ defined as $\operatorname{liftOn'}$ applied to $f$, $F$ and $\mathrm{hF}$.
Filter.Germ.mapdefMathlib.Order.Filter.Germ.Basic, function or constantWording
the map of op and x3 (from the name)
English
Let $\mathrm{op}$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a germ of $l$ and $x_{1}$. Then the map of $\mathrm{op}$ and $x_{3}$ is a germ of $l$ and $x_{2}$.
Filter.Germ.map'defMathlib.Order.Filter.Germ.Basic, function or constantWording
the map of F and x4 (from the name)
English
Let $F$ be a function from functions from elements of $x$ to elements of $x_{1}$ and elements of $x_{2}$ to elements of $x_{3}$ such that $\operatorname{LiftFun}$ holds for $\operatorname{EventuallyEq}$ applied to $l$, $\operatorname{EventuallyEq}$ applied to $\mathrm{lc}$, $F$ and $F$. Let $x_{4}$ be a germ of $l$ and $x_{1}$. Then the map of $F$ and $x_{4}$ is a germ of $\mathrm{lc}$ and $x_{3}$ defined as the map of $F$ and $x_{4}$.
Filter.Germ.map₂defMathlib.Order.Filter.Germ.Basic, function or constantWording
the map of x4 and x5 (from the name)
English
Let $\mathrm{op}$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to elements of $x_{3}$. Let $x_{4}$ be a germ of $l$ and $x_{1}$. Let $x_{5}$ be a germ of $l$ and $x_{2}$. Then the map of $x_{4}$ and $x_{5}$ is a germ of $l$ and $x_{3}$.
Filter.Germ.ofFundefMathlib.Order.Filter.Germ.Basic, function or constantWording
the germ corresponding to a global function of x2 (from the docstring)
English
Let $x_{2}$ be a function from elements of $x$ to elements of $x_{1}$. Then the germ corresponding to a global function of $x_{2}$ is a germ of $l$ and $x_{1}$ defined as $\operatorname{mk'}$ applied to $x_{2}$.
Filter.ProductdefMathlib.Order.Filter.Germ.Basic, typeWording
product of l and x1 (from the name)
English
Let $l$ be a filter of $x$. Let $x_{1}$ be a function from elements of $x$ to sets. Then a product of $l$ and $x_{1}$ is an element of the function that maps $l$ and $x_{1}$ to $\mathrm{Quotient}$ applied to $\operatorname{productSetoid}$ applied to $l$ and $x_{1}$.
Filter.TendstoIxxClassclassMathlib.Order.Filter.Interval, predicateEnglish
Let $\mathrm{Ixx}$ be a function from elements of $x$ and elements of $x$ to elements of $\wp x$. Let $x_{1}$ be a filter of $x$. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of filters of $x$. Then we can say that $\operatorname{TendstoIxxClass}$ holds for $\mathrm{Ixx}$, $x_{1}$ and $x_{2}$.
Filter.tacticIsBoundedDefaultdefMathlib.Order.Filter.IsBounded, function or constantEnglish
generation took over the time limit
Filter.giPrincipalKerdefMathlib.Order.Filter.Ker, function or constantEnglish
$\operatorname{giPrincipalKer}$ is a Galois coinsertion of $\operatorname{principal}$ and $\operatorname{ker}$.
Filter.kernMapdefMathlib.Order.Filter.Map, function or constantEnglish
Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be a filter of $x$. Then $\operatorname{kernMap}$ applied to $m$ and $f$ is a filter of $x_{1}$.
Filter.map₂defMathlib.Order.Filter.NAry, function or constantWording
the map of f and g (from the name)
English
Let $m$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $f$ be a filter of $x$. Let $g$ be a filter of $x_{1}$. Then the map of $f$ and $g$ is a filter of $x_{2}$.
Filter.PTendstodefMathlib.Order.Filter.Partial, predicateEnglish
Let $f$ be a function of $x$ and $x_{1}$. Let $x_{2}$ be a filter of $x$. Let $x_{3}$ be a filter of $x_{1}$. Then $\operatorname{PTendsto}$ holds for $f$, $x_{2}$ and $x_{3}$, if $\operatorname{pmap} (f , x_{2})\leq x_{3}$.
Filter.PTendsto'defMathlib.Order.Filter.Partial, predicateEnglish
Let $f$ be a function of $x$ and $x_{1}$. Let $x_{2}$ be a filter of $x$. Let $x_{3}$ be a filter of $x_{1}$. Then $\operatorname{PTendsto'}$ holds for $f$, $x_{2}$ and $x_{3}$, if $x_{2}$ is less than or equal to $\operatorname{rcomap'}$ applied to the graph of $f$ and $x_{3}$.
Filter.RTendstodefMathlib.Order.Filter.Partial, predicateEnglish
Let $r$ be a set relation of $x$ and $x_{1}$. Let $x_{2}$ be a filter of $x$. Let $x_{3}$ be a filter of $x_{1}$. Then $\operatorname{RTendsto}$ holds for $r$, $x_{2}$ and $x_{3}$, if $\operatorname{rmap} (r , x_{2})\leq x_{3}$.
Filter.RTendsto'defMathlib.Order.Filter.Partial, predicateEnglish
Let $r$ be a set relation of $x$ and $x_{1}$. Let $x_{2}$ be a filter of $x$. Let $x_{3}$ be a filter of $x_{1}$. Then $\operatorname{RTendsto'}$ holds for $r$, $x_{2}$ and $x_{3}$, if $x_{2} \leq \operatorname{rcomap'} (r , x_{3})$.
Filter.pcomap'defMathlib.Order.Filter.Partial, function or constantEnglish
Let $f$ be a function of $x$ and $x_{1}$. Let $l$ be a filter of $x_{1}$. Then $\operatorname{pcomap'}$ applied to $f$ and $l$ is a filter of $x$ defined as $\operatorname{rcomap'}$ applied to the graph of $f$ and $l$.
Filter.pmapdefMathlib.Order.Filter.Partial, function or constantEnglish
Let $f$ be a function of $x$ and $x_{1}$. Let $l$ be a filter of $x$. Then $\operatorname{pmap}$ applied to $f$ and $l$ is a filter of $x_{1}$ defined as $\operatorname{rmap}$ applied to the graph of $f$ and $l$.
Filter.rcomapdefMathlib.Order.Filter.Partial, function or constantEnglish
Let $r$ be a set relation of $x$ and $x_{1}$. Let $f$ be a filter of $x_{1}$. Then $\operatorname{rcomap}$ applied to $r$ and $f$ is a filter of $x$.
Filter.rcomap'defMathlib.Order.Filter.Partial, function or constantEnglish
Let $r$ be a set relation of $x$ and $x_{1}$. Let $f$ be a filter of $x_{1}$. Then $\operatorname{rcomap'}$ applied to $r$ and $f$ is a filter of $x$.
Filter.rmapdefMathlib.Order.Filter.Partial, function or constantEnglish
Let $r$ be a set relation of $x$ and $x_{1}$. Let $l$ be a filter of $x$. Then $\operatorname{rmap}$ applied to $r$ and $l$ is a filter of $x_{1}$.
Filter.coprodᵢdefMathlib.Order.Filter.Pi, function or constantWording
the coproduct of f (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $x$ to filters of $x_{1}$ applied to $i_{1}$. Then the coproduct of $i_{1}$ is a filter of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ defined as the function that maps $f$ to the supremum of the function that maps $i$ to the preimage of $\operatorname{eval}$ applied to $i$ and $i_{1}$ applied to $i$.
Filter.mapAddMonoidHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the map additive monoid homomorphism of x5 (from the name)
English
Let $x_{5}$ be an element of $F$. Then the map additive monoid homomorphism of $x_{5}$ is an additive monoid homomorphism of the set of filters of $x$ and the set of filters of $x_{1}$.
Filter.mapMonoidHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the map monoid homomorphism of x5 (from the name)
English
Let $x_{5}$ be an element of $F$. Then the map monoid homomorphism of $x_{5}$ is a monoid homomorphism of the set of filters of $x$ and the set of filters of $x_{1}$.
Filter.pureAddHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure additive homomorphism (from the name)
English
The pure additive homomorphism is an additive homomorphism of $x$ and the set of filters of $x$.
Filter.pureAddMonoidHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure additive monoid homomorphism (from the name)
English
The pure additive monoid homomorphism is an additive monoid homomorphism of $x$ and the set of filters of $x$.
Filter.pureMonoidHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure monoid homomorphism (from the name)
English
The pure monoid homomorphism is a monoid homomorphism of $x$ and the set of filters of $x$.
Filter.pureMulHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure multiplicative homomorphism (from the name)
English
The pure multiplicative homomorphism is a multiplicative homomorphism of $x$ and the set of filters of $x$.
Filter.pureOneHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure one homomorphism (from the name)
English
The pure one homomorphism is an one homomorphism of $x$ and the set of filters of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{pure}$ and $\mathrm{Filter\_\_pure\_one}$.
Filter.pureZeroHomdefMathlib.Order.Filter.Pointwise, function or constantWording
the pure zero homomorphism (from the name)
English
The pure zero homomorphism is a zero homomorphism of $x$ and the set of filters of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{pure}$ and $\mathrm{Filter\_\_pure\_zero}$.
Filter.smallSetsdefMathlib.Order.Filter.SmallSets, function or constantWording
the small set of l (from the name)
English
Let $l$ be a filter of $x$. Then the small set of $l$ is a filter of $\wp x$ defined as the lift of $l$ and $\operatorname{powerset}$.
Filter.SubsingletondefMathlib.Order.Filter.Subsingleton, predicateWording
l is a subsingleton (from the name)
English
Let $l$ be a filter of $x$. Then $l$ is a subsingleton, if there exists an element $s$ of $\wp x$, such that $s$ is an element of $l$ and $s$ is a subsingleton.
Filter.TendstoCofiniteclassMathlib.Order.Filter.TendstoCofinite, predicateWording
f is a limit cofinite (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $f$ is a limit cofinite.
Filter.TendstoCofinite.mapDomaindefMathlib.Order.Filter.TendstoCofinite, function or constantWording
the map domain of v and x3 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $v$ be a function from elements of $x$ to elements of $M$. Let $x_{3}$ be an element of $x_{1}$. Then the map domain of $v$ and $x_{3}$ is an element of $M$ defined as $\FinsetSum {\operatorname{toFinset} (\mathrm{Filter\_\_TendstoCofinite\_\_finite\_preimage\_singleton} (f , x_{3}))}{x_{4}}{v (x_{4})}$.
Filter.hyperfilterdefMathlib.Order.Filter.Ultrafilter.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{hyperfilter}$ applied to $x$ is a ultrafilter of $x$ defined as $\operatorname{of}$ applied to the cofinite filter.
UltrafilterstructureMathlib.Order.Filter.Ultrafilter.Defs, typeWording
ultrafilter of x (from the name)
English
Let $x$ be a set. Then the ultrafilters of $x$ are a basic type.
Ultrafilter.binddefMathlib.Order.Filter.Ultrafilter.Defs, function or constantEnglish
Let $f$ be a ultrafilter of $x$. Let $m$ be a function from elements of $x$ to ultrafilters of $x_{1}$. Then $\operatorname{bind}$ applied to $f$ and $m$ is a ultrafilter of $x_{1}$.
Ultrafilter.comapdefMathlib.Order.Filter.Ultrafilter.Defs, function or constantWording
the preimage of u (from the name)
English
Let $u$ be a ultrafilter of $x_{1}$. Assume that $m$ is injective. Assume that the range of $m$ is an element of $u$. Then the preimage of $u$ is a ultrafilter of $x$.
Ultrafilter.mapdefMathlib.Order.Filter.Ultrafilter.Defs, function or constantWording
the map of m and f (from the name)
English
Let $m$ be a function from elements of $x$ to elements of $x_{1}$. Let $f$ be a ultrafilter of $x$. Then the map of $m$ and $f$ is a ultrafilter of $x_{1}$.
Ultrafilter.ofdefMathlib.Order.Filter.Ultrafilter.Defs, function or constantEnglish
Let $f$ be a filter of $x$. Then $\operatorname{of}$ applied to $f$ is a ultrafilter of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{Ultrafilter\_\_exists\_le}$ applied to $f$.
Ultrafilter.ofAtomdefMathlib.Order.Filter.Ultrafilter.Defs, function or constantWording
the ultrafilter of f and hf (from the name)
English
Let $f$ be a filter of $x$ such that $f$ is an atom. Then the ultrafilter of $f$ and $\mathrm{hf}$ is a ultrafilter of $x$.
Ultrafilter.ofComapInfPrincipaldefMathlib.Order.Filter.Ultrafilter.Defs, function or constantWording
the ultrafilter of h (from the name)
English
Assume that the image of $m$ and $s$ is an element of $g$. Then the ultrafilter of $h$ is a ultrafilter of $x$ defined as $\operatorname{of}$ applied to the minimum of the preimage of $m$ and $\operatorname{toFilter}$ applied to $g$ and the principal filter of $s$.
Ultrafilter.ofComplNotMemIffdefMathlib.Order.Filter.Ultrafilter.Defs, function or constantWording
the ultrafilter of f and h (from the name)
English
Let $f$ be a filter of $x$ such that for all elements $s$ of $\wp x$, the complement of $s$ is not an element of $f$, if and only if $s$ is an element of $f$. Then the ultrafilter of $f$ and $h$ is a ultrafilter of $x$.
Filter.BoundedAtFilterdefMathlib.Order.Filter.ZeroAndBoundedAtFilter, predicateEnglish
Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{BoundedAtFilter}$ holds for $l$ and $f$, if $\operatorname{IsBigO}$ holds for $l$, $f$ and $1$.
Filter.ZeroAtFilterdefMathlib.Order.Filter.ZeroAndBoundedAtFilter, predicateWording
f is a zero at filter with respect to l (from the name)
English
Let $l$ be a filter of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is a zero at filter with respect to $l$, if $\operatorname{Tendsto}$ holds for $f$, $l$ and the neighbourhood filter of $0$.
Filter.boundedFilterSubalgebradefMathlib.Order.Filter.ZeroAndBoundedAtFilter, function or constantWording
the bounded filter subalgebra of x and l (from the name)
English
Let $x$ be a set. Let $l$ be a filter of $x_{1}$. Then the bounded filter subalgebra of $x$ and $l$ is a subalgebra of $x$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$.
Filter.boundedFilterSubmoduledefMathlib.Order.Filter.ZeroAndBoundedAtFilter, function or constantWording
the bounded filter submodule of x and l (from the name)
English
Let $x$ be a set. Let $l$ be a filter of $x_{1}$. Then the bounded filter submodule of $x$ and $l$ is a submodule of $x$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$.
Filter.zeroAtFilterAddSubmonoiddefMathlib.Order.Filter.ZeroAndBoundedAtFilter, function or constantWording
the additive submonoid of l (from the docstring)
English
Let $l$ be a filter of $x$. Then the additive submonoid of $l$ is an additive submonoid of the set of functions from elements of $x$ to elements of $x_{1}$.
Filter.zeroAtFilterSubmoduledefMathlib.Order.Filter.ZeroAndBoundedAtFilter, function or constantWording
the zero at filter submodule of x and l (from the name)
English
Let $x$ be a set. Let $l$ be a filter of $x_{1}$. Then the zero at filter submodule of $x$ and $l$ is a submodule of $x$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$.
Fin.addNatOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the additive natural order embedding of m (from the name)
English
Let $m$ be a natural number. Then the additive natural order embedding of $m$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + m$ defined as the order embedding of the function that maps $x$ to $\operatorname{addNat}$ applied to $x$ and $m$ and $\mathrm{Fin\_\_strictMono\_addNat}$ applied to $m$.
Fin.castAddOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the cast additive order embedding of m (from the name)
English
Let $m$ be a natural number. Then the cast additive order embedding of $m$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + m$ defined as the order embedding of $\operatorname{castAdd}$ applied to $m$ and $\mathrm{Fin\_\_strictMono\_castAdd}$ applied to $m$.
Fin.castLEOrderEmbdefMathlib.Order.Fin.Basic, function or constantEnglish
Assume that $n \leq m$. Then $\operatorname{castLEOrderEmb}$ applied to $h$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $m$ defined as the order embedding of $\operatorname{castLE}$ applied to $h$ and $\mathrm{Fin\_\_strictMono\_castLE}$ applied to $h$.
Fin.castOrderIsodefMathlib.Order.Fin.Basic, function or constantWording
the cast order isomorphism of eq (from the name)
English
Assume that $n = m$. Then the cast order isomorphism of $\mathrm{eq}$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $m$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{cast}$ applied to $\mathrm{eq}$, $\operatorname{cast}$ applied to $\operatorname{symm}$ applied to $\mathrm{eq}$, $\mathrm{Fin\_\_leftInverse\_cast}$ applied to $\mathrm{eq}$ and $\mathrm{Fin\_\_rightInverse\_cast}$ applied to $\mathrm{eq}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{Fin\_\_cast\_le\_cast}$ applied to $\mathrm{eq}$.
Fin.castSuccOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the cast successor order embedding (from the name)
English
The cast successor order embedding is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the order embedding of $\operatorname{castSucc}$ and $\mathrm{Fin\_\_strictMono\_castSucc}$.
Fin.natAddOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the natural additive order embedding of n (from the name)
English
Let $n$ be a natural number. Then the natural additive order embedding of $n$ is an order embedding of $\mathrm{Fin}$ applied to $m$ and $\mathrm{Fin}$ applied to $n + m$ defined as the order embedding of $\operatorname{natAdd}$ applied to $n$ and $\mathrm{Fin\_\_strictMono\_natAdd}$ applied to $n$.
Fin.orderIsoSubtypedefMathlib.Order.Fin.Basic, function or constantWording
the order isomorphism subtype (from the name)
English
The order isomorphism subtype is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {i}{\mathrm{Lt} (i , n)}$.
Fin.predAboveOrderHomdefMathlib.Order.Fin.Basic, function or constantWording
the predecessor above order homomorphism of p (from the name)
English
Let $p$ be an element of $\mathrm{Fin}$ applied to $n$. Then the predecessor above order homomorphism of $p$ is an order homomorphism of $\mathrm{Fin}$ applied to $n + 1$ and $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{mk}$ applied to $\operatorname{predAbove}$ applied to $p$ and $\mathrm{Fin\_\_predAbove\_right\_monotone}$ applied to $p$.
Fin.revOrderIsodefMathlib.Order.Fin.Basic, function or constantEnglish
$\operatorname{revOrderIso}$ is an order isomorphism of the set of order duals of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n$.
Fin.succAboveOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the successor above order embedding of p (from the name)
English
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the successor above order embedding of $p$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the order embedding of $\operatorname{succAbove}$ applied to $p$ and $\mathrm{Fin\_\_strictMono\_succAbove}$ applied to $p$.
Fin.succOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the successor order embedding of n (from the name)
English
Let $n$ be a natural number. Then the successor order embedding of $n$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\mathrm{Fin}$ applied to $n + 1$ defined as the order embedding of $\operatorname{succ}$ and $\mathrm{Fin\_\_strictMono\_succ}$.
Fin.valOrderEmbdefMathlib.Order.Fin.Basic, function or constantWording
the value order embedding of n (from the name)
English
Let $n$ be a natural number. Then the value order embedding of $n$ is an order embedding of $\mathrm{Fin}$ applied to $n$ and $\Natural$.
Fin.orderIsoPairdefMathlib.Order.Fin.Finset, function or constantWording
the order isomorphism pair of a and b (from the name)
English
Let $a$ and $b$ be elements of $x$ such that $a < b$. Then the order isomorphism pair of $a$ and $b$ is an order isomorphism of $\mathrm{Fin}$ applied to $2$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{insert} (a , \operatorname{singleton} (b))}{x_{3}})}$.
Fin.orderIsoSingletondefMathlib.Order.Fin.Finset, function or constantWording
the order isomorphism singleton of a (from the name)
English
Let $a$ be an element of $x$. Then the order isomorphism singleton of $a$ is an order isomorphism of $\mathrm{Fin}$ applied to $1$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{singleton} (a)}{x_{2}})}$ defined as the order isomorphism of $\mathrm{Fin}$ applied to $1$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{singleton} (a)}{x_{2}})}$.
Fin.orderIsoTripledefMathlib.Order.Fin.Finset, function or constantWording
the order isomorphism triple of b and c (from the name)
English
Let $a$, $b$ and $c$ be elements of $x$ such that $a < b < c$. Then the order isomorphism triple of $b$ and $c$ is an order isomorphism of $\mathrm{Fin}$ applied to $3$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{insert} (a , \operatorname{insert} (b , \operatorname{singleton} (c)))}{x_{3}})}$.
Fin.succAboveOrderIsodefMathlib.Order.Fin.SuccAboveOrderIso, function or constantWording
the successor above order isomorphism of i (from the name)
English
Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 2$. Then the successor above order isomorphism of $i$ is an order isomorphism of $\mathrm{Fin}$ applied to $n + 1$ and $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{compl} (\operatorname{singleton} (i))}{x})}$.
Fin.castLEOrderIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Assume that $n \leq m$. Then $\operatorname{castLEOrderIso}$ applied to $h$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {i}{\mathrm{Lt} (\operatorname{val} (i), n)}$.
Fin.consOrderIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Then $\operatorname{consOrderIso}$ applied to $x$ is an order isomorphism of $\mathrm{Prod}$ applied to $x$ applied to $0$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succ}$ applied to $i$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$.
Fin.insertNthOrderIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{insertNthOrderIso}$ applied to $x$ and $p$ is an order isomorphism of $\mathrm{Prod}$ applied to $x$ applied to $p$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$.
Fin.snocOrderIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Then $\operatorname{snocOrderIso}$ applied to $x$ is an order isomorphism of $\mathrm{Prod}$ applied to $x$ applied to $\operatorname{last}$ applied to $n$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $i_{1}$.
OrderIso.finTwoArrowIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Let $x$ be a set. Then $\operatorname{finTwoArrowIso}$ applied to $x$ is an order isomorphism of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $x$ and $\mathrm{Prod}$ applied to $x$ and $x$.
OrderIso.piFinTwoIsodefMathlib.Order.Fin.Tuple, function or constantEnglish
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwoIso}$ applied to $x$ is an order isomorphism of the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $2$ to elements of $x$ applied to $i$ and $\mathrm{Prod}$ applied to $x$ applied to $0$ and $x$ applied to $1$.
finSuccAboveOrderIsodefMathlib.Order.Fin.Tuple, function or constantWording
the finite successor above order isomorphism of p (from the name)
English
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the finite successor above order isomorphism of $p$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x}{\mathrm{Neq} (x , p)}$.
OrderHom.gfpdefMathlib.Order.FixedPoints, function or constantEnglish
$\operatorname{gfp}$ is an order homomorphism of the set of order homomorphisms of $x$ and $x$ and $x$.
OrderHom.lfpdefMathlib.Order.FixedPoints, function or constantEnglish
$\operatorname{lfp}$ is an order homomorphism of the set of order homomorphisms of $x$ and $x$ and $x$.
OrderHom.nextFixeddefMathlib.Order.FixedPoints, function or constantEnglish
Let $f$ be an order homomorphism of $x$ and $x$. Let $x_{2}$ be an element of $x$ such that $x_{2} \leq f (x_{2})$. Then $\operatorname{nextFixed}$ applied to $f$, $x_{2}$ and $\mathrm{hx}$ is an element of the fixed point of $\operatorname{coe}$ applied to $f$ defined as $\operatorname{lfp}$ applied to $\MaxmaxMACRoAF {\operatorname{const} (x , x_{2})}{f}$.
OrderHom.prevFixeddefMathlib.Order.FixedPoints, function or constantEnglish
Let $f$ be an order homomorphism of $x$ and $x$. Let $x_{2}$ be an element of $x$ such that $f (x_{2})\leq x_{2}$. Then $\operatorname{prevFixed}$ applied to $f$, $x_{2}$ and $\mathrm{hx}$ is an element of the fixed point of $\operatorname{coe}$ applied to $f$ defined as $\operatorname{gfp}$ applied to $\MinminMACRoAG {\operatorname{const} (x , x_{2})}{f}$.
OrderIso.toGaloisCoinsertiondefMathlib.Order.GaloisConnection.Basic, function or constantWording
the Galois coinsertion of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the Galois coinsertion of $e$ is a Galois coinsertion of $\operatorname{coe}$ applied to $e$ and $\operatorname{coe}$ applied to the inverse of $e$.
OrderIso.toGaloisInsertiondefMathlib.Order.GaloisConnection.Basic, function or constantWording
the Galois insertion of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the Galois insertion of $e$ is a Galois insertion of $\operatorname{coe}$ applied to $e$ and $\operatorname{coe}$ applied to the inverse of $e$.
WithBot.giUnbotDBotdefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
$\operatorname{giUnbotDBot}$ is a Galois insertion of $\operatorname{unbotD}$ applied to the bottom and $\operatorname{some}$.
WithTop.giUntopDTopdefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
$\operatorname{giUntopDTop}$ is a Galois coinsertion of $\operatorname{some}$ and $\operatorname{untopD}$ applied to the top.
gciIciSInfdefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
$\mathrm{gciIciSInf}$ is a Galois coinsertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{Ici}$ and $\operatorname{comp}$ applied to $\operatorname{sInf}$ and $\operatorname{coe}$ applied to the order dual.
gciMapBicompldefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
Assume that $f$ is injective. Assume that $g$ is injective. Then $\mathrm{gciMapBicompl}$ applied to $\mathrm{hf}$ and $\mathrm{hg}$ is a Galois coinsertion of the function that maps $x_{4}$ to $\operatorname{Map}$ applied to $x_{4}$, $f$ and $g$ and the function that maps $x_{5}$ to $\operatorname{bicompl}$ applied to $x_{5}$, $f$ and $g$.
gciMapOnFundefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
Assume that $f$ is injective. Then $\mathrm{gciMapOnFun}$ applied to $\mathrm{hf}$ is a Galois coinsertion of the function that maps $x_{2}$ to $\operatorname{Map}$ applied to $x_{2}$, $f$ and $f$ and the function that maps $x_{3}$ to $\operatorname{onFun}$ applied to $x_{3}$ and $f$ defined as $\mathrm{gciMapBicompl}$ applied to $\mathrm{hf}$ and $\mathrm{hf}$.
giMapBicompldefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
Assume that $\operatorname{Surjective}$ holds for $f$. Assume that $\operatorname{Surjective}$ holds for $g$. Then $\mathrm{giMapBicompl}$ applied to $\mathrm{hf}$ and $\mathrm{hg}$ is a Galois insertion of the function that maps $x_{4}$ to $\operatorname{Map}$ applied to $x_{4}$, $f$ and $g$ and the function that maps $x_{5}$ to $\operatorname{bicompl}$ applied to $x_{5}$, $f$ and $g$.
giMapOnFundefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
Assume that $\operatorname{Surjective}$ holds for $f$. Then $\mathrm{giMapOnFun}$ applied to $\mathrm{hf}$ is a Galois insertion of the function that maps $x_{2}$ to $\operatorname{Map}$ applied to $x_{2}$, $f$ and $f$ and the function that maps $x_{3}$ to $\operatorname{onFun}$ applied to $x_{3}$ and $f$ defined as $\mathrm{giMapBicompl}$ applied to $\mathrm{hf}$ and $\mathrm{hf}$.
giSSupIicdefMathlib.Order.GaloisConnection.Basic, function or constantEnglish
$\mathrm{giSSupIic}$ is a Galois insertion of $\operatorname{sSup}$ and $\operatorname{Iic}$.
GaloisCoinsertionstructureMathlib.Order.GaloisConnection.Defs, typeWording
Galois coinsertion of l and u (from the name)
English
Let $l$ be a function from elements of $x$ to elements of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then the Galois coinsertions of $l$ and $u$ are a basic type.
GaloisCoinsertion.choicedefMathlib.Order.GaloisConnection.Defs, function or constantWording
the choice of self and x4 (from the name)
English
Let $\mathrm{self}$ be a Galois coinsertion of $l$ and $u$. Let $x_{4}$ be an element of $x_{1}$ such that $x_{4} \leq l (u (x_{4}))$. Then the choice of $\mathrm{self}$ and $x_{4}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$ and $h$.
GaloisCoinsertion.dualdefMathlib.Order.GaloisConnection.Defs, function or constantWording
the dual of x4 (from the name)
English
Let $x_{4}$ be a Galois coinsertion of $l$ and $u$. Then the dual of $x_{4}$ is a Galois insertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $u$ and $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $l$ and $\operatorname{coe}$ applied to the order dual.
GaloisCoinsertion.monotoneIntrodefMathlib.Order.GaloisConnection.Defs, function or constantWording
the monotone intro of h_l_u and h_u_l (from the name)
English
Assume that $u$ is monotone. Assume that $l$ is monotone. Assume that for all elements $a$ of $x$, $l (u (a))\leq a$. Assume that for all elements $b$ of $x_{1}$, $\EqtMACRoH {u (l (b))}{b}$. Then the monotone intro of $\mathrm{h\_l\_u}$ and $\mathrm{h\_u\_l}$ is a Galois coinsertion of $l$ and $u$.
GaloisCoinsertion.ofDualdefMathlib.Order.GaloisConnection.Defs, function or constantWording
the Galois coinsertion of x4 (from the name)
English
Let $x_{4}$ be a Galois coinsertion of $l$ and $u$. Then the Galois coinsertion of $x_{4}$ is a Galois insertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $u$ and $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $l$ and $\operatorname{coe}$ applied to the dual.
GaloisConnectiondefMathlib.Order.GaloisConnection.Defs, predicateEnglish
Let $l$ be a function from elements of $x$ to elements of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{GaloisConnection}$ holds for $l$ and $u$, if for all elements $a$ of $x$, for all elements $b$ of $x_{1}$, $l (a)\leq b$, if and only if $a \leq u (b)$.
GaloisConnection.toGaloisCoinsertiondefMathlib.Order.GaloisConnection.Defs, function or constantWording
the Galois coinsertion of gc and h (from the name)
English
Assume that $\mathrm{GaloisConnection}$ holds for $l$ and $u$. Assume that for all elements $b$ of $x_{1}$, $u (l (b))\leq b$. Then the Galois coinsertion of $\mathrm{gc}$ and $h$ is a Galois coinsertion of $l$ and $u$.
GaloisConnection.toGaloisInsertiondefMathlib.Order.GaloisConnection.Defs, function or constantWording
the Galois insertion of gc and h (from the name)
English
Assume that $\mathrm{GaloisConnection}$ holds for $l$ and $u$. Assume that for all elements $b$ of $x_{1}$, $b \leq l (u (b))$. Then the Galois insertion of $\mathrm{gc}$ and $h$ is a Galois insertion of $l$ and $u$.
GaloisInsertionstructureMathlib.Order.GaloisConnection.Defs, typeWording
Galois insertion of l and u (from the name)
English
Let $l$ be a function from elements of $x$ to elements of $x_{1}$. Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then the Galois insertions of $l$ and $u$ are a basic type.
GaloisInsertion.choicedefMathlib.Order.GaloisConnection.Defs, function or constantWording
the choice of self and x4 (from the name)
English
Let $\mathrm{self}$ be a Galois insertion of $l$ and $u$. Let $x_{4}$ be an element of $x$ such that $u (l (x_{4}))\leq x_{4}$. Then the choice of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{4}$ and $h$.
GaloisInsertion.dualdefMathlib.Order.GaloisConnection.Defs, function or constantWording
the dual of x4 (from the name)
English
Let $x_{4}$ be a Galois insertion of $l$ and $u$. Then the dual of $x_{4}$ is a Galois coinsertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $u$ and $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $l$ and $\operatorname{coe}$ applied to the order dual.
GaloisInsertion.monotoneIntrodefMathlib.Order.GaloisConnection.Defs, function or constantWording
the monotone intro of h_u_l and h_l_u (from the name)
English
Assume that $u$ is monotone. Assume that $l$ is monotone. Assume that for all elements $a$ of $x$, $a \leq u (l (a))$. Assume that for all elements $b$ of $x_{1}$, $\EqtMACRoH {l (u (b))}{b}$. Then the monotone intro of $\mathrm{h\_u\_l}$ and $\mathrm{h\_l\_u}$ is a Galois insertion of $l$ and $u$.
GaloisInsertion.ofDualdefMathlib.Order.GaloisConnection.Defs, function or constantWording
the Galois insertion of x4 (from the name)
English
Let $x_{4}$ be a Galois insertion of $l$ and $u$. Then the Galois insertion of $x_{4}$ is a Galois coinsertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $u$ and $\operatorname{coe}$ applied to the dual and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the order dual and $\operatorname{comp}$ applied to $l$ and $\operatorname{coe}$ applied to the dual.
Prod.GameAddinductiveMathlib.Order.GameAdd, predicateEnglish
Let $x_{2}$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{3}$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $x_{4}$ and $x_{5}$ be elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then we can say that $\operatorname{GameAdd}$ holds for $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$.
Prod.GameAdd.recursiondefMathlib.Order.GameAdd, function or constantWording
the recursion of x4 and x5 (from the name)
English
Assume that $\mathrm{WellFounded}$ holds for $x_{2}$. Assume that $\mathrm{WellFounded}$ holds for $x_{3}$. Let $\mathrm{IH}$ be a function from elements $x_{4}$ of $x$ and elements $x_{5}$ of $x_{1}$ and functions from elements $x_{7}$ of $x$ and elements $x_{8}$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\operatorname{GameAdd}$ applied to $x_{2}$, $x_{3}$, $\ProdmkMACRoU {x_{7}}{x_{8}}$ and $\ProdmkMACRoU {x_{4}}{x_{5}}$ to elements of $C$ applied to $x_{7}$ and $x_{8}$ to elements of $C$ applied to $x_{4}$ and $x_{5}$. Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the recursion of $x_{5}$ and $\mathrm{IH}$ is an element of $C$ applied to $a$ and $b$.
Sym2.GameAdddefMathlib.Order.GameAdd, predicateEnglish
Let $x_{1}$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{2}$ and $x_{3}$ be symmetric squares of $x$. Then $\operatorname{GameAdd}$ holds for $x_{1}$, $x_{2}$ and $x_{3}$, if $\mathrm{Sym2\_\_lift\_u2082\_\_\_app}$ holds for the function that maps $x_{8}$, $x_{9}$, $x_{10}$ and $x_{11}$ to the proposition that $\operatorname{GameAdd}$ holds for $x_{1}$, $x_{1}$, $\ProdmkMACRoU {x_{8}}{x_{9}}$ and $\ProdmkMACRoU {x_{10}}{x_{11}}$ or $\operatorname{GameAdd}$ holds for $x_{1}$, $x_{1}$, $\ProdmkMACRoU {x_{9}}{x_{8}}$ and $\ProdmkMACRoU {x_{10}}{x_{11}}$, $x_{2}$ and $x_{3}$.
Sym2.GameAdd.recursiondefMathlib.Order.GameAdd, function or constantWording
the recursion of x2 and x3 (from the name)
English
Assume that $\mathrm{WellFounded}$ holds for $x_{1}$. Let $\mathrm{IH}$ be a function from elements $x_{2}$ of $x$ and elements $x_{3}$ of $x$ and functions from elements $x_{5}$ of $x$ and elements $x_{6}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{GameAdd}$ applied to $x_{1}$, $\operatorname{mk}$ applied to $x_{5}$ and $x_{6}$ and $\operatorname{mk}$ applied to $x_{2}$ and $x_{3}$ to elements of $C$ applied to $x_{5}$ and $x_{6}$ to elements of $C$ applied to $x_{2}$ and $x_{3}$. Let $a$ and $b$ be elements of $x$. Then the recursion of $x_{3}$ and $\mathrm{IH}$ is an element of $C$ applied to $a$ and $b$.
GradeBoundedOrderclassMathlib.Order.Grade, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{GradeBoundedOrder}$ holds for $x$ and $x_{1}$.
GradeMaxOrderclassMathlib.Order.Grade, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{GradeMaxOrder}$ holds for $x$ and $x_{1}$.
GradeMinOrderclassMathlib.Order.Grade, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{GradeMinOrder}$ holds for $x$ and $x_{1}$.
GradeOrderclassMathlib.Order.Grade, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{GradeOrder}$ holds for $x$ and $x_{1}$.
GradeOrder.gradedefMathlib.Order.Grade, function or constantWording
the grading function of x4 (from the docstring)
English
Let $x_{4}$ be an element of $x_{1}$. Then the grading function of $x_{4}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
gradedefMathlib.Order.Grade, function or constantEnglish
Let $x$ be a set. Let $x_{5}$ be an element of $x_{1}$. Then $\mathrm{grade}$ applied to $x$ and $x_{5}$ is an element of $x$ defined as the grading function of $x_{5}$.
Set.chainHeightdefMathlib.Order.Height, function or constantWording
the chain height of s and r (from the name)
English
Let $s$ be an element of $\wp x$. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the chain height of $s$ and $r$ is a natural number defined as the supremum of the function that maps $t$ to the cardinality in $t$.
BiheytingAlgebraclassMathlib.Order.Heyting.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{BiheytingAlgebra}$ holds for $x$.
CoheytingAlgebraclassMathlib.Order.Heyting.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{CoheytingAlgebra}$ holds for $x$.
GeneralizedCoheytingAlgebraclassMathlib.Order.Heyting.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{GeneralizedCoheytingAlgebra}$ holds for $x$.
GeneralizedHeytingAlgebraclassMathlib.Order.Heyting.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{GeneralizedHeytingAlgebra}$ holds for $x$.
HeytingAlgebraclassMathlib.Order.Heyting.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{HeytingAlgebra}$ holds for $x$.
Coheyting.boundarydefMathlib.Order.Heyting.Boundary, function or constantWording
the boundary of a (from the docstring)
English
Let $a$ be an element of $x$. Then the boundary of $a$ is an element of $x$ defined as $\MinminMACRoAG {a}{\operatorname{hnot} (a)}$.
BiheytingHomstructureMathlib.Order.Heyting.Hom, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{BiheytingHom}$ applied to $x$ and $x_{1}$ are a basic type.
BiheytingHom.compdefMathlib.Order.Heyting.Hom, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an element of $\mathrm{BiheytingHom}$ applied to $x_{1}$ and $x_{2}$. Let $g$ be an element of $\mathrm{BiheytingHom}$ applied to $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an element of $\mathrm{BiheytingHom}$ applied to $x$ and $x_{2}$.
BiheytingHom.copydefMathlib.Order.Heyting.Hom, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be an element of $\mathrm{BiheytingHom}$ applied to $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{BiheytingHom}$ applied to $x$ and $x_{1}$.
BiheytingHom.iddefMathlib.Order.Heyting.Hom, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an element of $\mathrm{BiheytingHom}$ applied to $x$ and $x$.
BiheytingHomClassclassMathlib.Order.Heyting.Hom, predicateEnglish
Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{BiheytingHomClass}$ holds for $F$, $x$ and $x_{1}$.
CoheytingHomstructureMathlib.Order.Heyting.Hom, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{CoheytingHom}$ applied to $x$ and $x_{1}$ are a basic type.
CoheytingHom.compdefMathlib.Order.Heyting.Hom, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an element of $\mathrm{CoheytingHom}$ applied to $x_{1}$ and $x_{2}$. Let $g$ be an element of $\mathrm{CoheytingHom}$ applied to $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an element of $\mathrm{CoheytingHom}$ applied to $x$ and $x_{2}$.
CoheytingHom.copydefMathlib.Order.Heyting.Hom, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be an element of $\mathrm{CoheytingHom}$ applied to $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{CoheytingHom}$ applied to $x$ and $x_{1}$.
CoheytingHom.iddefMathlib.Order.Heyting.Hom, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an element of $\mathrm{CoheytingHom}$ applied to $x$ and $x$.
CoheytingHomClassclassMathlib.Order.Heyting.Hom, predicateEnglish
Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{CoheytingHomClass}$ holds for $F$, $x$ and $x_{1}$.
HeytingHomstructureMathlib.Order.Heyting.Hom, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\mathrm{HeytingHom}$ applied to $x$ and $x_{1}$ are a basic type.
HeytingHom.compdefMathlib.Order.Heyting.Hom, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an element of $\mathrm{HeytingHom}$ applied to $x_{1}$ and $x_{2}$. Let $g$ be an element of $\mathrm{HeytingHom}$ applied to $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an element of $\mathrm{HeytingHom}$ applied to $x$ and $x_{2}$.
HeytingHom.copydefMathlib.Order.Heyting.Hom, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be an element of $\mathrm{HeytingHom}$ applied to $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an element of $\mathrm{HeytingHom}$ applied to $x$ and $x_{1}$.
HeytingHom.iddefMathlib.Order.Heyting.Hom, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an element of $\mathrm{HeytingHom}$ applied to $x$ and $x$.
HeytingHomClassclassMathlib.Order.Heyting.Hom, predicateEnglish
Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{HeytingHomClass}$ holds for $F$, $x$ and $x_{1}$.
Heyting.IsRegulardefMathlib.Order.Heyting.Regular, predicateWording
a is regular (from the docstring)
English
Let $a$ be an element of $x$. Then $a$ is regular, if the complement of the complement of $a$ is equal to $a$.
Heyting.RegulardefMathlib.Order.Heyting.Regular, typeWording
regular of x (from the name)
English
Let $x$ be a set. Then a regular of $x$ is an element of the function that maps $x$ to $\SubtypeSet {a}{\operatorname{IsRegular} (a)}$.
Heyting.Regular.gidefMathlib.Order.Heyting.Regular, function or constantEnglish
$\operatorname{gi}$ is a Galois insertion of $\operatorname{coe}$ applied to the regular and $\operatorname{val}$.
Heyting.Regular.toRegulardefMathlib.Order.Heyting.Regular, function or constantWording
the regular (from the name)
English
The regular is an order homomorphism of $x$ and the set of regulars of $x$.
Heyting.Regular.valdefMathlib.Order.Heyting.Regular, function or constantWording
the value of x2 (from the name)
English
Let $x_{2}$ be a regular of $x$. Then the value of $x_{2}$ is an element of $x$ defined as the proposition that $x_{2}$ is regular.
Equiv.toOrderIsodefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$ such that $\operatorname{coe}$ applied to $e$ and $\operatorname{coe}$ applied to the inverse of $e$ are monotone. Then the order isomorphism of $e$ is an order isomorphism of $x$ and $x_{1}$.
OrderEmbeddingdefMathlib.Order.Hom.Basic, typeWording
order embedding of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then an order embedding of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of relation embeddings of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Leq} (x_{6} , x_{7})$.
OrderEmbedding.compdefMathlib.Order.Hom.Basic, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an order embedding of $x$ and $x_{1}$. Let $g$ be an order embedding of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an order embedding of $x$ and $x_{2}$ defined as the composition of $f$ and $g$.
OrderEmbedding.dualdefMathlib.Order.Hom.Basic, function or constantWording
the dual of f (from the name)
English
Let $f$ be an order embedding of $x$ and $x_{1}$. Then the dual of $f$ is an order embedding of the set of order duals of $x$ and the set of order duals of $x_{1}$.
OrderEmbedding.gtEmbeddingdefMathlib.Order.Hom.Basic, function or constantEnglish
Let $f$ be an order embedding of $x$ and $x_{1}$. Then $\operatorname{gtEmbedding}$ applied to $f$ is a relation embedding of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{5} , x_{4})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{7} , x_{6})$.
OrderEmbedding.iddefMathlib.Order.Hom.Basic, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an order embedding of $x$ and $x$ defined as the identity of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
OrderEmbedding.ltEmbeddingdefMathlib.Order.Hom.Basic, function or constantEnglish
Let $f$ be an order embedding of $x$ and $x_{1}$. Then $\operatorname{ltEmbedding}$ applied to $f$ is a relation embedding of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$.
OrderEmbedding.ofIsEmptydefMathlib.Order.Hom.Basic, function or constantWording
the trivial embedding (from the docstring)
English
The trivial embedding is an order embedding of $x$ and $x_{1}$.
OrderEmbedding.ofMapLEIffdefMathlib.Order.Hom.Basic, function or constantWording
the order embedding of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $a$ and $b$ of $x$, $f (a)\leq f (b)$, if and only if $a \leq b$. Then the order embedding of $f$ and $\mathrm{hf}$ is an order embedding of $x$ and $x_{1}$ defined as the relation embedding of $f$ and $\mathrm{hf}$.
OrderEmbedding.ofStrictMonodefMathlib.Order.Hom.Basic, function or constantWording
the order embedding of f and h (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{StrictMono}$ holds for $f$. Then the order embedding of $f$ and $h$ is an order embedding of $x$ and $x_{1}$ defined as the order embedding of $f$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{StrictMono\_\_le\_iff\_le}$ applied to $h$.
OrderEmbedding.subtypedefMathlib.Order.Hom.Basic, function or constantWording
the subtype of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the subtype of $p$ is an order embedding of $\SubtypeSet {x_{2}}{p (x_{2})}$ and $x$.
OrderEmbedding.toOrderHomdefMathlib.Order.Hom.Basic, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an order embedding of $X$ and $Y$. Then the order homomorphism of $f$ is an order homomorphism of $X$ and $Y$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{monotone}$ applied to $f$.
OrderHomstructureMathlib.Order.Hom.Basic, typeWording
order homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the order homomorphisms of $x$ and $x_{1}$ are a basic type.
OrderHom.Subtype.valdefMathlib.Order.Hom.Basic, function or constantWording
the value of p (from the name)
English
Let $p$ be a function from elements of $x$ to propositions. Then the value of $p$ is an order homomorphism of $\SubtypeSet {x_{2}}{p (x_{2})}$ and $x$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $x_{2}$, $x_{3}$ and $h$ to $h$.
OrderHom.applydefMathlib.Order.Hom.Basic, function or constantWording
the order homomorphism of x4 (from the name)
English
Let $x_{4}$ be an element of $x$. Then the order homomorphism of $x_{4}$ is an order homomorphism of the set of order homomorphisms of $x$ and $x_{1}$ and $x_{1}$ defined as the composition of the evaluation order homomorphism of $x_{4}$ and the coercion function homomorphism.
OrderHom.coeFnHomdefMathlib.Order.Hom.Basic, function or constantWording
the coercion function homomorphism (from the name)
English
The coercion function homomorphism is an order homomorphism of the set of order homomorphisms of $x$ and $x_{1}$ and the set of functions from elements of $x$ to elements of $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $f$ to $\operatorname{coe}$ applied to $f$ and the function that maps $x_{4}$, $x_{5}$ and $h$ to $h$.
OrderHom.compdefMathlib.Order.Hom.Basic, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an order homomorphism of $x_{1}$ and $x_{2}$. Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is an order homomorphism of $x$ and $x_{2}$.
OrderHom.compₘdefMathlib.Order.Hom.Basic, function or constantWording
the composition (from the name)
English
The composition is an order homomorphism of the set of order homomorphisms of $x_{1}$ and $x_{2}$ and the set of order homomorphisms of the set of order homomorphisms of $x$ and $x_{1}$ and the set of order homomorphisms of $x$ and $x_{2}$.
OrderHom.constdefMathlib.Order.Hom.Basic, function or constantWording
the constant of x (from the name)
English
Let $x$ be a set. Then the constant of $x$ is an order homomorphism of $x_{2}$ and the set of order homomorphisms of $x$ and $x_{2}$.
OrderHom.copydefMathlib.Order.Hom.Basic, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an order homomorphism of $x$ and $x_{1}$.
OrderHom.currydefMathlib.Order.Hom.Basic, function or constantWording
the curry (from the name)
English
The curry is an order isomorphism of the set of order homomorphisms of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and the set of order homomorphisms of $x$ and the set of order homomorphisms of $x_{1}$ and $x_{2}$.
OrderHom.diagdefMathlib.Order.Hom.Basic, function or constantWording
the diagonal (from the name)
English
The diagonal is an order homomorphism of $x$ and $\mathrm{Prod}$ applied to $x$ and $x$ defined as the product of the identity function and the identity function.
OrderHom.dualdefMathlib.Order.Hom.Basic, function or constantWording
the dual (from the name)
English
The dual is an equivalence from the set of order homomorphisms of $x$ and $x_{1}$ to the set of order homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.
OrderHom.dualIsodefMathlib.Order.Hom.Basic, function or constantWording
the dual isomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the dual isomorphism of $x$ and $x_{1}$ is an order isomorphism of the set of order homomorphisms of $x$ and $x_{1}$ and the set of order duals of the set of order homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.
OrderHom.equivRelHomdefMathlib.Order.Hom.Basic, function or constantWording
the equivalence relation homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalence relation homomorphism of $x$ and $x_{1}$ is an equivalence from the set of order homomorphisms of $x$ and $x_{1}$ to the set of relation homomorphisms of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Leq} (x_{6} , x_{7})$.
OrderHom.fstdefMathlib.Order.Hom.Basic, function or constantWording
the first component (from the name)
English
The first component is an order homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.
OrderHom.iddefMathlib.Order.Hom.Basic, function or constantWording
the identity function (from the docstring)
English
The identity function is an order homomorphism of $x$ and $x$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and $\mathrm{monotone\_id}$.
OrderHom.ofClassdefMathlib.Order.Hom.Basic, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the order homomorphism of $f$ is an order homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\operatorname{monotone}$ applied to $f$.
OrderHom.onDiagdefMathlib.Order.Hom.Basic, function or constantEnglish
Let $f$ be an order homomorphism of $x$ and the set of order homomorphisms of $x$ and $x_{1}$. Then $\operatorname{onDiag}$ applied to $f$ is an order homomorphism of $x$ and $x_{1}$ defined as the composition of $\operatorname{symm}$ applied to the curry and $f$ and the diagonal.
OrderHom.pidefMathlib.Order.Hom.Basic, function or constantWording
the product of f (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $x_{2}$ to order homomorphisms of $x$ and $x_{3}$ applied to $i_{1}$. Then the product of $i_{1}$ is an order homomorphism of $x$ and the set of functions from elements $i$ of $x_{2}$ to elements of $x_{3}$ applied to $i$.
OrderHom.piIsodefMathlib.Order.Hom.Basic, function or constantWording
the product isomorphism (from the name)
English
The product isomorphism is an order isomorphism of the set of order homomorphisms of $x$ and the set of functions from elements $i$ of $x_{2}$ to elements of $x_{3}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{2}$ to order homomorphisms of $x$ and $x_{3}$ applied to $i_{1}$.
OrderHom.proddefMathlib.Order.Hom.Basic, function or constantWording
the product of f and g (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $g$ be an order homomorphism of $x$ and $x_{2}$. Then the product of $f$ and $g$ is an order homomorphism of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
OrderHom.prodIsodefMathlib.Order.Hom.Basic, function or constantWording
the product isomorphism (from the name)
English
The product isomorphism is an order isomorphism of the set of order homomorphisms of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to the set of order homomorphisms of $x$ and $x_{1}$ and the set of order homomorphisms of $x$ and $x_{2}$.
OrderHom.prodMapdefMathlib.Order.Hom.Basic, function or constantWording
the product map of f and g (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $g$ be an order homomorphism of $x_{2}$ and $x_{3}$. Then the product map of $f$ and $g$ is an order homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.
OrderHom.prodₘdefMathlib.Order.Hom.Basic, function or constantWording
the product (from the name)
English
The product is an order homomorphism of the set of order homomorphisms of $x$ and $x_{1}$ and the set of order homomorphisms of the set of order homomorphisms of $x$ and $x_{2}$ and the set of order homomorphisms of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
OrderHom.snddefMathlib.Order.Hom.Basic, function or constantWording
the second component (from the name)
English
The second component is an order homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.
OrderHom.toFundefMathlib.Order.Hom.Basic, function or constantWording
the order homomorphism of self and x4 (from the name)
English
Let $\mathrm{self}$ be an order homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the order homomorphism of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
OrderHom.uliftLeftMapdefMathlib.Order.Hom.Basic, function or constantWording
the lift left map of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the lift left map of $f$ is an order homomorphism of $\mathrm{ULift}$ applied to $x$ and $x_{1}$.
OrderHom.uliftMapdefMathlib.Order.Hom.Basic, function or constantWording
the lift map of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the lift map of $f$ is an order homomorphism of $\mathrm{ULift}$ applied to $x$ and $\mathrm{ULift}$ applied to $x_{1}$.
OrderHom.uliftRightMapdefMathlib.Order.Hom.Basic, function or constantWording
the lift right map of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the lift right map of $f$ is an order homomorphism of $x$ and $\mathrm{ULift}$ applied to $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $i$ to $\operatorname{up}$ applied to $f$ applied to $i$ and the function that maps $x_{4}$, $x_{5}$ and $h$ to $\operatorname{monotone}$ applied to $f$, $x_{4}$, $x_{5}$ and $h$.
OrderHomClassdefMathlib.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{OrderHomClass}$ holds for $F$, $x$ and $x_{1}$, if $\mathrm{RelHomClass}$ holds for $F$, the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Leq} (x_{5} , x_{6})$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Leq} (x_{7} , x_{8})$.
OrderIsodefMathlib.Order.Hom.Basic, typeWording
order isomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then an order isomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of relation isomorphisms of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Leq} (x_{6} , x_{7})$.
OrderIso.arrowCongrdefMathlib.Order.Hom.Basic, function or constantWording
the arrow congruence of f and g (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{2}$. Let $g$ be an order isomorphism of $x_{1}$ and $x_{3}$. Then the arrow congruence of $f$ and $g$ is an order isomorphism of the set of order homomorphisms of $x$ and $x_{1}$ and the set of order homomorphisms of $x_{2}$ and $x_{3}$.
OrderIso.conjdefMathlib.Order.Hom.Basic, function or constantWording
the conjugate of f (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then the conjugate of $f$ is an equivalence from the set of order homomorphisms of $x$ and $x$ to the set of order homomorphisms of $x_{1}$ and $x_{1}$ defined as the equivalence of the arrow congruence of $f$ and $f$.
OrderIso.dualdefMathlib.Order.Hom.Basic, function or constantWording
the dual of f (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then the dual of $f$ is an order isomorphism of the set of order duals of $x$ and the set of order duals of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $f$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{OrderIso\_\_le\_iff\_le}$ applied to $f$.
OrderIso.dualDualdefMathlib.Order.Hom.Basic, function or constantWording
the dual dual of x (from the name)
English
Let $x$ be a set. Then the dual dual of $x$ is an order isomorphism of $x$ and the set of order duals of the set of order duals of $x$ defined as the identity of $x$.
OrderIso.equivEmbeddingSurjectivedefMathlib.Order.Hom.Basic, function or constantEnglish
$\operatorname{equivEmbeddingSurjective}$ is an element of $\EquivMACRoAE {\mathrm{OrderIso} (x , x_{1})}{(\SubtypeSet {f}{\operatorname{Surjective} (\operatorname{coe} (f))})}$.
OrderIso.funUniquedefMathlib.Order.Hom.Basic, function or constantEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $x_{1}$ is an order isomorphism of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{1}$.
OrderIso.ofClassdefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the order isomorphism of $f$ is an order isomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{OrderIsoClass\_\_map\_le\_map\_iff}$ applied to $f$.
OrderIso.ofCmpEqCmpdefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of f and g (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$ such that for all elements $a$ of $x$, for all elements $b$ of $x_{1}$, the comparison of $a$ and $g$ applied to $b$ is equal to the comparison of $f$ applied to $a$ and $b$. Then the order isomorphism of $f$ and $g$ is an order isomorphism of $x$ and $x_{1}$.
OrderIso.ofHomInvdefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of f and g (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $g$ be an order homomorphism of $x_{1}$ and $x$ such that the composition of $f$ and $g$ is equal to the identity function and the composition of $g$ and $f$ is equal to the identity function. Then the order isomorphism of $f$ and $g$ is an order isomorphism of $x$ and $x_{1}$.
OrderIso.ofIsEmptydefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the order isomorphism of $x$ and $x_{1}$ is an order isomorphism of $x$ and $x_{1}$.
OrderIso.ofRelIsoLTdefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of e (from the name)
English
Let $e$ be a relation isomorphism of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$. Then the order isomorphism of $e$ is an order isomorphism of $x$ and $x_{1}$.
OrderIso.ofSurjectivedefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of f and hf (from the name)
English
Let $f$ be an order embedding of $x$ and $x_{1}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the order isomorphism of $f$ and $\mathrm{hf}$ is an order isomorphism of $x$ and $x_{1}$ defined as the relation isomorphism of $f$ and $\mathrm{hf}$.
OrderIso.ofUniquedefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of x and x1 (from the docstring)
English
Let $x$ and $x_{1}$ be sets. Then the order isomorphism of $x$ and $x_{1}$ is an order isomorphism of $x$ and $x_{1}$.
OrderIso.orderEmbeddingCongrdefMathlib.Order.Hom.Basic, function or constantWording
the order embedding congruence of f and g (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{2}$. Let $g$ be an order isomorphism of $x_{1}$ and $x_{3}$. Then the order embedding congruence of $f$ and $g$ is an equivalence from the set of order embeddings of $x$ and $x_{1}$ to the set of order embeddings of $x_{2}$ and $x_{3}$ defined as the relation embedding congruence of $f$ and $g$.
OrderIso.orderIsoCongrdefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism congruence of f and g (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{2}$. Let $g$ be an order isomorphism of $x_{1}$ and $x_{3}$. Then the order isomorphism congruence of $f$ and $g$ is an equivalence from the set of order isomorphisms of $x$ and $x_{1}$ to the set of order isomorphisms of $x_{2}$ and $x_{3}$ defined as the relation isomorphism congruence of $f$ and $g$.
OrderIso.prodAssocdefMathlib.Order.Hom.Basic, function or constantWording
the product associator of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the product associator of $x_{1}$ and $x_{2}$ is an order isomorphism of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
OrderIso.prodCommdefMathlib.Order.Hom.Basic, function or constantEnglish
$\operatorname{prodComm}$ is an order isomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{prodComm}$ applied to $x$ and $x_{1}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Prod\_\_swap\_le\_swap}$.
OrderIso.refldefMathlib.Order.Hom.Basic, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is an order isomorphism of $x$ and $x$ defined as the identity of the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
OrderIso.symmdefMathlib.Order.Hom.Basic, function or constantWording
the inverse of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the inverse of $e$ is an order isomorphism of $x_{1}$ and $x$ defined as the inverse of $e$.
OrderIso.toOrderEmbeddingdefMathlib.Order.Hom.Basic, function or constantWording
the order embedding of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the order embedding of $e$ is an order embedding of $x$ and $x_{1}$ defined as the relation embedding of $e$.
OrderIso.toRelIsoGTdefMathlib.Order.Hom.Basic, function or constantEnglish
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{toRelIsoGT}$ applied to $e$ is a relation isomorphism of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{5} , x_{4})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{7} , x_{6})$.
OrderIso.toRelIsoLTdefMathlib.Order.Hom.Basic, function or constantEnglish
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{toRelIsoLT}$ applied to $e$ is a relation isomorphism of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$ defined as $\operatorname{mk}$ applied to $\operatorname{toEquiv}$ applied to $e$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{OrderIso\_\_lt\_iff\_lt}$ applied to $e$.
OrderIso.transdefMathlib.Order.Hom.Basic, function or constantWording
the composition of e and #2 (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Let $\mathrm{e'}$ be an order isomorphism of $x_{1}$ and $x_{2}$. Then the composition of $e$ and $\mathrm{e'}$ is an order isomorphism of $x$ and $x_{2}$ defined as the composition of $e$ and $\mathrm{e'}$.
OrderIsoClassclassMathlib.Order.Hom.Basic, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{OrderIsoClass}$ holds for $F$, $x$ and $x_{1}$.
Pi.evalOrderHomdefMathlib.Order.Hom.Basic, function or constantWording
the evaluation order homomorphism of i (from the name)
English
Let $i$ be an element of $x$. Then the evaluation order homomorphism of $i$ is an order homomorphism of the set of functions from elements $j$ of $x$ to elements of $x_{1}$ applied to $j$ and $x_{1}$ applied to $i$ defined as $\operatorname{mk}$ applied to $\operatorname{eval}$ applied to $i$ and $\mathrm{Function\_\_monotone\_eval}$ applied to $i$.
RelEmbedding.orderEmbeddingOfLTEmbeddingdefMathlib.Order.Hom.Basic, function or constantWording
the order embedding of f (from the name)
English
Let $f$ be a relation embedding of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$. Then the order embedding of $f$ is an order embedding of $x$ and $x_{1}$.
RelHom.toOrderHomdefMathlib.Order.Hom.Basic, function or constantWording
the order homomorphism of f (from the name)
English
Let $f$ be a relation homomorphism of the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Lt} (x_{6} , x_{7})$. Then the order homomorphism of $f$ is an order homomorphism of $x$ and $x_{1}$.
StrictMono.orderIsoOfRightInversedefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism of f and g (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{StrictMono}$ holds for $f$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$ such that $\operatorname{RightInverse}$ holds for $g$ and $f$. Then the order isomorphism of $f$ and $g$ is an order isomorphism of $x$ and $x_{1}$.
Subtype.orderEmbeddingdefMathlib.Order.Hom.Basic, function or constantWording
the order embedding of h (from the name)
English
Assume that for all elements $a$ of $x$, if $p$ holds for $a$, then $q$ holds for $a$. Then the order embedding of $h$ is an order embedding of $\SubtypeSet {x_{2}}{p (x_{2})}$ and $\SubtypeSet {x_{3}}{q (x_{3})}$.
ULift.orderIsodefMathlib.Order.Hom.Basic, function or constantWording
the order isomorphism (from the name)
English
The order isomorphism is an order isomorphism of $\mathrm{ULift}$ applied to $x$ and $x$.
BotHomstructureMathlib.Order.Hom.Bounded, typeWording
bottom homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the bottom homomorphisms of $x$ and $x_{1}$ are a basic type.
BotHom.compdefMathlib.Order.Hom.Bounded, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a bottom homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a bottom homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a bottom homomorphism of $x$ and $x_{2}$.
BotHom.copydefMathlib.Order.Hom.Bounded, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a bottom homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a bottom homomorphism of $x$ and $x_{1}$.
BotHom.dualdefMathlib.Order.Hom.Bounded, function or constantWording
the dual (from the name)
English
The dual is an equivalence from the set of bottom homomorphisms of $x$ and $x_{1}$ to the set of top homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.
BotHom.iddefMathlib.Order.Hom.Bounded, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a bottom homomorphism of $x$ and $x$.
BotHom.toFundefMathlib.Order.Hom.Bounded, function or constantWording
the bottom homomorphism of self and x4 (from the name)
English
Let $\mathrm{self}$ be a bottom homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the bottom homomorphism of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
BotHomClassclassMathlib.Order.Hom.Bounded, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{BotHomClass}$ holds for $F$, $x$ and $x_{1}$.
BotHomClass.toBotHomdefMathlib.Order.Hom.Bounded, function or constantWording
the bottom homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the bottom homomorphism of $f$ is a bottom homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{BotHomClass\_\_map\_bot}$ applied to $f$.
BoundedOrderHomstructureMathlib.Order.Hom.Bounded, typeWording
bounded order homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the bounded order homomorphisms of $x$ and $x_{1}$ are a basic type.
BoundedOrderHom.compdefMathlib.Order.Hom.Bounded, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a bounded order homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a bounded order homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a bounded order homomorphism of $x$ and $x_{2}$.
BoundedOrderHom.copydefMathlib.Order.Hom.Bounded, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a bounded order homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a bounded order homomorphism of $x$ and $x_{1}$.
BoundedOrderHom.dualdefMathlib.Order.Hom.Bounded, function or constantWording
the dual (from the name)
English
The dual is an equivalence from the set of bounded order homomorphisms of $x$ and $x_{1}$ to the set of bounded order homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.
BoundedOrderHom.iddefMathlib.Order.Hom.Bounded, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a bounded order homomorphism of $x$ and $x$.
BoundedOrderHom.toBotHomdefMathlib.Order.Hom.Bounded, function or constantWording
the bottom homomorphism of f (from the name)
English
Let $f$ be a bounded order homomorphism of $x$ and $x_{1}$. Then the bottom homomorphism of $f$ is a bottom homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOrderHom}$ applied to $f$ and $\mathrm{BoundedOrderHom\_\_map\_bot'}$ applied to $f$.
BoundedOrderHom.toTopHomdefMathlib.Order.Hom.Bounded, function or constantWording
the top homomorphism of f (from the name)
English
Let $f$ be a bounded order homomorphism of $x$ and $x_{1}$. Then the top homomorphism of $f$ is a top homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toOrderHom}$ applied to $f$ and $\mathrm{BoundedOrderHom\_\_map\_top'}$ applied to $f$.
BoundedOrderHomClassclassMathlib.Order.Hom.Bounded, predicateEnglish
Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{BoundedOrderHomClass}$ holds for $F$, $x$ and $x_{1}$.
BoundedOrderHomClass.toBoundedOrderHomdefMathlib.Order.Hom.Bounded, function or constantWording
the bounded order homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the bounded order homomorphism of $f$ is a bounded order homomorphism of $x$ and $x_{1}$.
TopHomstructureMathlib.Order.Hom.Bounded, typeWording
top homomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the top homomorphisms of $x$ and $x_{1}$ are a basic type.
TopHom.compdefMathlib.Order.Hom.Bounded, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a top homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a top homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a top homomorphism of $x$ and $x_{2}$.
TopHom.copydefMathlib.Order.Hom.Bounded, function or constantWording
the copy of f and h (from the name)
English
Let $f$ be a top homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a top homomorphism of $x$ and $x_{1}$.
TopHom.dualdefMathlib.Order.Hom.Bounded, function or constantWording
the dual (from the name)
English
The dual is an equivalence from the set of top homomorphisms of $x$ and $x_{1}$ to the set of bottom homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.
TopHom.iddefMathlib.Order.Hom.Bounded, function or constantWording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a top homomorphism of $x$ and $x$.
TopHom.toFundefMathlib.Order.Hom.Bounded, function or constantWording
the top homomorphism of self and x4 (from the name)
English
Let $\mathrm{self}$ be a top homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the top homomorphism of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
TopHomClassclassMathlib.Order.Hom.Bounded, predicateEnglish
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{TopHomClass}$ holds for $F$, $x$ and $x_{1}$.
TopHomClass.toTopHomdefMathlib.Order.Hom.Bounded, function or constantWording
the top homomorphism of f (from the name)
English
Let $f$ be an element of $F$. Then the top homomorphism of $f$ is a top homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{TopHomClass\_\_map\_top}$ applied to $f$.