Definitions: Mathlib.Order, part 3 of 4

BoundedLatticeHomstructureMathlib.Order.Hom.BoundedLattice, type

Wording

bounded lattice homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the bounded lattice homomorphisms of $x$ and $x_{1}$ are a basic type.

BoundedLatticeHom.compdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a bounded lattice homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a bounded lattice homomorphism of $x$ and $x_{2}$.

BoundedLatticeHom.copydefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a bounded lattice homomorphism of $x$ and $x_{1}$.

BoundedLatticeHom.dualdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of bounded lattice homomorphisms of $x$ and $x_{1}$ to the set of bounded lattice homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

BoundedLatticeHom.iddefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a bounded lattice homomorphism of $x$ and $x$.

BoundedLatticeHom.subtypeValdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the subtype value of Psup and Pinf (from the name)

English

Assume that $P$ holds for the bottom. Assume that $P$ holds for the top. Assume that for all elements $x_{5}$ and $y_{1}$ of $x$, if $P$ holds for $x_{5}$, then if $P$ holds for $y_{1}$, then $P$ holds for $\MaxmaxMACRoAF {x_{5}}{y_{1}}$. Assume that for all elements $x_{4}$ and $y$ of $x$, if $P$ holds for $x_{4}$, then if $P$ holds for $y$, then $P$ holds for $\MinminMACRoAG {x_{4}}{y}$. Then the subtype value of $\mathrm{Psup}$ and $\mathrm{Pinf}$ is a bounded lattice homomorphism of $\SubtypeSet {x_{3}}{P (x_{3})}$ and $x$.

BoundedLatticeHom.toBoundedOrderHomdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the bounded order homomorphism of f (from the name)

English

Let $f$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Then the bounded order homomorphism of $f$ is a bounded order homomorphism of $x$ and $x_{1}$.

BoundedLatticeHom.toInfTopHomdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the infimum top homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Then the infimum top homomorphism of $\mathrm{self}$ is an infimum top homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toSupHom}$ applied to $\operatorname{toLatticeHom}$ applied to $\mathrm{self}$ and $\mathrm{LatticeHom\_\_map\_inf'}$ applied to $\operatorname{toLatticeHom}$ applied to $\mathrm{self}$ and $\mathrm{BoundedLatticeHom\_\_map\_top'}$ applied to $\mathrm{self}$.

