Definitions: Mathlib.Order, part 4 of 4

399 definitions of 56 modules, Mathlib.Order.Partition.Basic to Mathlib.Order.WithBotTop. ‹ previous next ›

Mathlib.Order.Partition.Basic

PartitionstructureMathlib.Order.Partition.Basic, type
Wording
partition of s (from the name)
English
Let $s$ be an element of $x$. Then the partitions of $s$ are a basic type.
Partition.IsRepFunstructureMathlib.Order.Partition.Basic, predicate
Wording
f is a representation function with respect to P (from the name)
English
Let $P$ be a partition of $u$. Let $f$ be a function from elements of $x$ to elements of $x$. Then we can say that $f$ is a representation function with respect to $P$.
Partition.ReldefMathlib.Order.Partition.Basic, predicate
Wording
no wording
English
Let $P$ be a partition of $s$. Let $a$ and $b$ be elements of $x$. Then $\operatorname{Rel}$ holds for $P$, $a$ and $b$, if there exists an element $t$ of $\wp x$, such that $t$ is an element of $P$, $a$ is an element of $t$ and $b$ is an element of $t$.
Partition.copydefMathlib.Order.Partition.Basic, function or constant
Wording
the copy of P and hst (from the name)
English
Let $P$ be a partition of $s$. Assume that $\EqtMACRoH {s}{t}$. Then the copy of $P$ and $\mathrm{hst}$ is a partition of $t$.
Partition.partOfdefMathlib.Order.Partition.Basic, function or constant
Wording
the part of P and a (from the docstring)
English
Let $P$ be a partition of $u$. Let $a$ be an element of $x$. Then the part of $P$ and $a$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to $\operatorname{Rel}$ applied to $P$, $a$ and $b$.
Partition.partsdefMathlib.Order.Partition.Basic, function or constant
Wording
the collection of parts of self (from the docstring)
English
Let $\mathrm{self}$ be a partition of $s$. Then the collection of parts of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Partition.partscopyEquivdefMathlib.Order.Partition.Basic, function or constant
Wording
no wording
English
Let $P$ be a partition of $s$. Assume that $\EqtMACRoH {s}{t}$. Then $\operatorname{partscopyEquiv}$ applied to $P$ and $\mathrm{hst}$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{copy} (P , \mathrm{hst})}{x_{2}})})}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {P}{x_{3}})})}$.
Partition.removeBotdefMathlib.Order.Partition.Basic, function or constant
Wording
no wording
English
Let $P$ be an element of $\wp x$ such that $\mathrm{sSupIndep}$ holds for $P$ and the supremum of $P$ is equal to $s$. Then $\operatorname{removeBot}$ applied to $P$, $\mathrm{indep}$ and $\mathrm{hsSup}$ is a partition of $s$.
Partition.repdefMathlib.Order.Partition.Basic, function or constant
Wording
the representation of P and ht (from the name)
English
Let $P$ be a partition of $u$ such that $t$ is an element of $P$. Then the representation of $P$ and $\mathrm{ht}$ is an element of $x$ defined as $\operatorname{some}$ applied to $\mathrm{Partition\_\_nonempty\_of\_mem}$ applied to $\mathrm{ht}$.

Mathlib.Order.Partition.Equipartition

Finpartition.IsEquipartitiondefMathlib.Order.Partition.Equipartition, predicate
Wording
P is a equipartition (from the name)
English
Let $P$ be a finpartition of $s$. Then $P$ is an equipartition, if $\operatorname{EquitableOn}$ holds for the set of parts of $P$ and $\FinsetcardMACRoM$.

Mathlib.Order.Partition.Finpartition

