Cardinal.alephdefMathlib.SetTheory.Cardinal.Aleph, function or constantEnglish
$\operatorname{aleph}$ is an order embedding of the set of ordinals and the set of cardinals defined as the composition of $\operatorname{addLeft}$ applied to the omega and the relation embedding of $\operatorname{preAleph}$.
Cardinal.bethdefMathlib.SetTheory.Cardinal.Aleph, function or constantEnglish
Let $o$ be an ordinal. Then $\operatorname{beth}$ applied to $o$ is a cardinal defined as $\operatorname{preBeth}$ applied to the sum of the omega and $o$.
Cardinal.preAlephdefMathlib.SetTheory.Cardinal.Aleph, function or constantEnglish
$\operatorname{preAleph}$ is an order isomorphism of the set of ordinals and the set of cardinals defined as the composition of $\operatorname{enum}$ applied to $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that $x$ is initial and $\mathrm{Ordinal\_\_isCofinal\_setOfPred\_isInitial}$ and $\operatorname{isInitialIso}$.
Cardinal.preBethdefMathlib.SetTheory.Cardinal.Aleph, function or constantEnglish
Let $o$ be an ordinal. Then $\operatorname{preBeth}$ applied to $o$ is a cardinal.
Ordinal.IsInitialdefMathlib.SetTheory.Cardinal.Aleph, predicateWording
o is initial (from the name)
English
Let $o$ be an ordinal. Then $o$ is initial, if the order of the cardinal of $o$ is equal to $o$.
Ordinal.isInitialIsodefMathlib.SetTheory.Cardinal.Aleph, function or constantEnglish
$\operatorname{isInitialIso}$ is an order isomorphism of $\SubtypeSet {x}{\operatorname{IsInitial} (x)}$ and the set of cardinals.
Ordinal.omegadefMathlib.SetTheory.Cardinal.Aleph, function or constantWording
the omega (from the name)
English
The omega is an order embedding of the set of ordinals and the set of ordinals defined as the composition of $\operatorname{addLeft}$ applied to the omega and the omega.
Ordinal.preOmegadefMathlib.SetTheory.Cardinal.Aleph, function or constantWording
the omega (from the name)
English
The omega is an order embedding of the set of ordinals and the set of ordinals.
Cardinal.powerltdefMathlib.SetTheory.Cardinal.Basic, function or constantEnglish
Let $a$ and $b$ be cardinals. Then $\operatorname{powerlt}$ applied to $a$ and $b$ is a cardinal defined as the supremum of the function that maps $c$ to $a ^ {c}$.
Order.cofdefMathlib.SetTheory.Cardinal.Cofinality.Basic, function or constantWording
the cofinality of x (from the docstring)
English
Let $x$ be a set. Then the cofinality of $x$ is a cardinal defined as the infimum of the function that maps $s$ to $\operatorname{mk}$ applied to the set of elements of $s$.
IsClubstructureMathlib.SetTheory.Cardinal.Cofinality.Club, predicateWording
s is a club (from the name)
English
Let $s$ be an element of $\wp x$. Then we can say that $s$ is a club.
IsStationarydefMathlib.SetTheory.Cardinal.Cofinality.Club, predicateWording
s is stationary (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is stationary, if for all elements $t$ of $\wp x$, if $t$ is a club, then $\operatorname{inter}$ applied to $s$ and $t$ is nonempty.
IsRegularCardinalOrderclassMathlib.SetTheory.Cardinal.Cofinality.Enum, predicateWording
x is a regular cardinal order (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a regular cardinal order.
Order.enumdefMathlib.SetTheory.Cardinal.Cofinality.Enum, function or constantEnglish
Let $s$ be a cofinal element of $\wp x$. Then $\operatorname{enum}$ applied to $s$ and $\mathrm{hs}$ is an order isomorphism of $x$ and the set of elements of $s$.
Ordinal.cofdefMathlib.SetTheory.Cardinal.Cofinality.Ordinal, function or constantWording
the cofinality of o (from the docstring)
English
Let $o$ be an ordinal. Then the cofinality of $o$ is a cardinal.
Cardinal.continuumdefMathlib.SetTheory.Cardinal.Continuum, function or constantWording
the continuum (from the name)
English
The continuum is a cardinal defined as $2 ^ {\operatorname{aleph0}}$.
CardinaldefMathlib.SetTheory.Cardinal.Defs, typeWording
cardinal (from the name)
English
A cardinal is an element of $\mathrm{Quotient}$ applied to $\operatorname{isEquivalent}$.
Cardinal.aleph0defMathlib.SetTheory.Cardinal.Defs, function or constantEnglish
$\operatorname{aleph0}$ is a cardinal defined as the lift of $\operatorname{mk}$ applied to $\Natural$.
Cardinal.liftdefMathlib.SetTheory.Cardinal.Defs, function or constantWording
the lift of c (from the name)
English
Let $c$ be a cardinal. Then the lift of $c$ is a cardinal defined as the map of the function that maps $x$, $x_{1}$ and $e$ to the composition of the lift and the composition of $e$ and the inverse of the lift and $c$.
Cardinal.mapdefMathlib.SetTheory.Cardinal.Defs, function or constantWording
the map of hf and x1 (from the name)
English
Let $f$ be a function from sets to sets. Let $\mathrm{hf}$ be a function from sets $x_{1}$ and sets $x_{2}$ and equivalences from $x_{1}$ to $x_{2}$ to elements of $\EquivMACRoAE {f (x_{1})}{f (x_{2})}$. Let $x$ be a cardinal. Then the map of $x_{1}$ and $x_{2}$ is a cardinal.
Cardinal.map₂defMathlib.SetTheory.Cardinal.Defs, function or constantWording
the map of x2 and x3 (from the name)
English
Let $f$ be a function from sets and sets to sets. Let $\mathrm{hf}$ be a function from sets $x_{2}$ and sets $x_{3}$ and sets $x_{4}$ and sets $x_{5}$ and equivalences from $x_{2}$ to $x_{3}$ and equivalences from $x_{4}$ to $x_{5}$ to elements of $\EquivMACRoAE {f (x_{2} , x_{4})}{f (x_{3} , x_{5})}$. Let $x$ and $x_{1}$ be cardinals. Then the map of $x_{3}$ and $x_{4}$ is a cardinal.
Cardinal.mkdefMathlib.SetTheory.Cardinal.Defs, function or constantEnglish
Let $x$ be a set. Then $\operatorname{mk}$ applied to $x$ is a cardinal defined as $\operatorname{mk'}$ applied to $x$.
Cardinal.outMkEquivdefMathlib.SetTheory.Cardinal.Defs, function or constantWording
the representative of the cardinal (from the docstring)
English
The representative of the cardinal is an element of $\EquivMACRoAE {\operatorname{out} (\operatorname{mk} (x))}{x}$.
Cardinal.proddefMathlib.SetTheory.Cardinal.Defs, function or constantWording
the product of f (from the name)
English
Let $f$ be a function from elements of $x$ to cardinals. Then the product of $f$ is a cardinal defined as $\operatorname{mk}$ applied to the set of functions from elements $i$ of $x$ to elements of $\operatorname{out}$ applied to $f$ applied to $i$.
Cardinal.sumdefMathlib.SetTheory.Cardinal.Defs, function or constantWording
the sum of f (from the name)
English
Let $f$ be a function from elements of $x$ to cardinals. Then the sum of $f$ is a cardinal defined as $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $i$ to $\operatorname{out}$ applied to $f$ applied to $i$.
Cardinal.gciENatdefMathlib.SetTheory.Cardinal.ENat, function or constantEnglish
$\operatorname{gciENat}$ is a Galois coinsertion of $\operatorname{ofENat}$ and $\operatorname{coe}$ applied to the natural number.
Cardinal.ofENatdefMathlib.SetTheory.Cardinal.ENat, function or constantWording
the cardinal of x (from the name)
English
Let $x$ be a natural number. Then the cardinal of $x$ is a cardinal.
Cardinal.ofENatHomdefMathlib.SetTheory.Cardinal.ENat, function or constantWording
the cardinal (from the name)
English
The cardinal is an order ring homomorphism of the set of natural numbers and the set of cardinals defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{ofENat}$ and $\mathrm{Cardinal\_\_ofENat\_one}$ and $\mathrm{Cardinal\_\_ofENat\_mul}$, $\mathrm{Cardinal\_\_ofENat\_zero}$ and $\mathrm{Cardinal\_\_ofENat\_add}$ and $\mathrm{Cardinal\_\_ofENat\_mono}$.
Cardinal.toENatdefMathlib.SetTheory.Cardinal.ENat, function or constantWording
the natural number (from the name)
English
The natural number is an order ring homomorphism of the set of cardinals and the set of natural numbers.
ENat.carddefMathlib.SetTheory.Cardinal.Finite, function or constantWording
the cardinality of x (from the docstring)
English
Let $x$ be a set. Then the cardinality of $x$ is a natural number defined as $\operatorname{toENat}$ applied to $\operatorname{mk}$ applied to $x$.
Nat.carddefMathlib.SetTheory.Cardinal.Finite, function or constantWording
the cardinality of x (from the docstring)
English
Let $x$ be a set. Then the cardinality of $x$ is a natural number defined as $\operatorname{toNat}$ applied to $\operatorname{mk}$ applied to $x$.
Nat.equivFinOfCardPosdefMathlib.SetTheory.Cardinal.Finite, function or constantEnglish
Assume that the cardinality of $x$ is distinct from $0$. Then $\operatorname{equivFinOfCardPos}$ applied to $h$ is an equivalence from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$.
HasCardinalLTdefMathlib.SetTheory.Cardinal.HasCardinalLT, predicateEnglish
Let $X$ be a set. Let $x$ be a cardinal. Then $\mathrm{HasCardinalLT}$ holds for $X$ and $x$, if the lift of $\operatorname{mk}$ applied to $X$ is less than the lift of $x$.
Finite.equivFindefMathlib.SetTheory.Cardinal.NatCard, function or constantEnglish
Let $x$ be a set. Then $\operatorname{equivFin}$ applied to $x$ is an equivalence from $x$ to $\mathrm{Fin}$ applied to the cardinality of $x$.
Finite.equivFinOfCardEqdefMathlib.SetTheory.Cardinal.NatCard, function or constantEnglish
Assume that the cardinality of $x$ is equal to $n$. Then $\operatorname{equivFinOfCardEq}$ applied to $h_{1}$ is an element of $\EquivMACRoAE {x}{\mathrm{Fin} (n)}$ defined as $\operatorname{ndrec}$ applied to $\operatorname{equivFin}$ applied to $x$ and $h_{1}$.
Cardinal.IsStrongLimitstructureMathlib.SetTheory.Cardinal.Order, predicateWording
c is a strong limit (from the docstring)
English
Let $c$ be a cardinal. Then we can say that $c$ is a strong limit.
Cardinal.IsStrongPrelimitdefMathlib.SetTheory.Cardinal.Order, predicateEnglish
Let $c$ be a cardinal. Then $\operatorname{IsStrongPrelimit}$ holds for $c$, if for all cardinals $x$, if $x < c$, then $2 ^ {x}< c$.
Cardinal.liftInitialSegdefMathlib.SetTheory.Cardinal.Order, function or constantEnglish
$\operatorname{liftInitialSeg}$ is an element of $\mathrm{InitialSeg}$ applied to the function that maps $x$ and $x_{1}$ to $\mathrm{Lt} (x , x_{1})$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$.
WellOrderingReldefMathlib.SetTheory.Cardinal.Order, predicateEnglish
Let $x_{1}$ and $x_{2}$ be elements of $x$. Then $\mathrm{WellOrderingRel}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{Preimage}$ holds for $\operatorname{coe}$ applied to the embedding to cardinal, the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$, $x_{1}$ and $x_{2}$.
embeddingToCardinaldefMathlib.SetTheory.Cardinal.Order, function or constantWording
the embedding to cardinal (from the name)
English
The embedding to cardinal is an embedding of $x$ and the set of cardinals defined as $\operatorname{choice}$ applied to $\mathrm{nonempty\_embedding\_to\_cardinal}$.
Cardinal.IsInaccessiblestructureMathlib.SetTheory.Cardinal.Regular, predicateWording
c is inaccessible (from the docstring)
English
Let $c$ be a cardinal. Then we can say that $c$ is inaccessible.
Cardinal.IsRegularstructureMathlib.SetTheory.Cardinal.Regular, predicateWording
c is regular (from the docstring)
English
Let $c$ be a cardinal. Then we can say that $c$ is regular.
Cardinal.IsSingularstructureMathlib.SetTheory.Cardinal.Regular, predicateWording
c is singular (from the docstring)
English
Let $c$ be a cardinal. Then we can say that $c$ is singular.
Cardinal.toNatdefMathlib.SetTheory.Cardinal.ToNat, function or constantWording
the natural number (from the name)
English
The natural number is a monoid with zero homomorphism of the set of cardinals and $\Natural$ defined as the composition of the natural homomorphism and the monoid with zero homomorphism of the ring homomorphism of the natural number.
Descriptive.Tree.dropdefMathlib.SetTheory.Descriptive.Tree, function or constantEnglish
Let $T$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{tree} (A)}{x_{3}})}$. Let $n$ be an element of $\Natural$. Let $x$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$. Then $\operatorname{drop}$ applied to $T$, $n$ and $x$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{subAt} (T , \operatorname{take} (n , x))}{x_{1}})}$ defined as $\operatorname{drop}$ applied to $n$ and $x$.
Descriptive.Tree.pullSubdefMathlib.SetTheory.Descriptive.Tree, function or constantEnglish
Let $T$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{tree} (A)}{x_{2}})}$. Let $x$ be a list of elements of $A$. Then $\operatorname{pullSub}$ applied to $T$ and $x$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{tree} (A)}{x_{1}})}$ defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to the proposition that $\operatorname{IsPrefix}$ holds for $\operatorname{take}$ applied to $\operatorname{length}$ applied to $x$ and $y$ and $x$ and $\MembershipmemMACRoT {T}{\operatorname{drop} (\operatorname{length} (x), y)}$.
Descriptive.Tree.subAtdefMathlib.SetTheory.Descriptive.Tree, function or constantEnglish
Let $T$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{tree} (A)}{x_{2}})}$. Let $x$ be a list of elements of $A$. Then $\operatorname{subAt}$ applied to $T$ and $x$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{tree} (A)}{x_{1}})}$ defined as the preimage of the function that maps $x_{1}$ to $\operatorname{hAppend}$ applied to $x$ and $x_{1}$ and $T$.
Descriptive.Tree.takedefMathlib.SetTheory.Descriptive.Tree, function or constantEnglish
Let $n$ be a natural number. Let $x$ be an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {T}{x_{2}})}$. Then $\operatorname{take}$ applied to $n$ and $x$ is an element of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {T}{x_{1}})}$ defined as $\operatorname{take}$ applied to $n$ and $x$.
Descriptive.treedefMathlib.SetTheory.Descriptive.Tree, function or constantWording
the tree of A (from the name)
English
Let $A$ be a set. Then the tree of $A$ is a complete sublattice of the power set of the set of lists of elements of $A$.
FinsetsdefMathlib.SetTheory.Lists, typeEnglish
Let $x$ be a set. Then an element of $\mathrm{Finsets}$ applied to $x$ is an element of the function that maps $x$ to $\mathrm{Quotient}$ applied to $\operatorname{instSetoidLists}$.
ListsdefMathlib.SetTheory.Lists, typeWording
list of x (from the name)
English
Let $x$ be a set. Then a list of $x$ is an element of the function that maps $x$ to $\Sigma$ applied to the function that maps $b$ to the set of lists of $x$ and $b$.
Lists'inductiveMathlib.SetTheory.Lists, typeWording
list of x and x1 (from the name)
English
Let $x$ be a set. Let $x_{1}$ be an element of $\mathrm{Bool}$. Then the lists of $x$ and $x_{1}$ are a basic type.
Lists'.SubsetinductiveMathlib.SetTheory.Lists, predicateEnglish
Let $x_{1}$ and $x_{2}$ be lists of $x$ and $\operatorname{true}$. Then we can say that $\operatorname{Subset}$ holds for $x_{1}$ and $x_{2}$.
Lists'.Subset.belowinductiveMathlib.SetTheory.Lists, predicateEnglish
Assume that $\operatorname{Subset}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
Lists'.atomconstructorMathlib.SetTheory.Lists, function or constantWording
the atom of x1 (from the name)
English
Let $x_{1}$ be an element of $x$. Then the atom of $x_{1}$ is a list of $x$ and $\operatorname{false}$.
Lists'.consdefMathlib.SetTheory.Lists, function or constantEnglish
Let $x_{1}$ be a list of $x$. Let $x_{2}$ be a list of $x$ and $\operatorname{true}$. Then $\operatorname{cons}$ applied to $x_{1}$ and $x_{2}$ is a list of $x$ and $\operatorname{true}$.
Lists'.cons'constructorMathlib.SetTheory.Lists, function or constantEnglish
Let $x_{1}$ be a list of $x$ and $b$. Let $x_{2}$ be a list of $x$ and $\operatorname{true}$. Then $\operatorname{cons'}$ applied to $x_{1}$ and $x_{2}$ is a list of $x$ and $\operatorname{true}$.
Lists'.ctorElimTypedefMathlib.SetTheory.Lists, typeEnglish
Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{false}$ and the atom of $x_{1}$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{true}$ and $\operatorname{nil}$ and $\mathrm{PULift}$ applied to the set of functions from elements $b$ of $\mathrm{Bool}$ and lists $x_{2}$ of $x$ and $b$ and lists $x_{3}$ of $x$ and $\operatorname{true}$ to elements of $\mathrm{motive}$ applied to $\operatorname{true}$ and $\operatorname{cons'}$ applied to $x_{2}$ and $x_{3}$.
Lists'.nilconstructorMathlib.SetTheory.Lists, function or constantEnglish
$\operatorname{nil}$ is a list of $x$ and $\operatorname{true}$.
Lists'.ofListdefMathlib.SetTheory.Lists, function or constantWording
the list of x1 (from the name)
English
Let $x_{1}$ be a list of lists of $x$. Then the list of $x_{1}$ is a list of $x$ and $\operatorname{true}$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Lists'\_\_ofList\_\_\_f}$.
Lists'.recOfListdefMathlib.SetTheory.Lists, function or constantEnglish
Let $\mathrm{ofList}$ be a function from lists $l_{1}$ of lists of $x$ to elements of $\mathrm{motive}$ applied to the list of $l_{1}$. Let $l$ be a list of $x$ and $\operatorname{true}$. Then $\operatorname{recOfList}$ applied to $l_{1}$, $\mathrm{ofList}$ and $l$ is an element of $\mathrm{motive}$ applied to $l$.
Lists'.toListdefMathlib.SetTheory.Lists, function or constantWording
the list of x1 (from the name)
English
Let $x_{1}$ be a list of $x$ and $b$. Then the list of $x_{1}$ is a list of lists of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Lists'\_\_toList\_\_\_f}$.
Lists.EquivinductiveMathlib.SetTheory.Lists, predicateEnglish
Let $x_{1}$ and $x_{2}$ be lists of $x$. Then we can say that $\operatorname{Equiv}$ holds for $x_{1}$ and $x_{2}$.
Lists.Equiv.belowinductiveMathlib.SetTheory.Lists, predicateEnglish
Assume that $\operatorname{Equiv}$ holds for $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.
Lists.IsListdefMathlib.SetTheory.Lists, predicateWording
l is a list (from the name)
English
Let $l$ be a list of $x$. Then $l$ is a list, if $\EqtMACRoH {\operatorname{fst} (l)}{\operatorname{true}}$.
Lists.atomdefMathlib.SetTheory.Lists, function or constantWording
the atom of a (from the name)
English
Let $a$ be an element of $x$. Then the atom of $a$ is a list of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{false}$ and the atom of $a$.
Lists.inductionMutdefMathlib.SetTheory.Lists, function or constantEnglish
Let $C$ be a function from lists of $x$ to sets. Let $D$ be a function from lists of $x$ and $\operatorname{true}$ to sets. Let $C_{0}$ be a function from elements $a_{1}$ of $x$ to elements of $C$ applied to the atom of $a_{1}$. Let $C_{1}$ be a function from lists $l_{3}$ of $x$ and $\operatorname{true}$ and elements of $D$ applied to $l_{3}$ to elements of $C$ applied to $\operatorname{of'}$ applied to $l_{3}$. Let $D_{0}$ be an element of $D$ applied to $\operatorname{nil}$. Let $D_{1}$ be a function from lists $a$ of $x$ and lists $l_{2}$ of $x$ and $\operatorname{true}$ and elements of $C$ applied to $a$ and elements of $D$ applied to $l_{2}$ to elements of $D$ applied to $\operatorname{cons}$ applied to $a$ and $l_{2}$. Then $\operatorname{inductionMut}$ applied to $C$, $D$, $a_{1}$, $C_{0}$, $l_{3}$, $C_{1}$, $D_{0}$, $a$, $l_{2}$ and $D_{1}$ is an element of $\mathrm{PProd}$ applied to the set of functions from lists $l$ of $x$ to elements of $C$ applied to $l$ and the set of functions from lists $l_{1}$ of $x$ and $\operatorname{true}$ to elements of $D$ applied to $l_{1}$.
Lists.memdefMathlib.SetTheory.Lists, predicateEnglish
Let $a$ and $x_{1}$ be lists of $x$. Then we can say that $\operatorname{mem}$ holds for $a$ and $x_{1}$.
Lists.of'defMathlib.SetTheory.Lists, function or constantEnglish
Let $l$ be a list of $x$ and $\operatorname{true}$. Then $\operatorname{of'}$ applied to $l$ is a list of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{true}$ and $l$.
Lists.ofListdefMathlib.SetTheory.Lists, function or constantWording
the list of l (from the name)
English
Let $l$ be a list of lists of $x$. Then the list of $l$ is a list of $x$ defined as $\operatorname{of'}$ applied to the list of $l$.
Lists.toListdefMathlib.SetTheory.Lists, function or constantWording
the list of x1 (from the name)
English
Let $x_{1}$ be a list of $x$. Then the list of $x_{1}$ is a list of lists of $x$.
Ordinal.limitRecOndefMathlib.SetTheory.Ordinal.Arithmetic, function or constantEnglish
Let $o$ be an ordinal. Let $\mathrm{zero}$ be an element of $\mathrm{motive}$ applied to $0$. Let $\mathrm{add\_one}$ be a function from ordinals $o_{2}$ and elements of $\mathrm{motive}$ applied to $o_{2}$ to elements of $\mathrm{motive}$ applied to $o_{2} + 1$. Let $\mathrm{limit}$ be a function from ordinals $o_{1}$ and elements of $\mathrm{Proof}$ applied to the proposition that $o_{1}$ is a successor limit and functions from ordinals $\mathrm{o'}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (\mathrm{o'} , o_{1})$ to elements of $\mathrm{motive}$ applied to $\mathrm{o'}$ to elements of $\mathrm{motive}$ applied to $o_{1}$. Then $\operatorname{limitRecOn}$ applied to $o$, $\mathrm{zero}$, $o_{2}$, $\mathrm{add\_one}$, $o_{1}$ and $\mathrm{limit}$ is an element of $\mathrm{motive}$ applied to $o$.
Ordinal.preddefMathlib.SetTheory.Ordinal.Arithmetic, function or constantWording
the ordinal predecessor of o (from the docstring)
English
Let $o$ be an ordinal. Then the ordinal predecessor of $o$ is an ordinal defined as $\operatorname{isSuccPrelimitRecOn}$ applied to $o$, the function that maps $a$ and $h$ to $a$ and the function that maps $a_{1}$ and $h_{1}$ to $a_{1}$.
Ordinal.predSuccGidefMathlib.SetTheory.Ordinal.Arithmetic, function or constantEnglish
$\operatorname{predSuccGi}$ is a Galois insertion of $\operatorname{pred}$ and $\operatorname{succ}$.
Cardinal.gciOrdCarddefMathlib.SetTheory.Ordinal.Basic, function or constantEnglish
$\operatorname{gciOrdCard}$ is a Galois coinsertion of $\operatorname{ord}$ and $\operatorname{card}$.
Cardinal.orddefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the order of c (from the name)
English
Let $c$ be a cardinal. Then the order of $c$ is an ordinal.
OrdinaldefMathlib.SetTheory.Ordinal.Basic, typeWording
ordinal (from the name)
English
An ordinal is an element of $\mathrm{Quotient}$ applied to $\operatorname{isEquivalent}$.
Ordinal.ToTypedefMathlib.SetTheory.Ordinal.Basic, typeWording
type of o (from the name)
English
Let $o$ be an ordinal. Then a type of $o$ is an element of the function that maps $o$ to the set of shrinks of the set of elements of $\operatorname{Iio}$ applied to $o$.
Ordinal.ToType.mkdefMathlib.SetTheory.Ordinal.Basic, function or constantEnglish
$\operatorname{mk}$ is an order isomorphism of the set of elements of $\operatorname{Iio}$ applied to $o$ and the set of types of $o$ defined as the order isomorphism of the set of elements of $\operatorname{Iio}$ applied to $o$.
Ordinal.ToType.toOrddefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the order of x (from the name)
English
Let $x$ be a type of $o$. Then the order of $x$ is an element of $\operatorname{Iio}$ applied to $o$ defined as $\operatorname{symm}$ applied to $\operatorname{mk}$ and $x$.
Ordinal.carddefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the cardinal of x (from the docstring)
English
Let $x$ be an ordinal. Then the cardinal of $x$ is a cardinal.
Ordinal.enumdefMathlib.SetTheory.Ordinal.Basic, function or constantEnglish
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then $\operatorname{enum}$ applied to $r$ is a relation isomorphism of the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$ and $r$ defined as $\operatorname{subrelIso}$ applied to the order type of $r$.
Ordinal.liftdefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the lift of o (from the name)
English
Let $o$ be an ordinal. Then the lift of $o$ is an ordinal.
Ordinal.liftInitialSegdefMathlib.SetTheory.Ordinal.Basic, function or constantEnglish
$\operatorname{liftInitialSeg}$ is an element of $\mathrm{InitialSeg}$ applied to the function that maps $x$ and $x_{1}$ to $\mathrm{Lt} (x , x_{1})$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$.
Ordinal.liftOnWellOrderdefMathlib.SetTheory.Ordinal.Basic, function or constantEnglish
Let $o$ be an ordinal. Let $f$ be a function from sets $x_{9}$ and elements $x_{10}$ of $\mathrm{Proof}$ applied to the proposition that $x_{9}$ is linearly ordered and elements of $\mathrm{Proof}$ applied to $\mathrm{WellFoundedLT}$ applied to $x_{9}$ to elements of $x$ such that for all sets $x_{1}$, for all elements $x_{2}$ of $\mathrm{LinearOrder}$ applied to $x_{1}$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{WellFoundedLT}$ applied to $x_{1}$, for all sets $x_{3}$, for all elements $x_{4}$ of $\mathrm{LinearOrder}$ applied to $x_{3}$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\mathrm{WellFoundedLT}$ applied to $x_{3}$, if the order type of the function that maps $x_{5}$ and $x_{6}$ to $\mathrm{Lt} (x_{5} , x_{6})$ is equal to the order type of the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Lt} (x_{7} , x_{8})$, then $\EqtMACRoH {f (x_{1} , x_{2} , h)}{f (x_{3} , x_{4} , h_{1})}$. Then $\operatorname{liftOnWellOrder}$ applied to $o$, $x_{9}$, $x_{10}$, $f$ and $c$ is an element of $x$.
Ordinal.omega0defMathlib.SetTheory.Ordinal.Basic, function or constantWording
the omega (from the name)
English
The omega is an ordinal defined as the lift of the order type of the function that maps $x$ and $x_{1}$ to $\mathrm{Lt} (x , x_{1})$.
Ordinal.typedefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the order type of r (from the docstring)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the order type of $r$ is an ordinal defined as $\operatorname{mk}$ applied to $\operatorname{isEquivalent}$ and $\operatorname{mk}$ applied to $x$, $r$ and $\mathrm{wo}$.
Ordinal.typeindefMathlib.SetTheory.Ordinal.Basic, function or constantWording
the order type of r (from the docstring)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Then the order type of $r$ is an element of $\mathrm{PrincipalSeg}$ applied to $r$ and the function that maps $x_{1}$ and $x_{2}$ to $\mathrm{Lt} (x_{1} , x_{2})$.
WellOrderstructureMathlib.SetTheory.Ordinal.Basic, typeEnglish
The elements of $\mathrm{WellOrder}$ are a basic type.
WellOrder.rdefMathlib.SetTheory.Ordinal.Basic, predicateEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WellOrder}$. Let $x$ and $x_{1}$ be elements of $\mathrm{WellOrder\_\_\_u3b1\_}$ applied to $\mathrm{self}$. Then $\operatorname{r}$ holds for $\mathrm{self}$, $x$ and $x_{1}$, if $\operatorname{proj1}$ holds for $\mathrm{self}$, $x$ and $x_{1}$.
WellOrder.αdefMathlib.SetTheory.Ordinal.Basic, typeEnglish
Let $\mathrm{self}$ be an element of $\mathrm{WellOrder}$. Then an element of $\mathrm{WellOrder\_\_\_u3b1\_}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
Ordinal.CNFdefMathlib.SetTheory.Ordinal.CantorNormalForm, function or constantEnglish
Let $b$ and $o$ be ordinals. Then $\operatorname{CNF}$ applied to $b$ and $o$ is a list of elements of $\mathrm{Prod}$ applied to the set of ordinals and the set of ordinals.
Ordinal.CNF.coeffdefMathlib.SetTheory.Ordinal.CantorNormalForm, function or constantWording
the coefficient of b and o (from the name)
English
Let $b$ and $o$ be ordinals. Then the coefficient of $b$ and $o$ is a finitely supported function from the set of ordinals to the set of ordinals.
Ordinal.CNF.evaldefMathlib.SetTheory.Ordinal.CantorNormalForm, function or constantWording
the evaluation of b and f (from the name)
English
Let $b$ be an ordinal. Let $f$ be a finitely supported function from the set of ordinals to the set of ordinals. Then the evaluation of $b$ and $f$ is an ordinal defined as $\operatorname{foldr}$ applied to the function that maps $p$ and $r$ to $b ^ {p}\times f (p)+ r$, $0$ and the sort of the support of $f$ and the function that maps $x$ and $x_{1}$ to $\mathrm{Geq} (x , x_{1})$.
Ordinal.enumOrddefMathlib.SetTheory.Ordinal.Enum, function or constantEnglish
Let $s$ be an element of the power set of the set of ordinals. Let $o$ be an ordinal. Then $\operatorname{enumOrd}$ applied to $s$ and $o$ is an ordinal.
Ordinal.enumOrdOrderIsodefMathlib.SetTheory.Ordinal.Enum, function or constantEnglish
Let $s$ be an element of the power set of the set of ordinals such that $s$ is not bounded above. Then $\operatorname{enumOrdOrderIso}$ applied to $s$ and $\mathrm{hs}$ is an order isomorphism of the set of ordinals and the set of elements of $s$.
Ordinal.logdefMathlib.SetTheory.Ordinal.Exponential, function or constantWording
the ordinal logarithm of b and x (from the docstring)
English
Let $b$ and $x$ be ordinals. Then the ordinal logarithm of $b$ and $x$ is an ordinal defined as the supremum of the preimage of the function that maps $x_{1}$ to $b ^ {x_{1}}$ and $\operatorname{Iic}$ applied to $x$.
Ordinal.derivdefMathlib.SetTheory.Ordinal.FixedPoint, function or constantWording
the derivative of f and x (from the docstring)
English
Let $f$ be a function from ordinals to ordinals. Let $x$ be an ordinal. Then the derivative of $f$ and $x$ is an ordinal defined as the derivative of the function that maps $x$ to $f$ and $x$.
Ordinal.derivFamilydefMathlib.SetTheory.Ordinal.FixedPoint, function or constantWording
the derivative of f and o (from the docstring)
English
Let $f$ be a function from elements of $x$ and ordinals to ordinals. Let $o$ be an ordinal. Then the derivative of $f$ and $o$ is an ordinal.
Ordinal.nfpdefMathlib.SetTheory.Ordinal.FixedPoint, function or constantEnglish
Let $f$ be a function from ordinals to ordinals. Let $x$ be an ordinal. Then $\operatorname{nfp}$ applied to $f$ and $x$ is an ordinal defined as $\operatorname{nfpFamily}$ applied to the function that maps $x$ to $f$ and $x$.
Ordinal.nfpFamilydefMathlib.SetTheory.Ordinal.FixedPoint, function or constantEnglish
Let $f$ be a function from elements of $x$ and ordinals to ordinals. Let $a$ be an ordinal. Then $\operatorname{nfpFamily}$ applied to $f$ and $a$ is an ordinal defined as the supremum of the function that maps $i$ to $\operatorname{foldr}$ applied to $f$, $a$ and $i$.
OrdinalApprox.gfpApproxdefMathlib.SetTheory.Ordinal.FixedPointApproximants, function or constantEnglish
Let $f$ be an order homomorphism of $x$ and $x$. Let $x_{2}$ be an element of $x$. Let $a$ be an ordinal. Then $\operatorname{gfpApprox}$ applied to $f$, $x_{2}$ and $a$ is an element of $x$.
OrdinalApprox.lfpApproxdefMathlib.SetTheory.Ordinal.FixedPointApproximants, function or constantEnglish
Let $f$ be an order homomorphism of $x$ and $x$. Let $x_{2}$ be an element of $x$. Let $a$ be an ordinal. Then $\operatorname{lfpApprox}$ applied to $f$, $x_{2}$ and $a$ is an element of $x$.
Ordinal.IsFundamentalSeqstructureMathlib.SetTheory.Ordinal.FundamentalSequence, predicateWording
f is a fundamental sequence (from the name)
English
Let $f$ be a function from elements of $\operatorname{Iio}$ applied to $a$ to elements of $\operatorname{Iio}$ applied to $o$. Then we can say that $f$ is a fundamental sequence.
NONotedefMathlib.SetTheory.Ordinal.Notation, typeEnglish
An element of $\mathrm{NONote}$ is an element of $\SubtypeSet {o}{\operatorname{NF} (o)}$.
NONote.belowdefMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Let $a$ and $b$ be elements of $\mathrm{NONote}$. Then $\operatorname{below}$ holds for $a$ and $b$, if $\operatorname{NFBelow}$ holds for $a$ and the representation of $b$.
NONote.cmpdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the comparison of a and b (from the name)
English
Let $a$ and $b$ be elements of $\mathrm{NONote}$. Then the comparison of $a$ and $b$ is an element of $\mathrm{Ordering}$ defined as the comparison of $a$ and $b$.
NONote.mkdefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $o$ be a note. Then $\operatorname{mk}$ applied to $o$ is an element of $\mathrm{NONote}$ defined as $o$.
NONote.oadddefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $e$ and $a$ be elements of $\mathrm{NONote}$. Let $n$ be a positive natural number. Assume that $\operatorname{below}$ holds for $a$ and $e$. Then $\operatorname{oadd}$ applied to $e$, $n$, $a$ and $h$ is an element of $\mathrm{NONote}$ defined as $\operatorname{oadd}$ applied to $e$, $n$ and $a$.
NONote.ofNatdefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{ofNat}$ applied to $n$ is an element of $\mathrm{NONote}$ defined as the note of $n$.
NONote.opowdefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $x$ and $y$ be elements of $\mathrm{NONote}$. Then $\operatorname{opow}$ applied to $x$ and $y$ is an element of $\mathrm{NONote}$ defined as $\operatorname{mk}$ applied to $x ^ {y}$.
NONote.recOndefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $o$ be an element of $\mathrm{NONote}$. Let $H_{0}$ be an element of $C$ applied to $0$. Let $H_{1}$ be a function from elements $e$ of $\mathrm{NONote}$ and positive natural numbers $n$ and elements $a$ of $\mathrm{NONote}$ and elements $h$ of $\mathrm{Proof}$ applied to $\operatorname{below}$ applied to $a$ and $e$ and elements of $C$ applied to $e$ and elements of $C$ applied to $a$ to elements of $C$ applied to $\operatorname{oadd}$ applied to $e$, $n$, $a$ and $h$. Then $\operatorname{recOn}$ applied to $o$, $H_{0}$, $e$, $n$, $a$, $h$ and $H_{1}$ is an element of $C$ applied to $o$.
NONote.reprdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the representation of o (from the name)
English
Let $o$ be an element of $\mathrm{NONote}$. Then the representation of $o$ is an ordinal defined as the representation of $o$.
ONoteinductiveMathlib.SetTheory.Ordinal.Notation, typeWording
note (from the name)
English
The notes are a basic type.
ONote.FundamentalSequencePropdefMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Let $o$ be a note. Let $x$ be an element of $\mathrm{Sum}$ applied to $\mathrm{Option}$ applied to the set of notes and the set of functions from natural numbers to notes. Then we can say that $\operatorname{FundamentalSequenceProp}$ holds for $o$ and $x$.
ONote.NFclassMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Let $o$ be a note. Then we can say that $\operatorname{NF}$ holds for $o$.
ONote.NFBelowinductiveMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Let $x$ be a note. Let $x_{1}$ be an ordinal. Then we can say that $\operatorname{NFBelow}$ holds for $x$ and $x_{1}$.
ONote.NFBelow.belowinductiveMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Assume that $\operatorname{NFBelow}$ holds for $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
ONote.TopBelowdefMathlib.SetTheory.Ordinal.Notation, predicateEnglish
Let $b$ and $x$ be notes. Then we can say that $\operatorname{TopBelow}$ holds for $b$ and $x$.
ONote.adddefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the sum of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be notes. Then the sum of $x$ and $x_{1}$ is a note defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{ONote\_\_add\_\_\_f}$ and $x_{1}$.
ONote.cmpdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the comparison of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be notes. Then the comparison of $x$ and $x_{1}$ is an element of $\mathrm{Ordering}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{ONote\_\_cmp\_\_\_f}$ and $x_{1}$.
ONote.ctorElimTypedefMathlib.SetTheory.Ordinal.Notation, typeEnglish
Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to the set of functions from notes $x$ and positive natural numbers $x_{1}$ and notes $x_{2}$ to elements of $\mathrm{motive}$ applied to $\operatorname{oadd}$ applied to $x$, $x_{1}$ and $x_{2}$.
ONote.fastGrowingdefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $x$ be a note. Let $x_{1}$ be a natural number. Then $\operatorname{fastGrowing}$ applied to $x$ and $x_{1}$ is a natural number.
ONote.fastGrowingε₀defMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $i$ be a natural number. Then $\mathrm{ONote\_\_fastGrowing\_u3b5\_\_u2080\_}$ applied to $i$ is a natural number defined as $\operatorname{fastGrowing}$ applied to $\operatorname{iterate}$ applied to the function that maps $a$ to $\operatorname{oadd}$ applied to $a$, $1$ and $0$, $i$ and $0$ and $i$.
ONote.fundamentalSequencedefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the fundamental sequence of x (from the name)
English
Let $x$ be a note. Then the fundamental sequence of $x$ is an element of $\mathrm{Sum}$ applied to $\mathrm{Option}$ applied to the set of notes and the set of functions from natural numbers to notes defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{ONote\_\_fundamentalSequence\_\_\_f}$.
ONote.muldefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the product of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be notes. Then the product of $x$ and $x_{1}$ is a note defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{ONote\_\_mul\_\_\_f}$ and $x$.
ONote.mulNatdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the multiplicative natural number of x and x1 (from the name)
English
Let $x$ be a note. Let $x_{1}$ be a natural number. Then the multiplicative natural number of $x$ and $x_{1}$ is a note.
ONote.oaddconstructorMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $x$ and $x_{2}$ be notes. Let $x_{1}$ be a positive natural number. Then $\operatorname{oadd}$ applied to $x$, $x_{1}$ and $x_{2}$ is a note.
ONote.ofNatdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the note of x (from the name)
English
Let $x$ be a natural number. Then the note of $x$ is a note.
ONote.omegadefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the omega (from the name)
English
The omega is a note defined as $\operatorname{oadd}$ applied to $1$, $1$ and $0$.
ONote.opowdefMathlib.SetTheory.Ordinal.Notation, function or constantEnglish
Let $x$ and $x_{1}$ be notes. Then $\operatorname{opow}$ applied to $x$ and $x_{1}$ is a note defined as $\operatorname{opowAux2}$ applied to $x_{1}$ and the split of $x$.
ONote.reprdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the representation of x (from the name)
English
Let $x$ be a note. Then the representation of $x$ is an ordinal defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{ONote\_\_repr\_\_\_f}$.
ONote.repr'defMathlib.SetTheory.Ordinal.Notation, function or constantWording
the representation of prec and x (from the name)
English
Let $\mathrm{prec}$ be a natural number. Let $x$ be a note. Then the representation of $\mathrm{prec}$ and $x$ is an element of $\operatorname{Format}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{ONote\_\_repr'\_\_\_f}$ and $\mathrm{prec}$.
ONote.scaledefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the scale of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be notes. Then the scale of $x$ and $x_{1}$ is a note defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{ONote\_\_scale\_\_\_f}$ applied to $x$.
ONote.splitdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the split of x (from the name)
English
Let $x$ be a note. Then the split of $x$ is an element of $\mathrm{Prod}$ applied to the set of notes and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{ONote\_\_split\_\_\_f}$.
ONote.split'defMathlib.SetTheory.Ordinal.Notation, function or constantWording
the split of x (from the name)
English
Let $x$ be a note. Then the split of $x$ is an element of $\mathrm{Prod}$ applied to the set of notes and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{ONote\_\_split'\_\_\_f}$.
ONote.subdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the difference of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be notes. Then the difference of $x$ and $x_{1}$ is a note defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{ONote\_\_sub\_\_\_f}$ and $x_{1}$.
ONote.toStringdefMathlib.SetTheory.Ordinal.Notation, function or constantWording
the string of x (from the name)
English
Let $x$ be a note. Then the string of $x$ is an element of $\mathrm{String}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{ONote\_\_toString\_\_\_f}$.
Ordinal.IsPrincipaldefMathlib.SetTheory.Ordinal.Principal, predicateEnglish
Let $\mathrm{op}$ be a function from ordinals and ordinals to ordinals. Let $o$ be an ordinal. Then $\operatorname{IsPrincipal}$ holds for $\mathrm{op}$ and $o$, if for all ordinals $a$ and $b$, if $a < o$, then if $b < o$, then $\mathrm{op} (a , b)< o$.
Acc.rankdefMathlib.SetTheory.Ordinal.Rank, function or constantWording
the rank of h (from the docstring)
English
Assume that $\mathrm{Acc}$ holds for $r$ and $a$. Then the rank of $h$ is an ordinal.
WellFounded.rankdefMathlib.SetTheory.Ordinal.Rank, function or constantWording
the rank of r and a (from the docstring)
English
Let $r$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ be an element of $x$. Then the rank of $r$ and $a$ is an ordinal defined as the rank of $\operatorname{apply}$ applied to $\mathrm{hwf}$ and $a$.
Cardinal.univdefMathlib.SetTheory.Ordinal.Univ, function or constantWording
the universal set (from the name)
English
The universal set is a cardinal defined as the lift of $\operatorname{mk}$ applied to the set of ordinals.
Ordinal.liftPrincipalSegdefMathlib.SetTheory.Ordinal.Univ, function or constantEnglish
$\operatorname{liftPrincipalSeg}$ is an element of $\mathrm{PrincipalSeg}$ applied to the function that maps $x$ and $x_{1}$ to $\mathrm{Lt} (x , x_{1})$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{Lt} (x_{2} , x_{3})$.
Ordinal.univdefMathlib.SetTheory.Ordinal.Univ, function or constantWording
the universal set (from the name)
English
The universal set is an ordinal defined as the lift of the order type of the function that maps $x$ and $x_{1}$ to $\mathrm{Lt} (x , x_{1})$.
Ordinal.epsilondefMathlib.SetTheory.Ordinal.Veblen, function or constantWording
the epsilon of x (from the name)
English
Let $x$ be an ordinal. Then the epsilon of $x$ is an ordinal defined as $\operatorname{veblen}$ applied to $1$ and $x$.
Ordinal.gammadefMathlib.SetTheory.Ordinal.Veblen, function or constantWording
the Gamma of x (from the name)
English
Let $x$ be an ordinal. Then the Gamma of $x$ is an ordinal defined as the derivative of the function that maps $x$ to $\operatorname{veblen}$ applied to $x$ and $0$ and $x$.
Ordinal.invVeblen₁defMathlib.SetTheory.Ordinal.Veblen, function or constantEnglish
Let $x$ be an ordinal. Then $\mathrm{Ordinal\_\_invVeblen\_u2081\_}$ applied to $x$ is an ordinal defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $y$ to $\mathrm{Neq} (\operatorname{veblen} (y , x), x)$.
Ordinal.invVeblen₂defMathlib.SetTheory.Ordinal.Veblen, function or constantEnglish
Let $x$ be an ordinal. Then $\mathrm{Ordinal\_\_invVeblen\_u2082\_}$ applied to $x$ is an ordinal.
Ordinal.veblendefMathlib.SetTheory.Ordinal.Veblen, function or constantEnglish
Let $x$ and $x_{1}$ be ordinals. Then $\operatorname{veblen}$ applied to $x$ and $x_{1}$ is an ordinal defined as $\operatorname{veblenWith}$ applied to the function that maps $x$ to the exponentiation of the omega to $x$, $x$ and $x_{1}$.
Ordinal.veblenWithdefMathlib.SetTheory.Ordinal.Veblen, function or constantEnglish
Let $f$ be a function from ordinals to ordinals. Let $o$ and $x$ be ordinals. Then $\operatorname{veblenWith}$ applied to $f$, $o$ and $x$ is an ordinal.
ZFSetdefMathlib.SetTheory.ZFC.Basic, typeEnglish
An element of $\mathrm{ZFSet}$ is an element of $\mathrm{Quotient}$ applied to $\operatorname{setoid}$.
ZFSet.DefinableclassMathlib.SetTheory.ZFC.Basic, predicateEnglish
Let $n$ be a natural number. Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Then we can say that $\operatorname{Definable}$ holds for $n$ and $f$.
ZFSet.Definable.outdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to sets. Then $\operatorname{out}$ applied to $f$ and $x$ is a set defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.
ZFSet.Definable₁defMathlib.SetTheory.ZFC.Basic, typeEnglish
Let $f$ be a function from elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Then an element of $\mathrm{ZFSet\_\_Definable\_u2081\_}$ applied to $f$ is an element of the function that maps $f$ to $\operatorname{Definable}$ applied to $1$ and the function that maps $s$ to $f$ applied to $s$ applied to $0$.
ZFSet.Definable₁.outdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $f$ be a function from elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Let $x_{1}$ be a set. Then $\mathrm{ZFSet\_\_Definable\_u2081\_\_\_out}$ applied to $f$ and $x_{1}$ is a set defined as $\operatorname{out}$ applied to the function that maps $s$ to $f$ applied to $s$ applied to $0$ and $\operatorname{vecCons}$ applied to $x_{1}$ and $\operatorname{vecEmpty}$.
ZFSet.Definable₂defMathlib.SetTheory.ZFC.Basic, typeEnglish
Let $f$ be a function from elements of $\mathrm{ZFSet}$ and elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Then an element of $\mathrm{ZFSet\_\_Definable\_u2082\_}$ applied to $f$ is an element of the function that maps $f$ to $\operatorname{Definable}$ applied to $2$ and the function that maps $s$ to $f$ applied to $s$ applied to $0$ and $s$ applied to $1$.
ZFSet.Definable₂.outdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $f$ be a function from elements of $\mathrm{ZFSet}$ and elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Let $x_{1}$ and $x_{2}$ be sets. Then $\mathrm{ZFSet\_\_Definable\_u2082\_\_\_out}$ applied to $f$, $x_{1}$ and $x_{2}$ is a set defined as $\operatorname{out}$ applied to the function that maps $s$ to $f$ applied to $s$ applied to $0$ and $s$ applied to $1$ and $\operatorname{vecCons}$ applied to $x_{1}$ and $\operatorname{vecCons}$ applied to $x_{2}$ and $\operatorname{vecEmpty}$.
ZFSet.HereditarilydefMathlib.SetTheory.ZFC.Basic, predicateEnglish
Let $p$ be a function from elements of $\mathrm{ZFSet}$ to propositions. Let $x$ be an element of $\mathrm{ZFSet}$. Then we can say that $\operatorname{Hereditarily}$ holds for $p$ and $x$.
ZFSet.InsertdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $x$ and $x_{1}$ be elements of $\mathrm{ZFSet}$. Then $\operatorname{Insert}$ applied to $x$ and $x_{1}$ is an element of $\mathrm{ZFSet}$.
ZFSet.IsFuncdefMathlib.SetTheory.ZFC.Basic, predicateEnglish
Let $x$, $y$ and $f$ be elements of $\mathrm{ZFSet}$. Then $\operatorname{IsFunc}$ holds for $x$, $y$ and $f$, if $f$ is less than or equal to the product of $x$ and $y$ and for all elements $z$ of $\mathrm{ZFSet}$, if $z$ is an element of $x$, then $\mathrm{ExistsUnique}$ holds for the function that maps $w$ to the proposition that the pair of $z$ and $w$ is an element of $f$.
ZFSet.NonemptydefMathlib.SetTheory.ZFC.Basic, predicateWording
u is nonempty (from the name)
English
Let $u$ be an element of $\mathrm{ZFSet}$. Then $u$ is nonempty, if $u$ is nonempty.
ZFSet.diffdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the set difference operation of x and y (from the docstring)
English
Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then the set difference operation of $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{sep}$ applied to the function that maps $z$ to the proposition that $z$ is not an element of $y$ and $x$.
ZFSet.emptydefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
$\operatorname{empty}$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{mk}$ applied to $\operatorname{emptyCollection}$.
ZFSet.funsdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then $\operatorname{funs}$ applied to $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{sep}$ applied to $\operatorname{IsFunc}$ applied to $x$ and $y$ and the powerset of the product of $x$ and $y$.
ZFSet.iUniondefMathlib.SetTheory.ZFC.Basic, function or constantWording
the union of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ZFSet}$. Then the union of $f$ is an element of $\mathrm{ZFSet}$ defined as the union of the range of $f$.
ZFSet.imagedefMathlib.SetTheory.ZFC.Basic, function or constantWording
the image of f and x1 (from the docstring)
English
Let $f$ be a function from elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Let $x_{1}$ be an element of $\mathrm{ZFSet}$. Then the image of $f$ and $x_{1}$ is an element of $\mathrm{ZFSet}$.
ZFSet.interdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the binary intersection operation of x and y (from the docstring)
English
Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then the binary intersection operation of $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{sep}$ applied to the function that maps $z$ to $\MembershipmemMACRoT {y}{z}$ and $x$.
ZFSet.mapdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the map of f and x1 (from the name)
English
Let $f$ be a function from elements of $\mathrm{ZFSet}$ to elements of $\mathrm{ZFSet}$. Let $x_{1}$ be an element of $\mathrm{ZFSet}$. Then the map of $f$ and $x_{1}$ is an element of $\mathrm{ZFSet}$ defined as the image of the function that maps $y$ to the pair of $y$ and $f$ applied to $y$ and $x_{1}$.
ZFSet.mkdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $x$ be a set. Then $\operatorname{mk}$ applied to $x$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{mk''}$ applied to $x$.
ZFSet.omegadefMathlib.SetTheory.ZFC.Basic, function or constantWording
the omega (from the name)
English
The omega is an element of $\mathrm{ZFSet}$ defined as $\operatorname{mk}$ applied to the omega.
ZFSet.pairdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the pair of x and y (from the name)
English
Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then the pair of $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{insert}$ applied to $\operatorname{singleton}$ applied to $x$ and $\operatorname{singleton}$ applied to $\operatorname{insert}$ applied to $x$ and $\operatorname{singleton}$ applied to $y$.
ZFSet.pairSepdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $p$ be a function from elements of $\mathrm{ZFSet}$ and elements of $\mathrm{ZFSet}$ to propositions. Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then $\operatorname{pairSep}$ applied to $p$, $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{sep}$ applied to the function that maps $z$ to the proposition that there exists an element $a$ of $\mathrm{ZFSet}$, such that $a$ is an element of $x$ and there exists an element $b$ of $\mathrm{ZFSet}$ such that $b$ is an element of $y$ and $z$ is equal to the pair of $a$ and $b$ and $p$ holds for $a$ and $b$ and the powerset of the powerset of $\UnionunionMACRoAB {x}{y}$.
ZFSet.powersetdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the powerset of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the powerset of $x$ is an element of $\mathrm{ZFSet}$.
ZFSet.powersetEquivdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the powerset equivalence of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the powerset equivalence of $x$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{powerset} (x)}{x_{1}})})}{\operatorname{Elem} (\operatorname{powerset} (x))}$.
ZFSet.proddefMathlib.SetTheory.ZFC.Basic, function or constantWording
the product of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be elements of $\mathrm{ZFSet}$. Then the product of $x$ and $x_{1}$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{pairSep}$ applied to the function that maps $x$ and $x_{1}$ to $\mathrm{True}$, $x$ and $x_{1}$.
ZFSet.rangedefMathlib.SetTheory.ZFC.Basic, function or constantWording
the range of f (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ZFSet}$. Then the range of $f$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{mk}$ applied to $\operatorname{setoid}$ and $\operatorname{mk}$ applied to the set of shrinks of $x$ and $\operatorname{comp}$ applied to $\operatorname{out}$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{coe}$ applied to the inverse of the equivalence shrink of $x$.
ZFSet.sInterdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the intersection of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the intersection of $x$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{sep}$ applied to the function that maps $y$ to the proposition that for all elements $z$ of $\mathrm{ZFSet}$, if $z$ is an element of $x$, then $y$ is an element of $z$ and the union of $x$.
ZFSet.sUniondefMathlib.SetTheory.ZFC.Basic, function or constantWording
the union of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the union of $x$ is an element of $\mathrm{ZFSet}$.
ZFSet.sepdefMathlib.SetTheory.ZFC.Basic, function or constantEnglish
Let $p$ be a function from elements of $\mathrm{ZFSet}$ to propositions. Let $x$ be an element of $\mathrm{ZFSet}$. Then $\operatorname{sep}$ applied to $p$ and $x$ is an element of $\mathrm{ZFSet}$.
ZFSet.toSetdefMathlib.SetTheory.ZFC.Basic, function or constantWording
the set of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the set of $x$ is an element of $\wp \mathrm{ZFSet}$.
ZFSet.uniondefMathlib.SetTheory.ZFC.Basic, function or constantWording
the binary union operation of x and y (from the docstring)
English
Let $x$ and $y$ be elements of $\mathrm{ZFSet}$. Then the binary union operation of $x$ and $y$ is an element of $\mathrm{ZFSet}$ defined as the union of $\operatorname{insert}$ applied to $x$ and $\operatorname{singleton}$ applied to $y$.
ZFSet.carddefMathlib.SetTheory.ZFC.Cardinal, function or constantWording
the cardinality of x (from the docstring)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the cardinality of $x$ is a cardinal defined as $\operatorname{mk}$ applied to the set of shrinks of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {x}{x_{1}})}$.
ZFClassdefMathlib.SetTheory.ZFC.Class, typeWording
collection of all classes (from the docstring)
English
A collection of all classes is an element of $\wp \mathrm{ZFSet}$.
ZFClass.CMemdefMathlib.SetTheory.ZFC.Class, predicateEnglish
Let $A$ and $B$ be collections of all classes. Then $\operatorname{CMem}$ holds for $A$ and $B$, if there exists an element $x$ of $\mathrm{ZFSet}$, such that $\EqtMACRoH {x}{A}$ and $x$ is an element of $B$.
ZFClass.classToCongdefMathlib.SetTheory.ZFC.Class, function or constantEnglish
Let $x$ be a collection of all classes. Then $\operatorname{classToCong}$ applied to $x$ is an element of the power set of the set of collections of all classes defined as $\operatorname{ofPred}$ applied to the function that maps $y$ to $\operatorname{CMem}$ applied to $y$ and $x$.
ZFClass.congToClassdefMathlib.SetTheory.ZFC.Class, function or constantEnglish
Let $x$ be an element of the power set of the set of collections of all classes. Then $\operatorname{congToClass}$ applied to $x$ is a collection of all classes defined as the preimage of $\operatorname{instSetLike}$ and $x$.
ZFClass.fvaldefMathlib.SetTheory.ZFC.Class, function or constantEnglish
Let $F$ and $A$ be collections of all classes. Then $\operatorname{fval}$ applied to $F$ and $A$ is a collection of all classes defined as $\operatorname{iota}$ applied to $\operatorname{ofPred}$ applied to the function that maps $y$ to $\operatorname{CMem}$ applied to $A$ and $\operatorname{ofPred}$ applied to the function that maps $x$ to $\operatorname{CMem}$ applied to the pair of $x$ and $y$ and $F$.
ZFClass.iotadefMathlib.SetTheory.ZFC.Class, function or constantEnglish
Let $A$ be a collection of all classes. Then $\operatorname{iota}$ applied to $A$ is a collection of all classes defined as the union of $\operatorname{ofPred}$ applied to the function that maps $x$ to the proposition that for all elements $y$ of $\mathrm{ZFSet}$, $\operatorname{CMem}$ holds for $y$ and $A$, if and only if $\EqtMACRoH {y}{x}$.
ZFClass.powersetdefMathlib.SetTheory.ZFC.Class, function or constantWording
the power class of x (from the docstring)
English
Let $x$ be a collection of all classes. Then the power class of $x$ is a collection of all classes defined as $\operatorname{congToClass}$ applied to the powerset of $x$.
ZFClass.sInterdefMathlib.SetTheory.ZFC.Class, function or constantWording
the intersection of x (from the docstring)
English
Let $x$ be a collection of all classes. Then the intersection of $x$ is a collection of all classes defined as the infimum of $\operatorname{classToCong}$ applied to $x$.
ZFClass.sUniondefMathlib.SetTheory.ZFC.Class, function or constantWording
the union of x (from the docstring)
English
Let $x$ be a collection of all classes. Then the union of $x$ is a collection of all classes defined as the supremum of $\operatorname{classToCong}$ applied to $x$.
ZFSet.choicedefMathlib.SetTheory.ZFC.Class, function or constantWording
the choice of x (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the choice of $x$ is an element of $\mathrm{ZFSet}$ defined as the map of the function that maps $y$ to $\operatorname{epsilon}$ applied to the function that maps $z$ to $\MembershipmemMACRoT {y}{z}$ and $x$.
ZFSet.coeEquivdefMathlib.SetTheory.ZFC.Class, function or constantWording
the coercion equivalence (from the name)
English
The coercion equivalence is an element of $\EquivMACRoAE {\mathrm{ZFSet}}{(\SubtypeSet {s}{\mathrm{Small} (\operatorname{Elem} (s))})}$.
Ordinal.toPSetdefMathlib.SetTheory.ZFC.Ordinal, function or constantWording
the set of o (from the name)
English
Let $o$ be an ordinal. Then the set of $o$ is a set.
Ordinal.toZFSetdefMathlib.SetTheory.ZFC.Ordinal, function or constantEnglish
Let $o$ be an ordinal. Then $\operatorname{toZFSet}$ applied to $o$ is an element of $\mathrm{ZFSet}$ defined as $\operatorname{mk}$ applied to the set of $o$.
Ordinal.toZFSetIsodefMathlib.SetTheory.ZFC.Ordinal, function or constantEnglish
$\operatorname{toZFSetIso}$ is an order isomorphism of the set of ordinals and $\SubtypeSet {x}{\operatorname{IsOrdinal} (x)}$.
ZFSet.IsOrdinalstructureMathlib.SetTheory.ZFC.Ordinal, predicateWording
x is a ordinal (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then we can say that $x$ is an ordinal.
ZFSet.IsTransitivedefMathlib.SetTheory.ZFC.Ordinal, predicateWording
x is transitive (from the name)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then $x$ is transitive, if for all elements $y$ of $\mathrm{ZFSet}$, if $y$ is an element of $x$, then $y \leq x$.
PSetstructureMathlib.SetTheory.ZFC.PSet, typeWording
set (from the name)
English
The sets are a basic type.
PSet.EquivdefMathlib.SetTheory.ZFC.PSet, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then $\operatorname{Equiv}$ holds for $x$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $x$, $\mathrm{PSet\_\_Equiv\_\_\_f}$ and $x_{1}$.
PSet.FuncdefMathlib.SetTheory.ZFC.PSet, function or constantWording
the function of self and x (from the name)
English
Let $\mathrm{self}$ be a set. Let $x$ be a type of $\mathrm{self}$. Then the function of $\mathrm{self}$ and $x$ is a set defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.
PSet.LiftdefMathlib.SetTheory.ZFC.PSet, function or constantWording
the lift of x (from the name)
English
Let $x$ be a set. Then the lift of $x$ is a set defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PSet\_\_Lift\_\_\_f}$.
PSet.MemdefMathlib.SetTheory.ZFC.PSet, predicateEnglish
Let $y$ and $x$ be sets. Then $\operatorname{Mem}$ holds for $y$ and $x$, if there exists a type $b$ of $y$, such that $\operatorname{Equiv}$ holds for $x$ and the function of $y$ and $b$.
PSet.NonemptydefMathlib.SetTheory.ZFC.PSet, predicateWording
u is nonempty (from the name)
English
Let $u$ be a set. Then $u$ is nonempty, if the set of $u$ is nonempty.
PSet.SubsetdefMathlib.SetTheory.ZFC.PSet, predicateEnglish
Let $x$ and $y$ be sets. Then $\operatorname{Subset}$ holds for $x$ and $y$, if for all types $a$ of $x$, there exists a type $b$ of $y$, such that $\operatorname{Equiv}$ holds for the function of $x$ and $a$ and the function of $y$ and $b$.
PSet.TypedefMathlib.SetTheory.ZFC.PSet, typeWording
type of self (from the name)
English
Let $\mathrm{self}$ be a set. Then a type of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
PSet.embeddefMathlib.SetTheory.ZFC.PSet, function or constantWording
the embed (from the name)
English
The embed is a set.
PSet.emptydefMathlib.SetTheory.ZFC.PSet, function or constantEnglish
$\operatorname{empty}$ is a set defined as $\operatorname{mk}$ applied to $\mathrm{PEmpty}$ and $\operatorname{elim}$.
PSet.imagedefMathlib.SetTheory.ZFC.PSet, function or constantWording
the image of f and x (from the docstring)
English
Let $f$ be a function from sets to sets. Let $x$ be a set. Then the image of $f$ and $x$ is a set defined as $\operatorname{mk}$ applied to the set of types of $x$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{Func}$ applied to $x$.
PSet.insertdefMathlib.SetTheory.ZFC.PSet, function or constantEnglish
Let $x$ and $y$ be sets. Then $\operatorname{insert}$ applied to $x$ and $y$ is a set.
PSet.ofNatdefMathlib.SetTheory.ZFC.PSet, function or constantWording
the set of x (from the name)
English
Let $x$ be a natural number. Then the set of $x$ is a set defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PSet\_\_ofNat\_\_\_f}$.
PSet.omegadefMathlib.SetTheory.ZFC.PSet, function or constantWording
the omega (from the name)
English
The omega is a set defined as $\operatorname{mk}$ applied to $\mathrm{ULift}$ applied to $\Natural$ and the function that maps $n$ to the set of $\operatorname{down}$ applied to $n$.
PSet.powersetdefMathlib.SetTheory.ZFC.PSet, function or constantWording
the powerset of x (from the name)
English
Let $x$ be a set. Then the powerset of $x$ is a set defined as $\operatorname{mk}$ applied to the power set of the set of types of $x$ and the function that maps $p$ to $\operatorname{mk}$ applied to the set of elements of $p$ and the function that maps $y$ to the function of $x$ and $y$.
PSet.sUniondefMathlib.SetTheory.ZFC.PSet, function or constantWording
the union of a (from the name)
English
Let $a$ be a set. Then the union of $a$ is a set.
PSet.sepdefMathlib.SetTheory.ZFC.PSet, function or constantEnglish
Let $p$ be a function from sets to propositions. Let $x$ be a set. Then $\operatorname{sep}$ applied to $p$ and $x$ is a set defined as $\operatorname{mk}$ applied to $\SubtypeSet {a}{p (\operatorname{Func} (x , a))}$ and the function that maps $y$ to the function of $x$ and $y$.
PSet.toSetdefMathlib.SetTheory.ZFC.PSet, function or constantWording
the set of u (from the name)
English
Let $u$ be a set. Then the set of $u$ is an element of the power set of the set of sets defined as $\operatorname{ofPred}$ applied to the function that maps $x$ to $\MembershipmemMACRoT {u}{x}$.
PSet.rankdefMathlib.SetTheory.ZFC.Rank, function or constantWording
the ordinal rank of x (from the docstring)
English
Let $x$ be a set. Then the ordinal rank of $x$ is an ordinal defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{PSet\_\_rank\_\_\_f}$.
ZFSet.rankdefMathlib.SetTheory.ZFC.Rank, function or constantWording
the ordinal rank of x (from the docstring)
English
Let $x$ be an element of $\mathrm{ZFSet}$. Then the ordinal rank of $x$ is an ordinal defined as $\operatorname{lift}$ applied to $\operatorname{rank}$, the function that maps $x$ and $x_{1}$ to $\mathrm{PSet\_\_rank\_congr}$ and $x$.
ZFSet.vonNeumanndefMathlib.SetTheory.ZFC.VonNeumann, function or constantEnglish
Let $o$ be an ordinal. Then $\operatorname{vonNeumann}$ applied to $o$ is an element of $\mathrm{ZFSet}$.