BoundedLatticeHom.toSupBotHomdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the supremum bottom homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Then the supremum bottom homomorphism of $\mathrm{self}$ is a supremum bottom homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toSupHom}$ applied to $\operatorname{toLatticeHom}$ applied to $\mathrm{self}$ and $\mathrm{BoundedLatticeHom\_\_map\_bot'}$ applied to $\mathrm{self}$.

BoundedLatticeHomClassclassMathlib.Order.Hom.BoundedLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{BoundedLatticeHomClass}$ holds for $F$, $x$ and $x_{1}$.

InfTopHomstructureMathlib.Order.Hom.BoundedLattice, type

Wording

infimum top homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the infimum top homomorphisms of $x$ and $x_{1}$ are a basic type.

InfTopHom.compdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an infimum top homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an infimum top homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an infimum top homomorphism of $x$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toInfHom}$ applied to $f$ and $\operatorname{toInfHom}$ applied to $g$ and $\mathrm{TopHom\_\_map\_top'}$ applied to the composition of the top homomorphism of $f$ and the top homomorphism of $g$.

InfTopHom.copydefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be an infimum top homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an infimum top homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the copy of $\operatorname{toInfHom}$ applied to $f$ and $\mathrm{f'}$ and $\mathrm{TopHom\_\_map\_top'}$ applied to the copy of the top homomorphism of $f$ and $\mathrm{f'}$.

InfTopHom.dualdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of infimum top homomorphisms of $x$ and $x_{1}$ to the set of supremum bottom homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

InfTopHom.iddefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is an infimum top homomorphism of $x$ and $x$.

InfTopHom.subtypeValdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the subtype value of Ptop and Pinf (from the name)

English

Assume that $P$ holds for the top. Assume that for all elements $x_{4}$ and $y$ of $x$, if $P$ holds for $x_{4}$, then if $P$ holds for $y$, then $P$ holds for $\MinminMACRoAG {x_{4}}{y}$. Then the subtype value of $\mathrm{Ptop}$ and $\mathrm{Pinf}$ is an infimum top homomorphism of $\SubtypeSet {x_{3}}{P (x_{3})}$ and $x$.

InfTopHom.toTopHomdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the top homomorphism of self (from the name)

English

Let $\mathrm{self}$ be an infimum top homomorphism of $x$ and $x_{1}$. Then the top homomorphism of $\mathrm{self}$ is a top homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toInfHom}$ applied to $\mathrm{self}$ and $\mathrm{InfTopHom\_\_map\_top'}$ applied to $\mathrm{self}$.

InfTopHomClassclassMathlib.Order.Hom.BoundedLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{InfTopHomClass}$ holds for $F$, $x$ and $x_{1}$.

SupBotHomstructureMathlib.Order.Hom.BoundedLattice, type

Wording

supremum bottom homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the supremum bottom homomorphisms of $x$ and $x_{1}$ are a basic type.

SupBotHom.compdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a supremum bottom homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a supremum bottom homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a supremum bottom homomorphism of $x$ and $x_{2}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toSupHom}$ applied to $f$ and $\operatorname{toSupHom}$ applied to $g$ and $\mathrm{BotHom\_\_map\_bot'}$ applied to the composition of the bottom homomorphism of $f$ and the bottom homomorphism of $g$.

SupBotHom.copydefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a supremum bottom homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a supremum bottom homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the copy of $\operatorname{toSupHom}$ applied to $f$ and $\mathrm{f'}$ and $\mathrm{BotHom\_\_map\_bot'}$ applied to the copy of the bottom homomorphism of $f$ and $\mathrm{f'}$.

SupBotHom.dualdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of supremum bottom homomorphisms of $x$ and $x_{1}$ to the set of infimum top homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

SupBotHom.iddefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a supremum bottom homomorphism of $x$ and $x$.

SupBotHom.subtypeValdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the subtype value of Pbot and Psup (from the name)

English

Assume that $P$ holds for the bottom. Assume that for all elements $x_{4}$ and $y$ of $x$, if $P$ holds for $x_{4}$, then if $P$ holds for $y$, then $P$ holds for $\MaxmaxMACRoAF {x_{4}}{y}$. Then the subtype value of $\mathrm{Pbot}$ and $\mathrm{Psup}$ is a supremum bottom homomorphism of $\SubtypeSet {x_{3}}{P (x_{3})}$ and $x$.

SupBotHom.toBotHomdefMathlib.Order.Hom.BoundedLattice, function or constant

Wording

the bottom homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a supremum bottom homomorphism of $x$ and $x_{1}$. Then the bottom homomorphism of $\mathrm{self}$ is a bottom homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toSupHom}$ applied to $\mathrm{self}$ and $\mathrm{SupBotHom\_\_map\_bot'}$ applied to $\mathrm{self}$.

SupBotHomClassclassMathlib.Order.Hom.BoundedLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{SupBotHomClass}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Order.Hom.CompleteLattice

CompleteLatticeHomstructureMathlib.Order.Hom.CompleteLattice, type

Wording

complete lattice homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the complete lattice homomorphisms of $x$ and $x_{1}$ are a basic type.

CompleteLatticeHom.OrderIso.toCompleteLatticeHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the complete lattice homomorphism of f (from the name)

English

Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then the complete lattice homomorphism of $f$ is a complete lattice homomorphism of $x$ and $x_{1}$.

CompleteLatticeHom.compdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a complete lattice homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a complete lattice homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a complete lattice homomorphism of $x$ and $x_{2}$.

CompleteLatticeHom.copydefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a complete lattice homomorphism of $x$ and $x_{1}$.

CompleteLatticeHom.dualdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of complete lattice homomorphisms of $x$ and $x_{1}$ to the set of complete lattice homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

CompleteLatticeHom.iddefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a complete lattice homomorphism of $x$ and $x$.

CompleteLatticeHom.setPreimagedefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the set preimage of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the set preimage of $f$ is a complete lattice homomorphism of $\wp x_{1}$ and $\wp x$.

CompleteLatticeHom.toBoundedLatticeHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the bounded lattice homomorphism of f (from the name)

English

Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$. Then the bounded lattice homomorphism of $f$ is a bounded lattice homomorphism of $x$ and $x_{1}$.

CompleteLatticeHom.tosSupHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a complete lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{tosSupHom}$ applied to $\mathrm{self}$ is a supremum homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{tosInfHom}$ applied to $\mathrm{self}$ and $\mathrm{CompleteLatticeHom\_\_map\_sSup'}$ applied to $\mathrm{self}$.

CompleteLatticeHomClassclassMathlib.Order.Hom.CompleteLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{CompleteLatticeHomClass}$ holds for $F$, $x$ and $x_{1}$.

Equiv.toOrderIsoSetdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the order isomorphism set of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the order isomorphism set of $e$ is an order isomorphism of $\wp x$ and $\wp x_{1}$.

FrameHomstructureMathlib.Order.Hom.CompleteLattice, type

Wording

frame homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the frame homomorphisms of $x$ and $x_{1}$ are a basic type.

FrameHom.compdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a frame homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a frame homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a frame homomorphism of $x$ and $x_{2}$.

FrameHom.copydefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a frame homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a frame homomorphism of $x$ and $x_{1}$.

FrameHom.iddefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a frame homomorphism of $x$ and $x$.

FrameHom.toLatticeHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the lattice homomorphism of f (from the name)

English

Let $f$ be a frame homomorphism of $x$ and $x_{1}$. Then the lattice homomorphism of $f$ is a lattice homomorphism of $x$ and $x_{1}$.

FrameHomClassclassMathlib.Order.Hom.CompleteLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{FrameHomClass}$ holds for $F$, $x$ and $x_{1}$.

infsInfHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

no wording

English

$\mathrm{infsInfHom}$ is an infimum homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

sInfHomstructureMathlib.Order.Hom.CompleteLattice, type

Wording

infimum homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the infimum homomorphisms of $x$ and $x_{1}$ are a basic type.

sInfHom.compdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an infimum homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an infimum homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an infimum homomorphism of $x$ and $x_{2}$.

sInfHom.copydefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be an infimum homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is an infimum homomorphism of $x$ and $x_{1}$.

sInfHom.dualdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of infimum homomorphisms of $x$ and $x_{1}$ to the set of supremum homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

sInfHom.iddefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is an infimum homomorphism of $x$ and $x$.

sInfHom.toFundefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the infimum homomorphism of self and x4 (from the name)

English

Let $\mathrm{self}$ be an infimum homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the infimum homomorphism of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

sInfHomClassclassMathlib.Order.Hom.CompleteLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{sInfHomClass}$ holds for $F$, $x$ and $x_{1}$.

sSupHomstructureMathlib.Order.Hom.CompleteLattice, type

Wording

supremum homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the supremum homomorphisms of $x$ and $x_{1}$ are a basic type.

sSupHom.compdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a supremum homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a supremum homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a supremum homomorphism of $x$ and $x_{2}$.

sSupHom.copydefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a supremum homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a supremum homomorphism of $x$ and $x_{1}$.

sSupHom.dualdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of supremum homomorphisms of $x$ and $x_{1}$ to the set of infimum homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

sSupHom.iddefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a supremum homomorphism of $x$ and $x$.

sSupHom.setImagedefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the set image of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the set image of $f$ is a supremum homomorphism of $\wp x$ and $\wp x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{image}$ applied to $f$ and $\mathrm{Set\_\_image\_sSup}$.

sSupHom.toFundefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

the supremum homomorphism of self and x4 (from the name)

English

Let $\mathrm{self}$ be a supremum homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then the supremum homomorphism of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

sSupHomClassclassMathlib.Order.Hom.CompleteLattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{sSupHomClass}$ holds for $F$, $x$ and $x_{1}$.

supsSupHomdefMathlib.Order.Hom.CompleteLattice, function or constant

Wording

no wording

English

$\mathrm{supsSupHom}$ is a supremum homomorphism of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.

Mathlib.Order.Hom.Lattice

InfHomstructureMathlib.Order.Hom.Lattice, type

Wording

infimum homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the infimum homomorphisms of $x$ and $x_{1}$ are a basic type.

InfHom.compdefMathlib.Order.Hom.Lattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an infimum homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be an infimum homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is an infimum homomorphism of $x$ and $x_{2}$.

InfHom.constdefMathlib.Order.Hom.Lattice, function or constant

Wording

the constant function of x and b (from the docstring)

English

Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant function of $x$ and $b$ is an infimum homomorphism of $x$ and $x_{1}$.

InfHom.copydefMathlib.Order.Hom.Lattice, function or constant

Wording

the copy of f and h (from the name)

English

InfHom.dualdefMathlib.Order.Hom.Lattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of infimum homomorphisms of $x$ and $x_{1}$ to the set of supremum homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

InfHom.iddefMathlib.Order.Hom.Lattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is an infimum homomorphism of $x$ and $x$.

InfHom.subtypeValdefMathlib.Order.Hom.Lattice, function or constant

Wording

the subtype value of Pinf (from the name)

English

Assume that for all elements $x_{3}$ and $y$ of $x$, if $P$ holds for $x_{3}$, then if $P$ holds for $y$, then $P$ holds for $\MinminMACRoAG {x_{3}}{y}$. Then the subtype value of $\mathrm{Pinf}$ is an infimum homomorphism of $\SubtypeSet {x_{2}}{P (x_{2})}$ and $x$.

InfHom.toFundefMathlib.Order.Hom.Lattice, function or constant

Wording

the infimum homomorphism of self and x4 (from the name)

English

InfHomClassclassMathlib.Order.Hom.Lattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{InfHomClass}$ holds for $F$, $x$ and $x_{1}$.

LatticeHomstructureMathlib.Order.Hom.Lattice, type

Wording

lattice homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the lattice homomorphisms of $x$ and $x_{1}$ are a basic type.

LatticeHom.compdefMathlib.Order.Hom.Lattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a lattice homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a lattice homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a lattice homomorphism of $x$ and $x_{2}$.

LatticeHom.copydefMathlib.Order.Hom.Lattice, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Let $\mathrm{f'}$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a lattice homomorphism of $x$ and $x_{1}$.

LatticeHom.dualdefMathlib.Order.Hom.Lattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of lattice homomorphisms of $x$ and $x_{1}$ to the set of lattice homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

LatticeHom.fstdefMathlib.Order.Hom.Lattice, function or constant

Wording

the first component (from the name)

English

The first component is a lattice homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

LatticeHom.iddefMathlib.Order.Hom.Lattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a lattice homomorphism of $x$ and $x$.

LatticeHom.snddefMathlib.Order.Hom.Lattice, function or constant

Wording

the second component (from the name)

English

The second component is a lattice homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

LatticeHom.subtypeValdefMathlib.Order.Hom.Lattice, function or constant

Wording

the subtype value of Psup and Pinf (from the name)

English

Assume that for all elements $x_{4}$ and $y_{1}$ of $x$, if $P$ holds for $x_{4}$, then if $P$ holds for $y_{1}$, then $P$ holds for $\MaxmaxMACRoAF {x_{4}}{y_{1}}$. Assume that for all elements $x_{3}$ and $y$ of $x$, if $P$ holds for $x_{3}$, then if $P$ holds for $y$, then $P$ holds for $\MinminMACRoAG {x_{3}}{y}$. Then the subtype value of $\mathrm{Psup}$ and $\mathrm{Pinf}$ is a lattice homomorphism of $\SubtypeSet {x_{2}}{P (x_{2})}$ and $x$.

LatticeHom.toInfHomdefMathlib.Order.Hom.Lattice, function or constant

Wording

the infimum homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a lattice homomorphism of $x$ and $x_{1}$. Then the infimum homomorphism of $\mathrm{self}$ is an infimum homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toSupHom}$ applied to $\mathrm{self}$ and $\mathrm{LatticeHom\_\_map\_inf'}$ applied to $\mathrm{self}$.

LatticeHomClassclassMathlib.Order.Hom.Lattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{LatticeHomClass}$ holds for $F$, $x$ and $x_{1}$.

OrderHomClass.toLatticeHomdefMathlib.Order.Hom.Lattice, function or constant

Wording

the lattice homomorphism of f (from the name)

English

Let $x$ and $x_{1}$ be sets. Let $f$ be an element of $F$. Then the lattice homomorphism of $f$ is a lattice homomorphism of $x$ and $x_{1}$.

Pi.evalLatticeHomdefMathlib.Order.Hom.Lattice, function or constant

Wording

the evaluation lattice homomorphism of i (from the name)

English

Let $i$ be an element of $x$. Then the evaluation lattice homomorphism of $i$ is a lattice homomorphism of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ and $x_{1}$ applied to $i$.

SupHomstructureMathlib.Order.Hom.Lattice, type

Wording

supremum homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the supremum homomorphisms of $x$ and $x_{1}$ are a basic type.

SupHom.compdefMathlib.Order.Hom.Lattice, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a supremum homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a supremum homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a supremum homomorphism of $x$ and $x_{2}$.

SupHom.constdefMathlib.Order.Hom.Lattice, function or constant

Wording

the constant function of x and b (from the docstring)

English

Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant function of $x$ and $b$ is a supremum homomorphism of $x$ and $x_{1}$.

SupHom.copydefMathlib.Order.Hom.Lattice, function or constant

Wording

the copy of f and h (from the name)

English

SupHom.dualdefMathlib.Order.Hom.Lattice, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of supremum homomorphisms of $x$ and $x_{1}$ to the set of infimum homomorphisms of the set of order duals of $x$ and the set of order duals of $x_{1}$.

SupHom.iddefMathlib.Order.Hom.Lattice, function or constant

Wording

the identity of x (from the name)

English

Let $x$ be a set. Then the identity of $x$ is a supremum homomorphism of $x$ and $x$.

SupHom.subtypeValdefMathlib.Order.Hom.Lattice, function or constant

Wording

the subtype value of Psup (from the name)

English

Assume that for all elements $x_{3}$ and $y$ of $x$, if $P$ holds for $x_{3}$, then if $P$ holds for $y$, then $P$ holds for $\MaxmaxMACRoAF {x_{3}}{y}$. Then the subtype value of $\mathrm{Psup}$ is a supremum homomorphism of $\SubtypeSet {x_{2}}{P (x_{2})}$ and $x$.

SupHom.toFundefMathlib.Order.Hom.Lattice, function or constant

Wording

the supremum homomorphism of self and x4 (from the name)

English

SupHomClassclassMathlib.Order.Hom.Lattice, predicate

Wording

no wording

English

Let $F$, $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{SupHomClass}$ holds for $F$, $x$ and $x_{1}$.

orderEmbeddingOfInjectivedefMathlib.Order.Hom.Lattice, function or constant

Wording

the order embedding of f and hf (from the name)

English

Let $f$ be an element of $F$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the order embedding of $f$ and $\mathrm{hf}$ is an order embedding of $x$ and $x_{1}$.

Mathlib.Order.Hom.Lex

OrderIso.sumLexIicIoidefMathlib.Order.Hom.Lex, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{sumLexIicIoi}$ applied to $x_{2}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to the set of elements of $\operatorname{Iic}$ applied to $x_{2}$ and the set of elements of $\operatorname{Ioi}$ applied to $x_{2}$ and $x$.

OrderIso.sumLexIioIcidefMathlib.Order.Hom.Lex, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{sumLexIioIci}$ applied to $x_{2}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Sum}$ applied to the set of elements of $\operatorname{Iio}$ applied to $x_{2}$ and the set of elements of $\operatorname{Ici}$ applied to $x_{2}$ and $x$.

Prod.Lex.prodLexAssocdefMathlib.Order.Hom.Lex, function or constant

Wording

the product lexicographic associator of x1 and x2 (from the name)

English

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the product lexicographic associator of $x_{1}$ and $x_{2}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

Prod.Lex.prodLexCongrdefMathlib.Order.Hom.Lex, function or constant

Wording

the product 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 product lexicographic congruence of $\mathrm{ea}$ and $\mathrm{eb}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.

Prod.Lex.prodUniquedefMathlib.Order.Hom.Lex, function or constant

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then $\operatorname{prodUnique}$ applied to $x$ and $x_{1}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

Prod.Lex.sumLexProdLexDistribdefMathlib.Order.Hom.Lex, function or constant

Wording

no wording

English

Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{sumLexProdLexDistrib}$ applied to $x$, $x_{1}$ and $x_{2}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ 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 $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

Prod.Lex.uniqueProddefMathlib.Order.Hom.Lex, function or constant

Wording

the unique product of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the unique product of $x$ and $x_{1}$ is an order isomorphism of $\mathrm{Lex}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

RelIso.sumLexComplLeftdefMathlib.Order.Hom.Lex, function or constant

Wording

the left sum lexicographic complement of r and x1 (from the name)

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ be an element of $x$. Then the left sum lexicographic complement of $r$ and $x_{1}$ is a relation isomorphism of $\operatorname{Lex}$ applied to $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{3}$ to $r$ applied to $x_{3}$ and $x_{1}$ and $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{4}$ to the proposition that it is not the case that $r$ holds for $x_{4}$ and $x_{1}$ and $r$.

RelIso.sumLexComplRightdefMathlib.Order.Hom.Lex, function or constant

Wording

the right sum lexicographic complement of r and x1 (from the name)

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ be an element of $x$. Then the right sum lexicographic complement of $r$ and $x_{1}$ is a relation isomorphism of $\operatorname{Lex}$ applied to $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{3}$ to the proposition that it is not the case that $r$ holds for $x_{1}$ and $x_{3}$ and $\mathrm{Subrel}$ applied to $r$ and $r$ applied to $x_{1}$ and $r$.

Mathlib.Order.Hom.PowersetCard

Set.powersetCard.ofFinEmbEquivdefMathlib.Order.Hom.PowersetCard, function or constant

Wording

the powerset cardinality (from the name)

English

The powerset cardinality is an equivalence from the set of order embeddings of $\mathrm{Fin}$ applied to $n$ and $I$ to the set of elements of the powerset cardinality of $I$ and $n$.

Set.powersetCard.orderIsoOfFindefMathlib.Order.Hom.PowersetCard, function or constant

Wording

the order isomorphism of s (from the name)

English

Let $s$ be an element of the powerset cardinality of $I$ and $n$. Then the order isomorphism of $s$ is an order isomorphism of $\mathrm{Fin}$ applied to $n$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$.

Set.powersetCard.permOfDisjointdefMathlib.Order.Hom.PowersetCard, function or constant

Wording

the permutation of h (from the docstring)

English

Assume that $s$ is disjoint to $t$. Then the permutation of $h$ is a permutation of $\mathrm{Fin}$ applied to $m + n$ defined as the composition of the inverse of the finite sum finite equivalence and the composition of the equivalence of the sum congruence of the order isomorphism of $s$ and the order isomorphism of $t$ and the composition of $\operatorname{disjUnionEquiv}$ applied to $s$, $t$ and $h$ and the equivalence of the inverse of the order isomorphism of $\operatorname{disjUnion}$ applied to $h$.

Set.powersetCard.signdefMathlib.Order.Hom.PowersetCard, function or constant

Wording

the sign of s (from the name)

English

Let $s$ be an element of the powerset cardinality of $I$ and $n$. Then the sign of $s$ is a unit of $\Integer$.

Mathlib.Order.Hom.Set

OrderEmbedding.orderIsodefMathlib.Order.Hom.Set, function or constant

Wording

the order isomorphism (from the name)

English

The order isomorphism is an order isomorphism of $x$ and the set of elements of the range of $\operatorname{coe}$ applied to $f$.

OrderIso.IccdefMathlib.Order.Hom.Set, function or constant

Wording

the closed interval of x4 and y (from the name)

English

Let $e$ be an order isomorphism of $x$ and $x_{1}$. Let $x_{4}$ and $y$ be elements of $x$. Then the closed interval of $x_{4}$ and $y$ is an order isomorphism of the set of elements of $\SetIccMACRoP {x_{4}}{y}$ and the set of elements of $\SetIccMACRoP {e (x_{4})}{e (y)}$.

OrderIso.IcidefMathlib.Order.Hom.Set, function or constant

Wording

no wording

English

Let $e$ be an order isomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{Ici}$ applied to $e$ and $x_{4}$ is an order isomorphism of the set of elements of $\operatorname{Ici}$ applied to $x_{4}$ and the set of elements of $\operatorname{Ici}$ applied to $e$ applied to $x_{4}$.

OrderIso.IicdefMathlib.Order.Hom.Set, function or constant

Wording

no wording

English

Let $e$ be an order isomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{Iic}$ applied to $e$ and $x_{4}$ is an order isomorphism of the set of elements of $\operatorname{Iic}$ applied to $x_{4}$ and the set of elements of $\operatorname{Iic}$ applied to $e$ applied to $x_{4}$.

OrderIso.Set.univdefMathlib.Order.Hom.Set, function or constant

Wording

the universal set (from the name)

English

The universal set is an order isomorphism of the set of elements of the universal set and $x$.

OrderIso.compldefMathlib.Order.Hom.Set, function or constant

Wording

the complement of x (from the name)

English

Let $x$ be a set. Then the complement of $x$ is an order isomorphism of $x$ and the set of order duals of $x$.

Set.memOrderIsodefMathlib.Order.Hom.Set, function or constant

Wording

the membership order isomorphism (from the name)

English

The membership order isomorphism is an order isomorphism of $\wp x$ and the set of functions from elements of $x$ to propositions.

Set.orderIsoOfEqdefMathlib.Order.Hom.Set, function or constant

Wording

the order isomorphism of s and t (from the name)

English

Let $s$ and $t$ be elements of $\wp x$ such that $\EqtMACRoH {s}{t}$. Then the order isomorphism of $s$ and $t$ is an order isomorphism of the set of elements of $s$ and the set of elements of $t$.

Set.sumEquivdefMathlib.Order.Hom.Set, function or constant

Wording

the sum equivalence (from the name)

English

The sum equivalence is an order isomorphism of $\wp \mathrm{Sum} (x , x_{1})$ and $\mathrm{Prod}$ applied to $\wp x$ and $\wp x_{1}$.

StrictMono.orderIsodefMathlib.Order.Hom.Set, function or constant

Wording

the order isomorphism of f and h_mono (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{StrictMono}$ holds for $f$. Then the order isomorphism of $f$ and $\mathrm{h\_mono}$ is an order isomorphism of $x$ and the set of elements of the range of $f$ defined as $\operatorname{mk}$ applied to the equivalence of $f$ and $\operatorname{injective}$ applied to $\mathrm{h\_mono}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{StrictMono\_\_le\_iff\_le}$ applied to $\mathrm{h\_mono}$.

StrictMono.orderIsoOfSurjectivedefMathlib.Order.Hom.Set, function or constant

Wording

the order isomorphism of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{StrictMono}$ holds for $f$ and $\operatorname{Surjective}$ holds for $f$. Then the order isomorphism of $f$ is an order isomorphism of $x$ and $x_{1}$ defined as the composition of the order isomorphism of $f$ and $\mathrm{h\_mono}$ and the composition of the order isomorphism of the range of $f$ and the universal set and the universal set.

StrictMonoOn.orderIsodefMathlib.Order.Hom.Set, function or constant

Wording

the order isomorphism 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 an element of $\wp x$ such that $\mathrm{StrictMonoOn}$ holds for $f$ and $s$. Then the order isomorphism of $f$ and $s$ is an order isomorphism of the set of elements of $s$ and the set of elements of the image of $f$ and $s$.

Mathlib.Order.Hom.WithTopBot

Function.Embedding.coeWithBotdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the coercion with bottom (from the name)

English

The coercion with bottom is an embedding of $x$ and $\mathrm{WithBot}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{some}$ and $\mathrm{WithBot\_\_coe\_injective}$.

Function.Embedding.coeWithTopdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the coercion with top (from the name)

English

The coercion with top is an embedding of $x$ and $\mathrm{WithTop}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\operatorname{some}$ and $\mathrm{WithTop\_\_coe\_injective}$.

InfHom.withBotdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an infimum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot}$ applied to $f$ is an infimum homomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

InfHom.withBot'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an infimum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot'}$ applied to $f$ is an infimum homomorphism of $\mathrm{WithBot}$ applied to $x$ and $x_{1}$.

InfHom.withTopdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an infimum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop}$ applied to $f$ is an infimum top homomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

InfHom.withTop'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an infimum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop'}$ applied to $f$ is an infimum top homomorphism of $\mathrm{WithTop}$ applied to $x$ and $x_{1}$.

LatticeHom.withBotdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot}$ applied to $f$ is a lattice homomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