FinpartitionstructureMathlib.Order.Partition.Finpartition, type
Wording
finpartition of a (from the name)
English
Let $a$ be an element of $x$. Then the finpartitions of $a$ are a basic type.
Finpartition.atomisedefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $s$ be a finite set of $x$. Let $F$ be a finite set of the set of finite sets of $x$. Then $\operatorname{atomise}$ applied to $s$ and $F$ is a finpartition of $s$.
Finpartition.avoiddefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $a$. Let $b$ be an element of $x$. Then $\operatorname{avoid}$ applied to $P$ and $b$ is a finpartition of $\operatorname{sdiff}$ applied to $a$ and $b$.
Finpartition.binddefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $a$. Let $Q$ be a function from elements $i$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $i$ is an element of the set of parts of $P$ to finpartitions of $i$. Then $\operatorname{bind}$ applied to $P$, $i$ and $Q$ is a finpartition of $a$.
Finpartition.combinedefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a function from elements $i$ of $x_{4}$ to finpartitions of $a$ applied to $i$. Assume that $I$ is a supremum independent with respect to $a$. Then $\operatorname{combine}$ applied to $i$, $P$ and $\mathrm{ha}$ is a finpartition of the supremum of $I$ and $a$.
Finpartition.copydefMathlib.Order.Partition.Finpartition, function or constant
Wording
the copy of P and h (from the name)
English
Let $P$ be a finpartition of $a$. Assume that $\EqtMACRoH {a}{b}$. Then the copy of $P$ and $h$ is a finpartition of $b$.
Finpartition.emptydefMathlib.Order.Partition.Finpartition, function or constant
Wording
the empty finpartition of x (from the docstring)
English
Let $x$ be a set. Then the empty finpartition of $x$ is a finpartition of the bottom.
Finpartition.equivSigmaPartsdefMathlib.Order.Partition.Finpartition, function or constant
Wording
the equivalence sigma part of P (from the name)
English
Let $P$ be a finpartition of $s$. Then the equivalence sigma part of $P$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})})}{\Sigma (\lambda t . \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {t}{x_{3}})})}$.
Finpartition.extenddefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $a$. Assume that $b$ is distinct from the bottom. Assume that $a$ is disjoint to $b$. Assume that $\EqtMACRoH {\MaxmaxMACRoAF {a}{b}}{c}$. Then $\operatorname{extend}$ applied to $P$, $\mathrm{hb}$, $\mathrm{hab}$ and $\mathrm{hc}$ is a finpartition of $c$.
Finpartition.extendOfLEdefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $a$. Assume that $a \leq b$. Then $\operatorname{extendOfLE}$ applied to $P$ and $\mathrm{hab}$ is a finpartition of $b$.
Finpartition.indiscretedefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Assume that $a$ is distinct from the bottom. Then $\operatorname{indiscrete}$ applied to $\mathrm{ha}$ is a finpartition of $a$.
Finpartition.mapdefMathlib.Order.Partition.Finpartition, function or constant
Wording
the map of e and P (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{3}$. Let $P$ be a finpartition of $a$. Then the map of $e$ and $P$ is a finpartition of $e$ applied to $a$.
Finpartition.ofErasedefMathlib.Order.Partition.Finpartition, function or constant
Wording
the finpartition of parts (from the name)
English
Let $\mathrm{parts}$ be a finite set of $x$ such that $\mathrm{parts}$ is a supremum independent with respect to $\mathrm{id}$ and the supremum of $\mathrm{parts}$ and $\mathrm{id}$ is equal to $a$. Then the finpartition of $\mathrm{parts}$ is a finpartition of $a$.
Finpartition.ofExistsUniquedefMathlib.Order.Partition.Finpartition, function or constant
Wording
the finpartition of parts (from the name)
English
Let $\mathrm{parts}$ be a finite set of the set of finite sets of $x$ such that for all finite sets $p$ of $x$, if $p$ is an element of $\mathrm{parts}$, then $p \leq s$, for all elements $a$ of $x$, if $a$ is an element of $s$, then $\mathrm{ExistsUnique}$ holds for the function that maps $t$ to the proposition that $t$ is an element of $\mathrm{parts}$ and $a$ is an element of $t$ and $\operatorname{emptyCollection}$ is not an element of $\mathrm{parts}$. Then the finpartition of $\mathrm{parts}$ is a finpartition of $s$.
Finpartition.ofSetSetoiddefMathlib.Order.Partition.Finpartition, function or constant
Wording
the finpartition of s and x2 (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Let $x_{2}$ be a finite set of $x$. Then the finpartition of $s$ and $x_{2}$ is a finpartition of $x_{2}$.
Finpartition.ofSetoiddefMathlib.Order.Partition.Finpartition, function or constant
Wording
the finpartition of s (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Then the finpartition of $s$ is a finpartition of the universal set defined as the finpartition of $s$ and the universal set.
Finpartition.ofSubsetdefMathlib.Order.Partition.Finpartition, function or constant
Wording
the finpartition of P (from the name)
English
Let $P$ be a finpartition of $a$ such that $\mathrm{parts}$ is less than or equal to the set of parts of $P$. Assume that the supremum of $\mathrm{parts}$ and $\mathrm{id}$ is equal to $b$. Then the finpartition of $P$ is a finpartition of $b$.
Finpartition.partdefMathlib.Order.Partition.Finpartition, function or constant
Wording
the part of P and a (from the name)
English
Let $P$ be a finpartition of $s$. Let $a$ be an element of $x$. Then the part of $P$ and $a$ is a finite set of $x$ defined as $\mathrm{dite}$ applied to $\MembershipmemMACRoT {s}{a}$, the function that maps $\mathrm{ha}$ to $\operatorname{choose}$ applied to the function that maps $a_{1}$ to $\MembershipmemMACRoT {a_{1}}{a}$, the set of parts of $P$ and $\mathrm{Finpartition\_\_existsUnique\_mem}$ applied to $P$ and $\mathrm{ha}$ and the function that maps $\mathrm{ha1}$ to $\operatorname{emptyCollection}$.
Finpartition.partsdefMathlib.Order.Partition.Finpartition, function or constant
Wording
the set of parts of self (from the name)
English
Let $\mathrm{self}$ be a finpartition of $a$. Then the set of parts of $\mathrm{self}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Finpartition.restrictdefMathlib.Order.Partition.Finpartition, function or constant
Wording
no wording
English
Let $P$ be a finpartition of $a$. Assume that $b \leq a$. Then $\operatorname{restrict}$ applied to $P$ and $\mathrm{hb}$ is a finpartition of $b$.
Finpartition.toSubtypedefMathlib.Order.Partition.Finpartition, function or constant
Wording
the subtype of P (from the name)
English
Let $P$ be a finpartition of $s$. Assume that for all elements $s_{2}$ and $t_{1}$ of $x$, if $\mathrm{Pr}$ holds for $s_{2}$, then if $\mathrm{Pr}$ holds for $t_{1}$, then $\mathrm{Pr}$ holds for $\MaxmaxMACRoAF {s_{2}}{t_{1}}$. Assume that for all elements $s_{1}$ and $t$ of $x$, if $\mathrm{Pr}$ holds for $s_{1}$, then if $\mathrm{Pr}$ holds for $t$, then $\mathrm{Pr}$ holds for $\MinminMACRoAG {s_{1}}{t}$. Assume that $\mathrm{Pr}$ holds for the bottom. Assume that $\mathrm{Pr}$ holds for $s$. Assume that for all elements $p$ of $x$, if $p$ is an element of the set of parts of $P$, then $\mathrm{Pr}$ holds for $p$. Then the subtype of $P$ is a finpartition of $s$.

Mathlib.Order.PiLex

Pi.LexdefMathlib.Order.PiLex, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements $i_{2}$ of $x$ and elements of $x_{1}$ applied to $i_{2}$ and elements of $x_{1}$ applied to $i_{2}$ to propositions. Let $x_{2}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $y$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\operatorname{Lex}$ holds for $r$, $i_{2}$, $s$, $i_{1}$, $x_{2}$, $i$ and $y$, if there exists an element $i$ of $x$, such that for all elements $j$ of $x$, if $r$ holds for $j$ and $i$, then $\EqtMACRoH {s (j)}{i_{1} (j)}$ and $i_{2}$ holds for $i$, $s$ applied to $i$ and $i_{1}$ applied to $i$.

Mathlib.Order.Preorder.Chain

FlagstructureMathlib.Order.Preorder.Chain, type
Wording
flag of x (from the name)
English
Let $x$ be a set. Then the flags of $x$ are a basic type.
Flag.carrierdefMathlib.Order.Preorder.Chain, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a flag of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Flag.mapdefMathlib.Order.Preorder.Chain, function or constant
Wording
the map of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the map of $e$ is an equivalence from the set of flags of $x$ to the set of flags of $x_{1}$.
Flag.ofIsMaxChaindefMathlib.Order.Preorder.Chain, function or constant
Wording
the flag of c and hc (from the name)
English
Let $c$ be an element of $\wp x$ such that $\mathrm{IsMaxChain}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $c$. Then the flag of $c$ and $\mathrm{hc}$ is a flag of $x$.
IsChaindefMathlib.Order.Preorder.Chain, predicate
Wording
no wording
English
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{IsChain}$ holds for $r$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the function that maps $x_{1}$ and $y$ to the proposition that $r$ holds for $x_{1}$ and $y$ or $r$ holds for $y$ and $x_{1}$.
IsMaxChaindefMathlib.Order.Preorder.Chain, predicate
Wording
no wording
English
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{IsMaxChain}$ holds for $r$ and $s$, if $\mathrm{IsChain}$ holds for $r$ and $s$ and for all elements $t$ of $\wp x$, if $\mathrm{IsChain}$ holds for $r$ and $t$, then if $s \leq t$, then $\EqtMACRoH {s}{t}$.
SuccChaindefMathlib.Order.Preorder.Chain, function or constant
Wording
the successor chain of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then the successor chain of $r$ and $s$ is an element of $\wp x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $t$ of $\wp x$, such that $\mathrm{IsChain}$ holds for $r$ and $s$ and $\mathrm{SuperChain}$ holds for $r$, $s$ and $t$, the function that maps $h$ to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to $s$.
SuperChaindefMathlib.Order.Preorder.Chain, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ and $t$ be elements of $\wp x$. Then $\mathrm{SuperChain}$ holds for $r$, $s$ and $t$, if $\mathrm{IsChain}$ holds for $r$ and $t$ and $s < t$.

Mathlib.Order.Preorder.Finsupp

Finsupp.orderEmbeddingToFundefMathlib.Order.Preorder.Finsupp, function or constant
Wording
the order embedding to function (from the name)
English
The order embedding to function is an order embedding of $\FinsuppMACRoQ {x}{M}$ and the set of functions from elements of $x$ to elements of $M$.
Finsupp.orderIsoFunOnFinitedefMathlib.Order.Preorder.Finsupp, function or constant
Wording
no wording
English
$\operatorname{orderIsoFunOnFinite}$ is an order isomorphism of $\FinsuppMACRoQ {x}{M}$ and the set of functions from elements of $x$ to elements of $M$.

Mathlib.Order.PrimeIdeal

Order.Ideal.IsPrimeclassMathlib.Order.PrimeIdeal, predicate
Wording
I is prime (from the name)
English
Let $I$ be an ideal of $P$. Then we can say that $I$ is prime.
Order.Ideal.IsPrime.toPrimePairdefMathlib.Order.PrimeIdeal, function or constant
Wording
the prime pair of h (from the name)
English
Assume that $I$ is prime. Then the prime pair of $h$ is a prime pair of $P$.
Order.Ideal.PrimePairstructureMathlib.Order.PrimeIdeal, type
Wording
prime pair of P (from the name)
English
Let $P$ be a set. Then the prime pairs of $P$ are a basic type.
Order.Ideal.PrimePair.FdefMathlib.Order.PrimeIdeal, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a prime pair of $P$. Then $\operatorname{F}$ applied to $\mathrm{self}$ is a filter of $P$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Order.Ideal.PrimePair.IdefMathlib.Order.PrimeIdeal, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be a prime pair of $P$. Then $\operatorname{I}$ applied to $\mathrm{self}$ is an ideal of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Order.PFilter.IsPrimeclassMathlib.Order.PrimeIdeal, predicate
Wording
F is prime (from the name)
English
Let $F$ be a filter of $P$. Then we can say that $F$ is prime.
Order.PFilter.IsPrime.toPrimePairdefMathlib.Order.PrimeIdeal, function or constant
Wording
the prime pair of h (from the name)
English
Assume that $F$ is prime. Then the prime pair of $h$ is a prime pair of $P$.

Mathlib.Order.Prod.Lex.Hom

Prod.Lex.toLexOrderHomdefMathlib.Order.Prod.Lex.Hom, function or constant
Wording
the lexicographic order homomorphism (from the name)
English
The lexicographic order homomorphism is an order homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $\mathrm{toLex}$ and $\mathrm{Prod\_\_Lex\_\_toLex\_mono}$.

Mathlib.Order.Radical

Order.radicaldefMathlib.Order.Radical, function or constant
Wording
the radical of x (from the name)
English
Let $x$ be a set. Then the radical of $x$ is an element of $x$ defined as the infimum of the function that maps $a$ to the infimum of the function that maps $h$ to $a$.

Mathlib.Order.Rel.GaloisConnection

SetRel.equivFixedPointsdefMathlib.Order.Rel.GaloisConnection, function or constant
Wording
the equivalence fixed point of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the equivalence fixed point of $R$ is an equivalence from the set of elements of the left fixed point of $R$ to the set of elements of the right fixed point of $R$.
SetRel.leftDualdefMathlib.Order.Rel.GaloisConnection, function or constant
Wording
the left dual of R and J (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $J$ be an element of $\wp x$. Then the left dual of $R$ and $J$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that for all elements $a$ of $x$, if $a$ is an element of $J$, then $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.leftFixedPointsdefMathlib.Order.Rel.GaloisConnection, function or constant
Wording
the left fixed point of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the left fixed point of $R$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $J$ to the proposition that the right dual of $R$ and the left dual of $R$ and $J$ is equal to $J$.
SetRel.rightDualdefMathlib.Order.Rel.GaloisConnection, function or constant
Wording
the right dual of R and I (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $I$ be an element of $\wp x_{1}$. Then the right dual of $R$ and $I$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that for all elements $b$ of $x_{1}$, if $b$ is an element of $I$, then $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.rightFixedPointsdefMathlib.Order.Rel.GaloisConnection, function or constant
Wording
the right fixed point of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the right fixed point of $R$ is an element of $\wp (\wp x_{1})$ defined as $\operatorname{ofPred}$ applied to the function that maps $I$ to the proposition that the left dual of $R$ and the right dual of $R$ and $I$ is equal to $I$.

Mathlib.Order.RelClasses

IsNonstrictStrictOrderclassMathlib.Order.RelClasses, predicate
Wording
no wording
English
Let $x$ be a set. Let $r$ be an element of $\mathrm{semiOutParam}$ applied to the set of functions from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x$ and elements of $x$ to propositions. Then we can say that $\mathrm{IsNonstrictStrictOrder}$ holds for $x$, $r$ and $s$.
IsOrderConnectedclassMathlib.Order.RelClasses, predicate
Wording
no wording
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{IsOrderConnected}$ holds for $x$ and $\mathrm{lt}$.
IsWellOrderclassMathlib.Order.RelClasses, predicate
Wording
no wording
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 $\mathrm{IsWellOrder}$ holds for $x$ and $r$.
Set.BoundeddefMathlib.Order.RelClasses, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\operatorname{Bounded}$ holds for $r$ and $s$, if there exists an element $a$ of $x$, such that for all elements $b$ of $x$, if $b$ is an element of $s$, then $r$ holds for $b$ and $a$.
Set.UnboundeddefMathlib.Order.RelClasses, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\operatorname{Unbounded}$ holds for $r$ and $s$, if for all elements $a$ of $x$, there exists an element $b$ of $x$, such that $b$ is an element of $s$ and it is not the case that $r$ holds for $b$ and $a$.
WellFounded.fix'defMathlib.Order.RelClasses, function or constant
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $\mathrm{ind}$ be a function from elements $x_{2}$ of $x$ and functions from elements $y$ of $x$ and elements of $\mathrm{Proof}$ applied to $r$ applied to $y$ and $x_{2}$ to elements of $\mathrm{motive}$ applied to $y$ to elements of $\mathrm{motive}$ applied to $x_{2}$. Let $x_{1}$ be an element of $x$. Then $\operatorname{fix'}$ applied to $r$, $x_{2}$, $\mathrm{ind}$ and $x_{1}$ is an element of $\mathrm{motive}$ applied to $x_{1}$ defined as the function that maps $x_{1}$ to $\operatorname{fix}$ applied to $i$, $x_{2}$, $\mathrm{ind}$ and $x_{1}$.
WellFoundedGTdefMathlib.Order.RelClasses, predicate
Wording
no wording
English
Let $x$ be a set. Then $\mathrm{WellFoundedGT}$ holds for $x$, if $\mathrm{WellFounded}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{3} , x_{2})$.
WellFoundedGT.fixdefMathlib.Order.RelClasses, function or constant
Wording
no wording
English
Let $\mathrm{ind}$ be a function from elements $x_{3}$ of $x$ and functions from elements $y$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (x_{3} , y)$ to elements of $\mathrm{motive}$ applied to $y$ to elements of $\mathrm{motive}$ applied to $x_{3}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{fix}$ applied to $x_{3}$, $\mathrm{ind}$ and $x_{2}$ is an element of $\mathrm{motive}$ applied to $x_{2}$ defined as the function that maps $x_{2}$ to $\operatorname{fix'}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{3} , x_{2})$, $x_{3}$, $\mathrm{ind}$ and $x_{2}$.
WellFoundedLTdefMathlib.Order.RelClasses, predicate
Wording
no wording
English
Let $x$ be a set. Then $\mathrm{WellFoundedLT}$ holds for $x$, if $\mathrm{WellFounded}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$.
WellFoundedLT.fixdefMathlib.Order.RelClasses, function or constant
Wording
no wording
English
Let $\mathrm{ind}$ be a function from elements $x_{3}$ of $x$ and functions from elements $y$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (y , x_{3})$ to elements of $\mathrm{motive}$ applied to $y$ to elements of $\mathrm{motive}$ applied to $x_{3}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{fix}$ applied to $x_{3}$, $\mathrm{ind}$ and $x_{2}$ is an element of $\mathrm{motive}$ applied to $x_{2}$ defined as the function that maps $x_{2}$ to $\operatorname{fix'}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$, $x_{3}$, $\mathrm{ind}$ and $x_{2}$.

Mathlib.Order.RelIso.Basic

Quotient.mkRelHomdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism of H (from the name)
English
Assume that for all elements $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $x$, if $\operatorname{Equiv}$ holds for $x_{2}$ and $x_{4}$, then if $\operatorname{Equiv}$ holds for $x_{3}$ and $x_{5}$, then $\EqtMACRoH {r (x_{2} , x_{3})}{r (x_{4} , x_{5})}$. Then the relation homomorphism of $H$ is a relation homomorphism of $r$ and $\mathrm{Quotient\_\_lift\_u2082\_}$ applied to $r$ and $H$.
Quotient.outRelEmbeddingdefMathlib.Order.RelIso.Basic, function or constant
Wording
no wording
English
Assume that for all elements $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ of $x$, if $\operatorname{Equiv}$ holds for $x_{2}$ and $x_{4}$, then if $\operatorname{Equiv}$ holds for $x_{3}$ and $x_{5}$, then $\EqtMACRoH {r (x_{2} , x_{3})}{r (x_{4} , x_{5})}$. Then $\operatorname{outRelEmbedding}$ applied to $H$ is a relation embedding of $\mathrm{Quotient\_\_lift\_u2082\_}$ applied to $r$ and $H$ and $r$.
RelEmbeddingstructureMathlib.Order.RelIso.Basic, type
Wording
relation embedding of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation embeddings of $r$ and $s$ are a basic type.
RelEmbedding.ofIsEmptydefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation embedding of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation embedding of $r$ and $s$ is a relation embedding of $r$ and $s$.
RelEmbedding.ofMapRelIffdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation 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$, $s$ holds for $f$ applied to $a$ and $f$ applied to $b$, if and only if $r$ holds for $a$ and $b$. Then the relation embedding of $f$ and $\mathrm{hf}$ is a relation embedding of $r$ and $s$.
RelEmbedding.ofMonotonedefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation 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 for all elements $a$ and $b$ of $x$, if $r$ holds for $a$ and $b$, then $s$ holds for $f$ applied to $a$ and $f$ applied to $b$. Then the relation embedding of $f$ and $H$ is a relation embedding of $r$ and $s$.
RelEmbedding.ofOnFundefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation embedding of r and f (from the name)
English
Let $r$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $f$ be an embedding of $x$ and $x_{1}$. Then the relation embedding of $r$ and $f$ is a relation embedding of $\operatorname{onFun}$ applied to $r$ and $\operatorname{coe}$ applied to $f$ and $r$.
RelEmbedding.preimagedefMathlib.Order.RelIso.Basic, function or constant
Wording
the preimage of f and s (from the name)
English
Let $f$ be an embedding of $x$ and $x_{1}$. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the preimage of $f$ and $s$ is a relation embedding of $\operatorname{Preimage}$ applied to $\operatorname{coe}$ applied to $f$ and $s$ and $s$.
RelEmbedding.prodLexMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the product lexicographic map of f and g (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Let $g$ be a relation embedding of $t$ and $u$. Then the product lexicographic map of $f$ and $g$ is a relation embedding of $\operatorname{Lex}$ applied to $r$ and $t$ and $\operatorname{Lex}$ applied to $s$ and $u$.
RelEmbedding.prodLexMkLeftdefMathlib.Order.RelIso.Basic, function or constant
Wording
no wording
English
Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Assume that it is not the case that $r$ holds for $a$ and $a$. Then $\operatorname{prodLexMkLeft}$ applied to $s$ and $h$ is a relation embedding of $s$ and $\operatorname{Lex}$ applied to $r$ and $s$.
RelEmbedding.prodLexMkRightdefMathlib.Order.RelIso.Basic, function or constant
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Assume that it is not the case that $s$ holds for $b$ and $b$. Then $\operatorname{prodLexMkRight}$ applied to $r$ and $h$ is a relation embedding of $r$ and $\operatorname{Lex}$ applied to $r$ and $s$.
RelEmbedding.refldefMathlib.Order.RelIso.Basic, function or constant
Wording
the identity of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the identity of $r$ is a relation embedding of $r$ and $r$.
RelEmbedding.sumLexInldefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lexicographic left injection of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the sum lexicographic left injection of $r$ and $s$ is a relation embedding of $r$ and $\operatorname{Lex}$ applied to $r$ and $s$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inl}$ and $\mathrm{Sum\_\_inl\_injective}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Sum\_\_lex\_inl\_inl}$.
RelEmbedding.sumLexInrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lexicographic right injection of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the sum lexicographic right injection of $r$ and $s$ is a relation embedding of $s$ and $\operatorname{Lex}$ applied to $r$ and $s$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inr}$ and $\mathrm{Sum\_\_inr\_injective}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Sum\_\_lex\_inr\_inr}$.
RelEmbedding.sumLexMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lexicographic map of f and g (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Let $g$ be a relation embedding of $t$ and $u$. Then the sum lexicographic map of $f$ and $g$ is a relation embedding of $\operatorname{Lex}$ applied to $r$ and $t$ and $\operatorname{Lex}$ applied to $s$ and $u$.
RelEmbedding.sumLiftRelInldefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lift relative left injection of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the sum lift relative left injection of $r$ and $s$ is a relation embedding of $r$ and $\operatorname{LiftRel}$ applied to $r$ and $s$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inl}$ and $\mathrm{Sum\_\_inl\_injective}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Sum\_\_liftRel\_inl\_inl}$.
RelEmbedding.sumLiftRelInrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lift relative right injection of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the sum lift relative right injection of $r$ and $s$ is a relation embedding of $s$ and $\operatorname{LiftRel}$ applied to $r$ and $s$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{inr}$ and $\mathrm{Sum\_\_inr\_injective}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Sum\_\_liftRel\_inr\_inr}$.
RelEmbedding.sumLiftRelMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lift relative map of f and g (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Let $g$ be a relation embedding of $t$ and $u$. Then the sum lift relative map of $f$ and $g$ is a relation embedding of $\operatorname{LiftRel}$ applied to $r$ and $t$ and $\operatorname{LiftRel}$ applied to $s$ and $u$.
RelEmbedding.swapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap of f (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Then the swap of $f$ is a relation embedding of $\operatorname{swap}$ and $\operatorname{swap}$ defined as $\operatorname{mk}$ applied to $\operatorname{toEmbedding}$ applied to $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelEmbedding\_\_map\_rel\_iff}$ applied to $f$.
RelEmbedding.swapEquivdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap equivalence (from the name)
English
The swap equivalence is an equivalence from the set of relation embeddings of $r$ and $s$ to the set of relation embeddings of $\operatorname{swap}$ and $\operatorname{swap}$.
RelEmbedding.toMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the map of r and f (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be an embedding of $x$ and $x_{1}$. Then the map of $r$ and $f$ is a relation embedding of $r$ and $\operatorname{Map}$ applied to $r$, $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.
RelEmbedding.toRelHomdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism of f (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Then the relation homomorphism of $f$ is a relation homomorphism of $r$ and $s$.
RelEmbedding.transdefMathlib.Order.RelIso.Basic, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$. Let $g$ be a relation embedding of $s$ and $t$. Then the composition of $f$ and $g$ is a relation embedding of $r$ and $t$.
RelHomstructureMathlib.Order.RelIso.Basic, type
Wording
relation homomorphism of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation homomorphisms of $r$ and $s$ are a basic type.
RelHom.compdefMathlib.Order.RelIso.Basic, function or constant
Wording
the composition of g and f (from the name)
English
Let $g$ be a relation homomorphism of $s$ and $t$. Let $f$ be a relation homomorphism of $r$ and $s$. Then the composition of $g$ and $f$ is a relation homomorphism of $r$ and $t$.
RelHom.iddefMathlib.Order.RelIso.Basic, function or constant
Wording
the identity of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the identity of $r$ is a relation homomorphism of $r$ and $r$ defined as $\operatorname{mk}$ applied to the function that maps $x_{1}$ to $x_{1}$ and the function that maps $x_{2}$, $x_{3}$ and $x_{4}$ to $x_{4}$.
RelHom.ofLEdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism of le (from the name)
English
Assume that $r \leq \mathrm{r'}$. Then the relation homomorphism of $\mathrm{le}$ is a relation homomorphism of $r$ and $\mathrm{r'}$ defined as $\operatorname{mk}$ applied to $\mathrm{id}$ and $\mathrm{le}$.
RelHom.ofOnFundefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism of r and f (from the name)
English
Let $r$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the relation homomorphism of $r$ and $f$ is a relation homomorphism of $\operatorname{onFun}$ applied to $r$ and $f$ and $r$.
RelHom.preimagedefMathlib.Order.RelIso.Basic, function or constant
Wording
the preimage of f and s (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the preimage of $f$ and $s$ is a relation homomorphism of $\operatorname{Preimage}$ applied to $f$ and $s$ and $s$.
RelHom.swapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap of f (from the name)
English
Let $f$ be a relation homomorphism of $r$ and $s$. Then the swap of $f$ is a relation homomorphism of $\operatorname{swap}$ and $\operatorname{swap}$ defined as $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelHom\_\_map\_rel}$ applied to $f$.
RelHom.swapEquivdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap equivalence (from the name)
English
The swap equivalence is an equivalence from the set of relation homomorphisms of $r$ and $s$ to the set of relation homomorphisms of $\operatorname{swap}$ and $\operatorname{swap}$.
RelHom.toFundefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism of self and x2 (from the name)
English
Let $\mathrm{self}$ be a relation homomorphism of $r$ and $s$. Let $x_{2}$ be an element of $x$. Then the relation homomorphism of $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
RelHom.toMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the map of r and f (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $r$ and $f$ is a relation homomorphism of $r$ and $\operatorname{Map}$ applied to $r$, $f$ and $f$.
RelHomClassclassMathlib.Order.RelIso.Basic, predicate
Wording
no wording
English
Let $F$ be a set. Let $r$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then we can say that $\mathrm{RelHomClass}$ holds for $F$, $r$ and $s$.
RelIsostructureMathlib.Order.RelIso.Basic, type
Wording
relation isomorphism of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation isomorphisms of $r$ and $s$ are a basic type.
RelIso.castdefMathlib.Order.RelIso.Basic, function or constant
Wording
the cast of h and h1 (from the name)
English
Assume that $\EqtMACRoH {x}{x_{1}}$. Assume that $\mathrm{HEq}$ holds for $r$ and $s$. Then the cast of $h$ and $h_{1}$ is a relation isomorphism of $r$ and $s$.
RelIso.compldefMathlib.Order.RelIso.Basic, function or constant
Wording
the complement of f (from the name)
English
Let $f$ be a relation isomorphism of $r$ and $s$. Then the complement of $f$ is a relation isomorphism of the complement of $r$ and the complement of $s$.
RelIso.complEquivdefMathlib.Order.RelIso.Basic, function or constant
Wording
the complement equivalence (from the name)
English
The complement equivalence is an equivalence from the set of relation isomorphisms of $r$ and $s$ to the set of relation isomorphisms of the complement of $r$ and the complement of $s$.
RelIso.copydefMathlib.Order.RelIso.Basic, function or constant
Wording
the copy of f and g (from the name)
English
Let $e$ be a relation isomorphism of $r$ and $s$. 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$. Assume that $f$ is equal to $\operatorname{coe}$ applied to $e$. Assume that $g$ is equal to $\operatorname{coe}$ applied to the inverse of $e$. Then the copy of $f$ and $g$ is a relation isomorphism of $r$ and $s$.
RelIso.embeddingSurjectiveEquivIsodefMathlib.Order.RelIso.Basic, function or constant
Wording
the embedding surjective equivalence isomorphism (from the name)
English
The embedding surjective equivalence isomorphism is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\operatorname{Surjective} (\operatorname{coe} (f))})}{\mathrm{RelIso} (r , s)}$.
RelIso.emptySumLexdefMathlib.Order.RelIso.Basic, function or constant
Wording
the lexicographic sum of r and s (from the docstring)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the lexicographic sum of $r$ and $s$ is a relation isomorphism of $\operatorname{Lex}$ applied to $r$ and $s$ and $s$.
RelIso.ofOnFundefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism of r and f (from the name)
English
Let $r$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $f$ be an equivalence from $x$ to $x_{1}$. Then the relation isomorphism of $r$ and $f$ is a relation isomorphism of $\operatorname{onFun}$ applied to $r$ and $\operatorname{coe}$ applied to $f$ and $r$.
RelIso.ofSurjectivedefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism of f and H (from the name)
English
Let $f$ be a relation embedding of $r$ and $s$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the relation isomorphism of $f$ and $H$ is a relation isomorphism of $r$ and $s$ defined as $\operatorname{mk}$ applied to the equivalence of $\operatorname{toEmbedding}$ applied to $f$ and $H$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelEmbedding\_\_map\_rel\_iff}$ applied to $f$.
RelIso.ofUniqueOfIrrefldefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation isomorphism of $r$ and $s$ is a relation isomorphism of $r$ and $s$.
RelIso.ofUniqueOfRefldefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation isomorphism of $r$ and $s$ is a relation isomorphism of $r$ and $s$.
RelIso.preimagedefMathlib.Order.RelIso.Basic, function or constant
Wording
the preimage of f and s (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the preimage of $f$ and $s$ is a relation isomorphism of $\operatorname{Preimage}$ applied to $\operatorname{coe}$ applied to $f$ and $s$ and $s$.
RelIso.prodLexCongrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the product lexicographic congruence of x8 and x9 (from the name)
English
Let $x_{8}$ be a relation isomorphism of $x_{4}$ and $x_{6}$. Let $x_{9}$ be a relation isomorphism of $x_{5}$ and $x_{7}$. Then the product lexicographic congruence of $x_{8}$ and $x_{9}$ is a relation isomorphism of $\operatorname{Lex}$ applied to $x_{4}$ and $x_{5}$ and $\operatorname{Lex}$ applied to $x_{6}$ and $x_{7}$.
RelIso.refldefMathlib.Order.RelIso.Basic, function or constant
Wording
the identity of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the identity of $r$ is a relation isomorphism of $r$ and $r$.
RelIso.relEmbeddingCongrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation embedding congruence of x8 and x9 (from the name)
English
Let $x_{8}$ be a relation isomorphism of $x_{4}$ and $x_{6}$. Let $x_{9}$ be a relation isomorphism of $x_{5}$ and $x_{7}$. Then the relation embedding congruence of $x_{8}$ and $x_{9}$ is an equivalence from the set of relation embeddings of $x_{4}$ and $x_{5}$ to the set of relation embeddings of $x_{6}$ and $x_{7}$.
RelIso.relHomCongrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation homomorphism congruence of x8 and x9 (from the name)
English
Let $x_{8}$ be a relation isomorphism of $x_{4}$ and $x_{6}$. Let $x_{9}$ be a relation isomorphism of $x_{5}$ and $x_{7}$. Then the relation homomorphism congruence of $x_{8}$ and $x_{9}$ is an equivalence from the set of relation homomorphisms of $x_{4}$ and $x_{5}$ to the set of relation homomorphisms of $x_{6}$ and $x_{7}$.
RelIso.relIsoCongrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism congruence of x8 and x9 (from the name)
English
Let $x_{8}$ be a relation isomorphism of $x_{4}$ and $x_{6}$. Let $x_{9}$ be a relation isomorphism of $x_{5}$ and $x_{7}$. Then the relation isomorphism congruence of $x_{8}$ and $x_{9}$ is an equivalence from the set of relation isomorphisms of $x_{4}$ and $x_{5}$ to the set of relation isomorphisms of $x_{6}$ and $x_{7}$.
RelIso.relIsoOfIsEmptydefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation isomorphism of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then the relation isomorphism of $r$ and $s$ is a relation isomorphism of $r$ and $s$.
RelIso.sumLexCongrdefMathlib.Order.RelIso.Basic, function or constant
Wording
the sum lexicographic congruence of x8 and x9 (from the name)
English
Let $x_{8}$ be a relation isomorphism of $x_{4}$ and $x_{6}$. Let $x_{9}$ be a relation isomorphism of $x_{5}$ and $x_{7}$. Then the sum lexicographic congruence of $x_{8}$ and $x_{9}$ is a relation isomorphism of $\operatorname{Lex}$ applied to $x_{4}$ and $x_{5}$ and $\operatorname{Lex}$ applied to $x_{6}$ and $x_{7}$.
RelIso.sumLexEmptydefMathlib.Order.RelIso.Basic, function or constant
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then $\operatorname{sumLexEmpty}$ applied to $r$ and $s$ is a relation isomorphism of $\operatorname{Lex}$ applied to $r$ and $s$ and $r$.
RelIso.swapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap of f (from the name)
English
Let $f$ be a relation isomorphism of $r$ and $s$. Then the swap of $f$ is a relation isomorphism of $\operatorname{swap}$ and $\operatorname{swap}$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelIso\_\_map\_rel\_iff}$ applied to $f$.
RelIso.swapEquivdefMathlib.Order.RelIso.Basic, function or constant
Wording
the swap equivalence (from the name)
English
The swap equivalence is an equivalence from the set of relation isomorphisms of $r$ and $s$ to the set of relation isomorphisms of $\operatorname{swap}$ and $\operatorname{swap}$.
RelIso.symmdefMathlib.Order.RelIso.Basic, function or constant
Wording
the inverse of f (from the name)
English
Let $f$ be a relation isomorphism of $r$ and $s$. Then the inverse of $f$ is a relation isomorphism of $s$ and $r$.
RelIso.toMapdefMathlib.Order.RelIso.Basic, function or constant
Wording
the map of r and f (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $f$ be an equivalence from $x$ to $x_{1}$. Then the map of $r$ and $f$ is a relation isomorphism of $r$ and $\operatorname{Map}$ applied to $r$, $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $f$.
RelIso.toRelEmbeddingdefMathlib.Order.RelIso.Basic, function or constant
Wording
the relation embedding of f (from the name)
English
Let $f$ be a relation isomorphism of $r$ and $s$. Then the relation embedding of $f$ is a relation embedding of $r$ and $s$ defined as $\operatorname{mk}$ applied to the embedding of $\operatorname{toEquiv}$ applied to $f$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelIso\_\_map\_rel\_iff'}$ applied to $f$.
RelIso.transdefMathlib.Order.RelIso.Basic, function or constant
Wording
the composition of x3 and x4 (from the name)
English
Let $x_{3}$ be a relation isomorphism of $r$ and $s$. Let $x_{4}$ be a relation isomorphism of $s$ and $t$. Then the composition of $x_{3}$ and $x_{4}$ is a relation isomorphism of $r$ and $t$.
Subtype.relEmbeddingdefMathlib.Order.RelIso.Basic, function or constant
Wording
the induced relation of r and p (from the docstring)
English
Let $r$ and $p$ be functions from elements of $X$ and elements of $X$ to propositions. Then the induced relation of $r$ and $p$ is a relation embedding of $\operatorname{Preimage}$ applied to $p$ and $r$ and $r$.

Mathlib.Order.RelIso.Set

RelEmbedding.codRestrictdefMathlib.Order.RelIso.Set, function or constant
Wording
no wording
English
Let $p$ be an element of $\wp x_{1}$. Let $f$ be a relation embedding of $r$ and $s$ such that for all elements $a$ of $x$, $\MembershipmemMACRoT {p}{f (a)}$. Then $\operatorname{codRestrict}$ applied to $p$, $f$ and $H$ is a relation embedding of $r$ and $\mathrm{Subrel}$ applied to $s$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {p}{x_{2}}$ defined as $\operatorname{mk}$ applied to $\operatorname{codRestrict}$ applied to $p$, $\operatorname{toEmbedding}$ applied to $f$ and $H$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{RelEmbedding\_\_map\_rel\_iff'}$ applied to $f$.
RelIso.subrelUnivIsodefMathlib.Order.RelIso.Set, function or constant
Wording
no wording
English
Assume that for all elements $x_{1}$ of $x$, $p$ holds for $x_{1}$. Then $\operatorname{subrelUnivIso}$ applied to $h$ is a relation isomorphism of $\mathrm{Subrel}$ applied to $r$ and $p$ and $r$.
SubreldefMathlib.Order.RelIso.Set, predicate
Wording
no wording
English
Let $r$ and $p$ be functions from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ be an element of $\SubtypeSet {x_{4}}{p (x_{4})}$. Let $x_{2}$ be an element of $\SubtypeSet {x_{3}}{p (x_{3})}$. Then $\mathrm{Subrel}$ holds for $r$, $p$, $x_{1}$ and $x_{2}$, if $\operatorname{Preimage}$ holds for $p$, $r$, $x_{1}$ and $x_{2}$.
Subrel.inclusionEmbeddingdefMathlib.Order.RelIso.Set, function or constant
Wording
the inclusion embedding of r and h (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Assume that $s \leq t$. Then the inclusion embedding of $r$ and $h$ is a relation embedding of $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {t}{x_{2}}$.
Subrel.relEmbeddingdefMathlib.Order.RelIso.Set, function or constant
Wording
the relation embedding of r and p (from the name)
English
Let $r$ and $p$ be functions from elements of $x$ and elements of $x$ to propositions. Then the relation embedding of $r$ and $p$ is a relation embedding of $\mathrm{Subrel}$ applied to $r$ and $p$ and $r$.

Mathlib.Order.RelSeries

FiniteDimensionalOrderdefMathlib.Order.RelSeries, predicate
Wording
x is a finite dimensional order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a finite dimensional order.
InfiniteDimensionalOrderdefMathlib.Order.RelSeries, predicate
Wording
x is a infinite dimensional order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an infinite dimensional order.
LTSeriesdefMathlib.Order.RelSeries, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\mathrm{LTSeries}$ applied to $x$ are a basic type.
LTSeries.comapdefMathlib.Order.RelSeries, function or constant
Wording
the preimage of p and f (from the name)
English
Let $p$ be an element of $\mathrm{LTSeries}$ applied to $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that for all elements $x_{4}$ of $x$, for all elements $y$ of $x$, if $f (x_{4})< f (y)$, then $x_{4} < y$ and $\operatorname{Surjective}$ holds for $f$. Then the preimage of $p$ and $f$ is an element of $\mathrm{LTSeries}$ applied to $x$.
LTSeries.injStrictMonodefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $n$ be a natural number. Then $\operatorname{injStrictMono}$ applied to $n$ is an embedding of $\SubtypeSet {f}{\mathrm{StrictMono} (\operatorname{snd} (f))}$ and $\mathrm{LTSeries}$ applied to $x$.
LTSeries.longestOfdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\operatorname{longestOf}$ applied to $x$ is an element of $\mathrm{LTSeries}$ applied to $x$.
LTSeries.mapdefMathlib.Order.RelSeries, function or constant
Wording
the map of p and f (from the name)
English
Let $p$ be an element of $\mathrm{LTSeries}$ applied to $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{StrictMono}$ holds for $f$. Then the map of $p$ and $f$ is an element of $\mathrm{LTSeries}$ applied to $x_{1}$.
LTSeries.mkdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $\mathrm{length}$ be a natural number. Let $\mathrm{toFun}$ be a function from elements of $\mathrm{Fin}$ applied to $\mathrm{length} + 1$ to elements of $x$ such that $\mathrm{StrictMono}$ holds for $\mathrm{toFun}$. Then $\operatorname{mk}$ applied to $\mathrm{length}$, $\mathrm{toFun}$ and $\mathrm{strictMono}$ is an element of $\mathrm{LTSeries}$ applied to $x$.
LTSeries.rangedefMathlib.Order.RelSeries, function or constant
Wording
the range of n (from the name)
English
Let $n$ be a natural number. Then the range of $n$ is an element of $\mathrm{LTSeries}$ applied to $\Natural$.
LTSeries.withLengthdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $x$ be a set. Let $n$ be a natural number. Then $\operatorname{withLength}$ applied to $x$ and $n$ is an element of $\mathrm{LTSeries}$ applied to $x$.
RelSeriesstructureMathlib.Order.RelSeries, type
Wording
relation series of r (from the name)
English
Let $r$ be a set relation of $x$ and $x$. Then the relation series of $r$ are a basic type.
RelSeries.EquivdefMathlib.Order.RelSeries, function or constant
Wording
the equivalence (from the name)
English
The equivalence is an equivalence from the set of relation series of $r$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $x_{1} \neq \operatorname{nil}$ and $\operatorname{IsChain}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\MembershipmemMACRoT {r}{(\ProdmkMACRoU {x_{2}}{x_{3}})}$ and $x_{1}$.
RelSeries.appenddefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ and $q$ be relation series of $r$ such that $\MembershipmemMACRoT {r}{\ProdmkMACRoU {\operatorname{last} (p)}{\operatorname{head} (q)}}$. Then $\operatorname{append}$ applied to $p$, $q$ and $\mathrm{connect}$ is a relation series of $r$.
RelSeries.consdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Let $\mathrm{newHead}$ be an element of $x$ such that $\MembershipmemMACRoT {r}{\ProdmkMACRoU {\mathrm{newHead}}{\operatorname{head} (p)}}$. Then $\operatorname{cons}$ applied to $p$, $\mathrm{newHead}$ and $\mathrm{rel}$ is a relation series of $r$ defined as $\operatorname{append}$ applied to the singleton of $r$ and $\mathrm{newHead}$, $p$ and $\mathrm{rel}$.
RelSeries.dropdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Let $i$ be an element of $\mathrm{Fin}$ applied to the sum of the length of $p$ and $1$. Then $\operatorname{drop}$ applied to $p$ and $i$ is a relation series of $r$.
RelSeries.eraseLastdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Then $\operatorname{eraseLast}$ applied to $p$ is a relation series of $r$.
RelSeries.fromListIsChaindefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $x_{1}$ be a list of elements of $x$ such that $x_{1} \neq \operatorname{nil}$ and $\operatorname{IsChain}$ holds for the function that maps $x_{2}$ and $x_{3}$ to $\MembershipmemMACRoT {r}{(\ProdmkMACRoU {x_{2}}{x_{3}})}$ and $x_{1}$. Then $\operatorname{fromListIsChain}$ applied to $x_{1}$, $\mathrm{x\_ne\_nil}$ and $\mathrm{hx}$ is a relation series of $r$.
RelSeries.headdefMathlib.Order.RelSeries, function or constant
Wording
the head of x1 (from the name)
English
Let $x_{1}$ be a relation series of $r$. Then the head of $x_{1}$ is an element of $x$ defined as the underlying function of $x_{1}$ and $0$.
RelSeries.inductionOndefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $\mathrm{motive}$ be a function from relation series of $r$ to sets. Let $\mathrm{singleton}$ be a function from elements $x_{2}$ of $x$ to elements of $\mathrm{motive}$ applied to the singleton of $r$ and $x_{2}$. Let $\mathrm{cons}$ be a function from relation series $p_{1}$ of $r$ and elements $x_{1}$ of $x$ and elements $\mathrm{hx}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {r}{(\ProdmkMACRoU {x_{1}}{\operatorname{head} (p_{1})})}$ and elements of $\mathrm{motive}$ applied to $p_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $p_{1}$, $x_{1}$ and $\mathrm{hx}$. Let $p$ be a relation series of $r$. Then $\operatorname{inductionOn}$ applied to $\mathrm{motive}$, $x_{2}$, $\mathrm{singleton}$, $p_{1}$, $x_{1}$, $\mathrm{hx}$, $\mathrm{cons}$ and $p$ is an element of $\mathrm{motive}$ applied to $p$.
RelSeries.inductionOn'defMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $\mathrm{motive}$ be a function from relation series of $r$ to sets. Let $\mathrm{singleton}$ be a function from elements $x_{2}$ of $x$ to elements of $\mathrm{motive}$ applied to the singleton of $r$ and $x_{2}$. Let $\mathrm{snoc}$ be a function from relation series $p_{1}$ of $r$ and elements $x_{1}$ of $x$ and elements $\mathrm{hx}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {r}{(\ProdmkMACRoU {\operatorname{last} (p_{1})}{x_{1}})}$ and elements of $\mathrm{motive}$ applied to $p_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{snoc}$ applied to $p_{1}$, $x_{1}$ and $\mathrm{hx}$. Let $p$ be a relation series of $r$. Then $\operatorname{inductionOn'}$ applied to $\mathrm{motive}$, $x_{2}$, $\mathrm{singleton}$, $p_{1}$, $x_{1}$, $\mathrm{hx}$, $\mathrm{snoc}$ and $p$ is an element of $\mathrm{motive}$ applied to $p$.
RelSeries.insertNthdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Let $i$ be an element of $\mathrm{Fin}$ applied to the length of $p$. Let $a$ be an element of $x$ such that $\MembershipmemMACRoT {r}{\ProdmkMACRoU {\operatorname{toFun} (p , \operatorname{castSucc} (i))}{a}}$ and $\MembershipmemMACRoT {r}{\ProdmkMACRoU {a}{\operatorname{toFun} (p , \operatorname{succ} (i))}}$. Then $\operatorname{insertNth}$ applied to $p$, $i$, $a$, $\mathrm{prev\_connect}$ and $\mathrm{connect\_next}$ is a relation series of $r$.
RelSeries.lastdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $x_{1}$ be a relation series of $r$. Then $\operatorname{last}$ applied to $x_{1}$ is an element of $x$ defined as the underlying function of $x_{1}$ and $\operatorname{last}$ applied to the length of $x_{1}$.
RelSeries.lengthdefMathlib.Order.RelSeries, function or constant
Wording
the length of self (from the name)
English
Let $\mathrm{self}$ be a relation series of $r$. Then the length of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RelSeries.longestOfdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $r$ be a set relation of $x$ and $x$. Then $\operatorname{longestOf}$ applied to $r$ is a relation series of $r$ defined as $\operatorname{choose}$ applied to $\mathrm{SetRel\_\_FiniteDimensional\_\_exists\_longest\_relSeries}$.
RelSeries.mapdefMathlib.Order.RelSeries, function or constant
Wording
the map of p and f (from the name)
English
Let $p$ be a relation series of $r$. Let $f$ be a homomorphism of $r$ and $s$. Then the map of $p$ and $f$ is a relation series of $s$.
RelSeries.ofLEdefMathlib.Order.RelSeries, function or constant
Wording
the relation series of x1 and h (from the name)
English
Let $x_{1}$ be a relation series of $r$. Assume that $r \leq s$. Then the relation series of $x_{1}$ and $h$ is a relation series of $s$.
RelSeries.reversedefMathlib.Order.RelSeries, function or constant
Wording
the reverse of p (from the name)
English
Let $p$ be a relation series of $r$. Then the reverse of $p$ is a relation series of the inverse of $r$.
RelSeries.singletondefMathlib.Order.RelSeries, function or constant
Wording
the singleton of r and a (from the name)
English
Let $r$ be a set relation of $x$ and $x$. Let $a$ be an element of $x$. Then the singleton of $r$ and $a$ is a relation series of $r$.
RelSeries.smashdefMathlib.Order.RelSeries, function or constant
Wording
the smash of p and q (from the name)
English
Let $p$ and $q$ be relation series of $r$ such that $\operatorname{last}$ applied to $p$ is equal to the head of $q$. Then the smash of $p$ and $q$ is a relation series of $r$.
RelSeries.snocdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Let $\mathrm{newLast}$ be an element of $x$ such that $\ProdmkMACRoU {\operatorname{last} (p)}{\mathrm{newLast}}$ is an element of $r$. Then $\operatorname{snoc}$ applied to $p$, $\mathrm{newLast}$ and $\mathrm{rel}$ is a relation series of $r$ defined as $\operatorname{append}$ applied to $p$, the singleton of $r$ and $\mathrm{newLast}$ and $\mathrm{rel}$.
RelSeries.taildefMathlib.Order.RelSeries, function or constant
Wording
the tail of p and len_pos (from the name)
English
Let $p$ be a relation series of $r$ such that the length of $p$ is distinct from $0$. Then the tail of $p$ and $\mathrm{len\_pos}$ is a relation series of $r$.
RelSeries.takedefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $p$ be a relation series of $r$. Let $i$ be an element of $\mathrm{Fin}$ applied to the sum of the length of $p$ and $1$. Then $\operatorname{take}$ applied to $p$ and $i$ is a relation series of $r$.
RelSeries.toFundefMathlib.Order.RelSeries, function or constant
Wording
the underlying function of self and x1 (from the docstring)
English
Let $\mathrm{self}$ be a relation series of $r$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to the sum of the length of $\mathrm{self}$ and $1$. Then the underlying function of $\mathrm{self}$ and $x_{1}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.
RelSeries.toListdefMathlib.Order.RelSeries, function or constant
Wording
the list of x1 (from the name)
English
Let $x_{1}$ be a relation series of $r$. Then the list of $x_{1}$ is a list of elements of $x$ defined as $\operatorname{ofFn}$ applied to $\operatorname{toFun}$ applied to $x_{1}$.
RelSeries.withLengthdefMathlib.Order.RelSeries, function or constant
Wording
no wording
English
Let $r$ be a set relation of $x$ and $x$. Let $n$ be a natural number. Then $\operatorname{withLength}$ applied to $r$ and $n$ is a relation series of $r$ defined as $\operatorname{choose}$ applied to $\mathrm{SetRel\_\_InfiniteDimensional\_\_exists\_relSeries\_with\_length}$ applied to $n$.
SetRel.FiniteDimensionalclassMathlib.Order.RelSeries, predicate
Wording
no wording
English
Let $r$ be a set relation of $x$ and $x$. Then we can say that $\operatorname{FiniteDimensional}$ holds for $r$.
SetRel.InfiniteDimensionalclassMathlib.Order.RelSeries, predicate
Wording
no wording
English
Let $r$ be a set relation of $x$ and $x$. Then we can say that $\operatorname{InfiniteDimensional}$ holds for $r$.

Mathlib.Order.Restriction

Preorder.frestrictLedefMathlib.Order.Restriction, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Let $f$ be a function from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$. Let $i$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{4}})}$. Then $\operatorname{frestrictLe}$ applied to $a$, $i_{1}$, $f$ and $i$ is an element of $x_{2}$ applied to $i$ defined as the function that maps $i$ to $\operatorname{restrict}$ applied to $\FinsetIicMACRoAJ {a}$, $i_{1}$, $f$ and $i$.
Preorder.frestrictLe₂defMathlib.Order.Restriction, function or constant
Wording
no wording
English
Assume that $a \leq b$. Let $f$ be a function from elements $i_{1}$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {b}}{x_{5}})}$ to elements of $x_{2}$ applied to $i_{1}$. Let $i$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{4}})}$. Then $\mathrm{Preorder\_\_frestrictLe\_u2082\_}$ applied to $\mathrm{hab}$, $i_{1}$, $f$ and $i$ is an element of $x_{2}$ applied to $i$.
Preorder.restrictLedefMathlib.Order.Restriction, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Let $f$ be a function from elements $a_{2}$ of $x$ to elements of $x_{2}$ applied to $a_{2}$. Let $a_{1}$ be an element of $\operatorname{Iic}$ applied to $a$. Then $\operatorname{restrictLe}$ applied to $a$, $a_{2}$, $f$ and $a_{1}$ is an element of $x_{2}$ applied to $a_{1}$ defined as the function that maps $a_{1}$ to $\operatorname{domRestrict}$ applied to $\operatorname{Iic}$ applied to $a$, $a_{2}$, $f$ and $a_{1}$.
Preorder.restrictLe₂defMathlib.Order.Restriction, function or constant
Wording
no wording
English
Assume that $a \leq b$. Let $f$ be a function from elements $a_{2}$ of $\operatorname{Iic}$ applied to $b$ to elements of $x_{2}$ applied to $a_{2}$. Let $a_{1}$ be an element of $\operatorname{Iic}$ applied to $a$. Then $\mathrm{Preorder\_\_restrictLe\_u2082\_}$ applied to $\mathrm{hab}$, $a_{2}$, $f$ and $a_{1}$ is an element of $x_{2}$ applied to $a_{1}$.

