IsAntichaindefMathlib.Order.Antichain, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{IsAntichain}$ holds for $r$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the complement of $r$.
IsMaxAntichaindefMathlib.Order.Antichain, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{IsMaxAntichain}$ holds for $r$ and $s$, if $\mathrm{IsAntichain}$ holds for $r$ and $s$ and for all elements $t$ of $\wp x$, if $\mathrm{IsAntichain}$ holds for $r$ and $t$, then if $s \leq t$, then $\EqtMACRoH {s}{t}$.
IsStrongAntichaindefMathlib.Order.Antichain, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{IsStrongAntichain}$ holds for $r$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the function that maps $a$ and $b$ to the proposition that for all elements $c$ of $x$, it is not the case that $r$ holds for $a$ and $c$ or it is not the case that $r$ holds for $b$ and $c$.
IsWeakAntichaindefMathlib.Order.Antichain, predicateWording
s is a weak antichain (from the name)
English
Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i))$. Then $s$ is a weak antichain, if $\mathrm{IsAntichain}$ holds for the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{StrongLT}$ applied to $x_{3}$ and $x_{4}$ and $s$.
AntisymmReldefMathlib.Order.Antisymmetrization, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $b$ be elements of $x$. Then $\mathrm{AntisymmRel}$ holds for $r$, $a$ and $b$, if $r$ holds for $a$ and $b$ and $r$ holds for $b$ and $a$.
AntisymmetrizationdefMathlib.Order.Antisymmetrization, typeWording
antisymmetrization of x and r (from the name)
English
Let $x$ be a set. Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then an antisymmetrization of $x$ and $r$ is an element of the function that maps $x$ and $r$ to $\mathrm{Quotient}$ applied to $\operatorname{setoid}$ applied to $x$ and $r$.
Antisymmetrization.prodEquivdefMathlib.Order.Antisymmetrization, function or constantWording
the product equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the product equivalence of $x$ and $x_{1}$ is an order isomorphism of the set of antisymmetrizations of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and $\mathrm{Prod}$ applied to the set of antisymmetrizations of $x$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Leq} (x_{6} , x_{7})$ and the set of antisymmetrizations of $x_{1}$ and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Leq} (x_{8} , x_{9})$.
OrderEmbedding.ofAntisymmetrizationdefMathlib.Order.Antisymmetrization, function or constantWording
the order embedding of x (from the name)
English
Let $x$ be a set. Then the order embedding of $x$ is an order embedding of the set of antisymmetrizations of $x$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and $x$.
OrderHom.antisymmetrizationdefMathlib.Order.Antisymmetrization, function or constantWording
the antisymmetrization of f (from the name)
English
Let $f$ be an order homomorphism of $x$ and $x_{1}$. Then the antisymmetrization of $f$ is an order homomorphism of the set of antisymmetrizations of $x$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$ and the set of antisymmetrizations of $x_{1}$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Leq} (x_{6} , x_{7})$.
OrderIso.dualAntisymmetrizationdefMathlib.Order.Antisymmetrization, function or constantWording
the dual antisymmetrization of x (from the name)
English
Let $x$ be a set. Then the dual antisymmetrization of $x$ is an order isomorphism of the set of order duals of the set of antisymmetrizations of $x$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$ and the set of antisymmetrizations of the set of order duals of $x$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{Leq} (x_{4} , x_{5})$.
ofAntisymmetrizationdefMathlib.Order.Antisymmetrization, function or constantWording
the antisymmetrization 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 antisymmetrization of $x$ and $r$. Then the antisymmetrization of $r$ and $x_{1}$ is an element of $x$ defined as $\operatorname{out}$ applied to $x_{1}$.
toAntisymmetrizationdefMathlib.Order.Antisymmetrization, function or constantWording
the antisymmetrization 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 antisymmetrization of $r$ and $x_{1}$ is an antisymmetrization of $x$ and $r$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ applied to $x$ and $r$ and $x_{1}$.
CompleteAtomicBooleanAlgebra.toSetOfIsAtomdefMathlib.Order.Atoms, function or constantWording
the set (from the name)
English
The set is an order isomorphism of $x$ and $\wp (\SubtypeSet {a}{\mathrm{IsAtom} (a)})$.
IsAtomdefMathlib.Order.Atoms, predicateWording
a is a atom (from the name)
English
Let $a$ be an element of $x$. Then $a$ is an atom, if $a$ is distinct from the bottom and for all elements $b$ of $x$, if $b < a$, then $b$ is equal to the bottom.
IsAtomicclassMathlib.Order.Atoms, predicateWording
x is atomic (from the name)
English
Let $x$ be a set. Then we can say that $x$ is atomic.
IsAtomisticclassMathlib.Order.Atoms, predicateWording
x is atomistic (from the name)
English
Let $x$ be a set. Then we can say that $x$ is atomistic.
IsCoatomdefMathlib.Order.Atoms, predicateEnglish
Let $a$ be an element of $x$. Then $\mathrm{IsCoatom}$ holds for $a$, if $a$ is distinct from the top and for all elements $b$ of $x$, if $a < b$, then $b$ is equal to the top.
IsCoatomicclassMathlib.Order.Atoms, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{IsCoatomic}$ holds for $x$.
IsCoatomisticclassMathlib.Order.Atoms, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{IsCoatomistic}$ holds for $x$.
IsSimpleOrderclassMathlib.Order.Atoms, predicateWording
x is a simple order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a simple order.
IsSimpleOrder.equivBooldefMathlib.Order.Atoms, function or constantWording
the equivalence bool (from the name)
English
The equivalence bool is an equivalence from $x$ to $\mathrm{Bool}$.
IsSimpleOrder.orderIsoBooldefMathlib.Order.Atoms, function or constantWording
the order isomorphism bool (from the name)
English
The order isomorphism bool is an order isomorphism of $x$ and $\mathrm{Bool}$.
IsStronglyAtomicclassMathlib.Order.Atoms, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{IsStronglyAtomic}$ holds for $x$.
IsStronglyCoatomicclassMathlib.Order.Atoms, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{IsStronglyCoatomic}$ holds for $x$.
DenselyOrderedclassMathlib.Order.Basic, predicateWording
x is dense (from the docstring)
English
Let $x$ be a set. Then we can say that $x$ is dense.
Order.PreimagedefMathlib.Order.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Let $x_{2}$ and $y$ be elements of $x$. Then $\operatorname{Preimage}$ holds for $f$, $s$, $x_{2}$ and $y$, if $s$ holds for $f$ applied to $x_{2}$ and $f$ applied to $y$.
StrongLTdefMathlib.Order.Basic, predicateEnglish
Let $a$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $b$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then $\mathrm{StrongLT}$ holds for $i_{1}$, $a$, $i$ and $b$, if for all elements $i$ of $x$, $i_{1} (i)< a (i)$.
LatticeHom.birkhoffFinsetdefMathlib.Order.Birkhoff, function or constantEnglish
$\operatorname{birkhoffFinset}$ is a lattice homomorphism of $x$ and the set of finite sets of $\SubtypeSet {a}{\mathrm{SupIrred} (a)}$.
LatticeHom.birkhoffSetdefMathlib.Order.Birkhoff, function or constantEnglish
$\operatorname{birkhoffSet}$ is a lattice homomorphism of $x$ and $\wp (\SubtypeSet {a}{\mathrm{SupIrred} (a)})$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $\operatorname{birkhoffSet}$ and $\mathrm{OrderEmbedding\_\_birkhoffSet\_sup}$ and $\mathrm{OrderEmbedding\_\_birkhoffSet\_inf}$.
OrderEmbedding.birkhoffFinsetdefMathlib.Order.Birkhoff, function or constantEnglish
$\operatorname{birkhoffFinset}$ is an order embedding of $x$ and the set of finite sets of $\SubtypeSet {a}{\mathrm{SupIrred} (a)}$ defined as the composition of $\operatorname{birkhoffSet}$ and the order embedding of the inverse of the finite set order isomorphism set.
OrderEmbedding.birkhoffSetdefMathlib.Order.Birkhoff, function or constantEnglish
$\operatorname{birkhoffSet}$ is an order embedding of $x$ and $\wp (\SubtypeSet {a}{\mathrm{SupIrred} (a)})$.
OrderEmbedding.infIrredUpperSetdefMathlib.Order.Birkhoff, function or constantWording
the infimum irreducible upper set (from the name)
English
The infimum irreducible upper set is an order embedding of $x$ and $\SubtypeSet {s}{\mathrm{InfIrred} (s)}$.
OrderEmbedding.supIrredLowerSetdefMathlib.Order.Birkhoff, function or constantWording
the supremum irreducible lower set (from the name)
English
The supremum irreducible lower set is an order embedding of $x$ and $\SubtypeSet {s}{\mathrm{SupIrred} (s)}$.
OrderIso.infIrredUpperSetdefMathlib.Order.Birkhoff, function or constantWording
the infimum irreducible upper set (from the name)
English
The infimum irreducible upper set is an order isomorphism of $x$ and $\SubtypeSet {s}{\mathrm{InfIrred} (s)}$.
OrderIso.lowerSetSupIrreddefMathlib.Order.Birkhoff, function or constantEnglish
$\operatorname{lowerSetSupIrred}$ is an order isomorphism of $x$ and the set of lower sets of $\SubtypeSet {a}{\mathrm{SupIrred} (a)}$.
OrderIso.supIrredLowerSetdefMathlib.Order.Birkhoff, function or constantWording
the supremum irreducible lower set (from the name)
English
The supremum irreducible lower set is an order isomorphism of $x$ and $\SubtypeSet {s}{\mathrm{SupIrred} (s)}$ defined as the relation isomorphism of the supremum irreducible lower set and $\mathrm{OrderEmbedding\_\_supIrredLowerSet\_surjective}$.
BooleanAlgebraclassMathlib.Order.BooleanAlgebra.Defs, predicateWording
x is a boolean algebra (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a boolean algebra.
GeneralizedBooleanAlgebraclassMathlib.Order.BooleanAlgebra.Defs, predicateWording
x is a generalized boolean algebra (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a generalized boolean algebra.
Set.itedefMathlib.Order.BooleanAlgebra.Set, function or constantEnglish
Let $t$, $s$ and $\mathrm{s'}$ be elements of $\wp x$. Then $\operatorname{ite}$ applied to $t$, $s$ and $\mathrm{s'}$ is an element of $\wp x$ defined as $\UnionunionMACRoAB {\operatorname{inter} (s , t)}{\operatorname{sdiff} (\mathrm{s'} , t)}$.
IsCompactlyGenerated.BooleanGeneratorsstructureMathlib.Order.BooleanGenerators, predicateEnglish
Let $S$ be an element of $\wp x$. Then we can say that $\operatorname{BooleanGenerators}$ holds for $S$.
BooleanSubalgebrastructureMathlib.Order.BooleanSubalgebra, typeWording
boolean subalgebra of x (from the name)
English
Let $x$ be a set. Then the boolean subalgebras of $x$ are a basic type.
BooleanSubalgebra.closuredefMathlib.Order.BooleanSubalgebra, function or constantWording
the closure of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the closure of $s$ is a boolean subalgebra of $x$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $L$ to $\mathrm{Leq} (s , L)$.
BooleanSubalgebra.comapdefMathlib.Order.BooleanSubalgebra, function or constantWording
the preimage of f and L (from the docstring)
English
Let $f$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a boolean subalgebra of $x_{1}$. Then the preimage of $f$ and $L$ is a boolean subalgebra of $x$.
BooleanSubalgebra.copydefMathlib.Order.BooleanSubalgebra, function or constantWording
the copy of L and s (from the name)
English
Let $L$ be a boolean subalgebra of $x$. Let $s$ be an element of $\wp x$ such that $\EqtMACRoH {s}{L}$. Then the copy of $L$ and $s$ is a boolean subalgebra of $x$.
BooleanSubalgebra.inclusiondefMathlib.Order.BooleanSubalgebra, function or constantWording
the inclusion of h (from the name)
English
Assume that $L \leq M$. Then the inclusion of $h$ is a bounded lattice homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$.
BooleanSubalgebra.mapdefMathlib.Order.BooleanSubalgebra, function or constantWording
the map of f and L (from the name)
English
Let $f$ be a bounded lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a boolean subalgebra of $x$. Then the map of $f$ and $L$ is a boolean subalgebra of $x_{1}$.
BooleanSubalgebra.subtypedefMathlib.Order.BooleanSubalgebra, function or constantWording
the subtype of L (from the name)
English
Let $L$ be a boolean subalgebra of $x$. Then the subtype of $L$ is a bounded lattice homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $\MembershipmemMACRoT {L}{x_{2}}$ and $\mathrm{BooleanSubalgebra\_\_val\_sup}$ and $\mathrm{BooleanSubalgebra\_\_val\_inf}$, $\mathrm{BooleanSubalgebra\_\_val\_top}$ and $\mathrm{BooleanSubalgebra\_\_val\_bot}$.
BooleanSubalgebra.topEquivdefMathlib.Order.BooleanSubalgebra, function or constantWording
the top equivalence (from the name)
English
The top equivalence is an order isomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{2}})}$ and $x$.
BooleanisationdefMathlib.Order.Booleanisation, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{Booleanisation}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Sum}$ applied to $x$ and $x$.
Booleanisation.LEinductiveMathlib.Order.Booleanisation, predicateEnglish
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Booleanisation}$ applied to $x$. Then we can say that $\operatorname{LE}$ holds for $x_{2}$ and $x_{3}$.
Booleanisation.LTinductiveMathlib.Order.Booleanisation, predicateEnglish
Let $x_{2}$ and $x_{3}$ be elements of $\mathrm{Booleanisation}$ applied to $x$. Then we can say that $\operatorname{LT}$ holds for $x_{2}$ and $x_{3}$.
Booleanisation.compdefMathlib.Order.Booleanisation, function or constantWording
the composition of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the composition of $x_{1}$ is an element of $\mathrm{Booleanisation}$ applied to $x$ defined as $\operatorname{inr}$ applied to $x_{1}$.
Booleanisation.liftdefMathlib.Order.Booleanisation, function or constantWording
the lift of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the lift of $x_{1}$ is an element of $\mathrm{Booleanisation}$ applied to $x$ defined as $\operatorname{inl}$ applied to $x_{1}$.
Booleanisation.liftLatticeHomdefMathlib.Order.Booleanisation, function or constantWording
the lift lattice homomorphism (from the name)
English
The lift lattice homomorphism is a lattice homomorphism of $x$ and $\mathrm{Booleanisation}$ applied to $x$.
BoundedOrderclassMathlib.Order.BoundedOrder.Basic, predicateWording
x is a bounded order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a bounded order.
OrderBotclassMathlib.Order.BoundedOrder.Basic, predicateWording
x is a order bottom (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order bottom.
OrderTopclassMathlib.Order.BoundedOrder.Basic, predicateWording
x is a order top (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order top.
botOrderOrNoBotOrderdefMathlib.Order.BoundedOrder.Basic, function or constantEnglish
Let $x$ be a set. Then $\mathrm{botOrderOrNoBotOrder}$ applied to $x$ is an element of $\mathrm{PSum}$ applied to the proposition that $x$ is an order bottom and $\mathrm{NoBotOrder}$ applied to $x$.
topOrderOrNoTopOrderdefMathlib.Order.BoundedOrder.Basic, function or constantEnglish
Let $x$ be a set. Then $\mathrm{topOrderOrNoTopOrder}$ applied to $x$ is an element of $\mathrm{PSum}$ applied to the proposition that $x$ is an order top and $\mathrm{NoTopOrder}$ applied to $x$.
tacticBddDefaultdefMathlib.Order.Bounds.Basic, function or constantEnglish
generation took over the time limit
BddAbovedefMathlib.Order.Bounds.Defs, predicateWording
s is bounded above (by hand)
English
Let $s$ be an element of $\wp x$. Then $s$ is bounded above, if the upper bound of $s$ is nonempty.
BddBelowdefMathlib.Order.Bounds.Defs, predicateWording
s is bounded below (from the docstring)
English
Let $s$ be an element of $\wp x$. Then $s$ is bounded below, if the lower bound of $s$ is nonempty.
InfSetclassMathlib.Order.Bounds.Defs, predicateWording
x is a infimum set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an infimum set.
InfSet.sInfdefMathlib.Order.Bounds.Defs, function or constantWording
the infimum of x1 (from the name)
English
Let $x_{1}$ be an element of $\wp x$. Then the infimum of $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
IsCofinaldefMathlib.Order.Bounds.Defs, predicateWording
s is cofinal (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is cofinal, if for all elements $x_{2}$ of $x$, there exists an element $y$ of $x$, such that $y$ is an element of $s$ and $x_{2} \leq y$.
IsCofinalFordefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ and $t$ be elements of $\wp x$. Then $\mathrm{IsCofinalFor}$ holds for $s$ and $t$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then there exists an element $b$ of $x$, such that $b$ is an element of $t$ and $a \leq b$.
IsCoinitialdefMathlib.Order.Bounds.Defs, predicateWording
s is coinitial (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is coinitial, if for all elements $x_{2}$ of $x$, there exists an element $y$ of $x$, such that $y$ is an element of $s$ and $y \leq x_{2}$.
IsCoinitialFordefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ and $t$ be elements of $\wp x$. Then $\mathrm{IsCoinitialFor}$ holds for $s$ and $t$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then there exists an element $b$ of $x$, such that $b$ is an element of $t$ and $b \leq a$.
IsGLBdefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{IsGLB}$ holds for $s$ and $x_{2}$, if $\mathrm{IsGreatest}$ holds for the lower bound of $s$ and $x_{2}$.
IsGreatestdefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsGreatest}$ holds for $s$ and $a$, if $a$ is an element of $s$ and $a$ is an element of the upper bound of $s$.
IsLUBdefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $x$. Then $\mathrm{IsLUB}$ holds for $s$ and $x_{2}$, if $\mathrm{IsLeast}$ holds for the upper bound of $s$ and $x_{2}$.
IsLeastdefMathlib.Order.Bounds.Defs, predicateEnglish
Let $s$ be an element of $\wp x$. Let $a$ be an element of $x$. Then $\mathrm{IsLeast}$ holds for $s$ and $a$, if $a$ is an element of $s$ and $a$ is an element of the lower bound of $s$.
OrderInfSetclassMathlib.Order.Bounds.Defs, predicateWording
x is a order infimum set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order infimum set.
OrderSupSetclassMathlib.Order.Bounds.Defs, predicateWording
x is a order supremum set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is an order supremum set.
SupSetclassMathlib.Order.Bounds.Defs, predicateWording
x is a supremum set (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a supremum set.
SupSet.sSupdefMathlib.Order.Bounds.Defs, function or constantWording
the supremum of x1 (from the name)
English
Let $x_{1}$ be an element of $\wp x$. Then the supremum of $x_{1}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
lowerBoundsdefMathlib.Order.Bounds.Defs, function or constantWording
the lower bound of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the lower bound of $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that for all elements $a$ of $x$, if $a$ is an element of $s$, then $x_{2} \leq a$.
upperBoundsdefMathlib.Order.Bounds.Defs, function or constantWording
the upper bound of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the upper bound of $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to the proposition that for all elements $a$ of $x$, if $a$ is an element of $s$, then $a \leq x_{2}$.
ChainCompletePartialOrderclassMathlib.Order.BourbakiWitt, predicateWording
x is a chain complete partial order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a chain complete partial order.
ChainCompletePartialOrder.IsAdmissiblestructureMathlib.Order.BourbakiWitt, predicateEnglish
Let $x_{2}$ be an element of $x$. Let $f$ be a function from elements of $x$ to elements of $x$. Let $s$ be an element of $\wp x$. Then we can say that $\operatorname{IsAdmissible}$ holds for $x_{2}$, $f$ and $s$.
ChainCompletePartialOrder.IsExtremePtstructureMathlib.Order.BourbakiWitt, predicateEnglish
Let $x_{2}$ and $y$ be elements of $x$. Let $f$ be a function from elements of $x$ to elements of $x$. Then we can say that $\operatorname{IsExtremePt}$ holds for $x_{2}$, $f$ and $y$.
ChainCompletePartialOrder.botdefMathlib.Order.BourbakiWitt, function or constantWording
the bottom admissible set with base point of x2 and f (from the docstring)
English
Let $x_{2}$ be an element of $x$. Let $f$ be a function from elements of $x$ to elements of $x$. Then the bottom admissible set with base point of $x_{2}$ and $f$ is an element of $\wp x$ defined as the intersection of $\operatorname{ofPred}$ applied to the function that maps $s$ to $\operatorname{IsAdmissible}$ applied to $x_{2}$, $f$ and $s$.
ChainCompletePartialOrder.cSupdefMathlib.Order.BourbakiWitt, function or constantWording
the supremum of x1 (from the docstring)
English
Let $x_{1}$ be a nonempty 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}$.
NonemptyChainstructureMathlib.Order.BourbakiWitt, typeWording
nonempty chain of x (from the name)
English
Let $x$ be a set. Then the nonempty chains of $x$ are a basic type.
NonemptyChain.carrierdefMathlib.Order.BourbakiWitt, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a nonempty chain of $x$. Then the carrier of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
BddDistLatstructureMathlib.Order.Category.BddDistLat, typeEnglish
The elements of $\mathrm{BddDistLat}$ are a basic type.
BddDistLat.HomstructureMathlib.Order.Category.BddDistLat, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{BddDistLat}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
BddDistLat.Hom.homdefMathlib.Order.Category.BddDistLat, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $X$ and the set of carriers of $\operatorname{toDistLat}$ applied to $Y$ defined as the homomorphism of $f$.
BddDistLat.Hom.hom'defMathlib.Order.Category.BddDistLat, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $X$ and the set of carriers of $\operatorname{toDistLat}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
BddDistLat.Iso.mkdefMathlib.Order.Category.BddDistLat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $x$ and the set of carriers of $\operatorname{toDistLat}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
BddDistLat.dualdefMathlib.Order.Category.BddDistLat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{BddDistLat}$ and $\mathrm{BddDistLat}$.
BddDistLat.dualEquivdefMathlib.Order.Category.BddDistLat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{BddDistLat}$ and $\mathrm{BddDistLat}$.
BddDistLat.ofdefMathlib.Order.Category.BddDistLat, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is an element of $\mathrm{BddDistLat}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $x$.
BddDistLat.ofHomdefMathlib.Order.Category.BddDistLat, function or constantEnglish
Let $f$ be a bounded lattice homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
BddDistLat.toBddLatdefMathlib.Order.Category.BddDistLat, function or constantEnglish
Let $X$ be an element of $\mathrm{BddDistLat}$. Then $\operatorname{toBddLat}$ applied to $X$ is an element of $\mathrm{BddLat}$ defined as $\operatorname{of}$ applied to the set of carriers of $\operatorname{toDistLat}$ applied to $X$.
BddLatstructureMathlib.Order.Category.BddLat, typeEnglish
The elements of $\mathrm{BddLat}$ are a basic type.
BddLat.HomstructureMathlib.Order.Category.BddLat, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{BddLat}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
BddLat.Hom.homdefMathlib.Order.Category.BddLat, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toLat}$ applied to $X$ and the set of carriers of $\operatorname{toLat}$ applied to $Y$ defined as the homomorphism of $f$.
BddLat.Hom.hom'defMathlib.Order.Category.BddLat, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toLat}$ applied to $X$ and the set of carriers of $\operatorname{toLat}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
BddLat.Iso.mkdefMathlib.Order.Category.BddLat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toLat}$ applied to $x$ and the set of carriers of $\operatorname{toLat}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
BddLat.dualdefMathlib.Order.Category.BddLat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{BddLat}$ and $\mathrm{BddLat}$.
BddLat.dualEquivdefMathlib.Order.Category.BddLat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{BddLat}$ and $\mathrm{BddLat}$.
BddLat.ofdefMathlib.Order.Category.BddLat, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is an element of $\mathrm{BddLat}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $x$.
BddLat.ofHomdefMathlib.Order.Category.BddLat, function or constantEnglish
Let $f$ be a bounded lattice homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
latToBddLatdefMathlib.Order.Category.BddLat, function or constantEnglish
$\mathrm{latToBddLat}$ is a functor of $\mathrm{Lat}$ and $\mathrm{BddLat}$.
latToBddLatCompDualIsoDualCompLatToBddLatdefMathlib.Order.Category.BddLat, function or constantEnglish
$\mathrm{latToBddLatCompDualIsoDualCompLatToBddLat}$ is an isomorphism of the composition of $\mathrm{latToBddLat}$ and the dual and the composition of the dual and $\mathrm{latToBddLat}$ defined as $\operatorname{leftAdjointUniq}$ applied to the composition of $\mathrm{latToBddLatForgetAdjunction}$ and the adjunction of the dual equivalence and the composition of the adjunction of the dual equivalence and $\mathrm{latToBddLatForgetAdjunction}$.
latToBddLatForgetAdjunctiondefMathlib.Order.Category.BddLat, function or constantEnglish
$\mathrm{latToBddLatForgetAdjunction}$ is an adjunction of $\mathrm{latToBddLat}$ and the forgetful functor of $\mathrm{BddLat}$ and $\mathrm{Lat}$.
BddOrdstructureMathlib.Order.Category.BddOrd, typeWording
bounded order (from the name)
English
The bounded orders are a basic type.
BddOrd.HomstructureMathlib.Order.Category.BddOrd, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be bounded orders. Then the homomorphisms of $X$ and $Y$ are a basic type.
BddOrd.Hom.homdefMathlib.Order.Category.BddOrd, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a bounded order homomorphism of the set of carriers of $\operatorname{toPartOrd}$ applied to $X$ and the set of carriers of $\operatorname{toPartOrd}$ applied to $Y$ defined as the homomorphism of $f$.
BddOrd.Hom.hom'defMathlib.Order.Category.BddOrd, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a bounded order homomorphism of the set of carriers of $\operatorname{toPartOrd}$ applied to $X$ and the set of carriers of $\operatorname{toPartOrd}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
BddOrd.Iso.mkdefMathlib.Order.Category.BddOrd, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toPartOrd}$ applied to $x$ and the set of carriers of $\operatorname{toPartOrd}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
BddOrd.dualdefMathlib.Order.Category.BddOrd, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of bounded orders and the set of bounded orders.
BddOrd.dualEquivdefMathlib.Order.Category.BddOrd, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of bounded orders and the set of bounded orders.
BddOrd.ofdefMathlib.Order.Category.BddOrd, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is a bounded order defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $X$.
BddOrd.ofHomdefMathlib.Order.Category.BddOrd, function or constantWording
the bounded order of f (from the name)
English
Let $f$ be a bounded order homomorphism of $X$ and $Y$. Then the bounded order of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
BoolAlgstructureMathlib.Order.Category.BoolAlg, typeWording
bool algebra (from the name)
English
The bool algebras are a basic type.
BoolAlg.HomstructureMathlib.Order.Category.BoolAlg, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be bool algebras. Then the homomorphisms of $X$ and $Y$ are a basic type.
BoolAlg.Hom.homdefMathlib.Order.Category.BoolAlg, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a bounded lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
BoolAlg.Hom.hom'defMathlib.Order.Category.BoolAlg, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a bounded lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
BoolAlg.Iso.mkdefMathlib.Order.Category.BoolAlg, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
BoolAlg.carrierdefMathlib.Order.Category.BoolAlg, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a bool algebra. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
BoolAlg.dualdefMathlib.Order.Category.BoolAlg, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of bool algebras and the set of bool algebras.
BoolAlg.dualEquivdefMathlib.Order.Category.BoolAlg, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of bool algebras and the set of bool algebras.
BoolAlg.ofHomdefMathlib.Order.Category.BoolAlg, function or constantWording
the bool algebra of f (from the name)
English
Let $f$ be a bounded lattice homomorphism of $X$ and $Y$. Then the bool algebra of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
BoolAlg.toBddDistLatdefMathlib.Order.Category.BoolAlg, function or constantEnglish
Let $X$ be a bool algebra. Then $\operatorname{toBddDistLat}$ applied to $X$ is an element of $\mathrm{BddDistLat}$ defined as $\operatorname{of}$ applied to the set of carriers of $X$.
typeToBoolAlgOpdefMathlib.Order.Category.BoolAlg, function or constantWording
the type to bool algebra opposite (from the name)
English
The type to bool algebra opposite is a functor of the set of sets and the set of opposites of the set of bool algebras.
CompleteLatstructureMathlib.Order.Category.CompleteLat, typeEnglish
The elements of $\mathrm{CompleteLat}$ are a basic type.
CompleteLat.Iso.mkdefMathlib.Order.Category.CompleteLat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
CompleteLat.carrierdefMathlib.Order.Category.CompleteLat, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{CompleteLat}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
CompleteLat.dualdefMathlib.Order.Category.CompleteLat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{CompleteLat}$ and $\mathrm{CompleteLat}$.
CompleteLat.dualEquivdefMathlib.Order.Category.CompleteLat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{CompleteLat}$ and $\mathrm{CompleteLat}$.
DistLatstructureMathlib.Order.Category.DistLat, typeEnglish
The elements of $\mathrm{DistLat}$ are a basic type.
DistLat.HomstructureMathlib.Order.Category.DistLat, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{DistLat}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
DistLat.Hom.homdefMathlib.Order.Category.DistLat, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
DistLat.Hom.hom'defMathlib.Order.Category.DistLat, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
DistLat.Iso.mkdefMathlib.Order.Category.DistLat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
DistLat.carrierdefMathlib.Order.Category.DistLat, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{DistLat}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
DistLat.dualdefMathlib.Order.Category.DistLat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{DistLat}$ and $\mathrm{DistLat}$.
DistLat.dualEquivdefMathlib.Order.Category.DistLat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{DistLat}$ and $\mathrm{DistLat}$.
DistLat.ofdefMathlib.Order.Category.DistLat, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{DistLat}$ defined as $\operatorname{mk}$ applied to $X$.
DistLat.ofHomdefMathlib.Order.Category.DistLat, function or constantEnglish
Let $f$ be a lattice homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
FinBddDistLatstructureMathlib.Order.Category.FinBddDistLat, typeEnglish
The elements of $\mathrm{FinBddDistLat}$ are a basic type.
FinBddDistLat.HomstructureMathlib.Order.Category.FinBddDistLat, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{FinBddDistLat}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
FinBddDistLat.Hom.homdefMathlib.Order.Category.FinBddDistLat, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $X$ and the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $Y$ defined as the homomorphism of $f$.
FinBddDistLat.Hom.hom'defMathlib.Order.Category.FinBddDistLat, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a bounded lattice homomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $X$ and the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
FinBddDistLat.Iso.mkdefMathlib.Order.Category.FinBddDistLat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $x$ and the set of carriers of $\operatorname{toDistLat}$ applied to $\operatorname{toBddDistLat}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
FinBddDistLat.dualdefMathlib.Order.Category.FinBddDistLat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{FinBddDistLat}$ and $\mathrm{FinBddDistLat}$.
FinBddDistLat.dualEquivdefMathlib.Order.Category.FinBddDistLat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{FinBddDistLat}$ and $\mathrm{FinBddDistLat}$.
FinBddDistLat.ofdefMathlib.Order.Category.FinBddDistLat, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is an element of $\mathrm{FinBddDistLat}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $x$.
FinBddDistLat.of'defMathlib.Order.Category.FinBddDistLat, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of'}$ applied to $x$ is an element of $\mathrm{FinBddDistLat}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $x$.
FinBddDistLat.ofHomdefMathlib.Order.Category.FinBddDistLat, function or constantEnglish
Let $f$ be a bounded lattice homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
FinBoolAlgstructureMathlib.Order.Category.FinBoolAlg, typeWording
finite bool algebra (from the name)
English
The finite bool algebras are a basic type.
FinBoolAlg.Iso.mkdefMathlib.Order.Category.FinBoolAlg, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toBoolAlg}$ applied to $x$ and the set of carriers of $\operatorname{toBoolAlg}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
FinBoolAlg.dualdefMathlib.Order.Category.FinBoolAlg, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of finite bool algebras and the set of finite bool algebras.
FinBoolAlg.dualEquivdefMathlib.Order.Category.FinBoolAlg, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of finite bool algebras and the set of finite bool algebras.
FinBoolAlg.ofdefMathlib.Order.Category.FinBoolAlg, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is a finite bool algebra defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $x$.
fintypeToFinBoolAlgOpdefMathlib.Order.Category.FinBoolAlg, function or constantWording
the finite type to finite bool algebra opposite (from the name)
English
The finite type to finite bool algebra opposite is a functor of the set of finite type categories and the set of opposites of the set of finite bool algebras.
FinPartOrdstructureMathlib.Order.Category.FinPartOrd, typeWording
finite part order (from the name)
English
The finite part orders are a basic type.
FinPartOrd.Iso.mkdefMathlib.Order.Category.FinPartOrd, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toPartOrd}$ applied to $x$ and the set of carriers of $\operatorname{toPartOrd}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
FinPartOrd.dualdefMathlib.Order.Category.FinPartOrd, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of finite part orders and the set of finite part orders.
FinPartOrd.dualEquivdefMathlib.Order.Category.FinPartOrd, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of finite part orders and the set of finite part orders.
FinPartOrd.ofdefMathlib.Order.Category.FinPartOrd, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is a finite part order defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $x$.
FinPartOrd.ofHomdefMathlib.Order.Category.FinPartOrd, function or constantWording
the finite part order of f (from the name)
English
Let $f$ be an order homomorphism of $X$ and $Y$. Then the finite part order of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
FrmstructureMathlib.Order.Category.Frm, typeEnglish
The elements of $\mathrm{Frm}$ are a basic type.
Frm.HomstructureMathlib.Order.Category.Frm, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{Frm}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
Frm.Hom.homdefMathlib.Order.Category.Frm, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a frame homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
Frm.Hom.hom'defMathlib.Order.Category.Frm, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a frame homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Frm.Iso.mkdefMathlib.Order.Category.Frm, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
Frm.carrierdefMathlib.Order.Category.Frm, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{Frm}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
Frm.ofHomdefMathlib.Order.Category.Frm, function or constantEnglish
Let $f$ be a frame homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
HeytAlgstructureMathlib.Order.Category.HeytAlg, typeEnglish
The elements of $\mathrm{HeytAlg}$ are a basic type.
HeytAlg.HomstructureMathlib.Order.Category.HeytAlg, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{HeytAlg}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
HeytAlg.Hom.homdefMathlib.Order.Category.HeytAlg, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an element of $\mathrm{HeytingHom}$ applied to the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
HeytAlg.Hom.hom'defMathlib.Order.Category.HeytAlg, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an element of $\mathrm{HeytingHom}$ applied to the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
HeytAlg.Iso.mkdefMathlib.Order.Category.HeytAlg, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
HeytAlg.carrierdefMathlib.Order.Category.HeytAlg, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{HeytAlg}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
HeytAlg.ofdefMathlib.Order.Category.HeytAlg, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{HeytAlg}$ defined as $\operatorname{mk}$ applied to $X$.
HeytAlg.ofHomdefMathlib.Order.Category.HeytAlg, function or constantEnglish
Let $f$ be an element of $\mathrm{HeytingHom}$ applied to $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
LatstructureMathlib.Order.Category.Lat, typeEnglish
The elements of $\mathrm{Lat}$ are a basic type.
Lat.HomstructureMathlib.Order.Category.Lat, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{Lat}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
Lat.Hom.homdefMathlib.Order.Category.Lat, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is a lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
Lat.Hom.hom'defMathlib.Order.Category.Lat, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is a lattice homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Lat.Iso.mkdefMathlib.Order.Category.Lat, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
Lat.carrierdefMathlib.Order.Category.Lat, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{Lat}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
Lat.dualdefMathlib.Order.Category.Lat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{Lat}$ and $\mathrm{Lat}$.
Lat.dualEquivdefMathlib.Order.Category.Lat, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{Lat}$ and $\mathrm{Lat}$.
Lat.ofdefMathlib.Order.Category.Lat, function or constantEnglish
Let $X$ be a set. Then $\operatorname{of}$ applied to $X$ is an element of $\mathrm{Lat}$ defined as $\operatorname{mk}$ applied to $X$.
Lat.ofHomdefMathlib.Order.Category.Lat, function or constantEnglish
Let $f$ be a lattice homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
LinOrd.HomstructureMathlib.Order.Category.LinOrd, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be linear orders. Then the homomorphisms of $X$ and $Y$ are a basic type.
LinOrd.Hom.homdefMathlib.Order.Category.LinOrd, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
LinOrd.Hom.hom'defMathlib.Order.Category.LinOrd, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
LinOrd.Iso.mkdefMathlib.Order.Category.LinOrd, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
LinOrd.dualdefMathlib.Order.Category.LinOrd, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of linear orders and the set of linear orders.
LinOrd.dualEquivdefMathlib.Order.Category.LinOrd, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of linear orders and the set of linear orders.
LinOrd.ofHomdefMathlib.Order.Category.LinOrd, function or constantWording
the linear order of f (from the name)
English
Let $f$ be an order homomorphism of $X$ and $Y$. Then the linear order of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
Fin.homSuccdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantWording
the homomorphism successor of i (from the name)
English
Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then the homomorphism successor of $i$ is a homomorphism of $\operatorname{castSucc}$ applied to $i$ and $\operatorname{succ}$ applied to $i$ defined as the homomorphism of $\mathrm{Fin\_\_castSucc\_le\_succ}$ applied to $i$.
NonemptyFinLinOrdstructureMathlib.Order.Category.NonemptyFinLinOrd, typeWording
nonempty finite linear order (from the name)
English
The nonempty finite linear orders are a basic type.
NonemptyFinLinOrd.Iso.mkdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $\operatorname{toLinOrd}$ applied to $x$ and the set of carriers of $\operatorname{toLinOrd}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
NonemptyFinLinOrd.dualdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of nonempty finite linear orders and the set of nonempty finite linear orders.
NonemptyFinLinOrd.dualEquivdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of nonempty finite linear orders and the set of nonempty finite linear orders.
NonemptyFinLinOrd.ofdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantEnglish
Let $x$ be a set. Then $\operatorname{of}$ applied to $x$ is a nonempty finite linear order defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $x$.
NonemptyFinLinOrd.ofHomdefMathlib.Order.Category.NonemptyFinLinOrd, function or constantWording
the nonempty finite linear order of f (from the name)
English
Let $f$ be an order homomorphism of $X$ and $Y$. Then the nonempty finite linear order of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
nonemptyFinLinOrdDualCompForgetToFinPartOrddefMathlib.Order.Category.NonemptyFinLinOrd, function or constantWording
the forgetful functor (from the docstring)
English
The forgetful functor is an isomorphism of the composition of the dual and the forgetful functor of the set of nonempty finite linear orders and the set of finite part orders and the composition of the forgetful functor of the set of nonempty finite linear orders and the set of finite part orders and the dual.
ωCPOstructureMathlib.Order.Category.OmegaCompletePartialOrder, typeEnglish
The elements of $\mathrm{\_u3c9\_CPO}$ are a basic type.
ωCPO.HasEqualizers.equalizerdefMathlib.Order.Category.OmegaCompletePartialOrder, function or constantWording
the equalizer of f and g (from the name)
English
Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer of $f$ and $g$ is a fork of $f$ and $g$.
ωCPO.HasEqualizers.equalizerιdefMathlib.Order.Category.OmegaCompletePartialOrder, function or constantWording
the equalizer inclusion function of f and g (from the docstring)
English
Let $f$ and $g$ be continuous homomorphisms of $x$ and $x_{1}$. Then the equalizer inclusion function of $f$ and $g$ is a continuous homomorphism of $\SubtypeSet {a}{(\EqtMACRoH {f (a)}{g (a)})}$ and $x$.
ωCPO.HasEqualizers.isEqualizerdefMathlib.Order.Category.OmegaCompletePartialOrder, function or constantWording
the equalizer fork of f and g (from the docstring)
English
Let $f$ and $g$ be homomorphisms of $X$ and $Y$. Then the equalizer fork of $f$ and $g$ is an element of $\operatorname{IsLimit}$ applied to the equalizer of $f$ and $g$.
ωCPO.HasProducts.isProductdefMathlib.Order.Category.OmegaCompletePartialOrder, function or constantEnglish
Let $J$ be a set. Let $f$ be a function from elements of $J$ to elements of $\mathrm{\_u3c9\_CPO}$. Then $\mathrm{\_u3c9\_CPO\_\_HasProducts\_\_isProduct}$ applied to $J$ and $f$ is an element of $\operatorname{IsLimit}$ applied to the product of $f$.
ωCPO.HasProducts.productdefMathlib.Order.Category.OmegaCompletePartialOrder, function or constantWording
the product of f (from the name)
English
Let $f$ be a function from elements of $J$ to elements of $\mathrm{\_u3c9\_CPO}$. Then the product of $f$ is an element of $\operatorname{Fan}$ applied to $f$.
ωCPO.carrierdefMathlib.Order.Category.OmegaCompletePartialOrder, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{\_u3c9\_CPO}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\mathrm{\_u3c9\_CPO\_\_proj0}$ applied to $\mathrm{self}$.
PartOrdstructureMathlib.Order.Category.PartOrd, typeWording
part order (from the name)
English
The part orders are a basic type.
PartOrd.HomstructureMathlib.Order.Category.PartOrd, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be part orders. Then the homomorphisms of $X$ and $Y$ are a basic type.
PartOrd.Hom.homdefMathlib.Order.Category.PartOrd, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
PartOrd.Hom.hom'defMathlib.Order.Category.PartOrd, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
PartOrd.Iso.mkdefMathlib.Order.Category.PartOrd, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
PartOrd.carrierdefMathlib.Order.Category.PartOrd, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a part order. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
PartOrd.dualdefMathlib.Order.Category.PartOrd, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of part orders and the set of part orders.
PartOrd.dualEquivdefMathlib.Order.Category.PartOrd, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of part orders and the set of part orders.
PartOrd.ofHomdefMathlib.Order.Category.PartOrd, function or constantWording
the part order of f (from the name)
English
Let $f$ be an order homomorphism of $X$ and $Y$. Then the part order of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
PartOrd.uliftFunctordefMathlib.Order.Category.PartOrd, function or constantWording
the lift functor (from the name)
English
The lift functor is a functor of the set of part orders and the set of part orders.
preordToPartOrddefMathlib.Order.Category.PartOrd, function or constantEnglish
$\mathrm{preordToPartOrd}$ is a functor of $\mathrm{Preord}$ and the set of part orders.
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrddefMathlib.Order.Category.PartOrd, function or constantEnglish
$\mathrm{preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd}$ is an isomorphism of the composition of $\mathrm{preordToPartOrd}$ and the dual and the composition of the dual and $\mathrm{preordToPartOrd}$.
preordToPartOrdForgetAdjunctiondefMathlib.Order.Category.PartOrd, function or constantEnglish
$\mathrm{preordToPartOrdForgetAdjunction}$ is an adjunction of $\mathrm{preordToPartOrd}$ and the forgetful functor of the set of part orders and $\mathrm{Preord}$.
PartOrdEmbstructureMathlib.Order.Category.PartOrdEmb, typeWording
part order embedding (from the name)
English
The part order embeddings are a basic type.
PartOrdEmb.HomstructureMathlib.Order.Category.PartOrdEmb, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be part order embeddings. Then the homomorphisms of $X$ and $Y$ are a basic type.
PartOrdEmb.Hom.homdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an order embedding of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
PartOrdEmb.Hom.hom'defMathlib.Order.Category.PartOrdEmb, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an order embedding of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
PartOrdEmb.Iso.mkdefMathlib.Order.Category.PartOrdEmb, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
PartOrdEmb.Limits.CoconePtdefMathlib.Order.Category.PartOrdEmb, typeEnglish
Let $x_{1}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then an element of $\operatorname{CoconePt}$ applied to $x_{1}$ is an element of the function that maps $x_{1}$ to $\operatorname{pt}$ applied to $c$.
PartOrdEmb.Limits.coconedefMathlib.Order.Category.PartOrdEmb, function or constantWording
the colimit cocone of hc (from the docstring)
English
Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then the colimit cocone of $\mathrm{hc}$ is a cocone of $F$.
PartOrdEmb.Limits.isColimitCoconedefMathlib.Order.Category.PartOrdEmb, function or constantEnglish
Let $\mathrm{hc}$ be an element of $\operatorname{IsColimit}$ applied to $c$. Then $\operatorname{isColimitCocone}$ applied to $\mathrm{hc}$ is an element of $\operatorname{IsColimit}$ applied to the colimit cocone of $\mathrm{hc}$.
PartOrdEmb.carrierdefMathlib.Order.Category.PartOrdEmb, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a part order embedding. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
PartOrdEmb.coconeOfPredicateSetdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the cocone of P (from the name)
English
Let $P$ be a function from elements of the power set of the set of carriers of $x$ to propositions. Then the cocone of $P$ is a cocone of the functor of $P$.
PartOrdEmb.dualdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the dual (from the name)
English
The dual is a functor of the set of part order embeddings and the set of part order embeddings.
PartOrdEmb.dualEquivdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of the set of part order embeddings and the set of part order embeddings.
PartOrdEmb.functorOfPredicateSetdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the functor of P (from the name)
English
Let $P$ be a function from elements of the power set of the set of carriers of $x$ to propositions. Then the functor of $P$ is a functor of $\SubtypeSet {x_{1}}{P (x_{1})}$ and the set of part order embeddings.
PartOrdEmb.isColimitOfPredicateSetdefMathlib.Order.Category.PartOrdEmb, function or constantEnglish
Let $P$ be a function from elements of the power set of the set of carriers of $x$ to propositions such that for all carriers $a$ of $x$, there exists an element $J$ of the power set of the set of carriers of $x$, such that $P$ holds for $J$ and $a$ is an element of $J$. Then $\operatorname{isColimitOfPredicateSet}$ applied to $P$ and $\mathrm{hP}$ is an element of $\operatorname{IsColimit}$ applied to the cocone of $P$.
PartOrdEmb.ofHomdefMathlib.Order.Category.PartOrdEmb, function or constantWording
the part order embedding of f (from the name)
English
Let $f$ be an order embedding of $X$ and $Y$. Then the part order embedding of $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
PartOrdEmb.orderIsoEquivIsodefMathlib.Order.Category.PartOrdEmb, function or constantWording
the order isomorphism equivalence isomorphism (from the name)
English
The order isomorphism equivalence isomorphism is an equivalence from the set of isomorphisms of $x$ and $x_{1}$ to the set of order isomorphisms of the set of carriers of $x$ and the set of carriers of $x_{1}$.
PartOrdEmb.orderIsoOfIsodefMathlib.Order.Category.PartOrdEmb, function or constantWording
the order isomorphism corresponding to an isomorphism in e (from the docstring)
English
Let $e$ be an isomorphism of $x$ and $x_{1}$. Then the order isomorphism corresponding to an isomorphism in $e$ is an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$.
PreordstructureMathlib.Order.Category.Preord, typeEnglish
The elements of $\mathrm{Preord}$ are a basic type.
Preord.HomstructureMathlib.Order.Category.Preord, typeWording
homomorphism of X and Y (from the name)
English
Let $X$ and $Y$ be elements of $\mathrm{Preord}$. Then the homomorphisms of $X$ and $Y$ are a basic type.
Preord.Hom.homdefMathlib.Order.Category.Preord, function or constantWording
the homomorphism of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $f$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as the homomorphism of $f$.
Preord.Hom.hom'defMathlib.Order.Category.Preord, function or constantWording
the homomorphism of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $X$ and $Y$. Then the homomorphism of $\mathrm{self}$ is an order homomorphism of the set of carriers of $X$ and the set of carriers of $Y$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Preord.Iso.mkdefMathlib.Order.Category.Preord, function or constantEnglish
Let $e$ be an order isomorphism of the set of carriers of $x$ and the set of carriers of $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
Preord.carrierdefMathlib.Order.Category.Preord, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be an element of $\mathrm{Preord}$. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
Preord.dualdefMathlib.Order.Category.Preord, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{Preord}$ and $\mathrm{Preord}$.
Preord.dualEquivdefMathlib.Order.Category.Preord, function or constantWording
the dual equivalence (from the name)
English
The dual equivalence is an equivalence of $\mathrm{Preord}$ and $\mathrm{Preord}$.
Preord.ofHomdefMathlib.Order.Category.Preord, function or constantEnglish
Let $f$ be an order homomorphism of $X$ and $Y$. Then $\operatorname{ofHom}$ applied to $f$ is a homomorphism of $\operatorname{of}$ applied to $X$ and $\operatorname{of}$ applied to $Y$ defined as the concrete category of $f$.
preordToCatdefMathlib.Order.Category.Preord, function or constantEnglish
$\mathrm{preordToCat}$ is a functor of $\mathrm{Preord}$ and the set of categories.
SemilatInfCatstructureMathlib.Order.Category.Semilat, typeEnglish
The elements of $\mathrm{SemilatInfCat}$ are a basic type.
SemilatInfCat.Iso.mkdefMathlib.Order.Category.Semilat, function or constantEnglish
Let $e$ be an order isomorphism of $\operatorname{X}$ applied to $x$ and $\operatorname{X}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
SemilatInfCat.XdefMathlib.Order.Category.Semilat, typeEnglish
Let $\mathrm{self}$ be an element of $\mathrm{SemilatInfCat}$. Then an element of $\operatorname{X}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
SemilatInfCat.dualdefMathlib.Order.Category.Semilat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{SemilatInfCat}$ and $\mathrm{SemilatSupCat}$.
SemilatSupCatstructureMathlib.Order.Category.Semilat, typeEnglish
The elements of $\mathrm{SemilatSupCat}$ are a basic type.
SemilatSupCat.Iso.mkdefMathlib.Order.Category.Semilat, function or constantEnglish
Let $e$ be an order isomorphism of $\operatorname{X}$ applied to $x$ and $\operatorname{X}$ applied to $x_{1}$. Then $\operatorname{mk}$ applied to $e$ is an isomorphism of $x$ and $x_{1}$.
SemilatSupCat.XdefMathlib.Order.Category.Semilat, typeEnglish
Let $\mathrm{self}$ be an element of $\mathrm{SemilatSupCat}$. Then an element of $\operatorname{X}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
SemilatSupCat.dualdefMathlib.Order.Category.Semilat, function or constantWording
the dual (from the name)
English
The dual is a functor of $\mathrm{SemilatSupCat}$ and $\mathrm{SemilatInfCat}$.
SemilatSupCatEquivSemilatInfCatdefMathlib.Order.Category.Semilat, function or constantEnglish
$\mathrm{SemilatSupCatEquivSemilatInfCat}$ is an equivalence of $\mathrm{SemilatSupCat}$ and $\mathrm{SemilatInfCat}$.
BtwclassMathlib.Order.Circular, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{Btw}$ holds for $x$.
Btw.btwdefMathlib.Order.Circular, predicateEnglish
Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $x$. Then $\operatorname{btw}$ holds for $x_{1}$, $x_{2}$ and $x_{3}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$, $x_{2}$ and $x_{3}$.
CircularOrderclassMathlib.Order.Circular, predicateWording
x is a circular order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a circular order.
CircularPartialOrderclassMathlib.Order.Circular, predicateWording
x is a circular partial order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a circular partial order.
CircularPreorderclassMathlib.Order.Circular, predicateWording
x is a circular preorder (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a circular preorder.
SBtwclassMathlib.Order.Circular, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{SBtw}$ holds for $x$.
SBtw.sbtwdefMathlib.Order.Circular, predicateEnglish
Let $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $x$. Then $\operatorname{sbtw}$ holds for $x_{1}$, $x_{2}$ and $x_{3}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$, $x_{1}$, $x_{2}$ and $x_{3}$.
Set.cIccdefMathlib.Order.Circular, function or constantWording
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 $\operatorname{ofPred}$ applied to the function that maps $x_{2}$ to $\operatorname{btw}$ applied to $a$, $x_{2}$ and $b$.
Set.cIoodefMathlib.Order.Circular, function or constantWording
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 $\operatorname{sbtw}$ applied to $a$, $x_{2}$ and $b$.
ClosureOperatorstructureMathlib.Order.Closure, typeWording
closure operator of x (from the name)
English
Let $x$ be a set. Then the closure operators of $x$ are a basic type.
ClosureOperator.ClosedsdefMathlib.Order.Closure, typeEnglish
Let $c$ be a closure operator of $x$. Then an element of $\operatorname{Closeds}$ applied to $c$ is an element of the function that maps $c$ to $\SubtypeSet {x_{2}}{\operatorname{IsClosed} (c , x_{2})}$.
ClosureOperator.IsCloseddefMathlib.Order.Closure, predicateEnglish
Let $\mathrm{self}$ be a closure operator of $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{IsClosed}$ holds for $\mathrm{self}$ and $x_{2}$, if $\operatorname{proj3}$ holds for $\mathrm{self}$ and $x_{2}$.
ClosureOperator.conjBydefMathlib.Order.Closure, function or constantEnglish
Let $c$ be a closure operator of $x$. Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then $\operatorname{conjBy}$ applied to $c$ and $e$ is a closure operator of $x_{1}$.
ClosureOperator.gidefMathlib.Order.Closure, function or constantEnglish
Let $c$ be a closure operator of $x$. Then $\operatorname{gi}$ applied to $c$ is a Galois insertion of $\operatorname{toCloseds}$ applied to $c$ and the function that maps $x_{2}$ to $\operatorname{IsClosed}$ applied to $c$ and $x_{2}$.
ClosureOperator.iddefMathlib.Order.Closure, function or constantWording
the identity function of x (from the docstring)
English
Let $x$ be a set. Then the identity function of $x$ is a closure operator of $x$.
ClosureOperator.mk'defMathlib.Order.Closure, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$ such that $f$ is monotone, for all elements $x_{3}$ of $x$, $x_{3} \leq f (x_{3})$ and for all elements $x_{2}$ of $x$, $f (f (x_{2}))\leq f (x_{2})$. Then $\operatorname{mk'}$ applied to $f$, $h$, $h_{1}$ and $h_{2}$ is a closure operator of $x$.
ClosureOperator.mkâ‚‚defMathlib.Order.Closure, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x$ such that for all elements $x_{3}$ of $x$, $x_{3} \leq f (x_{3})$ and for all elements $x_{2}$ of $x$, for all elements $y$ of $x$, if $x_{2} \leq f (y)$, then $f (x_{2})\leq f (y)$. Then $\mathrm{ClosureOperator\_\_mk\_u2082\_}$ applied to $f$, $\mathrm{hf}$ and $\mathrm{hmin}$ is a closure operator of $x$.
ClosureOperator.ofCompletePreddefMathlib.Order.Closure, function or constantWording
the closure operator of p and hsinf (from the name)
English
Let $p$ be a function from elements of $x$ to propositions such that for all elements $s$ of $\wp x$, if for all elements $a$ of $x$, if $a$ is an element of $s$, then $p$ holds for $a$, then $p$ holds for the infimum of $s$. Then the closure operator of $p$ and $\mathrm{hsinf}$ is a closure operator of $x$.
ClosureOperator.ofPreddefMathlib.Order.Closure, function or constantWording
the closure operator of f and p (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$. Let $p$ be a function from elements of $x$ to propositions. Assume that for all elements $x_{4}$ of $x$, $x_{4} \leq f (x_{4})$. Assume that for all elements $x_{3}$ of $x$, $p$ holds for $f$ applied to $x_{3}$. Assume that for all elements $x_{2}$ and $y$ of $x$, if $x_{2} \leq y$, then if $p$ holds for $y$, then $f (x_{2})\leq y$. Then the closure operator of $f$ and $p$ is a closure operator of $x$.
ClosureOperator.toClosedsdefMathlib.Order.Closure, function or constantEnglish
Let $c$ be a closure operator of $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{toCloseds}$ applied to $c$ and $x_{2}$ is an element of $\operatorname{Closeds}$ applied to $c$ defined as $c$ applied to $x_{2}$.
GaloisConnection.closureOperatordefMathlib.Order.Closure, function or constantWording
the closure operator of gc (from the name)
English
Assume that $\mathrm{GaloisConnection}$ holds for $l$ and $u$. Then the closure operator of $\mathrm{gc}$ is a closure operator of $x$ defined as the closure operator of the lower adjoint of $\mathrm{gc}$.
GaloisConnection.lowerAdjointdefMathlib.Order.Closure, function or constantWording
the lower adjoint of gc (from the name)
English
Assume that $\mathrm{GaloisConnection}$ holds for $l$ and $u$. Then the lower adjoint of $\mathrm{gc}$ is a lower adjoint of $u$ defined as $\operatorname{mk}$ applied to $l$ and $\mathrm{gc}$.
LowerAdjointstructureMathlib.Order.Closure, typeWording
lower adjoint of u (from the name)
English
Let $u$ be a function from elements of $x_{1}$ to elements of $x$. Then the lower adjoints of $u$ are a basic type.
LowerAdjoint.closeddefMathlib.Order.Closure, function or constantEnglish
Let $l$ be a lower adjoint of $u$. Then $\operatorname{closed}$ applied to $l$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $u$ applied to the lower adjoint of $l$ and $x_{4}$ is equal to $x_{4}$.
LowerAdjoint.closureOperatordefMathlib.Order.Closure, function or constantWording
the closure operator of l (from the name)
English
Let $l$ be a lower adjoint of $u$. Then the closure operator of $l$ is a closure operator of $x$.
LowerAdjoint.iddefMathlib.Order.Closure, function or constantWording
the identity function of x (from the docstring)
English
Let $x$ be a set. Then the identity function of $x$ is a lower adjoint of $\mathrm{id}$ defined as $\operatorname{mk}$ applied to the function that maps $x_{2}$ to $x_{2}$ and $\operatorname{id}$.
LowerAdjoint.toCloseddefMathlib.Order.Closure, function or constantEnglish
Let $l$ be a lower adjoint of $u$. Let $x_{4}$ be an element of $x$. Then $\operatorname{toClosed}$ applied to $l$ and $x_{4}$ is an element of $\operatorname{closed}$ applied to $l$ defined as $u$ applied to the lower adjoint of $l$ and $x_{4}$.
LowerAdjoint.toFundefMathlib.Order.Closure, function or constantWording
the lower adjoint of self and x4 (from the name)
English
Let $\mathrm{self}$ be a lower adjoint of $u$. Let $x_{4}$ be an element of $x$. Then the lower adjoint of $\mathrm{self}$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.
OrderIso.equivClosureOperatordefMathlib.Order.Closure, function or constantWording
the equivalence closure operator of e (from the name)
English
Let $e$ be an order isomorphism of $x$ and $x_{1}$. Then the equivalence closure operator of $e$ is an equivalence from the set of closure operators of $x$ to the set of closure operators of $x_{1}$.
IsCompactElementdefMathlib.Order.CompactlyGenerated.Basic, predicateWording
k is a compact element (from the name)
English
Let $k$ be an element of $x$. Then $k$ is a compact element, if for all elements $s$ of $\wp x$, for all elements $u$ of $x$, if $s$ is nonempty, then if $\mathrm{DirectedOn}$ holds for the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Leq} (x_{3} , x_{4})$ and $s$, then if $\mathrm{IsLUB}$ holds for $s$ and $u$, then if $k \leq u$, then there exists an element $x_{2}$ of $x$, such that $x_{2}$ is an element of $s$ and $k \leq x_{2}$.
IsCompactlyGeneratedclassMathlib.Order.CompactlyGenerated.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{IsCompactlyGenerated}$ holds for $x$.
IsSupClosedCompactdefMathlib.Order.CompactlyGenerated.Basic, predicateWording
x is a supremum closed compact (from the name)
English
Let $x$ be a set. Then $x$ is a supremum closed compact, if for all elements $s$ of $\wp x$, if $s$ is nonempty, then if $\mathrm{SupClosed}$ holds for $s$, then the supremum of $s$ is an element of $s$.
IsSupFiniteCompactdefMathlib.Order.CompactlyGenerated.Basic, predicateWording
x is a supremum finite compact (from the name)
English
Let $x$ be a set. Then $x$ is a supremum finite compact, if for all elements $s$ of $\wp x$, there exists a finite set $t$ of $x$, such that $t \leq s$ and the supremum of $s$ is equal to the supremum of $t$ and $\mathrm{id}$.
IncompReldefMathlib.Order.Comparable, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $b$ be elements of $x$. Then $\mathrm{IncompRel}$ holds for $r$, $a$ and $b$, if it is not the case that $r$ holds for $a$ and $b$ and it is not the case that $r$ holds for $b$ and $a$.
cmpLEdefMathlib.Order.Compare, function or constantEnglish
Let $x_{3}$ and $y$ be elements of $x$. Then $\mathrm{cmpLE}$ applied to $x_{3}$ and $y$ is an element of $\mathrm{Ordering}$ defined as $\iteMACRoG {\mathrm{Leq} (x_{3} , y)}{(\iteMACRoG {\mathrm{Leq} (y , x_{3})}{\operatorname{eq}}{\operatorname{lt}})}{\operatorname{gt}}$.
CompleteAtomicBooleanAlgebraclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a complete atomic boolean algebra (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete atomic boolean algebra.
CompleteBooleanAlgebraclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a complete boolean algebra (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete boolean algebra.
CompleteDistribLatticeclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a complete distributive lattice (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete distributive lattice.
CompleteDistribLattice.MinimalAxiomsstructureMathlib.Order.CompleteBooleanAlgebra, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{MinimalAxioms}$ holds for $x$.
CompletelyDistribLatticeclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a completely distributive lattice (from the name)
English
generation took over the time limit
CompletelyDistribLattice.MinimalAxiomsstructureMathlib.Order.CompleteBooleanAlgebra, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{MinimalAxioms}$ holds for $x$.
Order.CoframeclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a coframe (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a coframe.
Order.Coframe.MinimalAxiomsstructureMathlib.Order.CompleteBooleanAlgebra, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{MinimalAxioms}$ holds for $x$.
Order.FrameclassMathlib.Order.CompleteBooleanAlgebra, predicateWording
x is a frame (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a frame.
Order.Frame.MinimalAxiomsstructureMathlib.Order.CompleteBooleanAlgebra, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{MinimalAxioms}$ holds for $x$.
ChainClosureinductiveMathlib.Order.CompleteLattice.Chain, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\mathrm{ChainClosure}$ holds for $r$ and $x_{1}$.
ChainClosure.belowinductiveMathlib.Order.CompleteLattice.Chain, predicateEnglish
Assume that $\mathrm{ChainClosure}$ holds for $r$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
maxChaindefMathlib.Order.CompleteLattice.Chain, function or constantWording
the maximum chain of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the maximum chain of $r$ is an element of $\wp x$ defined as the union of $\operatorname{ofPred}$ applied to $\mathrm{ChainClosure}$ applied to $r$.
CompleteLatticeclassMathlib.Order.CompleteLattice.Defs, predicateWording
x is a complete lattice (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete lattice.
CompleteLinearOrderclassMathlib.Order.CompleteLattice.Defs, predicateWording
x is a complete linear order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete linear order.
CompleteSemilatticeInfclassMathlib.Order.CompleteLattice.Defs, predicateWording
x is a complete semilattice infimum (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete semilattice infimum.
CompleteSemilatticeSupclassMathlib.Order.CompleteLattice.Defs, predicateWording
x is a complete semilattice supremum (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete semilattice supremum.
CompleteLattice.MulticoequalizerDiagramstructureMathlib.Order.CompleteLattice.MulticoequalizerDiagram, predicateEnglish
Let $x_{2}$ be an element of $T$. Let $u$ and $v$ be functions from elements of $x_{1}$ to elements of $T$. Then we can say that $\operatorname{MulticoequalizerDiagram}$ holds for $x_{2}$, $u$ and $v$.
CompleteLattice.MulticoequalizerDiagram.multicoforkdefMathlib.Order.CompleteLattice.MulticoequalizerDiagram, function or constantWording
the multicofork of d (from the name)
English
Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $x_{2}$, $u$ and $v$. Then the multicofork of $d$ is a multicofork of the multispan index of $d$.
CompleteLattice.MulticoequalizerDiagram.multispanIndexdefMathlib.Order.CompleteLattice.MulticoequalizerDiagram, function or constantWording
the multispan index of d (from the name)
English
Assume that $\operatorname{MulticoequalizerDiagram}$ holds for $x_{2}$, $u$ and $v$. Then the multispan index of $d$ is a multispan index of the product of $x_{1}$ and $T$.
Lattice.BicartSqstructureMathlib.Order.CompleteLattice.MulticoequalizerDiagram, predicateEnglish
Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be elements of $T$. Then we can say that $\operatorname{BicartSq}$ holds for $x$, $x_{1}$, $x_{2}$ and $x_{3}$.
CompletePartialOrderclassMathlib.Order.CompletePartialOrder, predicateWording
x is a complete partial order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a complete partial order.
CompleteLatticeHom.rangedefMathlib.Order.CompleteSublattice, function or constantWording
the range of f (from the docstring)
English
Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$. Then the range of $f$ is a complete sublattice of $x_{1}$.
CompleteLatticeHom.toOrderIsoRangeOfInjectivedefMathlib.Order.CompleteSublattice, function or constantWording
the order isomorphism range of f and hf (from the name)
English
Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the order isomorphism range of $f$ and $\mathrm{hf}$ is an order isomorphism of $x$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{4}})}$ defined as the order isomorphism.
CompleteSublatticestructureMathlib.Order.CompleteSublattice, typeWording
complete sublattice of x (from the name)
English
Let $x$ be a set. Then the complete sublattices of $x$ are a basic type.
CompleteSublattice.comapdefMathlib.Order.CompleteSublattice, function or constantWording
the preimage of f and L (from the name)
English
Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a complete sublattice of $x_{1}$. Then the preimage of $f$ and $L$ is a complete sublattice of $x$.
CompleteSublattice.copydefMathlib.Order.CompleteSublattice, function or constantWording
the copy of L and s (from the name)
English
Let $L$ be a complete sublattice of $x$. Let $s$ be an element of $\wp x$ such that $\EqtMACRoH {s}{L}$. Then the copy of $L$ and $s$ is a complete sublattice of $x$.
CompleteSublattice.mapdefMathlib.Order.CompleteSublattice, function or constantWording
the map of f and L (from the name)
English
Let $f$ be a complete lattice homomorphism of $x$ and $x_{1}$. Let $L$ be a complete sublattice of $x$. Then the map of $f$ and $L$ is a complete sublattice of $x_{1}$.
CompleteSublattice.mk'defMathlib.Order.CompleteSublattice, function or constantEnglish
Let $\mathrm{carrier}$ be an element of $\wp x$ such that for all elements $s_{1}$ of $\wp x$, if $s_{1} \leq \mathrm{carrier}$, then the supremum of $s_{1}$ is an element of $\mathrm{carrier}$ and for all elements $s$ of $\wp x$, if $s \leq \mathrm{carrier}$, then the infimum of $s$ is an element of $\mathrm{carrier}$. Then $\operatorname{mk'}$ applied to $\mathrm{carrier}$, $\mathrm{sSupClosed'}$ and $\mathrm{sInfClosed'}$ is a complete sublattice of $x$.
CompleteSublattice.subtypedefMathlib.Order.CompleteSublattice, function or constantWording
the subtype of L (from the name)
English
Let $L$ be a complete sublattice of $x$. Then the subtype of $L$ is a complete lattice homomorphism of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$ and $x$.
DedekindCutdefMathlib.Order.Completion, typeWording
Dedekind cut of x (from the name)
English
Let $x$ be a set. Then a Dedekind cut of $x$ is an element of the function that maps $x$ to the set of concepts of $x$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Leq} (x_{2} , x_{3})$.
DedekindCut.factorEmbeddingdefMathlib.Order.Completion, function or constantWording
the factor embedding of f (from the name)
English
Let $f$ be an order embedding of $x_{1}$ and $x$. Then the factor embedding of $f$ is an order embedding of the set of Dedekind cuts of $x_{1}$ and $x$.
DedekindCut.leftdefMathlib.Order.Completion, function or constantWording
the left set of A (from the docstring)
English
Let $A$ be a Dedekind cut of $x$. Then the left set of $A$ is an element of $\wp x$ defined as the extent of $A$.
DedekindCut.principaldefMathlib.Order.Completion, function or constantEnglish
Let $a$ be an element of $x$. Then $\operatorname{principal}$ applied to $a$ is a Dedekind cut of $x$.
DedekindCut.principalEmbeddingdefMathlib.Order.Completion, function or constantWording
the principal embedding (from the name)
English
The principal embedding is an order embedding of $x$ and the set of Dedekind cuts of $x$.
DedekindCut.principalIsodefMathlib.Order.Completion, function or constantWording
the principal isomorphism (from the name)
English
The principal isomorphism is an order isomorphism of $x$ and the set of Dedekind cuts of $x$.
DedekindCut.rightdefMathlib.Order.Completion, function or constantWording
the right set of A (from the docstring)
English
Let $A$ be a Dedekind cut of $x$. Then the right set of $A$ is an element of $\wp x$ defined as $\operatorname{intent}$ applied to $A$.
ConceptstructureMathlib.Order.Concept, typeWording
concept of x1 and r (from the name)
English
Let $x$ and $x_{1}$ be sets. Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then the concepts of $x_{1}$ and $r$ are a basic type.
Concept.copydefMathlib.Order.Concept, function or constantWording
the copy of e and i (from the name)
English
Let $c$ be a concept of $x_{1}$ and $r$. Let $e$ be an element of $\wp x$. Let $i$ be an element of $\wp x_{1}$. Assume that $e$ is equal to the extent of $c$. Assume that $\EqtMACRoH {i}{\operatorname{intent} (c)}$. Then the copy of $e$ and $i$ is a concept of $x_{1}$ and $r$.
Concept.extentdefMathlib.Order.Concept, function or constantWording
the extent of self (from the docstring)
English
Let $\mathrm{self}$ be a concept of $x_{1}$ and $r$. Then the extent of $\mathrm{self}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Concept.intentdefMathlib.Order.Concept, function or constantEnglish
Let $\mathrm{self}$ be a concept of $x_{1}$ and $r$. Then $\operatorname{intent}$ applied to $\mathrm{self}$ is an element of $\wp x_{1}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Concept.ofAttributedefMathlib.Order.Concept, function or constantWording
the concept of r and b (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $b$ be an element of $x_{1}$. Then the concept of $r$ and $b$ is a concept of $x_{1}$ and $r$ defined as the concept of $r$ and $\operatorname{singleton}$ applied to $b$.
Concept.ofAttributesdefMathlib.Order.Concept, function or constantWording
the concept of r and t (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $t$ be an element of $\wp x_{1}$. Then the concept of $r$ and $t$ is a concept of $x_{1}$ and $r$ defined as the concept of $r$ and $\mathrm{lowerPolar}$ applied to $r$ and $t$.
Concept.ofIsExtentdefMathlib.Order.Concept, function or constantWording
the concept of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$ such that $\operatorname{IsExtent}$ holds for $r$ and $s$. Then the concept of $r$ and $s$ is a concept of $x_{1}$ and $r$.
Concept.ofIsIntentdefMathlib.Order.Concept, function or constantWording
the concept of r and t (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $t$ be an element of $\wp x_{1}$ such that $\operatorname{IsIntent}$ holds for $r$ and $t$. Then the concept of $r$ and $t$ is a concept of $x_{1}$ and $r$.
Concept.ofObjectdefMathlib.Order.Concept, function or constantWording
the concept generated by a single object of r and a (from the docstring)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $a$ be an element of $x$. Then the concept generated by a single object of $r$ and $a$ is a concept of $x_{1}$ and $r$ defined as the concept of $r$ and $\operatorname{singleton}$ applied to $a$.
Concept.ofObjectsdefMathlib.Order.Concept, function or constantWording
the concept of r and s (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$. Then the concept of $r$ and $s$ is a concept of $x_{1}$ and $r$ defined as the concept of $r$ and $\mathrm{upperPolar}$ applied to $r$ and $s$.
Concept.swapdefMathlib.Order.Concept, function or constantWording
the swap of c (from the name)
English
Let $c$ be a concept of $x_{1}$ and $r$. Then the swap of $c$ is a concept of $x$ and $\operatorname{swap}$ defined as $\operatorname{mk}$ applied to $\operatorname{intent}$ applied to $c$, the extent of $c$, $\mathrm{Concept\_\_lowerPolar\_intent}$ applied to $c$ and $\mathrm{Concept\_\_upperPolar\_extent}$ applied to $c$.
Concept.swapEquivdefMathlib.Order.Concept, function or constantWording
the swap equivalence (from the name)
English
The swap equivalence is an order isomorphism of the set of order duals of the set of concepts of $x_{1}$ and $r$ and the set of concepts of $x$ and $\operatorname{swap}$.
Order.IsExtentdefMathlib.Order.Concept, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$. Then $\operatorname{IsExtent}$ holds for $r$ and $s$, if $s$ is an element of the range of $\mathrm{lowerPolar}$ applied to $r$.
Order.IsIntentdefMathlib.Order.Concept, predicateEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{IsIntent}$ holds for $r$ and $t$, if $t$ is an element of the range of $\mathrm{upperPolar}$ applied to $r$.
extentClosuredefMathlib.Order.Concept, function or constantWording
the extent closure of r (from the name)
English
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then the extent closure of $r$ is a closure operator of $\wp x$ defined as the closure operator of $\mathrm{gc\_upperPolar\_lowerPolar}$ applied to $r$.
intentClosuredefMathlib.Order.Concept, function or constantEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Then $\mathrm{intentClosure}$ applied to $r$ is a closure operator of $\wp x_{1}$ defined as the closure operator of $\mathrm{gc\_lowerPolar\_upperPolar}$ applied to $r$.
lowerPolardefMathlib.Order.Concept, function or constantEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $t$ be an element of $\wp x_{1}$. Then $\mathrm{lowerPolar}$ applied to $r$ and $t$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that for all elements $b$ of $x_{1}$, if $b$ is an element of $t$, then $r$ holds for $a$ and $b$.
upperPolardefMathlib.Order.Concept, function or constantEnglish
Let $r$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be an element of $\wp x$. Then $\mathrm{upperPolar}$ applied to $r$ and $s$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that for all elements $a$ of $x$, if $a$ is an element of $s$, then $r$ holds for $a$ and $b$.
ConditionallyCompleteLatticeclassMathlib.Order.ConditionallyCompleteLattice.Defs, predicateWording
x is a conditionally complete lattice (from the name)
English
generation took over the time limit
ConditionallyCompleteLinearOrderclassMathlib.Order.ConditionallyCompleteLattice.Defs, predicateWording
x is a conditionally complete linear order (from the name)
English
generation took over the time limit
ConditionallyCompleteLinearOrderBotclassMathlib.Order.ConditionallyCompleteLattice.Defs, predicateWording
x is a conditionally complete linear order bottom (from the name)
English
generation took over the time limit
ConditionallyCompletePartialOrderclassMathlib.Order.ConditionallyCompletePartialOrder.Defs, predicateWording
x is a conditionally complete partial order (from the name)
English
generation took over the time limit
ConditionallyCompletePartialOrderInfclassMathlib.Order.ConditionallyCompletePartialOrder.Defs, predicateWording
x is a conditionally complete partial order infimum (from the name)
English
generation took over the time limit
ConditionallyCompletePartialOrderSupclassMathlib.Order.ConditionallyCompletePartialOrder.Defs, predicateWording
x is a conditionally complete partial order supremum (from the name)
English
generation took over the time limit
Order.PartialIsodefMathlib.Order.CountableDenseLinearOrder, typeWording
partial isomorphism of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then a partial isomorphism of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to $\SubtypeSet {f}{\mathrm{forall} (\mathrm{Prod} (x , x_{1}), \lambda p . \mathrm{if} (\MembershipmemMACRoT {f}{p}, \mathrm{forall} (\mathrm{Prod} (x , x_{1}), \lambda q . \mathrm{if} (\MembershipmemMACRoT {f}{q}, \EqtMACRoH {\mathrm{cmp} (\ProdfstMACRoZ {p}, \ProdfstMACRoZ {q})}{\mathrm{cmp} (\ProdsndMACRoAA {p}, \ProdsndMACRoAA {q})}))))}$.
Order.PartialIso.commdefMathlib.Order.CountableDenseLinearOrder, function or constantEnglish
Let $x_{4}$ be a partial isomorphism of $x$ and $x_{1}$. Then $\operatorname{comm}$ applied to $x_{4}$ is a partial isomorphism of $x_{1}$ and $x$.
Order.PartialIso.definedAtLeftdefMathlib.Order.CountableDenseLinearOrder, function or constantEnglish
Let $x_{1}$ be a set. Let $a$ be an element of $x$. Then $\operatorname{definedAtLeft}$ applied to $x_{1}$ and $a$ is an element of $\operatorname{Cofinal}$ applied to the set of partial isomorphisms of $x$ and $x_{1}$.
Order.PartialIso.definedAtRightdefMathlib.Order.CountableDenseLinearOrder, function or constantEnglish
Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then $\operatorname{definedAtRight}$ applied to $x$ and $b$ is an element of $\operatorname{Cofinal}$ applied to the set of partial isomorphisms of $x$ and $x_{1}$.
Order.PartialIso.funOfIdealdefMathlib.Order.CountableDenseLinearOrder, function or constantWording
the function of a and I (from the name)
English
Let $a$ be an element of $x$. Let $I$ be an ideal of the set of partial isomorphisms of $x$ and $x_{1}$ such that there exists a partial isomorphism $f_{1}$ of $x$ and $x_{1}$, such that $\MembershipmemMACRoT {\operatorname{definedAtLeft} (x_{1} , a)}{f_{1}}$ and $\MembershipmemMACRoT {I}{f_{1}}$. Then the function of $a$ and $I$ is an element of $\SubtypeSet {b}{\mathrm{exists} (\operatorname{PartialIso} (x , x_{1}), \lambda f . \mathrm{and} (\MembershipmemMACRoT {I}{f}, \MembershipmemMACRoT {f}{(\ProdmkMACRoU {a}{b})}))}$.
Order.PartialIso.invOfIdealdefMathlib.Order.CountableDenseLinearOrder, function or constantWording
the inverse of b and I (from the name)
English
Let $b$ be an element of $x_{1}$. Let $I$ be an ideal of the set of partial isomorphisms of $x$ and $x_{1}$ such that there exists a partial isomorphism $f_{1}$ of $x$ and $x_{1}$, such that $\MembershipmemMACRoT {\operatorname{definedAtRight} (x , b)}{f_{1}}$ and $\MembershipmemMACRoT {I}{f_{1}}$. Then the inverse of $b$ and $I$ is an element of $\SubtypeSet {a}{\mathrm{exists} (\operatorname{PartialIso} (x , x_{1}), \lambda f . \mathrm{and} (\MembershipmemMACRoT {I}{f}, \MembershipmemMACRoT {f}{(\ProdmkMACRoU {a}{b})}))}$.
CountableInfClosedstructureMathlib.Order.CountableSupClosed, predicateEnglish
Let $s$ be an element of $\wp x$. Then we can say that $\mathrm{CountableInfClosed}$ holds for $s$.
CountableSupClosedstructureMathlib.Order.CountableSupClosed, predicateEnglish
Let $s$ be an element of $\wp x$. Then we can say that $\mathrm{CountableSupClosed}$ holds for $s$.
countableInfClosuredefMathlib.Order.CountableSupClosed, function or constantWording
the countable infimum closure (from the name)
English
The countable infimum closure is a closure operator of $\wp x$.
countableSupClosuredefMathlib.Order.CountableSupClosed, function or constantWording
the countable supremum closure (from the name)
English
The countable supremum closure is a closure operator of $\wp x$.
DistribLatticeclassMathlib.Order.Defs.Lattice, predicateWording
x is a distributive lattice (by hand)
English
Let $x$ be a set. Then we can say that $x$ is a distributive lattice.
LatticeclassMathlib.Order.Defs.Lattice, predicateWording
x is a lattice (by hand)
English
Let $x$ be a set. Then we can say that $x$ is a lattice.
Lattice.infdefMathlib.Order.Defs.Lattice, function or constantWording
the infimum of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the infimum of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
SemilatticeInfclassMathlib.Order.Defs.Lattice, predicateWording
x is a meet semilattice (by hand)
English
Let $x$ be a set. Then we can say that $x$ is a meet semilattice.
SemilatticeInf.infdefMathlib.Order.Defs.Lattice, function or constantWording
the infimum of x1 and x2 (by hand)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the infimum of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
SemilatticeSupclassMathlib.Order.Defs.Lattice, predicateWording
x is a join semilattice (by hand)
English
Let $x$ be a set. Then we can say that $x$ is a join semilattice.
SemilatticeSup.supdefMathlib.Order.Defs.Lattice, function or constantWording
the supremum of x1 and x2 (by hand)
English
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then the supremum of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{1}$ and $x_{2}$.
LinOrdstructureMathlib.Order.Defs.LinearOrder, typeWording
linear order (from the name)
English
The linear orders are a basic type.
LinOrd.carrierdefMathlib.Order.Defs.LinearOrder, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a linear order. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
LinearOrderclassMathlib.Order.Defs.LinearOrder, predicateWording
x is linearly ordered (by hand)
English
Let $x$ be a set. Then we can say that $x$ is linearly ordered.
maxDefaultdefMathlib.Order.Defs.LinearOrder, function or constantWording
the maximum default of a and b (from the name)
English
Let $a$ and $b$ be elements of $x$. Then the maximum default of $a$ and $b$ is an element of $x$ defined as $\iteMACRoG {\mathrm{Leq} (a , b)}{b}{a}$.
minDefaultdefMathlib.Order.Defs.LinearOrder, function or constantWording
the minimum default of a and b (from the name)
English
Let $a$ and $b$ be elements of $x$. Then the minimum default of $a$ and $b$ is an element of $x$ defined as $\iteMACRoG {\mathrm{Leq} (a , b)}{a}{b}$.
tacticCompareOfLessAndEq_rfldefMathlib.Order.Defs.LinearOrder, function or constantEnglish
generation took over the time limit
CovBydefMathlib.Order.Defs.PartialOrder, predicateEnglish
Let $a$ and $b$ be elements of $x$. Then $\mathrm{CovBy}$ holds for $a$ and $b$, if $a < b$ and for all elements $c$ of $x$, if $a < c$, then $c$ is not less than $b$.
PartialOrderclassMathlib.Order.Defs.PartialOrder, predicateWording
x is partially ordered (by hand)
English
Let $x$ be a set. Then we can say that $x$ is partially ordered.
PreorderclassMathlib.Order.Defs.PartialOrder, predicateWording
x is preordered (by hand)
English
Let $x$ be a set. Then we can say that $x$ is preordered.
WCovBydefMathlib.Order.Defs.PartialOrder, predicateEnglish
Let $a$ and $b$ be elements of $x$. Then $\mathrm{WCovBy}$ holds for $a$ and $b$, if $a \leq b$ and for all elements $c$ of $x$, if $a < c$, then $c$ is not less than $b$.