LatticeHom.withBot'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot'}$ applied to $f$ is a lattice homomorphism of $\mathrm{WithBot}$ applied to $x$ and $x_{1}$.

LatticeHom.withBotWithTopdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBotWithTop}$ applied to $f$ is a bounded lattice homomorphism of $\mathrm{WithBot}$ applied to $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithBot}$ applied to $\mathrm{WithTop}$ applied to $x_{1}$.

LatticeHom.withBotWithTop'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBotWithTop'}$ applied to $f$ is a bounded lattice homomorphism of $\mathrm{WithBot}$ applied to $\mathrm{WithTop}$ applied to $x$ and $x_{1}$.

LatticeHom.withTopdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop}$ applied to $f$ is a lattice homomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

LatticeHom.withTop'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop'}$ applied to $f$ is a lattice homomorphism of $\mathrm{WithTop}$ applied to $x$ and $x_{1}$.

LatticeHom.withTopWithBotdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTopWithBot}$ applied to $f$ is a bounded lattice homomorphism of $\mathrm{WithTop}$ applied to $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithTop}$ applied to $\mathrm{WithBot}$ applied to $x_{1}$.

LatticeHom.withTopWithBot'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a lattice homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTopWithBot'}$ applied to $f$ is a bounded lattice homomorphism of $\mathrm{WithTop}$ applied to $\mathrm{WithBot}$ applied to $x$ and $x_{1}$.

OrderEmbedding.withBotMapdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an order embedding of $x$ and $x_{1}$. Then $\operatorname{withBotMap}$ applied to $f$ is an order embedding of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

OrderEmbedding.withTopMapdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an order embedding of $x$ and $x_{1}$. Then $\operatorname{withTopMap}$ applied to $f$ is an order embedding of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

OrderHom.withBotMapdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBotMap}$ applied to $f$ is an order homomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

OrderHom.withTopMapdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTopMap}$ applied to $f$ is an order homomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

OrderIso.withBotCongrdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{withBotCongr}$ applied to $e$ is an order isomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

OrderIso.withTopCongrdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{withTopCongr}$ applied to $e$ is an order isomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

SupHom.withBotdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a supremum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot}$ applied to $f$ is a supremum bottom homomorphism of $\mathrm{WithBot}$ applied to $x$ and $\mathrm{WithBot}$ applied to $x_{1}$.

SupHom.withBot'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a supremum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withBot'}$ applied to $f$ is a supremum bottom homomorphism of $\mathrm{WithBot}$ applied to $x$ and $x_{1}$.

SupHom.withTopdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a supremum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop}$ applied to $f$ is a supremum homomorphism of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{WithTop}$ applied to $x_{1}$.

SupHom.withTop'defMathlib.Order.Hom.WithTopBot, function or constant

Wording

no wording

English

Let $f$ be a supremum homomorphism of $x$ and $x_{1}$. Then $\operatorname{withTop'}$ applied to $f$ is a supremum homomorphism of $\mathrm{WithTop}$ applied to $x$ and $x_{1}$.

WithBot.coeOrderHomdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the coercion (from the docstring)

English

The coercion is an order embedding of $x$ and $\mathrm{WithBot}$ applied to $x$.

WithBot.subtypeOrderIsodefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the subtype order isomorphism (from the name)

English

The subtype order isomorphism is an order isomorphism of $\mathrm{WithBot}$ applied to $\SubtypeSet {a}{\mathrm{Neq} (a , \operatorname{bot})}$ and $x$.

WithBot.toDualTopEquivdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the dual top equivalence (from the name)

English

The dual top equivalence is an order isomorphism of $\mathrm{WithBot}$ applied to the set of order duals of $x$ and the set of order duals of $\mathrm{WithTop}$ applied to $x$.

WithTop.coeOrderHomdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the coercion (from the docstring)

English

The coercion is an order embedding of $x$ and $\mathrm{WithTop}$ applied to $x$.

WithTop.subtypeOrderIsodefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the subtype order isomorphism (from the name)

English

The subtype order isomorphism is an order isomorphism of $\mathrm{WithTop}$ applied to $\SubtypeSet {a}{\mathrm{Neq} (a , \operatorname{top})}$ and $x$.

WithTop.toDualBotEquivdefMathlib.Order.Hom.WithTopBot, function or constant

Wording

the dual bottom equivalence (from the name)

English

The dual bottom equivalence is an order isomorphism of $\mathrm{WithTop}$ applied to the set of order duals of $x$ and the set of order duals of $\mathrm{WithBot}$ applied to $x$.

Mathlib.Order.Ideal

Order.CofinalstructureMathlib.Order.Ideal, type

Wording

no wording

English

Let $P$ be a set. Then the elements of $\operatorname{Cofinal}$ applied to $P$ are a basic type.

Order.Cofinal.abovedefMathlib.Order.Ideal, function or constant

Wording

no wording

English

Let $D$ be an element of $\operatorname{Cofinal}$ applied to $P$. Let $x_{1}$ be an element of $P$. Then $\operatorname{above}$ applied to $D$ and $x_{1}$ is an element of $P$ defined as $\operatorname{choose}$ applied to $\operatorname{isCofinal}$ applied to $D$ and $x_{1}$.

Order.Cofinal.carrierdefMathlib.Order.Ideal, function or constant

Wording

the carrier of self (from the docstring)

English

Let $\mathrm{self}$ be an element of $\operatorname{Cofinal}$ applied to $P$. Then the carrier of $\mathrm{self}$ is an element of $\wp P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Order.IdealstructureMathlib.Order.Ideal, type

Wording

ideal of P (from the name)

English

Let $P$ be a set. Then the ideals of $P$ are a basic type.

Order.Ideal.IsMaximalclassMathlib.Order.Ideal, predicate

Wording

I is maximal (from the docstring)

English

Let $I$ be an ideal of $P$. Then we can say that $I$ is maximal.

Order.Ideal.IsProperclassMathlib.Order.Ideal, predicate

Wording

I is proper (from the name)

English

Let $I$ be an ideal of $P$. Then we can say that $I$ is proper.

Order.Ideal.principaldefMathlib.Order.Ideal, function or constant

Wording

no wording

English

Let $p$ be an element of $P$. Then $\operatorname{principal}$ applied to $p$ is an ideal of $P$.

Order.IsIdealstructureMathlib.Order.Ideal, predicate

Wording

I is a ideal (from the name)

English

Let $I$ be an element of $\wp P$. Then we can say that $I$ is an ideal.

Order.IsIdeal.toIdealdefMathlib.Order.Ideal, function or constant

Wording

the ideal of h (from the name)

English

Assume that $I$ is an ideal. Then the ideal of $h$ is an ideal of $P$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $I$ and $\operatorname{IsLowerSet}$ applied to $h$, $\operatorname{Nonempty}$ applied to $h$ and $\operatorname{Directed}$ applied to $h$.

Order.idealOfCofinalsdefMathlib.Order.Ideal, function or constant

Wording

the ideal of p and x3 (from the name)

English

Let $p$ be an element of $P$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $\operatorname{Cofinal}$ applied to $P$. Then the ideal of $p$ and $x_{3}$ is an ideal of $P$.

Order.sequenceOfCofinalsdefMathlib.Order.Ideal, function or constant

Wording

the sequence of x3 and x4 (from the name)

English

Let $p$ be an element of $P$. Let $x_{3}$ be a function from elements of $x_{1}$ to elements of $\operatorname{Cofinal}$ applied to $P$. Let $x_{4}$ be a natural number. Then the sequence of $x_{3}$ and $x_{4}$ is an element of $P$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Order\_\_sequenceOfCofinals\_\_\_f}$ applied to $p$ and $x_{3}$.

Mathlib.Order.InitialSeg

InitialSegstructureMathlib.Order.InitialSeg, type

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 the elements of $\mathrm{InitialSeg}$ applied to $r$ and $s$ are a basic type.

InitialSeg.antisymmdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$. Let $g$ be an element of $\mathrm{InitialSeg}$ applied to $s$ and $r$. Then $\operatorname{antisymm}$ applied to $f$ and $g$ is a relation isomorphism of $r$ and $s$.

InitialSeg.codRestrictdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $p$ be an element of $\wp x_{1}$. Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $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 an element of $\mathrm{InitialSeg}$ applied to $r$ and $\mathrm{Subrel}$ applied to $s$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {p}{x_{2}}$.

InitialSeg.leAdddefMathlib.Order.InitialSeg, 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{leAdd}$ applied to $r$ and $s$ is an element of $\mathrm{InitialSeg}$ applied to $r$ and $\operatorname{Lex}$ applied to $r$ and $s$.

InitialSeg.ofIsEmptydefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

InitialSeg.principalSumRelIsodefMathlib.Order.InitialSeg, function or constant

Wording

the principal sum relation isomorphism of f (from the name)

English

Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$. Then the principal sum relation isomorphism of $f$ is an element of $\mathrm{Sum}$ applied to $\mathrm{PrincipalSeg}$ applied to $r$ and $s$ and the set of relation isomorphisms of $r$ and $s$ defined as $\mathrm{dite}$ applied to $\operatorname{Surjective}$ applied to $\operatorname{coe}$ applied to $f$, the function that maps $h_{1}$ to $\operatorname{inr}$ applied to the relation isomorphism of $\operatorname{toRelEmbedding}$ applied to $f$ and $h_{1}$ and the function that maps $h_{2}$ to $\operatorname{inl}$ applied to $\operatorname{toPrincipalSeg}$ applied to $f$ and $h_{2}$.

InitialSeg.refldefMathlib.Order.InitialSeg, 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 an element of $\mathrm{InitialSeg}$ applied to $r$ and $r$ defined as $\operatorname{toInitialSeg}$ applied to the identity of $r$.

InitialSeg.toOrderEmbeddingdefMathlib.Order.InitialSeg, function or constant

Wording

the order embedding of f (from the name)

English

Let $f$ be an element of $\mathrm{InitialSeg}$ 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})$. Then the order embedding of $f$ is an order embedding of $x$ and $x_{1}$ defined as the order embedding of $\operatorname{toRelEmbedding}$ applied to $f$.

InitialSeg.toPrincipalSegdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$ such that it is not the case that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{toPrincipalSeg}$ applied to $f$ and $\mathrm{hf}$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$.

InitialSeg.totaldefMathlib.Order.InitialSeg, 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{total}$ applied to $r$ and $s$ is an element of $\mathrm{Sum}$ applied to $\mathrm{InitialSeg}$ applied to $r$ and $s$ and $\mathrm{InitialSeg}$ applied to $s$ and $r$.

InitialSeg.transdefMathlib.Order.InitialSeg, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$. Let $g$ be an element of $\mathrm{InitialSeg}$ applied to $s$ and $t$. Then the composition of $f$ and $g$ is an element of $\mathrm{InitialSeg}$ applied to $r$ and $t$.

InitialSeg.transPrincipaldefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$. Let $g$ be an element of $\mathrm{PrincipalSeg}$ applied to $s$ and $t$. Then $\operatorname{transPrincipal}$ applied to $f$ and $g$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $t$.

OrderIso.toInitialSegdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{toInitialSeg}$ applied to $f$ is an element of $\mathrm{InitialSeg}$ 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})$ defined as $\operatorname{toInitialSeg}$ applied to $\operatorname{toRelIsoLT}$ applied to $f$.