Mathlib.Order.SaddlePoint

IsSaddlePointOndefMathlib.Order.SaddlePoint, predicate
Wording
no wording
English
Let $X$ be an element of $\wp E$. Let $Y$ be an element of $\wp F$. Let $f$ be a function from elements of $E$ and elements of $F$ to elements of $x$. Let $a$ be an element of $E$. Let $b$ be an element of $F$. Then $\mathrm{IsSaddlePointOn}$ holds for $X$, $Y$, $f$, $a$ and $b$, if for all elements $x_{2}$ of $E$, if $x_{2}$ is an element of $X$, then for all elements $y$ of $F$, if $y$ is an element of $Y$, then $f (a , y)\leq f (x_{2} , b)$.

Mathlib.Order.ScottContinuity

ScottContinuousdefMathlib.Order.ScottContinuity, predicate
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{ScottContinuous}$ holds for $f$, if for all elements $d$ of $\wp x$, if $d$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then $\mathrm{IsLUB}$ holds for the image of $f$ and $d$ and $f$ applied to $a$.
ScottContinuousOndefMathlib.Order.ScottContinuity, predicate
Wording
no wording
English
Let $D$ be an element of $\wp (\wp x)$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{ScottContinuousOn}$ holds for $D$ and $f$, 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_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and $d$, then for all elements $a$ of $x$, if $\mathrm{IsLUB}$ holds for $d$ and $a$, then $\mathrm{IsLUB}$ holds for the image of $f$ and $d$ and $f$ applied to $a$.

Mathlib.Order.SemiconjSup

IsOrderRightAdjointdefMathlib.Order.SemiconjSup, predicate
Wording
no wording
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$. Then $\mathrm{IsOrderRightAdjoint}$ holds for $f$ and $g$, if for all elements $y$ of $x_{1}$, $\mathrm{IsLUB}$ holds for $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to $\mathrm{Leq} (f (x_{4}), y)$ and $g$ applied to $y$.

Mathlib.Order.SetAccumulate

Set.accumulatedefMathlib.Order.SetAccumulate, function or constant
Wording
no wording
English
Let $s$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{accumulate}$ applied to $s$ and $x_{3}$ is an element of $\wp x_{1}$ defined as the union of the function that maps $y$ to the union of the function that maps $h$ to $s$ applied to $y$.

Mathlib.Order.SetDissipate

Set.dissipatedefMathlib.Order.SetDissipate, function or constant
Wording
no wording
English
Let $s$ be a function from elements of $x$ to elements of $\wp x_{1}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{dissipate}$ applied to $s$ and $x_{3}$ is an element of $\wp x_{1}$ defined as the intersection of the function that maps $y$ to the intersection of the function that maps $h$ to $s$ applied to $y$.

Mathlib.Order.SetNotation

Set.iInterdefMathlib.Order.SetNotation, function or constant
Wording
the intersection of s (from the name)
English
Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then the intersection of $s$ is an element of $\wp x$ defined as the infimum of $s$.
Set.iUniondefMathlib.Order.SetNotation, function or constant
Wording
the union of s (from the name)
English
Let $s$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then the union of $s$ is an element of $\wp x$ defined as the supremum of $s$.
Set.sInterdefMathlib.Order.SetNotation, function or constant
Wording
the intersection of S (from the name)
English
Let $S$ be an element of $\wp (\wp x)$. Then the intersection of $S$ is an element of $\wp x$ defined as the infimum of $S$.
Set.sUniondefMathlib.Order.SetNotation, function or constant
Wording
the union of S (from the name)
English
Let $S$ be an element of $\wp (\wp x)$. Then the union of $S$ is an element of $\wp x$ defined as the supremum of $S$.
iInfdefMathlib.Order.SetNotation, function or constant
Wording
the infimum of s (from the name)
English
Let $s$ be a function from elements of $x_{1}$ to elements of $x$. Then the infimum of $s$ is an element of $x$ defined as the infimum of the range of $s$.
iSupdefMathlib.Order.SetNotation, function or constant
Wording
the supremum of s (from the name)
English
Let $s$ be a function from elements of $x_{1}$ to elements of $x$. Then the supremum of $s$ is an element of $x$ defined as the supremum of the range of $s$.

Mathlib.Order.Setoid.Basic