PrincipalSegstructureMathlib.Order.InitialSeg, type

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 the elements of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$ are a basic type.

PrincipalSeg.codRestrictdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $p$ be an element of $\wp x_{1}$. Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$ such that for all elements $a$ of $x$, $\MembershipmemMACRoT {p}{\operatorname{toRelEmbedding} (f , a)}$ and the top of $f$ is an element of $p$. Then $\operatorname{codRestrict}$ applied to $p$, $f$, $H$ and $h$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $\mathrm{Subrel}$ applied to $s$ and the function that maps $x_{2}$ to $\MembershipmemMACRoT {p}{x_{2}}$.

PrincipalSeg.ofElementdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ be an element of $x$. Then $\operatorname{ofElement}$ applied to $r$ and $a$ is an element of $\mathrm{PrincipalSeg}$ applied to $\mathrm{Subrel}$ applied to $r$ and the function that maps $x_{1}$ to $r$ applied to $x_{1}$ and $a$ and $r$.

PrincipalSeg.ofIsEmptydefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Assume that for all elements $\mathrm{b'}$ of $x_{1}$, it is not the case that $s$ holds for $\mathrm{b'}$ and $b$. Then $\operatorname{ofIsEmpty}$ applied to $r$ and $H$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$.

PrincipalSeg.pemptyToPUnitdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

$\operatorname{pemptyToPUnit}$ is an element of $\mathrm{PrincipalSeg}$ applied to $\mathrm{emptyRelation}$ and $\mathrm{emptyRelation}$ defined as $\operatorname{ofIsEmpty}$ applied to $\mathrm{emptyRelation}$ and the function that maps $x$ to $\mathrm{not\_false}$.

PrincipalSeg.relIsoTransdefMathlib.Order.InitialSeg, function or constant

Wording

the relation isomorphism composition of f and g (from the name)

English

Let $f$ be a relation isomorphism of $r$ and $s$. Let $g$ be an element of $\mathrm{PrincipalSeg}$ applied to $s$ and $t$. Then the relation isomorphism composition of $f$ and $g$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $t$.

PrincipalSeg.subrelIsodefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$. Then $\operatorname{subrelIso}$ applied to $f$ is a relation isomorphism of $\mathrm{Subrel}$ applied to $s$ and the function that maps $x_{2}$ to $s$ applied to $x_{2}$ and the top of $f$ and $r$.

PrincipalSeg.topdefMathlib.Order.InitialSeg, function or constant

Wording

the top of self (from the name)

English

Let $\mathrm{self}$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$. Then the top of $\mathrm{self}$ is an element of $x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

PrincipalSeg.transdefMathlib.Order.InitialSeg, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$. Let $g$ be an element of $\mathrm{PrincipalSeg}$ applied to $s$ and $t$. Then the composition of $f$ and $g$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $t$ defined as $\operatorname{transInitial}$ applied to $f$ and $\operatorname{mk}$ applied to $\operatorname{toRelEmbedding}$ applied to $g$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{PrincipalSeg\_\_mem\_range\_of\_rel}$ applied to $g$.

PrincipalSeg.transInitialdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$. Let $g$ be an element of $\mathrm{InitialSeg}$ applied to $s$ and $t$. Then $\operatorname{transInitial}$ applied to $f$ and $g$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $t$.

PrincipalSeg.transRelIsodefMathlib.Order.InitialSeg, function or constant

Wording

the composition relation isomorphism of f and g (from the name)

English

Let $f$ be an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $s$. Let $g$ be a relation isomorphism of $s$ and $t$. Then the composition relation isomorphism of $f$ and $g$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and $t$ defined as $\operatorname{transInitial}$ applied to $f$ and $\operatorname{toInitialSeg}$ applied to $g$.

PrincipalSeg.trichotomydefMathlib.Order.InitialSeg, 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{trichotomy}$ applied to $r$ and $s$ is an element of $\mathrm{Sum}$ applied to $\mathrm{PrincipalSeg}$ applied to $r$ and $s$ and $\mathrm{Sum}$ applied to the set of relation isomorphisms of $r$ and $s$ and $\mathrm{PrincipalSeg}$ applied to $s$ and $r$.

RelEmbedding.collapsedefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be a relation embedding of $r$ and $s$. Then $\operatorname{collapse}$ applied to $f$ is an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$.

RelIso.toInitialSegdefMathlib.Order.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be a relation isomorphism of $r$ and $s$. Then $\operatorname{toInitialSeg}$ applied to $f$ is an element of $\mathrm{InitialSeg}$ applied to $r$ and $s$.

Mathlib.Order.Int.LeastGreatest

Int.greatestOfBdddefMathlib.Order.Int.LeastGreatest, function or constant

Wording

no wording

English

Let $b$ be an integer such that for all integers $z_{2}$, if $P$ holds for $z_{2}$, then $z_{2} \leq b$. Assume that there exists an integer $z_{1}$, such that $P$ holds for $z_{1}$. Then $\operatorname{greatestOfBdd}$ applied to $b$, $\mathrm{Hb}$ and $\mathrm{Hinh}$ is an element of $\SubtypeSet {\mathrm{ub}}{\mathrm{and} (P (\mathrm{ub}), \mathrm{forall} (\Integer , \lambda z . \mathrm{if} (P (z), \mathrm{Leq} (z , \mathrm{ub}))))}$.

Int.leastOfBdddefMathlib.Order.Int.LeastGreatest, function or constant

Wording

no wording

English

Let $b$ be an integer such that for all integers $z_{2}$, if $P$ holds for $z_{2}$, then $b \leq z_{2}$. Assume that there exists an integer $z_{1}$, such that $P$ holds for $z_{1}$. Then $\operatorname{leastOfBdd}$ applied to $b$, $\mathrm{Hb}$ and $\mathrm{Hinh}$ is an element of $\SubtypeSet {\mathrm{lb}}{\mathrm{and} (P (\mathrm{lb}), \mathrm{forall} (\Integer , \lambda z . \mathrm{if} (P (z), \mathrm{Leq} (\mathrm{lb} , z))))}$.

Mathlib.Order.Interval.Basic

IntervaldefMathlib.Order.Interval.Basic, type

Wording

interval of x (from the name)

English

Let $x$ be a set. Then an interval of $x$ is an element of the function that maps $x$ to $\mathrm{WithBot}$ applied to the set of nonempty intervals of $x$.

Interval.coedefMathlib.Order.Interval.Basic, function or constant

Wording

the coercion of x2 (from the name)

English

Let $x_{2}$ be a nonempty interval of $x$. Then the coercion of $x_{2}$ is an interval of $x$ defined as $\operatorname{some}$ applied to $x_{2}$.

Interval.coeHomdefMathlib.Order.Interval.Basic, function or constant

Wording

the coercion homomorphism (from the name)

English

The coercion homomorphism is an order embedding of the set of intervals of $x$ and $\wp x$.

Interval.dualdefMathlib.Order.Interval.Basic, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of intervals of $x$ to the set of intervals of the set of order duals of $x$ defined as $\operatorname{withBotCongr}$ applied to the dual.

Interval.mapdefMathlib.Order.Interval.Basic, function or constant

Wording

the map of f and x4 (from the name)

English

Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $x_{4}$ be an interval of $x$. Then the map of $f$ and $x_{4}$ is an interval of $x_{1}$ defined as the map of $\operatorname{map}$ applied to $f$ and $x_{4}$.

Interval.puredefMathlib.Order.Interval.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{pure}$ applied to $a$ is an interval of $x$ defined as the coercion of $\operatorname{pure}$ applied to $a$.

Interval.recBotCoedefMathlib.Order.Interval.Basic, 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 nonempty intervals $a$ of $x$ to elements of $C$ applied to the coercion of $a$. Let $n$ be an interval of $x$. Then $\operatorname{recBotCoe}$ applied to $\mathrm{bot}$, $a$, $\mathrm{coe}$ and $n$ is an element of $C$ applied to $n$ defined as the function that maps $n$ to $\operatorname{recBotCoe}$ applied to $\mathrm{bot}$, $a$, $\mathrm{coe}$ and $n$.

NonemptyIntervalstructureMathlib.Order.Interval.Basic, type

Wording

nonempty interval of x (from the name)

English

Let $x$ be a set. Then the nonempty intervals of $x$ are a basic type.

NonemptyInterval.coeHomdefMathlib.Order.Interval.Basic, function or constant

Wording

the coercion homomorphism (from the name)

English

The coercion homomorphism is an order embedding of the set of nonempty intervals of $x$ and $\wp x$.

NonemptyInterval.dualdefMathlib.Order.Interval.Basic, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from the set of nonempty intervals of $x$ to the set of nonempty intervals of the set of order duals of $x$.

NonemptyInterval.mapdefMathlib.Order.Interval.Basic, function or constant

Wording

the map of f and a (from the name)

English

Let $f$ be an order homomorphism of $x$ and $x_{1}$. Let $a$ be a nonempty interval of $x$. Then the map of $f$ and $a$ is a nonempty interval of $x_{1}$.

NonemptyInterval.map₂defMathlib.Order.Interval.Basic, function or constant

Wording

the map of x6 and x7 (from the name)

English

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $b$ of $x_{1}$, the function that maps $a_{1}$ to $f$ applied to $a_{1}$ and $b$ is monotone and for all elements $a$ of $x$, $f$ applied to $a$ is monotone. Let $x_{6}$ be a nonempty interval of $x$. Let $x_{7}$ be a nonempty interval of $x_{1}$. Then the map of $x_{6}$ and $x_{7}$ is a nonempty interval of $x_{2}$.

NonemptyInterval.puredefMathlib.Order.Interval.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{pure}$ applied to $a$ is a nonempty interval of $x$.

NonemptyInterval.toDualProddefMathlib.Order.Interval.Basic, function or constant

Wording

the dual product of x2 (from the name)

English

Let $x_{2}$ be a nonempty interval of $x$. Then the dual product of $x_{2}$ is an element of $\mathrm{Prod}$ applied to the set of order duals of $x$ and $x$ defined as $\operatorname{toProd}$ applied to $x_{2}$.

NonemptyInterval.toDualProdHomdefMathlib.Order.Interval.Basic, function or constant

Wording

the dual product homomorphism (from the name)

English

The dual product homomorphism is an order embedding of the set of nonempty intervals of $x$ and $\mathrm{Prod}$ applied to the set of order duals of $x$ and $x$.

Mathlib.Order.Interval.Finset.Basic

Equiv.IicFinsetSetdefMathlib.Order.Interval.Finset.Basic, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{IicFinsetSet}$ applied to $a$ is an equivalence from $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\FinsetIicMACRoAJ {a}}{x_{3}})}$ to the set of elements of $\operatorname{Iic}$ applied to $a$.

Mathlib.Order.Interval.Finset.Box

Finset.boxdefMathlib.Order.Interval.Finset.Box, function or constant

Wording

no wording

English

Let $x_{5}$ be a natural number. Then $\operatorname{box}$ applied to $x_{5}$ is a finite set of $x$ defined as $\mathrm{disjointed}$ applied to the function that maps $n$ to $\FinsetIccMACRoAH {\operatorname{neg} (n)}{n}$ and $x_{5}$.

Mathlib.Order.Interval.Finset.Defs

Finset.IccdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

the closed interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then $\FinsetIccMACRoAH {a}{b}$ is a finite set of $x$ defined as the finite set closed interval of $a$ and $b$.

Finset.IcidefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{Ici}$ applied to $a$ is a finite set of $x$ defined as $\operatorname{finsetIci}$ applied to $a$.

Finset.IcodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\FinsetIcoMACRoO {a}{b}$ is a finite set of $x$ defined as $\operatorname{finsetIco}$ applied to $a$ and $b$.

Finset.IicdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\FinsetIicMACRoAJ {a}$ is a finite set of $x$ defined as $\operatorname{finsetIic}$ applied to $a$.

Finset.IiodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\FinsetIioMACRoAK {a}$ is a finite set of $x$ defined as $\operatorname{finsetIio}$ applied to $a$.

Finset.IocdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\FinsetIocMACRoAI {a}{b}$ is a finite set of $x$ defined as $\operatorname{finsetIoc}$ applied to $a$ and $b$.

Finset.IoidefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{Ioi}$ applied to $a$ is a finite set of $x$ defined as $\operatorname{finsetIoi}$ applied to $a$.

Finset.IoodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

the open interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the open interval of $a$ and $b$ is a finite set of $x$ defined as the finite set open interval of $a$ and $b$.

Finset.uIccdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

the closed interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the closed interval of $a$ and $b$ is a finite set of $x$ defined as $\FinsetIccMACRoAH {(\MinminMACRoAG {a}{b})}{(\MaxmaxMACRoAF {a}{b})}$.

LocallyFiniteOrderclassMathlib.Order.Interval.Finset.Defs, predicate

Wording

x is a locally finite order (from the name)

English

generation took over the time limit

LocallyFiniteOrder.finsetIccdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

the finite set closed interval of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then the finite set closed interval of $x_{2}$ and $x_{3}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

LocallyFiniteOrder.finsetIcodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then $\operatorname{finsetIco}$ applied to $x_{2}$ and $x_{3}$ is a finite set of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

LocallyFiniteOrder.finsetIocdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then $\operatorname{finsetIoc}$ applied to $x_{2}$ and $x_{3}$ is a finite set of $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

LocallyFiniteOrder.finsetIoodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

the finite set open interval of x2 and x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then the finite set open interval of $x_{2}$ and $x_{3}$ is a finite set of $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