Setoid.comapQuotientEquivdefMathlib.Order.Setoid.Basic, function or constant
Wording
the preimage quotient equivalence of f and r (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Assume that $\mathrm{Setoid}$ holds for $x_{1}$. Then the preimage quotient equivalence of $f$ and $r$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{comap}$ applied to $f$ and $r$ to the set of elements of the range of $\operatorname{comp}$ applied to $\operatorname{mk''}$ and $f$.
Setoid.correspondencedefMathlib.Order.Setoid.Basic, function or constant
Wording
the correspondence of r (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Then the correspondence of $r$ is an order isomorphism of $\SubtypeSet {s}{\mathrm{Leq} (r , s)}$ and $\mathrm{Setoid}$ applied to $\mathrm{Quotient}$ applied to $r$.
Setoid.gidefMathlib.Order.Setoid.Basic, function or constant
Wording
no wording
English
$\operatorname{gi}$ is a Galois insertion of $\operatorname{setoid}$ and $\operatorname{r}$.
Setoid.kerLiftdefMathlib.Order.Setoid.Basic, function or constant
Wording
the kernel lift of f and x2 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $f$. Then the kernel lift of $f$ and $x_{2}$ is an element of $x_{1}$.
Setoid.liftEquivdefMathlib.Order.Setoid.Basic, function or constant
Wording
the lift equivalence of r (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Then the lift equivalence of $r$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{Leq} (r , \operatorname{ker} (f))})}{(\mathrm{Elem} (\mathrm{Quotient} (r))\rightarrow x_{1})}$.
Setoid.map_of_ledefMathlib.Order.Setoid.Basic, function or constant
Wording
the map of h and x1 (from the name)
English
Assume that $s \leq t$. Let $x_{1}$ be an element of $\mathrm{Quotient}$ applied to $s$. Then the map of $h$ and $x_{1}$ is an element of $\mathrm{Quotient}$ applied to $t$ defined as the map of $\mathrm{id}$ and $x_{1}$.
Setoid.map_sInfdefMathlib.Order.Setoid.Basic, function or constant
Wording
the map from the quotient of the infimum of h and x1 (from the docstring)
English
Assume that $s$ is an element of $S$. Let $x_{1}$ be an element of $\mathrm{Quotient}$ applied to the infimum of $S$. Then the map from the quotient of the infimum of $h$ and $x_{1}$ is an element of $\mathrm{Quotient}$ applied to $s$ defined as the map of the function that maps $x_{1}$, $x_{2}$ and $a$ to $a$ applied to $s$ and $h$ and $x_{1}$.
Setoid.piQuotientEquivdefMathlib.Order.Setoid.Basic, function or constant
Wording
the product quotient equivalence of r (from the name)
English
Assume that for all elements $i_{1}$ of $x$, $\mathrm{Setoid}$ holds for $x_{1}$ applied to $i_{1}$. Then the product quotient equivalence of $r$ is an element of $\EquivMACRoAE {(\mathrm{Elem} (x)\rightarrow \mathrm{Quotient} (r (i)))}{\mathrm{Quotient} (\mathrm{piSetoid})}$.
Setoid.prodQuotientEquivdefMathlib.Order.Setoid.Basic, function or constant
Wording
the product quotient equivalence of r and s (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Assume that $\mathrm{Setoid}$ holds for $x_{1}$. Then the product quotient equivalence of $r$ and $s$ is an element of $\EquivMACRoAE {\mathrm{Prod} (\mathrm{Quotient} (r), \mathrm{Quotient} (s))}{\mathrm{Quotient} (\operatorname{prod} (r , s))}$.
Setoid.quotientBotEquivdefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient by the trivial relation (from the docstring)
English
The quotient by the trivial relation is an equivalence from $\mathrm{Quotient}$ applied to the bottom to $x$.
Setoid.quotientKerEquivOfRightInversedefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient kernel equivalence 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 $\operatorname{RightInverse}$ holds for $g$ and $f$. Then the quotient kernel equivalence of $f$ and $g$ is an element of $\EquivMACRoAE {\mathrm{Quotient} (\operatorname{ker} (f))}{x_{1}}$.
Setoid.quotientKerEquivOfSurjectivedefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient kernel equivalence of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{Surjective}$ holds for $f$. Then the quotient kernel equivalence of $f$ and $\mathrm{hf}$ is an element of $\EquivMACRoAE {\mathrm{Quotient} (\operatorname{ker} (f))}{x_{1}}$ defined as the quotient kernel equivalence of $f$ and $\operatorname{surjInv}$ applied to $\mathrm{hf}$.
Setoid.quotientKerEquivRangedefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient kernel equivalence range of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the quotient kernel equivalence range of $f$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $f$ to the set of elements of the range of $f$ defined as the composition of the quotient of $f$ and the equivalence of $\mathrm{Setoid\_\_range\_kerLift\_eq\_range}$ applied to $f$.
Setoid.quotientKerEquivRangeKerLiftdefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient of f (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the quotient of $f$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $f$ to the set of elements of the range of $\operatorname{kerLift}$ applied to $f$ defined as the equivalence of $\operatorname{kerLift}$ applied to $f$ and $\mathrm{Setoid\_\_kerLift\_injective}$ applied to $f$.
Setoid.quotientQuotientEquivQuotientdefMathlib.Order.Setoid.Basic, function or constant
Wording
the quotient quotient equivalence quotient of s and h (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Assume that $\mathrm{Setoid}$ holds for $x$. Assume that $r \leq s$. Then the quotient quotient equivalence quotient of $s$ and $h$ is an equivalence from $\mathrm{Quotient}$ applied to $\operatorname{ker}$ applied to $\operatorname{mapRight}$ applied to $h$ to $\mathrm{Quotient}$ applied to $s$.
Setoid.sigmaQuotientEquivOfLedefMathlib.Order.Setoid.Basic, function or constant
Wording
the sigma quotient equivalence of hle (from the name)
English
Assume that $r \leq s$. Then the sigma quotient equivalence of $\mathrm{hle}$ is an equivalence from $\Sigma$ applied to the function that maps $q$ to $\mathrm{Quotient}$ applied to $\operatorname{comap}$ applied to the function that maps $x_{1}$ to the proposition that $x_{1}$ is an element of the preimage of $\operatorname{mk}$ applied to $s$ and $\operatorname{singleton}$ applied to $q$ and $r$ to $\mathrm{Quotient}$ applied to $r$.

Mathlib.Order.Setoid.Partition

IndexedPartitionstructureMathlib.Order.Setoid.Partition, type
Wording
indexed partition of s (from the name)
English
Let $s$ be a function from elements of $x$ to elements of $\wp x_{1}$. Then the indexed partitions of $s$ are a basic type.
IndexedPartition.QuotientdefMathlib.Order.Setoid.Partition, type
Wording
quotient of hs (from the name)
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Then a quotient of $\mathrm{hs}$ is an element of the function that maps $\mathrm{hs}$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $\mathrm{hs}$.
IndexedPartition.coarserPartitiondefMathlib.Order.Setoid.Partition, function or constant
Wording
no wording
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Let $g$ be a function from elements of $x$ to elements of $x_{2}$ such that $\operatorname{Surjective}$ holds for $g$. Then $\operatorname{coarserPartition}$ applied to $\mathrm{hs}$, $g$ and $\mathrm{hg}$ is an indexed partition of the function that maps $k$ to the union of the function that maps $i$ to the union of the function that maps $h$ to $s$ applied to $i$.
IndexedPartition.equivQuotientdefMathlib.Order.Setoid.Partition, function or constant
Wording
the equivalence quotient of hs (from the name)
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Then the equivalence quotient of $\mathrm{hs}$ is an equivalence from $x$ to the set of quotients of $\mathrm{hs}$ defined as the inverse of the quotient kernel equivalence of $\operatorname{index}$ applied to $\mathrm{hs}$ and $\operatorname{some}$ applied to $\mathrm{hs}$.
IndexedPartition.indexdefMathlib.Order.Setoid.Partition, function or constant
Wording
the index of self and x2 (from the name)
English
Let $\mathrm{self}$ be an indexed partition of $s$. Let $x_{2}$ be an element of $x_{1}$. Then the index of $\mathrm{self}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{2}$.
IndexedPartition.mk'defMathlib.Order.Setoid.Partition, function or constant
Wording
no wording
English
Let $s$ be a function from elements of $x$ to elements of $\wp x_{1}$ such that $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $s$ is pairwise, for all elements $i_{1}$ of $x$, $s$ applied to $i_{1}$ is nonempty and for all elements $x_{2}$ of $x_{1}$, there exists an element $i$ of $x$ such that $\MembershipmemMACRoT {s (i)}{x_{2}}$. Then $\operatorname{mk'}$ applied to $s$, $\mathrm{dis}$, $\mathrm{nonempty}$ and $\mathrm{ex}$ is an indexed partition of $s$.
IndexedPartition.outdefMathlib.Order.Setoid.Partition, function or constant
Wording
no wording
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Then $\operatorname{out}$ applied to $\mathrm{hs}$ is an embedding of the set of quotients of $\mathrm{hs}$ and $x_{1}$.
IndexedPartition.piecewisedefMathlib.Order.Setoid.Partition, function or constant
Wording
no wording
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be an element of $x_{1}$. Then $\operatorname{piecewise}$ applied to $\mathrm{hs}$, $f$ and $x_{3}$ is an element of $x_{2}$ defined as $f$ applied to the index of $\mathrm{hs}$ and $x_{3}$ and $x_{3}$.
IndexedPartition.projdefMathlib.Order.Setoid.Partition, function or constant
Wording
the projection of hs and x2 (from the name)
English
Let $\mathrm{hs}$ be an indexed partition of $s$. Let $x_{2}$ be an element of $x_{1}$. Then the projection of $\mathrm{hs}$ and $x_{2}$ is a quotient of $\mathrm{hs}$ defined as $\operatorname{mk''}$ applied to $x_{2}$.
IndexedPartition.somedefMathlib.Order.Setoid.Partition, function or constant
Wording
no wording
English
Let $\mathrm{self}$ be an indexed partition of $s$. Let $x_{2}$ be an element of $x$. Then $\operatorname{some}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
Setoid.IsPartitiondefMathlib.Order.Setoid.Partition, predicate
Wording
c is a partition (from the name)
English
Let $c$ be an element of $\wp (\wp x)$. Then $c$ is a partition, if $\operatorname{emptyCollection}$ is not an element of $c$ and for all elements $a$ of $x$, $\mathrm{ExistsUnique}$ holds for the function that maps $b$ to the proposition that $b$ is an element of $c$ and $a$ is an element of $b$.
Setoid.IsPartition.finpartitiondefMathlib.Order.Setoid.Partition, function or constant
Wording
the finpartition of hc (from the name)
English
Assume that $c$ is a partition. Then the finpartition of $\mathrm{hc}$ is a finpartition of the universal set.
Setoid.Partition.orderIsodefMathlib.Order.Setoid.Partition, function or constant
Wording
the order isomorphism of x (from the name)
English
Let $x$ be a set. Then the order isomorphism of $x$ is an order isomorphism of $\mathrm{Setoid}$ applied to $x$ and the set of partitions of $x$.
Setoid.PartitionsdefMathlib.Order.Setoid.Partition, type
Wording
partition of x (from the name)
English
Let $x$ be a set. Then a partition of $x$ is an element of the function that maps $x$ to $\SubtypeSet {c}{\operatorname{IsPartition} (c)}$.
Setoid.Partitions.toSetdefMathlib.Order.Setoid.Partition, function or constant
Wording
the set of p (from the name)
English
Let $p$ be a partition of $x$. Then the set of $p$ is an element of $\wp (\wp x)$ defined as $p$.
Setoid.classesdefMathlib.Order.Setoid.Partition, function or constant
Wording
the class of r (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Then the class of $r$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exists an element $y$ of $x$, such that $\EqtMACRoH {s}{\operatorname{ofPred} (\lambda x_{1} . \operatorname{r} (x_{1} , y))}$.
Setoid.quotientEquivClassesdefMathlib.Order.Setoid.Partition, function or constant
Wording
the quotient equivalence class of r (from the name)
English
Assume that $\mathrm{Setoid}$ holds for $x$. Then the quotient equivalence class of $r$ is an equivalence from $\mathrm{Quotient}$ applied to $r$ to the set of elements of the class of $r$.

Mathlib.Order.Shrink

orderIsoShrinkdefMathlib.Order.Shrink, function or constant
Wording
the order isomorphism of x (from the docstring)
English
Let $x$ be a set. Then the order isomorphism of $x$ is an order isomorphism of $x$ and the set of shrinks of $x$.

Mathlib.Order.Sigma

Sigma.LEinductiveMathlib.Order.Sigma, predicate
Wording
no wording
English
Let $\mathrm{\_a}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Let $\mathrm{\_b}$ be an element of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$. Then we can say that $\operatorname{LE}$ holds for $\mathrm{\_a}$ and $\mathrm{\_b}$.
Sigma.LTinductiveMathlib.Order.Sigma, predicate
Wording
no wording
English
Let $\mathrm{\_a}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Let $\mathrm{\_b}$ be an element of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$. Then we can say that $\operatorname{LT}$ holds for $\mathrm{\_a}$ and $\mathrm{\_b}$.

Mathlib.Order.Sigma.Lex

Sigma.LexinductiveMathlib.Order.Sigma.Lex, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be a function from elements $i_{2}$ of $x$ and elements of $x_{1}$ applied to $i_{2}$ and elements of $x_{1}$ applied to $i_{2}$ to propositions. Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$. Let $x_{3}$ be an element of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$. Then we can say that $\operatorname{Lex}$ holds for $r$, $i_{2}$, $s$, $x_{2}$ and $x_{3}$.

Mathlib.Order.Std

LinearOrder.OfStdArgsstructureMathlib.Order.Std, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\operatorname{OfStdArgs}$ applied to $x$ are a basic type.
PartialOrder.OfStdArgsstructureMathlib.Order.Std, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\operatorname{OfStdArgs}$ applied to $x$ are a basic type.
Preorder.OfStdArgsstructureMathlib.Order.Std, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\operatorname{OfStdArgs}$ applied to $x$ are a basic type.

Mathlib.Order.Sublattice

SublatticestructureMathlib.Order.Sublattice, type
Wording
sublattice of x (from the name)
English
Let $x$ be a set. Then the sublattices of $x$ are a basic type.
Sublattice.LatticeHom.rangedefMathlib.Order.Sublattice, function or constant
Wording
the range of f (from the docstring)
English
Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then the range of $f$ is a sublattice of $x_{1}$.
Sublattice.carrierdefMathlib.Order.Sublattice, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a sublattice of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Sublattice.comapdefMathlib.Order.Sublattice, function or constant
Wording
the preimage of f and L (from the docstring)
English
Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a sublattice of $x_{1}$. Then the preimage of $f$ and $L$ is a sublattice of $x$.
Sublattice.copydefMathlib.Order.Sublattice, function or constant
Wording
the copy of L and s (from the name)
English
Let $L$ be a sublattice of $x$. Let $s$ be an element of $\wp x$ such that $\EqtMACRoH {s}{L}$. Then the copy of $L$ and $s$ is a sublattice of $x$.
Sublattice.inclusiondefMathlib.Order.Sublattice, function or constant
Wording
the inclusion homomorphism of h (from the docstring)
English
Assume that $L \leq M$. Then the inclusion homomorphism of $h$ is a lattice homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$.
Sublattice.mapdefMathlib.Order.Sublattice, function or constant
Wording
the map of f and L (from the name)
English
Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a sublattice of $x$. Then the map of $f$ and $L$ is a sublattice of $x_{1}$.
Sublattice.ofIsSublatticedefMathlib.Order.Sublattice, function or constant
Wording
the sublattice of s and hs (from the name)
English
Let $s$ be an element of $\wp x$ such that $s$ is a sublattice. Then the sublattice of $s$ and $\mathrm{hs}$ is a sublattice of $x$ defined as $\operatorname{mk}$ applied to $s$, $\operatorname{supClosed}$ applied to $\mathrm{hs}$ and $\operatorname{infClosed}$ applied to $\mathrm{hs}$.
Sublattice.pidefMathlib.Order.Sublattice, function or constant
Wording
the product of s and L (from the name)
English
Let $s$ be an element of $\wp x$. Let $L$ be a function from elements $i_{1}$ of $x$ to sublattices of $x_{1}$ applied to $i_{1}$. Then the product of $s$ and $i_{1}$ is a sublattice of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$.
Sublattice.proddefMathlib.Order.Sublattice, function or constant
Wording
the product of L and M (from the name)
English
Let $L$ be a sublattice of $x$. Let $M$ be a sublattice of $x_{1}$. Then the product of $L$ and $M$ is a sublattice of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
Sublattice.prodEquivdefMathlib.Order.Sublattice, function or constant
Wording
the product equivalence of L and M (from the name)
English
Let $L$ be a sublattice of $x$. Let $M$ be a sublattice of $x_{1}$. Then the product equivalence of $L$ and $M$ is an order isomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{prod} (L , M)}{x_{4}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {L}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {M}{x_{6}})}$.
Sublattice.subtypedefMathlib.Order.Sublattice, function or constant
Wording
the subtype of L (from the name)
English
Let $L$ be a sublattice of $x$. Then the subtype of $L$ is a lattice homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$ and $x$.
Sublattice.topEquivdefMathlib.Order.Sublattice, function or constant
Wording
the top sublattice (from the docstring)
English
The top sublattice is an order isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{2}})}$ and $x$.

Mathlib.Order.Sublocale

Nucleus.toSublocaledefMathlib.Order.Sublocale, function or constant
Wording
the range of n (from the docstring)
English
Let $n$ be a nucleus of $X$. Then the range of $n$ is a sublocale of $X$.
SublocalestructureMathlib.Order.Sublocale, type
Wording
sublocale of X (from the name)
English
Let $X$ be a set. Then the sublocales of $X$ are a basic type.
Sublocale.carrierdefMathlib.Order.Sublocale, function or constant
Wording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a sublocale of $X$. Then the carrier of $\mathrm{self}$ is an element of $\wp X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Sublocale.giRestrictdefMathlib.Order.Sublocale, function or constant
Wording
no wording
English
Let $S$ be a sublocale of $X$. Then $\operatorname{giRestrict}$ applied to $S$ is a Galois insertion of $\operatorname{coe}$ applied to $\operatorname{restrict}$ applied to $S$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {S}{x_{1}}$.
Sublocale.restrictdefMathlib.Order.Sublocale, function or constant
Wording
no wording
English
Let $S$ be a sublocale of $X$. Then $\operatorname{restrict}$ applied to $S$ is a frame homomorphism of $X$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {S}{x_{1}})}$.
Sublocale.toNucleusdefMathlib.Order.Sublocale, function or constant
Wording
the nucleus of S (from the name)
English
Let $S$ be a sublocale of $X$. Then the nucleus of $S$ is a nucleus of $X$.
nucleusIsoSublocaledefMathlib.Order.Sublocale, function or constant
Wording
the nucleus isomorphism sublocale (from the name)
English
The nucleus isomorphism sublocale is an order isomorphism of the set of order duals of the set of nuclei of $X$ and the set of sublocales of $X$.

Mathlib.Order.SuccPred.Archimedean

IsPredArchimedeanclassMathlib.Order.SuccPred.Archimedean, predicate
Wording
x is a predecessor archimedean (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a predecessor archimedean.
IsSuccArchimedeanclassMathlib.Order.SuccPred.Archimedean, predicate
Wording
x is a successor archimedean (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a successor archimedean.

Mathlib.Order.SuccPred.Basic

Order.preddefMathlib.Order.SuccPred.Basic, function or constant
Wording
the predecessor of x3 (from the docstring)
English
Let $x_{3}$ be an element of $x$. Then the predecessor of $x_{3}$ is an element of $x$ defined as the predecessor of $x_{3}$.
Order.succdefMathlib.Order.SuccPred.Basic, function or constant
Wording
the successor of x3 (from the docstring)
English
Let $x_{3}$ be an element of $x$. Then the successor of $x_{3}$ is an element of $x$ defined as the successor of $x_{3}$.
PredOrderclassMathlib.Order.SuccPred.Basic, predicate
Wording
x is a predecessor order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a predecessor order.
PredOrder.preddefMathlib.Order.SuccPred.Basic, function or constant
Wording
the predecessor of x2 (from the name)
English
Let $x_{2}$ be an element of $x$. Then the predecessor of $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
SuccOrderclassMathlib.Order.SuccPred.Basic, predicate
Wording
x is a successor order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a successor order.
SuccOrder.succdefMathlib.Order.SuccPred.Basic, function or constant
Wording
the successor of x2 (from the name)
English
Let $x_{2}$ be an element of $x$. Then the successor of $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

Mathlib.Order.SuccPred.Limit

Order.IsPredLimitstructureMathlib.Order.SuccPred.Limit, predicate
Wording
a is a predecessor limit (from the name)
English
Let $a$ be an element of $x$. Then we can say that $a$ is a predecessor limit.
Order.IsPredPrelimitdefMathlib.Order.SuccPred.Limit, predicate
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{IsPredPrelimit}$ holds for $a$, if for all elements $b$ of $x$, it is not the case that $\mathrm{CovBy}$ holds for $a$ and $b$.
Order.IsPredPrelimit.middefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Assume that $\operatorname{IsPredPrelimit}$ holds for $i$. Assume that $i < j$. Then $\operatorname{mid}$ applied to $\mathrm{hi}$ and $\mathrm{hj}$ is an element of the open interval of $i$ and $j$.
Order.IsSuccLimitstructureMathlib.Order.SuccPred.Limit, predicate
Wording
a is a successor limit (from the name)
English
Let $a$ be an element of $x$. Then we can say that $a$ is a successor limit.
Order.IsSuccPrelimitdefMathlib.Order.SuccPred.Limit, predicate
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{IsSuccPrelimit}$ holds for $a$, if for all elements $b$ of $x$, it is not the case that $\mathrm{CovBy}$ holds for $b$ and $a$.
Order.IsSuccPrelimit.middefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSuccPrelimit}$ holds for $i$. Assume that $j < i$. Then $\operatorname{mid}$ applied to $\mathrm{hi}$ and $\mathrm{hj}$ is an element of the open interval of $j$ and $i$.
Order.isPredLimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{isMax}$ be a function from elements $a_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{2}$ is a maximum to elements of $\mathrm{motive}$ applied to $a_{2}$. Let $\mathrm{pred}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a minimum to elements of $\mathrm{motive}$ applied to the predecessor of $a_{1}$. Let $\mathrm{isPredLimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is a predecessor limit to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{isPredLimitRecOn}$ applied to $b$, $a_{2}$, $\mathrm{isMax}$, $a_{1}$, $\mathrm{pred}$, $a$ and $\mathrm{isPredLimit}$ is an element of $\mathrm{motive}$ applied to $b$.
Order.isPredPrelimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{pred}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a minimum to elements of $\mathrm{motive}$ applied to the predecessor of $a_{1}$. Let $\mathrm{isPredPrelimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{IsPredPrelimit}$ applied to $a$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{isPredPrelimitRecOn}$ applied to $b$, $a_{1}$, $\mathrm{pred}$, $a$ and $\mathrm{isPredPrelimit}$ is an element of $\mathrm{motive}$ applied to $b$.
Order.isSuccLimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{isMin}$ be a function from elements $a_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{2}$ is a minimum to elements of $\mathrm{motive}$ applied to $a_{2}$. Let $\mathrm{succ}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a maximum to elements of $\mathrm{motive}$ applied to the successor of $a_{1}$. Let $\mathrm{isSuccLimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is a successor limit to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{isSuccLimitRecOn}$ applied to $b$, $a_{2}$, $\mathrm{isMin}$, $a_{1}$, $\mathrm{succ}$, $a$ and $\mathrm{isSuccLimit}$ is an element of $\mathrm{motive}$ applied to $b$.
Order.isSuccPrelimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{succ}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a maximum to elements of $\mathrm{motive}$ applied to the successor of $a_{1}$. Let $\mathrm{isSuccPrelimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{IsSuccPrelimit}$ applied to $a$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{isSuccPrelimitRecOn}$ applied to $b$, $a_{1}$, $\mathrm{succ}$, $a$ and $\mathrm{isSuccPrelimit}$ is an element of $\mathrm{motive}$ applied to $b$.
PredOrder.colimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{isMax}$ be a function from elements $a_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{2}$ is a maximum to elements of $\mathrm{motive}$ applied to $a_{2}$. Let $\mathrm{pred}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a minimum and elements of $\mathrm{motive}$ applied to $a_{1}$ to elements of $\mathrm{motive}$ applied to the predecessor of $a_{1}$. Let $\mathrm{isPredLimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is a predecessor limit and functions from elements $b_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (a , b_{1})$ to elements of $\mathrm{motive}$ applied to $b_{1}$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{colimitRecOn}$ applied to $b$, $a_{2}$, $\mathrm{isMax}$, $a_{1}$, $\mathrm{pred}$, $a$ and $\mathrm{isPredLimit}$ is an element of $\mathrm{motive}$ applied to $b$.
PredOrder.prelimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{pred}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a minimum and elements of $\mathrm{motive}$ applied to $a_{1}$ to elements of $\mathrm{motive}$ applied to the predecessor of $a_{1}$. Let $\mathrm{isPredPrelimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{IsPredPrelimit}$ applied to $a$ and functions from elements $b_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (a , b_{1})$ to elements of $\mathrm{motive}$ applied to $b_{1}$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{prelimitRecOn}$ applied to $b$, $a_{1}$, $\mathrm{pred}$, $a$ and $\mathrm{isPredPrelimit}$ is an element of $\mathrm{motive}$ applied to $b$.
SuccOrder.limitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{isMin}$ be a function from elements $a_{2}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{2}$ is a minimum to elements of $\mathrm{motive}$ applied to $a_{2}$. Let $\mathrm{succ}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a maximum and elements of $\mathrm{motive}$ applied to $a_{1}$ to elements of $\mathrm{motive}$ applied to the successor of $a_{1}$. Let $\mathrm{isSuccLimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a$ is a successor limit and functions from elements $b_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (b_{1} , a)$ to elements of $\mathrm{motive}$ applied to $b_{1}$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{limitRecOn}$ applied to $b$, $a_{2}$, $\mathrm{isMin}$, $a_{1}$, $\mathrm{succ}$, $a$ and $\mathrm{isSuccLimit}$ is an element of $\mathrm{motive}$ applied to $b$.
SuccOrder.prelimitRecOndefMathlib.Order.SuccPred.Limit, function or constant
Wording
no wording
English
Let $b$ be an element of $x$. Let $\mathrm{succ}$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to the proposition that $a_{1}$ is not a maximum and elements of $\mathrm{motive}$ applied to $a_{1}$ to elements of $\mathrm{motive}$ applied to the successor of $a_{1}$. Let $\mathrm{isSuccPrelimit}$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $\operatorname{IsSuccPrelimit}$ applied to $a$ and functions from elements $b_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (b_{1} , a)$ to elements of $\mathrm{motive}$ applied to $b_{1}$ to elements of $\mathrm{motive}$ applied to $a$. Then $\operatorname{prelimitRecOn}$ applied to $b$, $a_{1}$, $\mathrm{succ}$, $a$ and $\mathrm{isSuccPrelimit}$ is an element of $\mathrm{motive}$ applied to $b$.

Mathlib.Order.SuccPred.LinearLocallyFinite

LinearLocallyFiniteOrder.succFndefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
the successor function of i (from the name)
English
Let $i$ be an element of $x$. Then the successor function of $i$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{exists\_glb\_Ioi}$ applied to $i$.
orderIsoIntOfLinearSuccPredArchdefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
the order isomorphism integer (from the name)
English
The order isomorphism integer is an order isomorphism of $x$ and $\Integer$.
orderIsoNatOfLinearSuccPredArchdefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
no wording
English
$\mathrm{orderIsoNatOfLinearSuccPredArch}$ is an order isomorphism of $x$ and $\Natural$.
orderIsoRangeOfLinearSuccPredArchdefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
the order isomorphism range (from the name)
English
The order isomorphism range is an order isomorphism of $x$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\FinsetrangeMACRoN {(\operatorname{toNat} (\mathrm{toZ} (\operatorname{bot} , \operatorname{top}))+ 1)}}{x_{6}})}$.
orderIsoRangeToZOfLinearSuccPredArchdefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
no wording
English
$\mathrm{orderIsoRangeToZOfLinearSuccPredArch}$ is an order isomorphism of $x$ and the set of elements of the range of $\mathrm{toZ}$ applied to $\operatorname{some}$ applied to $h_{1}$.
toZdefMathlib.Order.SuccPred.LinearLocallyFinite, function or constant
Wording
no wording
English
Let $i_{0}$ and $i$ be elements of $x$. Then $\mathrm{toZ}$ applied to $i_{0}$ and $i$ is an integer.

Mathlib.Order.SuccPred.Tree

IsPredArchimedean.findAtomdefMathlib.Order.SuccPred.Tree, function or constant
Wording
no wording
English
Let $r$ be an element of $x$. Then $\operatorname{findAtom}$ applied to $r$ is an element of $x$.
RootedTreestructureMathlib.Order.SuccPred.Tree, type
Wording
rooted tree (from the name)
English
The rooted trees are a basic type.
RootedTree.subtreedefMathlib.Order.SuccPred.Tree, function or constant
Wording
the subtree of t and r (from the name)
English
Let $t$ be a rooted tree. Let $r$ be an element of $\mathrm{RootedTree\_\_\_u3b1\_}$ applied to $t$. Then the subtree of $t$ and $r$ is a difference rooted tree of $t$ defined as $r$.
RootedTree.subtreeOfdefMathlib.Order.SuccPred.Tree, function or constant
Wording
the subtree of t and v (from the name)
English
Let $t$ be a rooted tree. Let $v$ be an element of $\mathrm{RootedTree\_\_\_u3b1\_}$ applied to $t$. Then the subtree of $t$ and $v$ is a difference rooted tree of $t$ defined as the subtree of $t$ and $\operatorname{findAtom}$ applied to $v$.
RootedTree.subtreesdefMathlib.Order.SuccPred.Tree, function or constant
Wording
the subtree of t (from the name)
English
Let $t$ be a rooted tree. Then the subtree of $t$ is an element of the power set of the set of difference rooted trees of $t$ defined as $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that the root of $x$ is an atom.
RootedTree.αdefMathlib.Order.SuccPred.Tree, type
Wording
no wording
English
Let $\mathrm{self}$ be a rooted tree. Then an element of $\mathrm{RootedTree\_\_\_u3b1\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
SubRootedTreedefMathlib.Order.SuccPred.Tree, type
Wording
difference rooted tree of t (from the name)
English
Let $t$ be a rooted tree. Then a difference rooted tree of $t$ is an element of the function that maps $t$ to $\mathrm{RootedTree\_\_\_u3b1\_}$ applied to $t$.
SubRootedTree.coeTreedefMathlib.Order.SuccPred.Tree, function or constant
Wording
the coercion tree of r (from the name)
English
Let $r$ be a difference rooted tree of $t$. Then the coercion tree of $r$ is a rooted tree defined as $\operatorname{mk}$ applied to the set of elements of $\operatorname{Ici}$ applied to the root of $r$.
SubRootedTree.rootdefMathlib.Order.SuccPred.Tree, function or constant
Wording
the root of v (from the docstring)
English
Let $v$ be a difference rooted tree of $t$. Then the root of $v$ is an element of $\mathrm{RootedTree\_\_\_u3b1\_}$ applied to $t$ defined as $v$.

Mathlib.Order.SuccPred.WithBot

WithBot.succdefMathlib.Order.SuccPred.WithBot, function or constant
Wording
the successor of a (from the docstring)
English
Let $a$ be an element of $\mathrm{WithBot}$ applied to $x$. Then the successor of $a$ is an element of $x$ defined as $\operatorname{recBotCoe}$ applied to the bottom, $\operatorname{succ}$ and $a$.
WithTop.preddefMathlib.Order.SuccPred.WithBot, function or constant
Wording
the predecessor of a (from the docstring)
English
Let $a$ be an element of $\mathrm{WithTop}$ applied to $x$. Then the predecessor of $a$ is an element of $x$ defined as $\operatorname{recTopCoe}$ applied to the top, $\operatorname{pred}$ and $a$.

Mathlib.Order.Sum.Lattice

Sum.Lex.inlLatticeHomdefMathlib.Order.Sum.Lattice, function or constant
Wording
the left injection lattice homomorphism (from the name)
English
The left injection lattice homomorphism is a lattice homomorphism of $x$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$.
Sum.Lex.inrLatticeHomdefMathlib.Order.Sum.Lattice, function or constant
Wording
the right injection lattice homomorphism (from the name)
English
The right injection lattice homomorphism is a lattice homomorphism of $x_{1}$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

Mathlib.Order.Sum.Order

OrderIso.emptySumLexdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
$\operatorname{emptySumLex}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x_{1}$ and $x$ and $x$ defined as the lexicographic sum 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.sumAssocdefMathlib.Order.Sum.Order, function or constant
Wording
the sum associator of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the sum associator of $x_{1}$ and $x_{2}$ is an order isomorphism of $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.
OrderIso.sumCommdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
Let $x$ and $x_{1}$ be sets. Then $\operatorname{sumComm}$ applied to $x$ and $x_{1}$ is an order isomorphism of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{sumComm}$ applied to $x$ and $x_{1}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Sum\_\_swap\_le\_swap\_iff}$.
OrderIso.sumCongrdefMathlib.Order.Sum.Order, function or constant
Wording
the sum congruence of ea and eb (from the name)
English
Let $\mathrm{ea}$ be an order isomorphism of $x$ and $x_{1}$. Let $\mathrm{eb}$ be an order isomorphism of $x_{2}$ and $x_{3}$. Then the sum congruence of $\mathrm{ea}$ and $\mathrm{eb}$ is an order isomorphism of $\mathrm{Sum}$ applied to $x$ and $x_{2}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{3}$.
OrderIso.sumDualDistribdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
Let $x$ and $x_{1}$ be sets. Then $\operatorname{sumDualDistrib}$ applied to $x$ and $x_{1}$ is an order isomorphism of the set of order duals of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $\mathrm{Sum}$ applied to the set of order duals of $x$ and the set of order duals of $x_{1}$.
OrderIso.sumLexAssocdefMathlib.Order.Sum.Order, function or constant
Wording
the sum lexicographic associator of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the sum lexicographic associator of $x_{1}$ and $x_{2}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$.
OrderIso.sumLexCongrdefMathlib.Order.Sum.Order, function or constant
Wording
the sum lexicographic congruence of ea and eb (from the name)
English
Let $\mathrm{ea}$ be an order isomorphism of $x$ and $x_{1}$. Let $\mathrm{eb}$ be an order isomorphism of $x_{2}$ and $x_{3}$. Then the sum lexicographic congruence of $\mathrm{ea}$ and $\mathrm{eb}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{2}$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x_{1}$ and $x_{3}$.
OrderIso.sumLexDualAntidistribdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
Let $x$ and $x_{1}$ be sets. Then $\operatorname{sumLexDualAntidistrib}$ applied to $x$ and $x_{1}$ is an order isomorphism of the set of order duals of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to the set of order duals of $x_{1}$ and the set of order duals of $x$.
OrderIso.sumLexEmptydefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
$\operatorname{sumLexEmpty}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $x$ defined as $\operatorname{sumLexEmpty}$ applied to 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})$.
Sum.Lex.toLexRelIsoLEdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
$\operatorname{toLexRelIsoLE}$ is a relation isomorphism of $\operatorname{Lex}$ applied to 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})$ and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Leq} (x_{8} , x_{9})$.
Sum.Lex.toLexRelIsoLTdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
$\operatorname{toLexRelIsoLT}$ is a relation isomorphism of $\operatorname{Lex}$ applied to 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})$ and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Lt} (x_{8} , x_{9})$.
Sum.inlₗdefMathlib.Order.Sum.Order, function or constant
Wording
the left injection of x2 (from the name)
English
Let $x_{2}$ be an element of $x$. Then the left injection of $x_{2}$ is an element of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as $\operatorname{toLex}$ applied to $\operatorname{inl}$ applied to $x_{2}$.
Sum.inrₗdefMathlib.Order.Sum.Order, function or constant
Wording
the right injection of x2 (from the name)
English
Let $x_{2}$ be an element of $x_{1}$. Then the right injection of $x_{2}$ is an element of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as $\operatorname{toLex}$ applied to $\operatorname{inr}$ applied to $x_{2}$.
WithBot.orderIsoPUnitSumLexdefMathlib.Order.Sum.Order, function or constant
Wording
no wording
English
$\operatorname{orderIsoPUnitSumLex}$ is an order isomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $\mathrm{PUnit}$ and $x$.
WithTop.orderIsoSumLexPUnitdefMathlib.Order.Sum.Order, function or constant
Wording
the order isomorphism sum lexicographic unit (from the name)
English
The order isomorphism sum lexicographic unit is an order isomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to $x$ and $\mathrm{PUnit}$.