LocallyFiniteOrderBotclassMathlib.Order.Interval.Finset.Defs, predicate

Wording

x is a locally finite order bottom (from the name)

English

generation took over the time limit

LocallyFiniteOrderBot.finsetIicdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{finsetIic}$ applied to $x_{2}$ is a finite set of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

LocallyFiniteOrderBot.finsetIiodefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{finsetIio}$ applied to $x_{2}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

LocallyFiniteOrderTopclassMathlib.Order.Interval.Finset.Defs, predicate

Wording

x is a locally finite order top (from the name)

English

generation took over the time limit

LocallyFiniteOrderTop.finsetIcidefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{finsetIci}$ applied to $x_{2}$ is a finite set of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.

LocallyFiniteOrderTop.finsetIoidefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

Let $x_{2}$ be an element of $x$. Then $\operatorname{finsetIoi}$ applied to $x_{2}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.

WithBot.insertBotdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

$\operatorname{insertBot}$ is an order embedding of the set of finite sets of $x$ and the set of finite sets of $\mathrm{WithBot}$ applied to $x$.

WithTop.insertTopdefMathlib.Order.Interval.Finset.Defs, function or constant

Wording

no wording

English

$\operatorname{insertTop}$ is an order embedding of the set of finite sets of $x$ and the set of finite sets of $\mathrm{WithTop}$ applied to $x$.

Mathlib.Order.Interval.Finset.Gaps

Finset.intervalGapsWithindefMathlib.Order.Interval.Finset.Gaps, function or constant

Wording

no wording

English

Let $F$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $x$ such that $\FinsetcardMACRoM {F}= k$. Let $a$ and $b$ be elements of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $k + 1$. Then $\operatorname{intervalGapsWithin}$ applied to $F$, $h$, $a$, $b$ and $i$ is an element of $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\ProdmkMACRoU {\operatorname{fst} (F)}{\operatorname{snd} (F)}$.

Finset.intervalGapsWithin.fstdefMathlib.Order.Interval.Finset.Gaps, function or constant

Wording

the first coordinate of F (from the docstring)

English

Let $F$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $x$ such that $\FinsetcardMACRoM {F}= k$. Let $a$ be an element of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $k + 1$. Then the first coordinate of $F$ is an element of $x$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {i}{0}$, the function that maps $\mathrm{hi}$ to $a$ and the function that maps $\mathrm{hi1}$ to $\ProdsndMACRoAA {\operatorname{orderEmbOfFin} (F , h , \operatorname{pred} (i , \mathrm{hi1}))}$.

Finset.intervalGapsWithin.snddefMathlib.Order.Interval.Finset.Gaps, function or constant

Wording

the second coordinate of F (from the docstring)

English

Let $F$ be a finite set of $\mathrm{Prod}$ applied to $x$ and $x$ such that $\FinsetcardMACRoM {F}= k$. Let $b$ be an element of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $k + 1$. Then the second coordinate of $F$ is an element of $x$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {i}{\operatorname{last} (k)}$, the function that maps $\mathrm{hi}$ to $b$ and the function that maps $\mathrm{hi1}$ to the first element of $\operatorname{orderEmbOfFin}$ applied to $F$, $h$ and the cast predecessor of $i$ and $\mathrm{hi1}$.

Mathlib.Order.Interval.Multiset

Multiset.IccdefMathlib.Order.Interval.Multiset, function or constant

Wording

the closed interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the closed interval of $a$ and $b$ is a multiset of $x$ defined as the value of $\FinsetIccMACRoAH {a}{b}$.

Multiset.IcidefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{Ici}$ applied to $a$ is a multiset of $x$ defined as the value of $\operatorname{Ici}$ applied to $a$.

Multiset.IcodefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\operatorname{Ico}$ applied to $a$ and $b$ is a multiset of $x$ defined as the value of $\FinsetIcoMACRoO {a}{b}$.

Multiset.IicdefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Iic}$ applied to $b$ is a multiset of $x$ defined as the value of $\FinsetIicMACRoAJ {b}$.

Multiset.IiodefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Iio}$ applied to $b$ is a multiset of $x$ defined as the value of $\FinsetIioMACRoAK {b}$.

Multiset.IocdefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\operatorname{Ioc}$ applied to $a$ and $b$ is a multiset of $x$ defined as the value of $\FinsetIocMACRoAI {a}{b}$.

Multiset.IoidefMathlib.Order.Interval.Multiset, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{Ioi}$ applied to $a$ is a multiset of $x$ defined as the value of $\operatorname{Ioi}$ applied to $a$.

Multiset.IoodefMathlib.Order.Interval.Multiset, function or constant

Wording

the open interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the open interval of $a$ and $b$ is a multiset of $x$ defined as the value of the open interval of $a$ and $b$.

Mathlib.Order.Interval.Set.Defs

Set.IccdefMathlib.Order.Interval.Set.Defs, function or constant

Wording

the closed interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then $\SetIccMACRoP {a}{b}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $a \leq x_{2} \leq b$.

Set.IcidefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Ici}$ applied to $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Leq} (b , x_{2})$.

Set.IcodefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\operatorname{Ico}$ applied to $a$ and $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $a \leq x_{2} < b$.

Set.IicdefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Iic}$ applied to $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Leq} (x_{2} , b)$.

Set.IiodefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Iio}$ applied to $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Lt} (x_{2} , b)$.

Set.IocdefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $a$ and $b$ be elements of $x$. Then $\operatorname{Ioc}$ applied to $a$ and $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $a < x_{2} \leq b$.

Set.IoidefMathlib.Order.Interval.Set.Defs, function or constant

Wording

no wording

English

Let $b$ be an element of $x$. Then $\operatorname{Ioi}$ applied to $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\mathrm{Lt} (b , x_{2})$.

Set.IoodefMathlib.Order.Interval.Set.Defs, function or constant

Wording

the open interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the open interval of $a$ and $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that $a < x_{2} < b$.

Set.OrdConnectedclassMathlib.Order.Interval.Set.Defs, predicate

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then we can say that $\operatorname{OrdConnected}$ holds for $s$.

Mathlib.Order.Interval.Set.InitialSeg

PrincipalSeg.orderIsoIiodefMathlib.Order.Interval.Set.InitialSeg, function or constant

Wording

no wording

English

Let $f$ be an element of $\mathrm{PrincipalSeg}$ 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})$. Then $\operatorname{orderIsoIio}$ applied to $f$ is an order isomorphism of $x$ and the set of elements of $\operatorname{Iio}$ applied to the top of $f$ defined as the order isomorphism of the inverse of $\operatorname{subrelIso}$ applied to $f$.

Set.initialSegIicdefMathlib.Order.Interval.Set.InitialSeg, function or constant

Wording

the initial segment of j (from the docstring)

English

Let $j$ be an element of $x$. Then the initial segment of $j$ is an element of $\mathrm{InitialSeg}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

Set.initialSegIicIicOfLEdefMathlib.Order.Interval.Set.InitialSeg, function or constant

Wording

no wording

English

Assume that $i \leq j$. Then $\operatorname{initialSegIicIicOfLE}$ applied to $h$ is an element of $\mathrm{InitialSeg}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

Set.principalSegIiodefMathlib.Order.Interval.Set.InitialSeg, function or constant

Wording

the principal segment of j (from the docstring)

English

Let $j$ be an element of $x$. Then the principal segment of $j$ is an element of $\mathrm{PrincipalSeg}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

Set.principalSegIioIicOfLEdefMathlib.Order.Interval.Set.InitialSeg, function or constant

Wording

no wording

English

Assume that $i \leq j$. Then $\operatorname{principalSegIioIicOfLE}$ applied to $h$ is an element of $\mathrm{PrincipalSeg}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Lt} (x_{4} , x_{5})$.

Mathlib.Order.Interval.Set.IsoIoo

orderIsoIooNegOneOnedefMathlib.Order.Interval.Set.IsoIoo, function or constant

Wording

the order isomorphism open interval negation one one of k (from the name)

English

Let $k$ be a set. Then the order isomorphism open interval negation one one of $k$ is an order isomorphism of $k$ and the set of elements of the open interval of $\operatorname{neg}$ applied to $1$ and $1$.

Mathlib.Order.Interval.Set.OrdConnectedComponent

Set.ordConnectedComponentdefMathlib.Order.Interval.Set.OrdConnectedComponent, function or constant

Wording

the order connected component of s and x2 (from the name)

English

Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $x$. Then the order connected component of $s$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that the closed interval of $x_{2}$ and $y$ is less than or equal to $s$.

Set.ordConnectedProjdefMathlib.Order.Interval.Set.OrdConnectedComponent, function or constant

Wording

the order connected projection of s and x2 (from the name)

English

Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $s$. Then the order connected projection of $s$ and $x_{2}$ is an element of $x$.

Set.ordConnectedSectiondefMathlib.Order.Interval.Set.OrdConnectedComponent, function or constant

Wording

the order connected section of s (from the name)

English

Let $s$ be an element of $\wp x$. Then the order connected section of $s$ is an element of $\wp x$ defined as the range of $\operatorname{ordConnectedProj}$ applied to $s$.

Set.ordSeparatingSetdefMathlib.Order.Interval.Set.OrdConnectedComponent, function or constant

Wording

the order separating set of s and t (from the name)

English

Let $s$ and $t$ be elements of $\wp x$. Then the order separating set of $s$ and $t$ is an element of $\wp x$ defined as $\operatorname{inter}$ applied to the union of the function that maps $x_{2}$ to the union of the function that maps $h$ to the order connected component of the complement of $t$ and $x_{2}$ and the union of the function that maps $x_{3}$ to the union of the function that maps $h_{1}$ to the order connected component of the complement of $s$ and $x_{3}$.

Mathlib.Order.Interval.Set.OrderIso

OrderIso.IciBotdefMathlib.Order.Interval.Set.OrderIso, function or constant

Wording

no wording

English

$\operatorname{IciBot}$ is an order isomorphism of the set of elements of $\operatorname{Ici}$ applied to the bottom and $x$.

OrderIso.IicTopdefMathlib.Order.Interval.Set.OrderIso, function or constant

Wording

no wording

English

$\operatorname{IicTop}$ is an order isomorphism of the set of elements of $\operatorname{Iic}$ applied to the top and $x$.

Mathlib.Order.Interval.Set.ProjIcc

Set.IccExtenddefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

no wording

English

Assume that $a \leq b$. Let $f$ be a function from elements of $\SetIccMACRoP {a}{b}$ to elements of $x_{1}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{IccExtend}$ applied to $h$, $f$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{comp}$ applied to $f$, $\operatorname{projIcc}$ applied to $b$ and $x_{3}$.

Set.IciExtenddefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\operatorname{Ici}$ applied to $a$ to elements of $x_{1}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{IciExtend}$ applied to $f$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{comp}$ applied to $f$, $\operatorname{projIci}$ applied to $a$ and $x_{3}$.

Set.IicExtenddefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $\operatorname{Iic}$ applied to $b$ to elements of $x_{1}$. Let $x_{3}$ be an element of $x$. Then $\operatorname{IicExtend}$ applied to $f$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{comp}$ applied to $f$, $\operatorname{projIic}$ applied to $b$ and $x_{3}$.

Set.projIccdefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

the projection closed interval of b and x2 (from the name)

English

Let $a$, $b$ and $x_{2}$ be elements of $x$ such that $a \leq b$. Then the projection closed interval of $b$ and $x_{2}$ is an element of $\SetIccMACRoP {a}{b}$ defined as $\MaxmaxMACRoAF {a}{(\MinminMACRoAG {b}{x_{2}})}$.

Set.projIcidefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

no wording

English

Let $a$ and $x_{2}$ be elements of $x$. Then $\operatorname{projIci}$ applied to $a$ and $x_{2}$ is an element of $\operatorname{Ici}$ applied to $a$ defined as $\MaxmaxMACRoAF {a}{x_{2}}$.

Set.projIicdefMathlib.Order.Interval.Set.ProjIcc, function or constant

Wording

no wording

English

Let $b$ and $x_{2}$ be elements of $x$. Then $\operatorname{projIic}$ applied to $b$ and $x_{2}$ is an element of $\operatorname{Iic}$ applied to $b$ defined as $\MinminMACRoAG {b}{x_{2}}$.

Mathlib.Order.Interval.Set.UnorderedInterval

Set.uIccdefMathlib.Order.Interval.Set.UnorderedInterval, function or constant

Wording

the closed interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the closed interval of $a$ and $b$ is an element of $\wp x$ defined as $\SetIccMACRoP {(\MinminMACRoAG {a}{b})}{(\MaxmaxMACRoAF {a}{b})}$.

Set.uIocdefMathlib.Order.Interval.Set.UnorderedInterval, function or constant

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $x$. Then $\operatorname{uIoc}$ applied to $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as $\operatorname{Ioc}$ applied to $\MinminMACRoAG {x_{2}}{x_{3}}$ and $\MaxmaxMACRoAF {x_{2}}{x_{3}}$.

Set.uIoodefMathlib.Order.Interval.Set.UnorderedInterval, function or constant

Wording

the open interval of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$. Then the open interval of $a$ and $b$ is an element of $\wp x$ defined as the open interval of $\MinminMACRoAG {a}{b}$ and $\MaxmaxMACRoAF {a}{b}$.

Mathlib.Order.Irreducible