Mathlib.Order.SupClosed

InfCloseddefMathlib.Order.SupClosed, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\mathrm{InfClosed}$ holds for $s$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then for all elements $b$ of $x$, if $b$ is an element of $s$, then $\MinminMACRoAG {a}{b}$ is an element of $s$.
IsSublatticestructureMathlib.Order.SupClosed, predicate
Wording
s is a sublattice (from the name)
English
Let $s$ be an element of $\wp x$. Then we can say that $s$ is a sublattice.
SupCloseddefMathlib.Order.SupClosed, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\mathrm{SupClosed}$ holds for $s$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then for all elements $b$ of $x$, if $b$ is an element of $s$, then $\MaxmaxMACRoAF {a}{b}$ is an element of $s$.
infClosuredefMathlib.Order.SupClosed, function or constant
Wording
the infimum closure (from the name)
English
The infimum closure is a closure operator of $\wp x$.
latticeClosuredefMathlib.Order.SupClosed, function or constant
Wording
the lattice closure (from the name)
English
The lattice closure is a closure operator of $\wp x$ defined as the closure operator of the proposition that $\mathrm{IsSublattice}$ and the function that maps $x_{2}$ to $\mathrm{isSublattice\_sInter}$.
supClosuredefMathlib.Order.SupClosed, function or constant
Wording
the supremum closure (from the name)
English
The supremum closure is a closure operator of $\wp x$.

Mathlib.Order.SupIndep

Finset.SupIndepdefMathlib.Order.SupIndep, predicate
Wording
s is a supremum independent with respect to f (from the name)
English
Let $s$ be a finite set of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then $s$ is a supremum independent with respect to $f$, if for all finite sets $t$ of $x_{1}$, if $t \leq s$, then for all elements $i$ of $x_{1}$, if $i$ is an element of $s$, then if $i$ is not an element of $t$, then $f$ applied to $i$ is disjoint to the supremum of $t$ and $f$.
iSupIndepdefMathlib.Order.SupIndep, predicate
Wording
no wording
English
Let $t$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{iSupIndep}$ holds for $t$, if for all elements $i$ of $x$, $t$ applied to $i$ is disjoint to the supremum of the function that maps $j$ to the supremum of the function that maps $h$ to $t$ applied to $j$.
sSupIndepdefMathlib.Order.SupIndep, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\mathrm{sSupIndep}$ holds for $s$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $a$ is disjoint to the supremum of $\operatorname{sdiff}$ applied to $s$ and $\operatorname{singleton}$ applied to $a$.

Mathlib.Order.Sym2

Sym2.infdefMathlib.Order.Sym2, function or constant
Wording
the infimum of x2 (from the name)
English
Let $x_{2}$ be a symmetric square of $x$. Then the infimum of $x_{2}$ is an element of $x$ defined as $\operatorname{lift}$ applied to the function that maps $x_{5}$ and $x_{6}$ to $\MinminMACRoAG {x_{5}}{x_{6}}$ and $x_{2}$.
Sym2.sortEquivdefMathlib.Order.Sym2, function or constant
Wording
the sort equivalence (from the name)
English
The sort equivalence is an equivalence from the set of symmetric squares of $x$ to $\SubtypeSet {p}{\mathrm{Leq} (\ProdfstMACRoZ {p}, \ProdsndMACRoAA {p})}$.
Sym2.supdefMathlib.Order.Sym2, function or constant
Wording
the supremum of x2 (from the name)
English
Let $x_{2}$ be a symmetric square of $x$. Then the supremum of $x_{2}$ is an element of $x$ defined as $\operatorname{lift}$ applied to the function that maps $x_{5}$ and $x_{6}$ to $\MaxmaxMACRoAF {x_{5}}{x_{6}}$ and $x_{2}$.

Mathlib.Order.SymmDiff

bihimpdefMathlib.Order.SymmDiff, function or constant
Wording
no wording
English
Let $a$ and $b$ be elements of $x$. Then $\mathrm{bihimp}$ applied to $a$ and $b$ is an element of $x$ defined as $\MinminMACRoAG {\operatorname{himp} (b , a)}{\operatorname{himp} (a , b)}$.
symmDiffdefMathlib.Order.SymmDiff, function or constant
Wording
the symmetric difference operator of a and b (from the docstring)
English
Let $a$ and $b$ be elements of $x$. Then the symmetric difference operator of $a$ and $b$ is an element of $x$ defined as $\MaxmaxMACRoAF {\operatorname{sdiff} (a , b)}{\operatorname{sdiff} (b , a)}$.

Mathlib.Order.TeichmullerTukey

Order.IsOfFiniteCharacterdefMathlib.Order.TeichmullerTukey, predicate
Wording
no wording
English
Let $F$ be an element of $\wp (\wp x)$. Then $\operatorname{IsOfFiniteCharacter}$ holds for $F$, if for all elements $x_{1}$ of $\wp x$, $x_{1}$ is an element of $F$, if and only if for all elements $y$ of $\wp x$, if $y \leq x_{1}$, then if $y$ is finite, then $y$ is an element of $F$.

Mathlib.Order.TransfiniteIteration

transfiniteIteratedefMathlib.Order.TransfiniteIteration, function or constant
Wording
no wording
English
Let $x_{1}$ be a function from elements of $I$ to elements of $I$. Let $j$ be an element of $J$. Let $x_{4}$ be an element of $I$. Then $\mathrm{transfiniteIterate}$ applied to $x_{1}$, $j$ and $x_{4}$ is an element of $I$.

Mathlib.Order.TypeTags

WithBotdefMathlib.Order.TypeTags, type
Wording
no wording
English
Let $x$ be a set. Then an element of $\mathrm{WithBot}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Option}$ applied to $x$.
WithBot.recBotCoedefMathlib.Order.TypeTags, function or constant
Wording
no wording
English
Let $\mathrm{bot}$ be an element of $C$ applied to the bottom. Let $\mathrm{coe}$ be a function from elements $a$ of $x$ to elements of $C$ applied to $\operatorname{some}$ applied to $a$. Let $n$ be an element of $\mathrm{WithBot}$ applied to $x$. Then $\operatorname{recBotCoe}$ applied to $\mathrm{bot}$, $a$, $\mathrm{coe}$ and $n$ is an element of $C$ applied to $n$.
WithBot.somedefMathlib.Order.TypeTags, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{some}$ applied to $x_{1}$ is an element of $\mathrm{WithBot}$ applied to $x$ defined as $\operatorname{some}$ applied to $x_{1}$.
WithTopdefMathlib.Order.TypeTags, type
Wording
no wording
English
Let $x$ be a set. Then an element of $\mathrm{WithTop}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Option}$ applied to $x$.
WithTop.recTopCoedefMathlib.Order.TypeTags, function or constant
Wording
no wording
English
Let $\mathrm{top}$ be an element of $C$ applied to the top. Let $\mathrm{coe}$ be a function from elements $a$ of $x$ to elements of $C$ applied to $\operatorname{some}$ applied to $a$. Let $n$ be an element of $\mathrm{WithTop}$ applied to $x$. Then $\operatorname{recTopCoe}$ applied to $\mathrm{top}$, $a$, $\mathrm{coe}$ and $n$ is an element of $C$ applied to $n$.
WithTop.somedefMathlib.Order.TypeTags, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $x$. Then $\operatorname{some}$ applied to $x_{1}$ is an element of $\mathrm{WithTop}$ applied to $x$ defined as $\operatorname{some}$ applied to $x_{1}$.

Mathlib.Order.Types.Arithmetic

OrderType.carddefMathlib.Order.Types.Arithmetic, function or constant
Wording
the cardinal of o (from the docstring)
English
Let $o$ be an order type. Then the cardinal of $o$ is a cardinal.
OrderType.etadefMathlib.Order.Types.Arithmetic, function or constant
Wording
no wording
English
$\operatorname{eta}$ is an order type defined as the type of $\Rational$.
OrderType.thetadefMathlib.Order.Types.Arithmetic, function or constant
Wording
the order type of the real numbers (from the docstring)
English
The order type of the real numbers is an order type defined as the type of $\Real$.

Mathlib.Order.Types.Defs

OrderTypedefMathlib.Order.Types.Defs, type
Wording
order type (from the name)
English
An order type is an element of $\mathrm{Quotient}$ applied to $\operatorname{instSetoid}$.
OrderType.ToTypedefMathlib.Order.Types.Defs, type
Wording
type of o (from the name)
English
Let $o$ be an order type. Then a type of $o$ is an element of the function that maps $o$ to the set of carriers of $\operatorname{out}$ applied to $o$.
OrderType.liftdefMathlib.Order.Types.Defs, function or constant
Wording
the lift of o (from the name)
English
Let $o$ be an order type. Then the lift of $o$ is an order type.
OrderType.liftOndefMathlib.Order.Types.Defs, function or constant
Wording
no wording
English
Let $o$ be an order type. Let $f$ be a function from sets $x_{5}$ and elements of $\mathrm{Proof}$ applied to the proposition that $x_{5}$ is linearly ordered to elements of $x$ such that for all sets $x_{1}$, for all elements $x_{2}$ of $\mathrm{LinearOrder}$ applied to $x_{1}$, for all sets $x_{3}$, for all elements $x_{4}$ of $\mathrm{LinearOrder}$ applied to $x_{3}$, if the type of $x_{1}$ is equal to the type of $x_{3}$, then $\EqtMACRoH {f (x_{1} , x_{2})}{f (x_{3} , x_{4})}$. Then $\operatorname{liftOn}$ applied to $o$, $x_{5}$, $f$ and $c$ is an element of $x$.
OrderType.liftOn₂defMathlib.Order.Types.Defs, function or constant
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be order types. Let $f$ be a function from sets $x_{11}$ and elements of $\mathrm{Proof}$ applied to the proposition that $x_{11}$ is linearly ordered and sets $x_{13}$ and elements of $\mathrm{Proof}$ applied to the proposition that $x_{13}$ is linearly ordered to elements of $x$ such that for all sets $x_{3}$, for all elements $x_{4}$ of $\mathrm{LinearOrder}$ applied to $x_{3}$, for all sets $x_{5}$, for all elements $x_{6}$ of $\mathrm{LinearOrder}$ applied to $x_{5}$, for all sets $x_{7}$, for all elements $x_{8}$ of $\mathrm{LinearOrder}$ applied to $x_{7}$, for all sets $x_{9}$, for all elements $x_{10}$ of $\mathrm{LinearOrder}$ applied to $x_{9}$, if the type of $x_{3}$ is equal to the type of $x_{7}$, then if the type of $x_{5}$ is equal to the type of $x_{9}$, then $\EqtMACRoH {f (x_{3} , x_{4} , x_{5} , x_{6})}{f (x_{7} , x_{8} , x_{9} , x_{10})}$. Then $\mathrm{OrderType\_\_liftOn\_u2082\_}$ applied to $x_{1}$, $x_{2}$, $x_{11}$, $x_{13}$, $f$ and $c$ is an element of $x$.
OrderType.omega0defMathlib.Order.Types.Defs, function or constant
Wording
the omega (from the name)
English
The omega is an order type defined as the lift of the type of $\Natural$.
OrderType.typedefMathlib.Order.Types.Defs, function or constant
Wording
the type of x (from the name)
English
Let $x$ be a set. Then the type of $x$ is an order type defined as $\operatorname{mk}$ applied to $\operatorname{instSetoid}$ and $\operatorname{of}$ applied to $x$.

Mathlib.Order.UpperLower.Closure

LowerSet.erasedefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
Let $s$ be a lower set of $x$. Let $a$ be an element of $x$. Then $\operatorname{erase}$ applied to $s$ and $a$ is a lower set of $x$.
LowerSet.sdiffdefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
Let $s$ be a lower set of $x$. Let $t$ be an element of $\wp x$. Then $\operatorname{sdiff}$ applied to $s$ and $t$ is a lower set of $x$.
UpperSet.erasedefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
Let $s$ be a upper set of $x$. Let $a$ be an element of $x$. Then $\operatorname{erase}$ applied to $s$ and $a$ is a upper set of $x$.
UpperSet.sdiffdefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
Let $s$ be a upper set of $x$. Let $t$ be an element of $\wp x$. Then $\operatorname{sdiff}$ applied to $s$ and $t$ is a upper set of $x$.
giLowerClosureCoedefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
$\mathrm{giLowerClosureCoe}$ is a Galois insertion of $\mathrm{lowerClosure}$ and $\operatorname{instSetLike}$.
giUpperClosureCoedefMathlib.Order.UpperLower.Closure, function or constant
Wording
no wording
English
$\mathrm{giUpperClosureCoe}$ is a Galois insertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\mathrm{upperClosure}$ and $\operatorname{comp}$ applied to $\operatorname{instSetLike}$ and $\operatorname{coe}$ applied to the order dual.
lowerClosuredefMathlib.Order.UpperLower.Closure, function or constant
Wording
the lower closure of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the lower closure of $s$ is a lower set of $x$.
upperClosuredefMathlib.Order.UpperLower.Closure, function or constant
Wording
the upper closure of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the upper closure of $s$ is a upper set of $x$.

Mathlib.Order.UpperLower.CompleteLattice

LowerSet.compldefMathlib.Order.UpperLower.CompleteLattice, function or constant
Wording
the complement of s (from the docstring)
English
Let $s$ be a lower set of $x$. Then the complement of $s$ is a upper set of $x$.
LowerSet.mapdefMathlib.Order.UpperLower.CompleteLattice, function or constant
Wording
the map of f (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then the map of $f$ is an order isomorphism of the set of lower sets of $x$ and the set of lower sets of $x_{1}$.
UpperSet.compldefMathlib.Order.UpperLower.CompleteLattice, function or constant
Wording
the complement of s (from the docstring)
English
Let $s$ be a upper set of $x$. Then the complement of $s$ is a lower set of $x$.
UpperSet.mapdefMathlib.Order.UpperLower.CompleteLattice, function or constant
Wording
the map of f (from the name)
English
Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then the map of $f$ is an order isomorphism of the set of upper sets of $x$ and the set of upper sets of $x_{1}$.
upperSetIsoLowerSetdefMathlib.Order.UpperLower.CompleteLattice, function or constant
Wording
the upper set isomorphism lower set (from the name)
English
The upper set isomorphism lower set is an order isomorphism of the set of upper sets of $x$ and the set of lower sets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{compl}$, $\operatorname{compl}$, $\mathrm{UpperSet\_\_compl\_compl}$ and $\mathrm{LowerSet\_\_compl\_compl}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{UpperSet\_\_compl\_le\_compl}$.

Mathlib.Order.UpperLower.Hom

LowerSet.iicInfHomdefMathlib.Order.UpperLower.Hom, function or constant
Wording
no wording
English
$\operatorname{iicInfHom}$ is an infimum homomorphism of $x$ and the set of lower sets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Iic}$ and $\mathrm{LowerSet\_\_Iic\_inf}$.
LowerSet.iicsInfHomdefMathlib.Order.UpperLower.Hom, function or constant
Wording
no wording
English
$\operatorname{iicsInfHom}$ is an infimum homomorphism of $x$ and the set of lower sets of $x$.
UpperSet.iciSupHomdefMathlib.Order.UpperLower.Hom, function or constant
Wording
no wording
English
$\operatorname{iciSupHom}$ is a supremum homomorphism of $x$ and the set of upper sets of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Ici}$ and $\mathrm{UpperSet\_\_Ici\_sup}$.
UpperSet.icisSupHomdefMathlib.Order.UpperLower.Hom, function or constant
Wording
no wording
English
$\operatorname{icisSupHom}$ is a supremum homomorphism of $x$ and the set of upper sets of $x$.

Mathlib.Order.UpperLower.Principal

LowerSet.IicdefMathlib.Order.UpperLower.Principal, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{Iic}$ applied to $a$ is a lower set of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Iic}$ applied to $a$ and $\operatorname{Iic}$ applied to $a$.
LowerSet.IiodefMathlib.Order.UpperLower.Principal, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{Iio}$ applied to $a$ is a lower set of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Iio}$ applied to $a$ and $\operatorname{Iio}$ applied to $a$.
UpperSet.IcidefMathlib.Order.UpperLower.Principal, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{Ici}$ applied to $a$ is a upper set of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Ici}$ applied to $a$ and $\operatorname{Ici}$ applied to $a$.
UpperSet.IoidefMathlib.Order.UpperLower.Principal, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\operatorname{Ioi}$ applied to $a$ is a upper set of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Ioi}$ applied to $a$ and $\operatorname{Ioi}$ applied to $a$.

Mathlib.Order.UpperLower.Prod

LowerSet.proddefMathlib.Order.UpperLower.Prod, function or constant
Wording
the product of s and t (from the name)
English
Let $s$ be a lower set of $x$. Let $t$ be a lower set of $x_{1}$. Then the product of $s$ and $t$ is a lower set of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
UpperSet.proddefMathlib.Order.UpperLower.Prod, function or constant
Wording
the product of s and t (from the name)
English
Let $s$ be a upper set of $x$. Let $t$ be a upper set of $x_{1}$. Then the product of $s$ and $t$ is a upper set of $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

Mathlib.Order.WellFounded

Function.argmaxdefMathlib.Order.WellFounded, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{argmax}$ applied to $f$ is an element of $x$.
Function.argmaxOndefMathlib.Order.WellFounded, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a nonempty element of $\wp x$. Then $\operatorname{argmaxOn}$ applied to $f$, $s$ and $\mathrm{hs}$ is an element of $x$.
Function.argmindefMathlib.Order.WellFounded, function or constant
Wording
the argmin of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the argmin of $f$ is an element of $x$.
Function.argminOndefMathlib.Order.WellFounded, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a nonempty element of $\wp x$. Then $\operatorname{argminOn}$ applied to $f$, $s$ and $\mathrm{hs}$ is an element of $x$.
WellFounded.mindefMathlib.Order.WellFounded, function or constant
Wording
the minimum of s (from the name)
English
Assume that $\mathrm{WellFounded}$ holds for $r$. Let $s$ be a nonempty element of $\wp x$. Then the minimum of $s$ is an element of $x$ defined as $\operatorname{choose}$ applied to $\mathrm{WellFounded\_\_has\_min}$ applied to $H$, $s$ and $h$.
WellFoundedGT.maxdefMathlib.Order.WellFounded, function or constant
Wording
the maximum of s and h1 (from the name)
English
Let $s$ be a nonempty element of $\wp x$. Then the maximum of $s$ and $h_{1}$ is an element of $x$ defined as the minimum of $s$.
WellFoundedLT.mindefMathlib.Order.WellFounded, function or constant
Wording
the minimum of s and h1 (from the name)
English
Let $s$ be a nonempty element of $\wp x$. Then the minimum of $s$ and $h_{1}$ is an element of $x$ defined as the minimum of $s$.

Mathlib.Order.WellFoundedSet

Set.IsPWOdefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\operatorname{IsPWO}$ holds for $s$, if $\operatorname{PartiallyWellOrderedOn}$ holds for $s$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
Set.IsWFdefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\operatorname{IsWF}$ holds for $s$, if $\operatorname{WellFoundedOn}$ holds for $s$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$.
Set.IsWF.mindefMathlib.Order.WellFoundedSet, function or constant
Wording
the minimum of hs and hn (from the name)
English
Assume that $\operatorname{IsWF}$ holds for $s$. Assume that $s$ is nonempty. Then the minimum of $\mathrm{hs}$ and $\mathrm{hn}$ is an element of $x$.
Set.PartiallyWellOrderedOndefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
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 $\operatorname{PartiallyWellOrderedOn}$ holds for $s$ and $r$, if $\mathrm{WellQuasiOrdered}$ holds for $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$.
Set.PartiallyWellOrderedOn.IsBadSeqdefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Let $f$ be a function from natural numbers to elements of $x$. Then $\operatorname{IsBadSeq}$ holds for $r$, $s$ and $f$, if for all natural numbers $n$, $\MembershipmemMACRoT {s}{f (n)}$ and for all natural numbers $m$, for all natural numbers $n_{1}$, if $m < n_{1}$, then it is not the case that $r$ holds for $f$ applied to $m$ and $f$ applied to $n_{1}$.
Set.PartiallyWellOrderedOn.IsMinBadSeqdefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $\mathrm{rk}$ be a function from elements of $x$ to natural numbers. Let $s$ be an element of $\wp x$. Let $n$ be a natural number. Let $f$ be a function from natural numbers to elements of $x$. Then $\operatorname{IsMinBadSeq}$ holds for $r$, $\mathrm{rk}$, $s$, $n$ and $f$, if for all functions $g$ from natural numbers to elements of $x$, if for all natural numbers $m$, if $m < n$, then $\EqtMACRoH {f (m)}{g (m)}$, then if $\mathrm{rk} (g (n))< \mathrm{rk} (f (n))$, then it is not the case that $\operatorname{IsBadSeq}$ holds for $r$, $s$ and $g$.
Set.PartiallyWellOrderedOn.minBadSeqOfBadSeqdefMathlib.Order.WellFoundedSet, function or constant
Wording
the minimum bad sequence of n and f (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $\mathrm{rk}$ be a function from elements of $x$ to natural numbers. Let $s$ be an element of $\wp x$. Let $n$ be a natural number. Let $f$ be a function from natural numbers to elements of $x$ such that $\operatorname{IsBadSeq}$ holds for $r$, $s$ and $f$. Then the minimum bad sequence of $n$ and $f$ is an element of $\SubtypeSet {g}{\mathrm{and} (\mathrm{forall} (\Natural , \lambda m . \mathrm{if} (\mathrm{Lt} (m , n), \EqtMACRoH {f (m)}{g (m)})), \mathrm{and} (\operatorname{IsBadSeq} (r , s , g), \operatorname{IsMinBadSeq} (r , \mathrm{rk} , s , n , g)))}$.
Set.WellFoundedOndefMathlib.Order.WellFoundedSet, predicate
Wording
no wording
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 $\operatorname{WellFoundedOn}$ holds for $s$ and $r$, if $\mathrm{WellFounded}$ holds for $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$.

Mathlib.Order.WellQuasiOrder

WellQuasiOrdereddefMathlib.Order.WellQuasiOrder, predicate
Wording
no wording
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then $\mathrm{WellQuasiOrdered}$ holds for $r$, if for all functions $f$ from natural numbers to elements of $x$, there exist natural numbers $m$ and $n$, such that $m < n$ and $r$ holds for $f$ applied to $m$ and $f$ applied to $n$.
WellQuasiOrderedLEclassMathlib.Order.WellQuasiOrder, predicate
Wording
no wording
English
Let $x$ be a set. Then we can say that $\mathrm{WellQuasiOrderedLE}$ holds for $x$.

Mathlib.Order.WithBot

Equiv.withBotCongrdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{withBotCongr}$ applied to $e$ is an element of $\EquivMACRoAE {\mathrm{WithBot} (x)}{\mathrm{WithBot} (x_{1})}$.
Equiv.withBotSubtypeNedefMathlib.Order.WithBot, function or constant
Wording
no wording
English
$\operatorname{withBotSubtypeNe}$ is an element of $\EquivMACRoAE {(\SubtypeSet {y}{\mathrm{Neq} (y , \operatorname{bot})})}{x}$.
Equiv.withTopCongrdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then $\operatorname{withTopCongr}$ applied to $e$ is an element of $\EquivMACRoAE {\mathrm{WithTop} (x)}{\mathrm{WithTop} (x_{1})}$.
Equiv.withTopSubtypeNedefMathlib.Order.WithBot, function or constant
Wording
no wording
English
$\operatorname{withTopSubtypeNe}$ is an element of $\EquivMACRoAE {(\SubtypeSet {y}{\mathrm{Neq} (y , \operatorname{top})})}{x}$.
WithBot.LEinductiveMathlib.Order.WithBot, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{WithBot}$ applied to $x$. Then we can say that $\operatorname{LE}$ holds for $x_{2}$ and $x_{3}$.
WithBot.LTinductiveMathlib.Order.WithBot, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{WithBot}$ applied to $x$. Then we can say that $\operatorname{LT}$ holds for $x_{2}$ and $x_{3}$.
WithBot.mapdefMathlib.Order.WithBot, function or constant
Wording
the map of f and x2 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{WithBot}$ applied to $x$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{WithBot}$ applied to $x_{1}$ defined as $\operatorname{map}$ applied to $f$ and $x_{2}$.
WithBot.map₂defMathlib.Order.WithBot, function or constant
Wording
the map of x4 and x5 (from the name)
English
Let $x_{3}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\mathrm{WithBot}$ applied to $x$. Let $x_{5}$ be an element of $\mathrm{WithBot}$ applied to $x_{1}$. Then the map of $x_{4}$ and $x_{5}$ is an element of $\mathrm{WithBot}$ applied to $x_{2}$ defined as the map of $x_{4}$ and $x_{5}$.
WithBot.ofDualdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
$\operatorname{ofDual}$ is an equivalence from $\mathrm{WithBot}$ applied to the set of order duals of $x$ to $\mathrm{WithTop}$ applied to $x$ defined as the identity of $\mathrm{WithBot}$ applied to the set of order duals of $x$.
WithBot.toDualdefMathlib.Order.WithBot, function or constant
Wording
the dual (from the name)
English
The dual is an equivalence from $\mathrm{WithBot}$ applied to $x$ to $\mathrm{WithTop}$ applied to the set of order duals of $x$ defined as the identity of $\mathrm{WithBot}$ applied to $x$.
WithBot.unbotdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $\mathrm{WithBot}$ applied to $x$ such that $x_{1}$ is distinct from the bottom. Then $\operatorname{unbot}$ applied to $x_{1}$ and $h$ is an element of $x$.
WithBot.unbotAdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $\mathrm{WithBot}$ applied to $x$. Then $\operatorname{unbotA}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{unbotD}$ applied to $\operatorname{arbitrary}$ applied to $x$ and $x_{1}$.
WithBot.unbotDdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $d$ be an element of $x$. Let $x_{1}$ be an element of $\mathrm{WithBot}$ applied to $x$. Then $\operatorname{unbotD}$ applied to $d$ and $x_{1}$ is an element of $x$ defined as $\operatorname{recBotCoe}$ applied to $d$, $\mathrm{id}$ and $x_{1}$.
WithTop.LEinductiveMathlib.Order.WithBot, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{WithTop}$ applied to $x$. Then we can say that $\operatorname{LE}$ holds for $x_{2}$ and $x_{3}$.
WithTop.LTinductiveMathlib.Order.WithBot, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{WithTop}$ applied to $x$. Then we can say that $\operatorname{LT}$ holds for $x_{2}$ and $x_{3}$.
WithTop.mapdefMathlib.Order.WithBot, function or constant
Wording
the map of f and x2 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{WithTop}$ applied to $x$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{WithTop}$ applied to $x_{1}$ defined as $\operatorname{map}$ applied to $f$ and $x_{2}$.
WithTop.map₂defMathlib.Order.WithBot, function or constant
Wording
the map of x4 and x5 (from the name)
English
Let $x_{3}$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{4}$ be an element of $\mathrm{WithTop}$ applied to $x$. Let $x_{5}$ be an element of $\mathrm{WithTop}$ applied to $x_{1}$. Then the map of $x_{4}$ and $x_{5}$ is an element of $\mathrm{WithTop}$ applied to $x_{2}$ defined as the map of $x_{4}$ and $x_{5}$.
WithTop.ofDualdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
$\operatorname{ofDual}$ is an equivalence from $\mathrm{WithTop}$ applied to the set of order duals of $x$ to $\mathrm{WithBot}$ applied to $x$ defined as the identity of $\mathrm{WithTop}$ applied to the set of order duals of $x$.
WithTop.toDualdefMathlib.Order.WithBot, function or constant
Wording
the dual (from the name)
English
The dual is an equivalence from $\mathrm{WithTop}$ applied to $x$ to $\mathrm{WithBot}$ applied to the set of order duals of $x$ defined as the identity of $\mathrm{WithTop}$ applied to $x$.
WithTop.untopdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $\mathrm{WithTop}$ applied to $x$ such that $x_{1}$ is distinct from the top. Then $\operatorname{untop}$ applied to $x_{1}$ and $h$ is an element of $x$.
WithTop.untopAdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $\mathrm{WithTop}$ applied to $x$. Then $\operatorname{untopA}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{untopD}$ applied to $\operatorname{arbitrary}$ applied to $x$ and $x_{1}$.
WithTop.untopDdefMathlib.Order.WithBot, function or constant
Wording
no wording
English
Let $d$ be an element of $x$. Let $x_{1}$ be an element of $\mathrm{WithTop}$ applied to $x$. Then $\operatorname{untopD}$ applied to $d$ and $x_{1}$ is an element of $x$ defined as $\operatorname{recTopCoe}$ applied to $d$, $\mathrm{id}$ and $x_{1}$.

Mathlib.Order.WithBotTop

EIntdefMathlib.Order.WithBotTop, type
Wording
integer (from the name)
English
An integer is an element of $\mathrm{WithBotTop}$ applied to $\Integer$.
WithBotTopdefMathlib.Order.WithBotTop, type
Wording
no wording
English
Let $x$ be a set. Then an element of $\mathrm{WithBotTop}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{WithBot}$ applied to $\mathrm{WithTop}$ applied to $x$.
WithBotTop.coedefMathlib.Order.WithBotTop, function or constant
Wording
the coercion of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the coercion of $x_{1}$ is an element of $\mathrm{WithBotTop}$ applied to $x$ defined as $\operatorname{comp}$ applied to $\operatorname{some}$, $\operatorname{some}$ and $x_{1}$.
WithTopBotdefMathlib.Order.WithBotTop, type
Wording
no wording
English
Let $x$ be a set. Then an element of $\mathrm{WithTopBot}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{WithTop}$ applied to $\mathrm{WithBot}$ applied to $x$.

‹ previous next ›