InfIrreddefMathlib.Order.Irreducible, predicate

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{InfIrred}$ holds for $a$, if $a$ is not a maximum and for all elements $b$ of $x$, for all elements $c$ of $x$, if $\EqtMACRoH {\MinminMACRoAG {b}{c}}{a}$, then $\EqtMACRoH {b}{a}$ or $\EqtMACRoH {c}{a}$.

InfPrimedefMathlib.Order.Irreducible, predicate

Wording

a is a infimum prime (from the name)

English

Let $a$ be an element of $x$. Then $a$ is an infimum prime, if $a$ is not a maximum and for all elements $b$ of $x$, for all elements $c$ of $x$, if $\MinminMACRoAG {b}{c}\leq a$, then $b \leq a$ or $c \leq a$.

SupIrreddefMathlib.Order.Irreducible, predicate

Wording

no wording

English

Let $a$ be an element of $x$. Then $\mathrm{SupIrred}$ holds for $a$, if $a$ is not a minimum and for all elements $b$ of $x$, for all elements $c$ of $x$, if $\EqtMACRoH {\MaxmaxMACRoAF {b}{c}}{a}$, then $\EqtMACRoH {b}{a}$ or $\EqtMACRoH {c}{a}$.

SupPrimedefMathlib.Order.Irreducible, predicate

Wording

a is a supremum prime (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a supremum prime, if $a$ is not a minimum and for all elements $b$ of $x$, for all elements $c$ of $x$, if $a \leq \MaxmaxMACRoAF {b}{c}$, then $a \leq b$ or $a \leq c$.

Mathlib.Order.IsNormal

Order.IsNormalstructureMathlib.Order.IsNormal, predicate

Wording

f is normal (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $f$ is normal.

Mathlib.Order.JordanHolder

CompositionSeriesdefMathlib.Order.JordanHolder, type

Wording

composition series of X (from the name)

English

Let $X$ be a set. Then the composition series of $X$ are a basic type.

CompositionSeries.EquivalentdefMathlib.Order.JordanHolder, predicate

Wording

x2 is equivalent to x3 (from the name)

English

Let $x_{2}$ and $x_{3}$ be composition series of $X$. Then $x_{2}$ is equivalent to $x_{3}$, if there exists an element $f$ of $\EquivMACRoAE {\mathrm{Fin} (\operatorname{length} (x_{2}))}{\mathrm{Fin} (\operatorname{length} (x_{3}))}$, such that for all elements $i$ of $\mathrm{Fin}$ applied to the length of $x_{2}$, $\operatorname{Iso}$ holds for $\ProdmkMACRoU {\operatorname{toFun} (x_{2} , \operatorname{castSucc} (i))}{\operatorname{toFun} (x_{2} , \operatorname{succ} (i))}$ and $\ProdmkMACRoU {\operatorname{toFun} (x_{3} , \operatorname{castSucc} (f (i)))}{\operatorname{toFun} (x_{3} , \operatorname{succ} (f (i)))}$.

JordanHolderLatticeclassMathlib.Order.JordanHolder, predicate

Wording

X is a Jordan Holder lattice (from the name)

English

Let $X$ be a set. Then we can say that $X$ is a Jordan Holder lattice.

JordanHolderLattice.IsMaximaldefMathlib.Order.JordanHolder, predicate

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be elements of $X$. Then $\operatorname{IsMaximal}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$ and $x_{2}$.

JordanHolderLattice.IsodefMathlib.Order.JordanHolder, predicate

Wording

no wording

English

Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Prod}$ applied to $X$ and $X$. Then we can say that $\operatorname{Iso}$ holds for $x_{2}$ and $x_{3}$.

Mathlib.Order.KrullDimension

Order.KrullDimLEclassMathlib.Order.KrullDimension, predicate

Wording

no wording

English

Let $n$ be a natural number. Let $x$ be a set. Then we can say that $\operatorname{KrullDimLE}$ holds for $n$ and $x$.

Order.coheightdefMathlib.Order.KrullDimension, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{coheight}$ applied to $a$ is a natural number defined as the height of $a$.

Order.heightdefMathlib.Order.KrullDimension, function or constant

Wording

the height of a (from the name)

English

Let $a$ be an element of $x$. Then the height of $a$ is a natural number defined as the supremum of the function that maps $p$ to the supremum of the function that maps $h$ to the length of $p$.

Order.krullDimdefMathlib.Order.KrullDimension, function or constant

Wording

the Krull dimension of x (from the name)

English

Let $x$ be a set. Then the Krull dimension of $x$ is an element of $\mathrm{WithBot}$ applied to the set of natural numbers defined as the supremum of the function that maps $p$ to the length of $p$.

Mathlib.Order.Lattice.Congruence

LatticeConstructureMathlib.Order.Lattice.Congruence, type

Wording

lattice congruence relation of x (from the name)

English

Let $x$ be a set. Then the lattice congruence relations of $x$ are a basic type.

LatticeCon.kerdefMathlib.Order.Lattice.Congruence, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be an element of $F$. Then the kernel of $f$ is a lattice congruence relation of $x$.

LatticeCon.mk'defMathlib.Order.Lattice.Congruence, function or constant

Wording

no wording

English

Let $r$ be a function from elements of $x$ and elements of $x$ to propositions such that for all elements $x_{4}$ of $x$, for all elements $y_{2}$ of $x$, $r$ holds for $x_{4}$ and $y_{2}$, if and only if $r$ holds for $\MinminMACRoAG {x_{4}}{y_{2}}$ and $\MaxmaxMACRoAF {x_{4}}{y_{2}}$, for all elements $x_{3}$ of $x$, for all elements $y_{1}$ of $x$, for all elements $z$ of $x$, if $x_{3} \leq y_{1}$, then if $y_{1} \leq z$, then if $r$ holds for $x_{3}$ and $y_{1}$, then if $r$ holds for $y_{1}$ and $z$, then $r$ holds for $x_{3}$ and $z$ and for all elements $x_{2}$ of $x$, for all elements $y$ of $x$, for all elements $t$ of $x$, if $x_{2} \leq y$, then if $r$ holds for $x_{2}$ and $y$, then $r$ holds for $\MinminMACRoAG {x_{2}}{t}$ and $\MinminMACRoAG {y}{t}$ and $r$ holds for $\MaxmaxMACRoAF {x_{2}}{t}$ and $\MaxmaxMACRoAF {y}{t}$. Then $\operatorname{mk'}$ applied to $r$, $h_{1}$, $h_{2}$ and $h_{3}$ is a lattice congruence relation of $x$.

Mathlib.Order.Lex

ColexdefMathlib.Order.Lex, type

Wording

no wording

English

Let $x$ be a set. Then an element of $\mathrm{Colex}$ applied to $x$ is an element of the function that maps $x$ to $x$.

LexdefMathlib.Order.Lex, type

Wording

no wording

English

Let $x$ be a set. Then an element of $\mathrm{Lex}$ applied to $x$ is an element of the function that maps $x$ to $x$.

ofColexdefMathlib.Order.Lex, function or constant

Wording

no wording

English

$\mathrm{ofColex}$ is an element of $\EquivMACRoAE {\mathrm{Colex} (x)}{x}$ defined as the identity of $\mathrm{Colex}$ applied to $x$.

ofLexdefMathlib.Order.Lex, function or constant

Wording

no wording

English

$\mathrm{ofLex}$ is an element of $\EquivMACRoAE {\mathrm{Lex} (x)}{x}$ defined as the identity of $\mathrm{Lex}$ applied to $x$.

toColexdefMathlib.Order.Lex, function or constant

Wording

no wording

English

$\mathrm{toColex}$ is an element of $\EquivMACRoAE {x}{\mathrm{Colex} (x)}$ defined as the identity of $x$.

toLexdefMathlib.Order.Lex, function or constant

Wording

no wording

English

$\mathrm{toLex}$ is an element of $\EquivMACRoAE {x}{\mathrm{Lex} (x)}$ defined as the identity of $x$.

Mathlib.Order.LiminfLimsup

Filter.bliminfdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a filter of $x_{1}$. Let $p$ be a function from elements of $x_{1}$ to propositions. Then $\operatorname{bliminf}$ applied to $u$, $f$ and $p$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $a$ to $\operatorname{Eventually}$ applied to the function that maps $x_{3}$ to the proposition that if $p$ holds for $x_{3}$, then $a \leq u (x_{3})$ and $f$.

Filter.blimsupdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a filter of $x_{1}$. Let $p$ be a function from elements of $x_{1}$ to propositions. Then $\operatorname{blimsup}$ applied to $u$, $f$ and $p$ is an element of $x$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $a$ to $\operatorname{Eventually}$ applied to the function that maps $x_{3}$ to the proposition that if $p$ holds for $x_{3}$, then $u (x_{3})\leq a$ and $f$.

Filter.liminfdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a filter of $x_{1}$. Then $\operatorname{liminf}$ applied to $u$ and $f$ is an element of $x$ defined as $\operatorname{limsInf}$ applied to the forward map of $u$ and $f$.

Filter.liminfReparamdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be a function from elements of $x_{2}$ to elements of $\wp x_{1}$. Let $p$ be a function from elements of $x_{2}$ to propositions. Let $j$ be an element of $\SubtypeSet {x_{5}}{p (x_{5})}$. Then $\operatorname{liminfReparam}$ applied to $f$, $s$, $p$ and $j$ is an element of $\SubtypeSet {x_{4}}{p (x_{4})}$.

Filter.limsInfdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $f$ be a filter of $x$. Then $\operatorname{limsInf}$ applied to $f$ is an element of $x$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $a$ to $\operatorname{Eventually}$ applied to the function that maps $n$ to $\mathrm{Leq} (a , n)$ and $f$.

Filter.limsSupdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $f$ be a filter of $x$. Then $\operatorname{limsSup}$ applied to $f$ is an element of $x$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $a$ to $\operatorname{Eventually}$ applied to the function that maps $n$ to $\mathrm{Leq} (n , a)$ and $f$.

Filter.limsupdefMathlib.Order.LiminfLimsup, function or constant

Wording

the limsup of u and f (from the name)

English

Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Let $f$ be a filter of $x_{1}$. Then the limsup of $u$ and $f$ is an element of $x$ defined as $\operatorname{limsSup}$ applied to the forward map of $u$ and $f$.

Filter.limsupReparamdefMathlib.Order.LiminfLimsup, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Let $s$ be a function from elements of $x_{2}$ to elements of $\wp x_{1}$. Let $p$ be a function from elements of $x_{2}$ to propositions. Let $j$ be an element of $\SubtypeSet {x_{5}}{p (x_{5})}$. Then $\operatorname{limsupReparam}$ applied to $f$, $s$, $p$ and $j$ is an element of $\SubtypeSet {x_{4}}{p (x_{4})}$.

Mathlib.Order.Max

IsBotdefMathlib.Order.Max, predicate

Wording

a is a bottom (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a bottom, if for all elements $b$ of $x$, $a \leq b$.

IsMaxdefMathlib.Order.Max, predicate

Wording

a is a maximum (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a maximum, if for all elements $b$ of $x$, if $a \leq b$, then $b \leq a$.

IsMindefMathlib.Order.Max, predicate

Wording

a is a minimum (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a minimum, if for all elements $b$ of $x$, if $b \leq a$, then $a \leq b$.

IsTopdefMathlib.Order.Max, predicate

Wording

a is a top (from the name)

English

Let $a$ be an element of $x$. Then $a$ is a top, if for all elements $b$ of $x$, $b \leq a$.

NoBotOrderclassMathlib.Order.Max, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{NoBotOrder}$ holds for $x$.

NoMaxOrderclassMathlib.Order.Max, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{NoMaxOrder}$ holds for $x$.

NoMinOrderclassMathlib.Order.Max, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{NoMinOrder}$ holds for $x$.

NoTopOrderclassMathlib.Order.Max, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{NoTopOrder}$ holds for $x$.

Mathlib.Order.Minimal

OrderIso.mapSetOfPredMaximaldefMathlib.Order.Minimal, function or constant

Wording

the map set of f (from the name)

English

Let $f$ be an order isomorphism of the set of elements of $s$ and the set of elements of $t$. Then the map set of $f$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is maximal with respect to the function that maps $x_{5}$ to $\MembershipmemMACRoT {s}{x_{5}}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $x_{6}$ is maximal with respect to the function that maps $x_{7}$ to $\MembershipmemMACRoT {t}{x_{7}}$.

OrderIso.mapSetOfPredMinimaldefMathlib.Order.Minimal, function or constant

Wording

the map set of f (from the name)

English

Let $f$ be an order isomorphism of the set of elements of $s$ and the set of elements of $t$. Then the map set of $f$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is minimal with respect to the function that maps $x_{5}$ to $\MembershipmemMACRoT {s}{x_{5}}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $x_{6}$ is minimal with respect to the function that maps $x_{7}$ to $\MembershipmemMACRoT {t}{x_{7}}$.

OrderIso.setOfPredMaximalIsoSetOfPredMinimaldefMathlib.Order.Minimal, function or constant

Wording

the set of f (from the name)

English

Let $f$ be an order isomorphism of the set of elements of $s$ and the set of order duals of the set of elements of $t$. Then the set of $f$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is maximal with respect to the function that maps $x_{5}$ to $\MembershipmemMACRoT {s}{x_{5}}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $\operatorname{ofDual}$ applied to $x_{6}$ is minimal with respect to the function that maps $x_{7}$ to $\MembershipmemMACRoT {t}{x_{7}}$ defined as the map set of $f$.

OrderIso.setOfPredMinimalIsoSetOfPredMaximaldefMathlib.Order.Minimal, function or constant

Wording

the set of f (from the name)

English

Let $f$ be an order isomorphism of the set of elements of $s$ and the set of order duals of the set of elements of $t$. Then the set of $f$ is an order isomorphism of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is minimal with respect to the function that maps $x_{5}$ to $\MembershipmemMACRoT {s}{x_{5}}$ and the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $\operatorname{ofDual}$ applied to $x_{6}$ is maximal with respect to the function that maps $x_{7}$ to $\MembershipmemMACRoT {t}{x_{7}}$ defined as the map set of $f$.

Mathlib.Order.ModularLattice

IsCompl.IicOrderIsoIcidefMathlib.Order.ModularLattice, function or constant

Wording

the diamond isomorphism between the intervals of h1 (from the docstring)

English

Assume that $\mathrm{IsCompl}$ holds for $a$ and $b$. Then the diamond isomorphism between the intervals of $h_{1}$ is an order isomorphism of the set of elements of $\operatorname{Iic}$ applied to $a$ and the set of elements of $\operatorname{Ici}$ applied to $b$.

IsLowerModularLatticeclassMathlib.Order.ModularLattice, predicate

Wording

x is a lower modular lattice (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a lower modular lattice.

IsModularLatticeclassMathlib.Order.ModularLattice, predicate

Wording

x is a modular lattice (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a modular lattice.

IsUpperModularLatticeclassMathlib.Order.ModularLattice, predicate

Wording

x is a upper modular lattice (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a upper modular lattice.

IsWeakLowerModularLatticeclassMathlib.Order.ModularLattice, predicate

Wording

x is a weak lower modular lattice (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a weak lower modular lattice.

IsWeakUpperModularLatticeclassMathlib.Order.ModularLattice, predicate

Wording

x is a weak upper modular lattice (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a weak upper modular lattice.

infIccOrderIsoIccSupdefMathlib.Order.ModularLattice, function or constant

Wording

the diamond isomorphism between the closed intervals of a and b (from the docstring)

English

Let $a$ and $b$ be elements of $x$. Then the diamond isomorphism between the closed intervals of $a$ and $b$ is an order isomorphism of the set of elements of $\SetIccMACRoP {(\MinminMACRoAG {a}{b})}{a}$ and the set of elements of $\SetIccMACRoP {b}{(\MaxmaxMACRoAF {a}{b})}$.

infIccOrderIsoIccSup'defMathlib.Order.ModularLattice, function or constant

Wording

the diamond isomorphism between the closed intervals of a and b (from the docstring)

English

Let $a$ and $b$ be elements of $x$. Then the diamond isomorphism between the closed intervals of $a$ and $b$ is an order isomorphism of the set of elements of $\SetIccMACRoP {(\MinminMACRoAG {a}{b})}{b}$ and the set of elements of $\SetIccMACRoP {a}{(\MaxmaxMACRoAF {a}{b})}$.

infIooOrderIsoIooSupdefMathlib.Order.ModularLattice, function or constant

Wording

the diamond isomorphism between the open intervals of a and b (from the docstring)

English

Let $a$ and $b$ be elements of $x$. Then the diamond isomorphism between the open intervals of $a$ and $b$ is an order isomorphism of the set of elements of the open interval of $\MinminMACRoAG {a}{b}$ and $a$ and the set of elements of the open interval of $b$ and $\MaxmaxMACRoAF {a}{b}$.

infIooOrderIsoIooSup'defMathlib.Order.ModularLattice, function or constant

Wording

the diamond isomorphism between the open intervals of a and b (from the docstring)

English

Let $a$ and $b$ be elements of $x$. Then the diamond isomorphism between the open intervals of $a$ and $b$ is an order isomorphism of the set of elements of the open interval of $\MinminMACRoAG {a}{b}$ and $b$ and the set of elements of the open interval of $a$ and $\MaxmaxMACRoAF {a}{b}$.

Mathlib.Order.Monotone.Defs

AntitonedefMathlib.Order.Monotone.Defs, predicate

Wording

f is a antitone (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is an antitone, if for all elements $a$ and $b$ of $x$, if $a \leq b$, then $f (b)\leq f (a)$.

AntitoneOndefMathlib.Order.Monotone.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{AntitoneOn}$ holds for $f$ and $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 if $a \leq b$, then $f (b)\leq f (a)$.

IsStabledefMathlib.Order.Monotone.Defs, predicate

Wording

x3 is a stable with respect to f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be a function from elements of $x$ to elements of $x$. Then $x_{3}$ is a stable with respect to $f$, if for all elements $i$ and $j$ of $x$, if $i \leq j$, then if $\EqtMACRoH {f (x_{3} (i))}{f (x_{3} (j))}$, then $x_{3} (i)\leq x_{3} (j)$.

MonotonedefMathlib.Order.Monotone.Defs, predicate

Wording

f is monotone (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is monotone, if for all elements $a$ and $b$ of $x$, if $a \leq b$, then $f (a)\leq f (b)$.

MonotoneOndefMathlib.Order.Monotone.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{MonotoneOn}$ holds for $f$ and $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 if $a \leq b$, then $f (a)\leq f (b)$.

StrictAntidefMathlib.Order.Monotone.Defs, predicate

Wording

f is a strict antitone (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is a strict antitone, if for all elements $a$ and $b$ of $x$, if $a < b$, then $f (b)< f (a)$.

StrictAntiOndefMathlib.Order.Monotone.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{StrictAntiOn}$ holds for $f$ and $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 if $a < b$, then $f (b)< f (a)$.

StrictMonodefMathlib.Order.Monotone.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{StrictMono}$ holds for $f$, if for all elements $a$ and $b$ of $x$, if $a < b$, then $f (a)< f (b)$.

StrictMonoOndefMathlib.Order.Monotone.Defs, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then $\mathrm{StrictMonoOn}$ holds for $f$ and $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 if $a < b$, then $f (a)< f (b)$.

Mathlib.Order.Monotone.Monovary

AntivarydefMathlib.Order.Monotone.Monovary, 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$ to elements of $x_{2}$. Then $\mathrm{Antivary}$ holds for $f$ and $g$, if for all elements $i$ and $j$ of $x$, if $g (i)< g (j)$, then $f (j)\leq f (i)$.

AntivaryOndefMathlib.Order.Monotone.Monovary, 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$ to elements of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{AntivaryOn}$ holds for $f$, $g$ and $s$, if for all elements $i$ of $x$, if $i$ is an element of $s$, then for all elements $j$ of $x$, if $j$ is an element of $s$, then if $g (i)< g (j)$, then $f (j)\leq f (i)$.

MonovarydefMathlib.Order.Monotone.Monovary, 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$ to elements of $x_{2}$. Then $\mathrm{Monovary}$ holds for $f$ and $g$, if for all elements $i$ and $j$ of $x$, if $g (i)< g (j)$, then $f (i)\leq f (j)$.

MonovaryOndefMathlib.Order.Monotone.Monovary, 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$ to elements of $x_{2}$. Let $s$ be an element of $\wp x$. Then $\mathrm{MonovaryOn}$ holds for $f$, $g$ and $s$, if for all elements $i$ of $x$, if $i$ is an element of $s$, then for all elements $j$ of $x$, if $j$ is an element of $s$, then if $g (i)< g (j)$, then $f (i)\leq f (j)$.

Mathlib.Order.Monotone.MonovaryOrder

MonovaryOrderdefMathlib.Order.Monotone.MonovaryOrder, 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$ to elements of $x_{2}$. Let $i$ and $j$ be elements of $x$. Then $\mathrm{MonovaryOrder}$ holds for $f$, $g$, $i$ and $j$, if $\operatorname{Lex}$ holds for the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (x_{5} , x_{6})$, $\operatorname{Lex}$ applied to the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Lt} (x_{7} , x_{8})$ and $\mathrm{WellOrderingRel}$, $\ProdmkMACRoU {f (i)}{(\ProdmkMACRoU {g (i)}{i})}$ and $\ProdmkMACRoU {f (j)}{(\ProdmkMACRoU {g (j)}{j})}$.

Mathlib.Order.NonemptyFiniteChains

PartOrd.nonemptyFiniteChainsFunctordefMathlib.Order.NonemptyFiniteChains, function or constant

Wording

the functor (from the docstring)

English

The functor is a functor of the set of part orders and the set of part orders.

PartialOrder.NonemptyFiniteChainsstructureMathlib.Order.NonemptyFiniteChains, type

Wording

nonempty finite chain of X (from the name)

English

Let $X$ be a set. Then the nonempty finite chains of $X$ are a basic type.

PartialOrder.NonemptyFiniteChains.finsetdefMathlib.Order.NonemptyFiniteChains, function or constant

Wording

the finite set of self (from the name)

English

Let $\mathrm{self}$ be a nonempty finite chain of $X$. Then the finite set of $\mathrm{self}$ is a finite set of $X$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

PartialOrder.NonemptyFiniteChains.mapdefMathlib.Order.NonemptyFiniteChains, function or constant

Wording

the image of s and f (from the docstring)

English

Let $s$ be a nonempty finite chain of $X$. Let $f$ be an order homomorphism of $X$ and $Y$. Then the image of $s$ and $f$ is a nonempty finite chain of $Y$.

PartialOrder.NonemptyFiniteChains.orderHomMapdefMathlib.Order.NonemptyFiniteChains, function or constant

Wording

the monotone map of f (from the docstring)

English

Let $f$ be an order homomorphism of $X$ and $Y$. Then the monotone map of $f$ is an order homomorphism of the set of nonempty finite chains of $X$ and the set of nonempty finite chains of $Y$.

Mathlib.Order.Northcott

NorthcottclassMathlib.Order.Northcott, predicate

Wording

no wording

English

Let $h$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $\mathrm{Northcott}$ holds for $h$.

Mathlib.Order.Notation

BotclassMathlib.Order.Notation, predicate

Wording

x is bottom (from the name)

English

Let $x$ be a set. Then we can say that $x$ is bottom.

Bot.botdefMathlib.Order.Notation, function or constant

Wording

the bottom (from the name)

English

The bottom is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

ComplclassMathlib.Order.Notation, predicate

Wording

x is a complement (from the name)

English

Let $x$ be a set. Then we can say that $x$ is a complement.

Compl.compldefMathlib.Order.Notation, function or constant

Wording

the complement of x1 (from the name)

English

Let $x_{1}$ be an element of $x$. Then the complement of $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

HImpclassMathlib.Order.Notation, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{HImp}$ holds for $x$.

HImp.himpdefMathlib.Order.Notation, function or constant

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\operatorname{himp}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.

HNotclassMathlib.Order.Notation, predicate

Wording

no wording

English

Let $x$ be a set. Then we can say that $\mathrm{HNot}$ holds for $x$.

HNot.hnotdefMathlib.Order.Notation, function or constant

Wording

no wording

English

Let $x_{1}$ be an element of $x$. Then $\operatorname{hnot}$ applied to $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

TopclassMathlib.Order.Notation, predicate

Wording

x is top (from the name)

English

Let $x$ be a set. Then we can say that $x$ is top.

Top.topdefMathlib.Order.Notation, function or constant

Wording

the top (from the name)

English

The top is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Order.Nucleus

NucleusstructureMathlib.Order.Nucleus, type

Wording

nucleus of X (from the name)

English

Let $X$ be a set. Then the nuclei of $X$ are a basic type.

Nucleus.giRestrictdefMathlib.Order.Nucleus, function or constant

Wording

the restriction of n (from the docstring)

English

Let $n$ be a nucleus of $X$. Then the restriction of $n$ is a Galois insertion of $\operatorname{coe}$ applied to $\operatorname{restrict}$ applied to $n$ and the function that maps $x_{1}$ to the proposition that $x_{1}$ is an element of the range of $\operatorname{coe}$ applied to $n$.

Nucleus.restrictdefMathlib.Order.Nucleus, function or constant

Wording

no wording

English

Let $n$ be a nucleus of $X$. Then $\operatorname{restrict}$ applied to $n$ is a frame homomorphism of $X$ and the set of elements of the range of $\operatorname{coe}$ applied to $n$.

Nucleus.toClosureOperatordefMathlib.Order.Nucleus, function or constant

Wording

the closure operator of n (from the name)

English

Let $n$ be a nucleus of $X$. Then the closure operator of $n$ is a closure operator of $X$.

NucleusClassclassMathlib.Order.Nucleus, predicate

Wording

no wording

English

Let $F$ and $X$ be sets. Then we can say that $\mathrm{NucleusClass}$ holds for $F$ and $X$.

Mathlib.Order.OmegaCompletePartialOrder

OmegaCompletePartialOrderclassMathlib.Order.OmegaCompletePartialOrder, predicate

Wording

x is a omega complete partial order (from the name)

English

Let $x$ be a set. Then we can say that $x$ is an omega complete partial order.

OmegaCompletePartialOrder.ChainstructureMathlib.Order.OmegaCompletePartialOrder, type

Wording

chain of x (from the name)

English

Let $x$ be a set. Then the chains of $x$ are a basic type.

OmegaCompletePartialOrder.Chain.mapdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the map of c and f (from the name)

English

Let $c$ be a chain of $x$. Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the map of $c$ and $f$ is a chain of $x_{1}$ defined as $\operatorname{mk}$ applied to the composition of $f$ and $\operatorname{toOrderHom}$ applied to $c$.

OmegaCompletePartialOrder.Chain.pairdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the pair of a and b (from the name)

English

Let $a$ and $b$ be elements of $x$ such that $a \leq b$. Then the pair of $a$ and $b$ is a chain of $x$.

OmegaCompletePartialOrder.Chain.zipdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

no wording

English

Let $x_{4}$ be a chain of $x$. Let $x_{5}$ be a chain of $x_{1}$. Then $\operatorname{zip}$ applied to $x_{4}$ and $x_{5}$ is a chain of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the product of $\operatorname{toOrderHom}$ applied to $x_{4}$ and $\operatorname{toOrderHom}$ applied to $x_{5}$.

OmegaCompletePartialOrder.ContinuousHomstructureMathlib.Order.OmegaCompletePartialOrder, type

Wording

continuous homomorphism of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be sets. Then the continuous homomorphisms of $x$ and $x_{1}$ are a basic type.

OmegaCompletePartialOrder.ContinuousHom.Prod.applydefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the product (from the name)

English

The product is a continuous homomorphism of $\mathrm{Prod}$ applied to the set of continuous homomorphisms of $x$ and $x_{1}$ and $x$ and $x_{1}$.

OmegaCompletePartialOrder.ContinuousHom.binddefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

no wording

English

Let $f$ be a continuous homomorphism of $x$ and the set of parts of $x_{2}$. Let $g$ be a continuous homomorphism of $x$ and the set of functions from elements of $x_{2}$ to parts of $x_{3}$. Then $\operatorname{bind}$ applied to $f$ and $g$ is a continuous homomorphism of $x$ and the set of parts of $x_{3}$.

OmegaCompletePartialOrder.ContinuousHom.compdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a continuous homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a continuous homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a continuous homomorphism of $x$ and $x_{2}$.

OmegaCompletePartialOrder.ContinuousHom.constdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the constant of x4 (from the name)

English

Let $x_{4}$ be an element of $x_{1}$. Then the constant of $x_{4}$ is a continuous homomorphism of $x$ and $x_{1}$.

OmegaCompletePartialOrder.ContinuousHom.copydefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the copy 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 continuous homomorphism of $x$ and $x_{1}$ such that $f$ is equal to $\operatorname{coe}$ applied to $g$. Then the copy of $f$ and $g$ is a continuous homomorphism of $x$ and $x_{1}$.

OmegaCompletePartialOrder.ContinuousHom.flipdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the flip of f (from the name)

English

Let $f$ be a function from elements of $x_{4}$ to continuous homomorphisms of $x$ and $x_{1}$. Then the flip of $f$ is a continuous homomorphism of $x$ and the set of functions from elements of $x_{4}$ to elements of $x_{1}$.

OmegaCompletePartialOrder.ContinuousHom.iddefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the identity (from the docstring)

English

The identity is a continuous homomorphism of $x$ and $x$.

OmegaCompletePartialOrder.ContinuousHom.mapdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the map of f and g (from the name)

English

Let $f$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Let $g$ be a continuous homomorphism of $x$ and the set of parts of $x_{2}$. Then the map of $f$ and $g$ is a continuous homomorphism of $x$ and the set of parts of $x_{3}$.

OmegaCompletePartialOrder.ContinuousHom.ofFundefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the continuous homomorphism of f and hf (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{autoParam}$ holds for $\mathrm{OmegaCompletePartialOrder\_\_\_u3c9\_ScottContinuous}$ applied to $f$ and $\mathrm{OmegaCompletePartialOrder\_\_ContinuousHom\_\_ofFun\_\_\_auto\_1}$. Then the continuous homomorphism of $f$ and $\mathrm{hf}$ is a continuous homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{OmegaCompletePartialOrder\_\_\_u3c9\_ScottContinuous\_\_monotone}$ applied to $\mathrm{hf}$ and $\mathrm{OmegaCompletePartialOrder\_\_\_u3c9\_ScottContinuous\_\_map\_\_u3c9\_Sup}$ applied to $\mathrm{hf}$.

OmegaCompletePartialOrder.ContinuousHom.seqdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the sequence of f and g (from the name)

English

Let $f$ be a continuous homomorphism of $x$ and the set of parts of the set of functions from elements of $x_{2}$ to elements of $x_{3}$. Let $g$ be a continuous homomorphism of $x$ and the set of parts of $x_{2}$. Then the sequence of $f$ and $g$ is a continuous homomorphism of $x$ and the set of parts of $x_{3}$.

OmegaCompletePartialOrder.ContinuousHom.toMonodefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

no wording

English

$\operatorname{toMono}$ is an order homomorphism of the set of continuous homomorphisms of $x$ and $x_{1}$ and the set of order homomorphisms of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the function that maps $f$ to the order homomorphism of $f$ and the function that maps $x_{4}$, $x_{5}$ and $h$ to $h$.

OmegaCompletePartialOrder.ContinuousHom.ωSupdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the supremum of c (from the name)

English

Let $c$ be a chain of the set of continuous homomorphisms of $x$ and $x_{1}$. Then the supremum of $c$ is a continuous homomorphism of $x$ and $x_{1}$.

OmegaCompletePartialOrder.OrderHom.ωSupdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the supremum of c (from the name)

English

Let $c$ be a chain of the set of order homomorphisms of $x$ and $x_{1}$. Then the supremum of $c$ is an order homomorphism of $x$ and $x_{1}$.

OmegaCompletePartialOrder.fixedPoints.iterateChaindefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

no wording

English

Let $f$ be an order homomorphism of $x$ and $x$. Let $x_{2}$ be an element of $x$ such that $x_{2} \leq f (x_{2})$. Then $\operatorname{iterateChain}$ applied to $f$, $x_{2}$ and $h$ is a chain of $x$.

OmegaCompletePartialOrder.ωScottContinuousdefMathlib.Order.OmegaCompletePartialOrder, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{OmegaCompletePartialOrder\_\_\_u3c9\_ScottContinuous}$ holds for $f$, if $\mathrm{ScottContinuousOn}$ holds for the range of the function that maps $c$ to the range of $\operatorname{coe}$ applied to $c$ and $f$.

OmegaCompletePartialOrder.ωSupdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the supremum of x1 (from the docstring)

English

Let $x_{1}$ be a chain of $x$. Then the supremum of $x_{1}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

Part.ωSupdefMathlib.Order.OmegaCompletePartialOrder, function or constant

Wording

the supremum of c (from the name)

English

Let $c$ be a chain of the set of parts of $x$. Then the supremum of $c$ is a part of $x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $a$ of $x$, such that $\MembershipmemMACRoT {c}{\operatorname{some} (a)}$, the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{choose}$ applied to $h$ and the function that maps $h_{1}$ to the none.

Mathlib.Order.OrdContinuous

LeftOrdContinuousdefMathlib.Order.OrdContinuous, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{LeftOrdContinuous}$ holds for $f$, if for all elements $s$ of $\wp x$, for all elements $x_{4}$ of $x$, if $s$ is nonempty, then if $\mathrm{IsLUB}$ holds for $s$ and $x_{4}$, then $\mathrm{IsLUB}$ holds for the image of $f$ and $s$ and $f$ applied to $x_{4}$.

LeftOrdContinuous.toOrderEmbeddingdefMathlib.Order.OrdContinuous, function or constant

Wording

the order embedding of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{LeftOrdContinuous}$ holds for $f$ and $f$ is injective. Then the order embedding of $f$ is an order embedding of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $h$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{LeftOrdContinuous\_\_le\_iff}$ applied to $\mathrm{hf}$ and $h$.

RightOrdContinuousdefMathlib.Order.OrdContinuous, predicate

Wording

no wording

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\mathrm{RightOrdContinuous}$ holds for $f$, if for all elements $s$ of $\wp x$, for all elements $x_{4}$ of $x$, if $s$ is nonempty, then if $\mathrm{IsGLB}$ holds for $s$ and $x_{4}$, then $\mathrm{IsGLB}$ holds for the image of $f$ and $s$ and $f$ applied to $x_{4}$.

RightOrdContinuous.toOrderEmbeddingdefMathlib.Order.OrdContinuous, function or constant

Wording

the order embedding of f (from the name)

English

Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\mathrm{RightOrdContinuous}$ holds for $f$ and $f$ is injective. Then the order embedding of $f$ is an order embedding of $x$ and $x_{1}$.

Mathlib.Order.OrderDual

OrderDualdefMathlib.Order.OrderDual, type

Wording

order dual of x (from the name)

English

Let $x$ be a set. Then an order dual of $x$ is an element of the function that maps $x$ to $x$.

OrderDual.ofDualdefMathlib.Order.OrderDual, function or constant

Wording

the order dual (from the name)

English

The order dual is an equivalence from the set of order duals of $x$ to $x$ defined as the identity of the set of order duals of $x$.

OrderDual.toDualdefMathlib.Order.OrderDual, function or constant

Wording

the dual (from the name)

English

The dual is an equivalence from $x$ to the set of order duals of $x$ defined as the identity of $x$.

Mathlib.Order.OrderIsoNat

Nat.Subtype.orderIsoOfNatdefMathlib.Order.OrderIsoNat, function or constant

Wording

the order isomorphism of s (from the name)

English

Let $s$ be an element of $\wp \Natural$. Then the order isomorphism of $s$ is an order isomorphism of $\Natural$ and the set of elements of $s$.

Nat.orderEmbeddingOfSetdefMathlib.Order.OrderIsoNat, function or constant

Wording

the order embedding of s (from the name)

English

Let $s$ be an element of $\wp \Natural$. Then the order embedding of $s$ is an order embedding of $\Natural$ and $\Natural$.

RelEmbedding.natGTdefMathlib.Order.OrderIsoNat, function or constant

Wording

no wording

English

Let $f$ be a function from natural numbers to elements of $x$ such that for all natural numbers $n$, $r$ holds for $f$ applied to $n + 1$ and $f$ applied to $n$. Then $\operatorname{natGT}$ applied to $f$ and $H$ is a relation embedding of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Gt} (x_{1} , x_{2})$ and $r$ defined as the swap of $\operatorname{natLT}$ applied to $f$ and $H$.

RelEmbedding.natLTdefMathlib.Order.OrderIsoNat, function or constant

Wording

no wording

English

Let $f$ be a function from natural numbers to elements of $x$ such that for all natural numbers $n$, $r$ holds for $f$ applied to $n$ and $f$ applied to $n + 1$. Then $\operatorname{natLT}$ applied to $f$ and $H$ is a relation embedding of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$ and $r$.

monotonicSequenceLimitdefMathlib.Order.OrderIsoNat, function or constant

Wording

the constant value of a (from the docstring)

English

Let $a$ be an order homomorphism of $\Natural$ and $x$. Then the constant value of $a$ is an element of $x$ defined as $a$ applied to the monotonic sequence limit index of $a$.

monotonicSequenceLimitIndexdefMathlib.Order.OrderIsoNat, function or constant

Wording

the monotonic sequence limit index of a (from the name)

English

Let $a$ be an order homomorphism of $\Natural$ and $x$. Then the monotonic sequence limit index of $a$ is a natural number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $n$ to the proposition that for all natural numbers $m$, if $n \leq m$, then $\EqtMACRoH {a (n)}{a (m)}$.

Mathlib.Order.PFilter

Order.IsPFilterdefMathlib.Order.PFilter, predicate

Wording

F is a filter (from the name)

English

Let $F$ be an element of $\wp P$. Then $F$ is a filter, if the preimage of $\operatorname{coe}$ applied to the order dual and $F$ is an ideal.

Order.IsPFilter.toPFilterdefMathlib.Order.PFilter, function or constant

Wording

the filter of h (from the name)

English

Assume that $F$ is a filter. Then the filter of $h$ is a filter of $P$ defined as $\operatorname{mk}$ applied to the ideal of $h$.

Order.PFilterstructureMathlib.Order.PFilter, type

Wording

filter of P (from the name)

English

Let $P$ be a set. Then the filters of $P$ are a basic type.

Order.PFilter.dualdefMathlib.Order.PFilter, function or constant

Wording

the dual of self (from the name)

English

Let $\mathrm{self}$ be a filter of $P$. Then the dual of $\mathrm{self}$ is an ideal of the set of order duals of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Order.PFilter.infGidefMathlib.Order.PFilter, function or constant

Wording

no wording

English

$\operatorname{infGi}$ is a Galois coinsertion of the function that maps $x_{1}$ to $\operatorname{toDual}$ applied to $\operatorname{principal}$ applied to $x_{1}$ and the function that maps $F$ to the infimum of $\operatorname{ofDual}$ applied to $F$.

Order.PFilter.principaldefMathlib.Order.PFilter, function or constant

Wording

no wording

English

Let $p$ be an element of $P$. Then $\operatorname{principal}$ applied to $p$ is a filter of $P$ defined as $\operatorname{mk}$ applied to $\operatorname{principal}$ applied to $\operatorname{toDual}$ applied to $p$.

Mathlib.Order.Part

OrderHom.partBinddefMathlib.Order.Part, function or constant

Wording

no wording

English

Let $f$ be an order homomorphism of $x$ and the set of parts of $x_{1}$. Let $g$ be an order homomorphism of $x$ and the set of functions from elements of $x_{1}$ to parts of $x_{2}$. Then $\operatorname{partBind}$ applied to $f$ and $g$ is an order homomorphism of $x$ and the set of parts of $x_{2}$.

Mathlib.Order.PartialSups

partialSupsdefMathlib.Order.PartialSups, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $x_{1}$ to elements of $x$. Then $\mathrm{partialSups}$ applied to $f$ is an order homomorphism of $x_{1}$ and $x$.