Definitions: Mathlib.Basic

168 definitions of 35 modules, Mathlib.Basic.Complex.Basic to Mathlib.Basic.UnivLE. ‹ previous next ›

Mathlib.Basic.Complex.Basic

ComplexstructureMathlib.Basic.Complex.Basic, type
Wording
complex (from the name)
English
The complexes are a basic type.
Complex.IdefMathlib.Basic.Complex.Basic, function or constant
Wording
no wording
English
$\operatorname{I}$ is a complex defined as $\operatorname{mk}$ applied to $0$ and $1$.
Complex.I_pow_eq_pow_mod'defMathlib.Basic.Complex.Basic, function or constant
Wording
no wording
English
$\operatorname{Simproc}$.
Complex.RectangledefMathlib.Basic.Complex.Basic, function or constant
Wording
the rectangle of z and w (from the name)
English
Let $z$ and $w$ be complexes. Then the rectangle of $z$ and $w$ is an element of the power set of the set of complexes defined as the product of the closed interval of the real part of $z$ and the real part of $w$ and the closed interval of the imaginary part of $z$ and the imaginary part of $w$.
Complex.equivRealProddefMathlib.Basic.Complex.Basic, function or constant
Wording
the equivalence real product (from the name)
English
The equivalence real product is an equivalence from the set of complexes to $\mathrm{Prod}$ applied to $\Real$ and $\Real$.
Complex.equivRealProdAddHomdefMathlib.Basic.Complex.Basic, function or constant
Wording
the equivalence real product additive homomorphism (from the name)
English
The equivalence real product additive homomorphism is an additive equivalence of the set of complexes and $\mathrm{Prod}$ applied to $\Real$ and $\Real$.
Complex.imdefMathlib.Basic.Complex.Basic, function or constant
Wording
the imaginary part of self (from the docstring)
English
Let $\mathrm{self}$ be a complex. Then the imaginary part of $\mathrm{self}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Complex.imAddGroupHomdefMathlib.Basic.Complex.Basic, function or constant
Wording
the imaginary part additive group homomorphism (from the name)
English
The imaginary part additive group homomorphism is an additive monoid homomorphism of the set of complexes and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{im}$ and $\mathrm{Complex\_\_zero\_im}$ and $\mathrm{Complex\_\_add\_im}$.
Complex.normSqdefMathlib.Basic.Complex.Basic, function or constant
Wording
the norm squared function (from the docstring)
English
The norm squared function is a monoid with zero homomorphism of the set of complexes and $\Real$.
Complex.ofRealdefMathlib.Basic.Complex.Basic, function or constant
Wording
the natural inclusion of the real numbers into the complex numbers of r (from the docstring)
English
Let $r$ be a real number. Then the natural inclusion of the real numbers into the complex numbers of $r$ is a complex defined as $\operatorname{mk}$ applied to $r$ and $0$.
Complex.ofRealHomdefMathlib.Basic.Complex.Basic, function or constant
Wording
the complex (from the name)
English
The complex is a ring homomorphism of $\Real$ and the set of complexes defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $x$ to the natural inclusion of the real numbers into the complex numbers of $x$ and $\mathrm{Complex\_\_ofReal\_one}$ and $\mathrm{Complex\_\_ofReal\_mul}$, $\mathrm{Complex\_\_ofReal\_zero}$ and $\mathrm{Complex\_\_ofReal\_add}$.
Complex.redefMathlib.Basic.Complex.Basic, function or constant
Wording
the real part of self (from the docstring)
English
Let $\mathrm{self}$ be a complex. Then the real part of $\mathrm{self}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Complex.reAddGroupHomdefMathlib.Basic.Complex.Basic, function or constant
Wording
the real part additive group homomorphism (from the name)
English
The real part additive group homomorphism is an additive monoid homomorphism of the set of complexes and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{re}$ and $\mathrm{Complex\_\_zero\_re}$ and $\mathrm{Complex\_\_add\_re}$.
Complex.reProdImdefMathlib.Basic.Complex.Basic, function or constant
Wording
the product of s and t (from the docstring)
English
Let $s$ and $t$ be elements of $\wp \Real$. Then the product of $s$ and $t$ is an element of the power set of the set of complexes defined as $\operatorname{inter}$ applied to the preimage of $\operatorname{re}$ and $s$ and the preimage of $\operatorname{im}$ and $t$.

Mathlib.Basic.Countable.Defs

CountableclassMathlib.Basic.Countable.Defs, predicate
Wording
x is countable (from the name)
English
Let $x$ be a set. Then we can say that $x$ is countable.
UncountableclassMathlib.Basic.Countable.Defs, predicate
Wording
x is uncountable (from the name)
English
Let $x$ be a set. Then we can say that $x$ is uncountable.

Mathlib.Basic.Denumerable

DenumerableclassMathlib.Basic.Denumerable, predicate
Wording
x is denumerable (from the name)
English
Let $x$ be a set. Then we can say that $x$ is denumerable.
Denumerable.equiv₂defMathlib.Basic.Denumerable, function or constant
Wording
the equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalence of $x$ and $x_{1}$ is an equivalence from $x$ to $x_{1}$ defined as the composition of $\operatorname{eqv}$ applied to $x$ and the inverse of $\operatorname{eqv}$ applied to $x_{1}$.
Denumerable.eqvdefMathlib.Basic.Denumerable, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\operatorname{eqv}$ applied to $x$ is an equivalence from $x$ to $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{encode}$, $\operatorname{ofNat}$ applied to $x$, $\mathrm{Denumerable\_\_ofNat\_encode}$ and $\mathrm{Denumerable\_\_encode\_ofNat}$.
Denumerable.ofNatdefMathlib.Basic.Denumerable, function or constant
Wording
no wording
English
Let $x$ be a set. Let $n$ be a natural number. Then $\operatorname{ofNat}$ applied to $x$ and $n$ is an element of $x$ defined as $\operatorname{get}$ applied to the decode of $n$ and $\mathrm{Denumerable\_\_decode\_isSome}$ applied to $x$ and $n$.
Denumerable.pairdefMathlib.Basic.Denumerable, function or constant
Wording
the pair (from the name)
English
The pair is an element of $\EquivMACRoAE {\mathrm{Prod} (x , x)}{x}$ defined as the equivalence of $\mathrm{Prod}$ applied to $x$ and $x$ and $x$.
Nat.Subtype.ofNatdefMathlib.Basic.Denumerable, function or constant
Wording
the subtype of s and x1 (from the name)
English
Let $s$ be an element of $\wp \Natural$. Let $x_{1}$ be a natural number. Then the subtype of $s$ and $x_{1}$ is an element of $s$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Nat\_\_Subtype\_\_ofNat\_\_\_f}$ applied to $s$.
Nat.Subtype.succdefMathlib.Basic.Denumerable, function or constant
Wording
the successor of x1 (from the name)
English
Let $x_{1}$ be an element of $s$. Then the successor of $x_{1}$ is an element of $s$ defined as $x_{1} + \operatorname{find} (\mathrm{Nat\_\_Subtype\_\_exists\_succ} (x_{1}))+ 1$.

Mathlib.Basic.ENNReal.Basic

ENNRealdefMathlib.Basic.ENNReal.Basic, type
Wording
no wording
English
An element of $\mathrm{ENNReal}$ is an element of $\mathrm{WithTop}$ applied to $\mathrm{NNReal}$.
ENNReal.neTopEquivNNRealdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
$\operatorname{neTopEquivNNReal}$ is an equivalence from the set of elements of $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $a$ is distinct from the top to $\mathrm{NNReal}$.
ENNReal.ofNNRealdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{NNReal}$. Then $\operatorname{ofNNReal}$ applied to $x$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{some}$ applied to $x$.
ENNReal.ofNNRealHomdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
$\operatorname{ofNNRealHom}$ is a ring homomorphism of $\mathrm{NNReal}$ and $\mathrm{ENNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{some}$ and $\mathrm{ENNReal\_\_coe\_one}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{ENNReal\_\_coe\_mul}$ applied to $x$ and $x_{1}$, $\mathrm{ENNReal\_\_coe\_zero}$ and the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{ENNReal\_\_coe\_add}$ applied to $x_{2}$ and $x_{3}$.
ENNReal.ofRealdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
Let $r$ be a real number. Then $\operatorname{ofReal}$ applied to $r$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofNNReal}$ applied to $\operatorname{toNNReal}$ applied to $r$.
ENNReal.recTopCoedefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
Let $\mathrm{top}$ be an element of $C$ applied to the top. Let $\mathrm{coe}$ be a function from elements $x_{1}$ of $\mathrm{NNReal}$ to elements of $C$ applied to $\operatorname{ofNNReal}$ applied to $x_{1}$. Let $x$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{recTopCoe}$ applied to $\mathrm{top}$, $x_{1}$, $\mathrm{coe}$ and $x$ is an element of $C$ applied to $x$ defined as the function that maps $x$ to $\operatorname{recTopCoe}$ applied to $\mathrm{top}$, $x_{1}$, $\mathrm{coe}$ and $x$.
ENNReal.toNNRealdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{toNNReal}$ applied to $x$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{untopD}$ applied to $0$ and $x$.
ENNReal.toRealdefMathlib.Basic.ENNReal.Basic, function or constant
Wording
no wording
English
Let $a$ be an element of $\mathrm{ENNReal}$. Then $\operatorname{toReal}$ applied to $a$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{toNNReal}$ applied to $a$.

Mathlib.Basic.ENNReal.Holder

ENNReal.HolderConjugatedefMathlib.Basic.ENNReal.Holder, predicate
Wording
p is a Holder conjugate with respect to q (from the name)
English
Let $p$ and $q$ be elements of $\mathrm{ENNReal}$. Then $p$ is a Holder conjugate with respect to $q$, if $\operatorname{HolderTriple}$ holds for $p$, $q$ and $1$.
ENNReal.HolderTripleclassMathlib.Basic.ENNReal.Holder, predicate
Wording
no wording
English
Let $p$ and $q$ be elements of $\mathrm{ENNReal}$. Let $r$ be an element of $\mathrm{semiOutParam}$ applied to $\mathrm{ENNReal}$. Then we can say that $\operatorname{HolderTriple}$ holds for $p$, $q$ and $r$.

Mathlib.Basic.ENNReal.Inv

ENNReal.mulLeftOrderIsodefMathlib.Basic.ENNReal.Inv, function or constant
Wording
the multiplicative left order isomorphism of a and ha (from the name)
English
Let $a$ be an element of $\mathrm{ENNReal}$ such that $a$ is a unit. Then the multiplicative left order isomorphism of $a$ and $\mathrm{ha}$ is an order isomorphism of $\mathrm{ENNReal}$ and $\mathrm{ENNReal}$.
ENNReal.mulRightOrderIsodefMathlib.Basic.ENNReal.Inv, function or constant
Wording
the multiplicative right order isomorphism of a and ha (from the name)
English
Let $a$ be an element of $\mathrm{ENNReal}$ such that $a$ is a unit. Then the multiplicative right order isomorphism of $a$ and $\mathrm{ha}$ is an order isomorphism of $\mathrm{ENNReal}$ and $\mathrm{ENNReal}$.
ENNReal.orderIsoIicCoedefMathlib.Basic.ENNReal.Inv, function or constant
Wording
no wording
English
Let $a$ be an element of $\mathrm{NNReal}$. Then $\operatorname{orderIsoIicCoe}$ applied to $a$ is an order isomorphism of the set of elements of $\operatorname{Iic}$ applied to $\operatorname{ofNNReal}$ applied to $a$ and the set of elements of $\operatorname{Iic}$ applied to $a$.
ENNReal.orderIsoIicOneBirationaldefMathlib.Basic.ENNReal.Inv, function or constant
Wording
no wording
English
$\operatorname{orderIsoIicOneBirational}$ is an order isomorphism of $\mathrm{ENNReal}$ and the set of elements of $\operatorname{Iic}$ applied to $1$.
ENNReal.orderIsoUnitIntervalBirationaldefMathlib.Basic.ENNReal.Inv, function or constant
Wording
no wording
English
$\operatorname{orderIsoUnitIntervalBirational}$ is an order isomorphism of $\mathrm{ENNReal}$ and the set of elements of $\SetIccMACRoP {0}{1}$ defined as the composition of $\operatorname{orderIsoIicOneBirational}$ and the composition of $\operatorname{orderIsoIicCoe}$ applied to $1$ and the inverse of the order isomorphism closed interval zero coercion of $1$.
OrderIso.invENNRealdefMathlib.Basic.ENNReal.Inv, function or constant
Wording
the inverse map (from the docstring)
English
The inverse map is an order isomorphism of $\mathrm{ENNReal}$ and the set of order duals of $\mathrm{ENNReal}$ defined as $\operatorname{mk}$ applied to the composition of the inverse of $\mathrm{ENNReal}$ and the dual and the function that maps $x$ and $x_{1}$ to $\mathrm{ENNReal\_\_inv\_le\_inv}$.

Mathlib.Basic.ENNReal.Real

ENNReal.toNNRealHomdefMathlib.Basic.ENNReal.Real, function or constant
Wording
the nonnegative real homomorphism (from the name)
English
The nonnegative real homomorphism is a monoid with zero homomorphism of $\mathrm{ENNReal}$ and $\mathrm{NNReal}$.
ENNReal.toRealHomdefMathlib.Basic.ENNReal.Real, function or constant
Wording
the real homomorphism (from the name)
English
The real homomorphism is a monoid with zero homomorphism of $\mathrm{ENNReal}$ and $\Real$ defined as the composition of the monoid with zero homomorphism of the real homomorphism and the nonnegative real homomorphism.

Mathlib.Basic.ExistsUnique

ExistsUniquedefMathlib.Basic.ExistsUnique, predicate
Wording
no wording
English
Let $p$ be a function from elements of $x$ to propositions. Then $\mathrm{ExistsUnique}$ holds for $p$, if there exists an element $x_{1}$ of $x$, such that $p$ holds for $x_{1}$ and for all elements $y$ of $x$, if $p$ holds for $y$, then $\EqtMACRoH {y}{x_{1}}$.
Mathlib.Notation.isExplicitBinderSingulardefMathlib.Basic.ExistsUnique, function or constant
Wording
no wording
English
generation took over the time limit

Mathlib.Basic.Finite.Defs

FiniteclassMathlib.Basic.Finite.Defs, predicate
Wording
x is finite (from the name)
English
Let $x$ be a set. Then we can say that $x$ is finite.
InfiniteclassMathlib.Basic.Finite.Defs, predicate
Wording
x is infinite (from the name)
English
Let $x$ be a set. Then we can say that $x$ is infinite.
Set.FinitedefMathlib.Basic.Finite.Defs, predicate
Wording
s is finite (from the docstring)
English
Let $s$ be an element of $\wp x$. Then $s$ is finite, if the set of elements of $s$ is finite.
Set.InfinitedefMathlib.Basic.Finite.Defs, predicate
Wording
s is infinite (from the docstring)
English
Let $s$ be an element of $\wp x$. Then $s$ is infinite, if $s$ is not finite.

Mathlib.Basic.FunLike.Basic

DFunLikeclassMathlib.Basic.FunLike.Basic, predicate
Wording
no wording
English
Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $x_{1}$ be an element of $\mathrm{outParam}$ applied to the set of functions from elements of $x$ to sets. Then we can say that $\mathrm{DFunLike}$ holds for $F$, $x$ and $x_{1}$.
DFunLike.coedefMathlib.Basic.FunLike.Basic, function or constant
Wording
the coercion of x2 and a (from the name)
English
Let $x_{2}$ be an element of $F$. Let $a$ be an element of $x$. Then the coercion of $x_{2}$ and $a$ is an element of $x_{1}$ applied to $a$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $a$.
FunLikedefMathlib.Basic.FunLike.Basic, type
Wording
no wording
English
Let $F$, $x$ and $x_{1}$ be sets. Then an element of $\mathrm{FunLike}$ applied to $F$, $x$ and $x_{1}$ is an element of the function that maps $F$, $x$ and $x_{1}$ to $\mathrm{DFunLike}$ applied to $F$, $x$ and the function that maps $x_{2}$ to $x_{1}$.

Mathlib.Basic.FunLike.Embedding

EmbeddingLikeclassMathlib.Basic.FunLike.Embedding, predicate
Wording
no wording
English
Let $F$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{EmbeddingLike}$ holds for $F$, $x$ and $x_{1}$.

Mathlib.Basic.FunLike.Equiv

EquivLikeclassMathlib.Basic.FunLike.Equiv, predicate
Wording
no wording
English
Let $E$ be a set. Let $x$ and $x_{1}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{EquivLike}$ holds for $E$, $x$ and $x_{1}$.
EquivLike.coedefMathlib.Basic.FunLike.Equiv, function or constant
Wording
the coercion to a function in the forward direction of x2 and x3 (from the docstring)
English
Let $x_{2}$ be an element of $E$. Let $x_{3}$ be an element of $x$. Then the coercion to a function in the forward direction of $x_{2}$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.
EquivLike.invdefMathlib.Basic.FunLike.Equiv, function or constant
Wording
the inverse of x2 and x3 (from the name)
English
Let $x_{2}$ be an element of $E$. Let $x_{3}$ be an element of $x_{1}$. Then the inverse of $x_{2}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$, $x_{2}$ and $x_{3}$.

Mathlib.Basic.IsEmpty.Defs

IsEmptyclassMathlib.Basic.IsEmpty.Defs, predicate
Wording
x is empty (from the name)
English
Let $x$ be a set. Then we can say that $x$ is empty.
IsEmpty.elimdefMathlib.Basic.IsEmpty.Defs, function or constant
Wording
the eliminator of h and a (from the name)
English
Assume that $x$ is empty. Let $a$ be an element of $x$. Then the eliminator of $h$ and $a$ is an element of $p$ applied to $a$ defined as $\mathrm{isEmptyElim}$ applied to $a$.
IsEmpty.elim'defMathlib.Basic.IsEmpty.Defs, function or constant
Wording
the eliminator of h and a (from the name)
English
Assume that $x$ is empty. Let $a$ be an element of $x$. Then the eliminator of $h$ and $a$ is an element of $x_{1}$ defined as $\mathrm{falseE}$ applied to $x_{1}$ and $\operatorname{false}$ applied to $a$.
isEmptyElimdefMathlib.Basic.IsEmpty.Defs, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Then $\mathrm{isEmptyElim}$ applied to $a$ is an element of $p$ applied to $a$ defined as $\mathrm{falseE}$ applied to $p$ applied to $a$ and $\operatorname{false}$ applied to $a$.

Mathlib.Basic.Logic.Basic

Classical.byContradiction'defMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
Assume that it is not the case that for all elements $x_{1}$ of $x$, we have a contradiction. Then $\operatorname{byContradiction'}$ applied to $H$ is an element of $x$.
Classical.choice_of_byContradiction'defMathlib.Basic.Logic.Basic, function or constant
Wording
the choice of contra and h (from the name)
English
Let $\mathrm{contra}$ be a function from elements of $\mathrm{Proof}$ applied to the proposition that it is not the case that for all elements $x_{1}$ of $x$, we have a contradiction to elements of $x$. Assume that $\mathrm{Nonempty}$ holds for $x$. Then the choice of $\mathrm{contra}$ and $h$ is an element of $x$ defined as $\mathrm{contra}$ applied to $\operatorname{elim}$ applied to $h$.
Classical.existsCasesdefMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
Let $H_{0}$ be an element of $C$. Let $H$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $p$ applied to $a$ to elements of $C$. Then $\operatorname{existsCases}$ applied to $H_{0}$, $a$ and $H$ is an element of $C$ defined as the function that maps $H$ to $\mathrm{dite}$ applied to the proposition that there exists an element $a$ of $x$, such that $p$ holds for $a$, the function that maps $h$ to $a$ applied to $\operatorname{choose}$ applied to $h$ and $\mathrm{Classical\_\_choose\_spec}$ applied to $h$, the function that maps $h_{1}$ to $H_{0}$ and $H$.
Exists.classicalRecOndefMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
Assume that there exists an element $a_{1}$ of $x$, such that $p$ holds for $a_{1}$. Let $H$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $p$ applied to $a$ to elements of $C$. Then $\operatorname{classicalRecOn}$ applied to $h$, $a$ and $H$ is an element of $C$ defined as the function that maps $H$ to $a$ applied to $\operatorname{choose}$ applied to $h$, $\mathrm{Classical\_\_choose\_spec}$ applied to $h$ and $H$.
FactclassMathlib.Basic.Logic.Basic, predicate
Wording
p is a fact (from the name)
English
Let $p$ be a proposition. Then we can say that $p$ is a fact.
Function.swap₂defMathlib.Basic.Logic.Basic, function or constant
Wording
the swap of x11 and x12 (from the name)
English
Let $f$ be a function from elements $x_{9}$ of $x$ and elements $x_{10}$ of $x_{2}$ applied to $x_{9}$ and elements $x_{11}$ of $x_{1}$ and elements $x_{12}$ of $x_{3}$ applied to $x_{11}$ to elements of $x_{4}$ applied to $x_{9}$, $x_{10}$, $x_{11}$ and $x_{12}$. Let $x_{5}$ be an element of $x_{1}$. Let $x_{6}$ be an element of $x_{3}$ applied to $x_{5}$. Let $x_{7}$ be an element of $x$. Let $x_{8}$ be an element of $x_{2}$ applied to $x_{7}$. Then the swap of $x_{12}$ and $f$ is an element of $x_{4}$ applied to $x_{7}$, $x_{8}$, $x_{5}$ and $x_{6}$ defined as the function that maps $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$ to $x_{9}$ applied to $x_{12}$, $f$, $x_{10}$, $x_{11}$, $x_{5}$, $x_{6}$, $x_{7}$ and $x_{8}$.
LibraryNote.decidable_argumentsdefMathlib.Basic.Logic.Basic, function or constant
Wording
the decidable argument (from the name)
English
The decidable argument is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.
LibraryNote.decidable_namespacedefMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
$\mathrm{LibraryNote\_\_decidable\_namespace}$ is an element of $\operatorname{LibraryNote}$ defined as $\operatorname{default}$.
XordefMathlib.Basic.Logic.Basic, predicate
Wording
no wording
English
Let $a$ and $b$ be propositions. Then $\mathrm{Xor}$ holds for $a$ and $b$, if $a$ and it is not the case that $b$ or $b$ and it is not the case that $a$.
eqCommdefMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
$\operatorname{Simproc}$.
iffCommdefMathlib.Basic.Logic.Basic, function or constant
Wording
no wording
English
$\operatorname{Simproc}$.

Mathlib.Basic.NNReal.Defs

NNRealdefMathlib.Basic.NNReal.Defs, type
Wording
no wording
English
An element of $\mathrm{NNReal}$ is an element of $\SubtypeSet {r}{\mathrm{Leq} (0 , r)}$.
NNReal.gidefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
$\operatorname{gi}$ is a Galois insertion of $\operatorname{toNNReal}$ and $\operatorname{toReal}$ defined as the monotone intro of $\mathrm{Real\_\_le\_coe\_toNNReal}$ and the function that maps $x$ to $\mathrm{Real\_\_toNNReal\_coe}$.
NNReal.mkdefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
Let $x$ be a real number such that $0 \leq x$. Then $\operatorname{mk}$ applied to $x$ and $\mathrm{hx}$ is an element of $\mathrm{NNReal}$ defined as $x$.
NNReal.orderIsoIccZeroCoedefMathlib.Basic.NNReal.Defs, function or constant
Wording
the order isomorphism closed interval zero coercion of a (from the name)
English
Let $a$ be an element of $\mathrm{NNReal}$. Then the order isomorphism closed interval zero coercion of $a$ is an order isomorphism of the set of elements of $\SetIccMACRoP {0}{\operatorname{toReal} (a)}$ and the set of elements of $\operatorname{Iic}$ applied to $a$.
NNReal.recToNNRealdefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
Let $\mathrm{mk}$ be a function from real numbers $x$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (0 , x)$ to elements of $C$ applied to $\operatorname{toNNReal}$ applied to $x$. Let $t$ be an element of $\mathrm{NNReal}$. Then $\operatorname{recToNNReal}$ applied to $x$, $\mathrm{mk}$ and $t$ is an element of $C$ applied to $t$.
NNReal.toRealdefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{NNReal}$. Then $\operatorname{toReal}$ applied to $x$ is a real number defined as $\mathrm{Leq} (0 , x)$.
NNReal.toRealHomdefMathlib.Basic.NNReal.Defs, function or constant
Wording
the real homomorphism (from the name)
English
The real homomorphism is a ring homomorphism of $\mathrm{NNReal}$ and $\Real$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toReal}$ and $\mathrm{NNReal\_\_coe\_one}$ and $\mathrm{NNReal\_\_coe\_mul}$, $\mathrm{NNReal\_\_coe\_zero}$ and $\mathrm{NNReal\_\_coe\_add}$.
Real.nnabsdefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
$\operatorname{nnabs}$ is a monoid with zero homomorphism of $\Real$ and $\mathrm{NNReal}$.
Real.toNNRealdefMathlib.Basic.NNReal.Defs, function or constant
Wording
no wording
English
Let $r$ be a real number. Then $\operatorname{toNNReal}$ applied to $r$ is an element of $\mathrm{NNReal}$.

Mathlib.Basic.Nonempty

Classical.arbitrarydefMathlib.Basic.Nonempty, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\operatorname{arbitrary}$ applied to $x$ is an element of $x$ defined as $\operatorname{choice}$ applied to $h$.
Nonempty.somedefMathlib.Basic.Nonempty, function or constant
Wording
no wording
English
Assume that $\mathrm{Nonempty}$ holds for $x$. Then $\operatorname{some}$ applied to $h$ is an element of $x$ defined as $\operatorname{choice}$ applied to $h$.

Mathlib.Basic.Nontrivial.Basic

nontrivialPSumUniquedefMathlib.Basic.Nontrivial.Basic, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\mathrm{nontrivialPSumUnique}$ applied to $x$ is an element of $\mathrm{PSum}$ applied to the proposition that $x$ is nontrivial and the proposition that $x$ is unique.

Mathlib.Basic.Nontrivial.Defs

NontrivialclassMathlib.Basic.Nontrivial.Defs, predicate
Wording
x is nontrivial (from the name)
English
Let $x$ be a set. Then we can say that $x$ is nontrivial.

Mathlib.Basic.Opposite

OppositestructureMathlib.Basic.Opposite, type
Wording
opposite of x (from the name)
English
Let $x$ be a set. Then the opposites of $x$ are a basic type.
Opposite.equivToOppositedefMathlib.Basic.Opposite, function or constant
Wording
the equivalence to opposite (from the name)
English
The equivalence to opposite is an equivalence from $x$ to the set of opposites of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{op}$, $\operatorname{unop}$, $\mathrm{Opposite\_\_unop\_op}$ and $\mathrm{Opposite\_\_op\_unop}$.
Opposite.unopdefMathlib.Basic.Opposite, function or constant
Wording
the opposite of self (from the name)
English
Let $\mathrm{self}$ be an opposite of $x$. Then the opposite of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Basic.PEquiv

Equiv.toPEquivdefMathlib.Basic.PEquiv, function or constant
Wording
the equivalence of f (from the name)
English
Let $f$ be an equivalence from $x$ to $x_{1}$. Then the equivalence of $f$ is an equivalence of $x$ and $x_{1}$.
PEquivstructureMathlib.Basic.PEquiv, type
Wording
equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the equivalences of $x$ and $x_{1}$ are a basic type.
PEquiv.invFundefMathlib.Basic.PEquiv, function or constant
Wording
the inverse function of self and x2 (from the name)
English
Let $\mathrm{self}$ be an equivalence of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then the inverse function of $\mathrm{self}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
PEquiv.ofSetdefMathlib.Basic.PEquiv, function or constant
Wording
the equivalence of s (from the name)
English
Let $s$ be an element of $\wp x$. Then the equivalence of $s$ is an equivalence of $x$ and $x$.
PEquiv.refldefMathlib.Basic.PEquiv, function or constant
Wording
the identity map of x (from the docstring)
English
Let $x$ be a set. Then the identity map of $x$ is an equivalence of $x$ and $x$.
PEquiv.singledefMathlib.Basic.PEquiv, function or constant
Wording
no wording
English
Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then $\operatorname{single}$ applied to $a$ and $b$ is an equivalence of $x$ and $x_{1}$.
PEquiv.symmdefMathlib.Basic.PEquiv, function or constant
Wording
the inverse partial equivalence of f (from the docstring)
English
Let $f$ be an equivalence of $x$ and $x_{1}$. Then the inverse partial equivalence of $f$ is an equivalence of $x_{1}$ and $x$.
PEquiv.toFundefMathlib.Basic.PEquiv, function or constant
Wording
the equivalence of self and x2 (from the name)
English
Let $\mathrm{self}$ be an equivalence of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then the equivalence of $\mathrm{self}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
PEquiv.transdefMathlib.Basic.PEquiv, function or constant
Wording
the composition of f and g (from the name)
English
Let $f$ be an equivalence of $x$ and $x_{1}$. Let $g$ be an equivalence of $x_{1}$ and $x_{2}$. Then the composition of $f$ and $g$ is an equivalence of $x$ and $x_{2}$.

Mathlib.Basic.Real.Basic

IsPowMuldefMathlib.Basic.Real.Basic, predicate
Wording
f is a power product (from the name)
English
Let $f$ be a function from elements of $R$ to real numbers. Then $f$ is a power product, if for all elements $a$ of $R$, for all natural numbers $n$, if $1 \leq n$, then $f (a ^ {n})= f (a)^ {n}$.
RealstructureMathlib.Basic.Real.Basic, type
Wording
no wording
English
$\Real$ is a set.
Real.cauchydefMathlib.Basic.Real.Basic, function or constant
Wording
the underlying Cauchy completion of self (from the docstring)
English
Let $\mathrm{self}$ be a real number. Then the underlying Cauchy completion of $\mathrm{self}$ is an element of $\operatorname{Cauchy}$ applied to $\mathrm{abs}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Real.equivCauchydefMathlib.Basic.Real.Basic, function or constant
Wording
no wording
English
$\operatorname{equivCauchy}$ is an equivalence from $\Real$ to $\operatorname{Cauchy}$ applied to $\mathrm{abs}$.
Real.mkdefMathlib.Basic.Real.Basic, function or constant
Wording
no wording
English
Let $x$ be an element of $\mathrm{CauSeq}$ applied to $\Rational$ and $\mathrm{abs}$. Then $\operatorname{mk}$ applied to $x$ is a real number defined as $\operatorname{ofCauchy}$ applied to $\operatorname{mk}$ applied to $x$.
Real.ringEquivCauchydefMathlib.Basic.Real.Basic, function or constant
Wording
no wording
English
$\operatorname{ringEquivCauchy}$ is a ring isomorphism of $\Real$ and $\operatorname{Cauchy}$ applied to $\mathrm{abs}$.
RingHom.IsBoundedWrtdefMathlib.Basic.Real.Basic, predicate
Wording
no wording
English
Let $x_{4}$ be a function from elements of $x$ to real numbers. Let $x_{5}$ be a function from elements of $x_{2}$ to real numbers. Let $f$ be a ring homomorphism of $x$ and $x_{2}$. Then $\operatorname{IsBoundedWrt}$ holds for $x_{4}$, $x_{5}$ and $f$, if there exists a real number $C$, such that $0 < C$ and for all elements $x_{6}$ of $x$, $x_{5} (f (x_{6}))\leq C \times x_{4} (x_{6})$.

Mathlib.Basic.Real.ConjExponents

ENNReal.conjExponentdefMathlib.Basic.Real.ConjExponents, function or constant
Wording
the conjugate exponent of p (from the docstring)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Then the conjugate exponent of $p$ is an element of $\mathrm{ENNReal}$ defined as $1 + \operatorname{inv} (p - 1)$.
NNReal.HolderConjugatedefMathlib.Basic.Real.ConjExponents, predicate
Wording
p is a Holder conjugate with respect to q (from the name)
English
Let $p$ and $q$ be elements of $\mathrm{NNReal}$. Then $p$ is a Holder conjugate with respect to $q$, if $\operatorname{HolderTriple}$ holds for $p$, $q$ and $1$.
NNReal.HolderTriplestructureMathlib.Basic.Real.ConjExponents, predicate
Wording
no wording
English
Let $p$, $q$ and $r$ be elements of $\mathrm{NNReal}$. Then we can say that $\operatorname{HolderTriple}$ holds for $p$, $q$ and $r$.
NNReal.conjExponentdefMathlib.Basic.Real.ConjExponents, function or constant
Wording
the conjugate exponent of p (from the docstring)
English
Let $p$ be an element of $\mathrm{NNReal}$. Then the conjugate exponent of $p$ is an element of $\mathrm{NNReal}$ defined as $\frac{ p}{p - 1}$.
Real.HolderConjugatedefMathlib.Basic.Real.ConjExponents, predicate
Wording
p is a Holder conjugate with respect to q (from the name)
English
Let $p$ and $q$ be real numbers. Then $p$ is a Holder conjugate with respect to $q$, if $\operatorname{HolderTriple}$ holds for $p$, $q$ and $1$.
Real.HolderTriplestructureMathlib.Basic.Real.ConjExponents, predicate
Wording
no wording
English
Let $p$, $q$ and $r$ be real numbers. Then we can say that $\operatorname{HolderTriple}$ holds for $p$, $q$ and $r$.
Real.conjExponentdefMathlib.Basic.Real.ConjExponents, function or constant
Wording
the conjugate exponent of p (from the docstring)
English
Let $p$ be a real number. Then the conjugate exponent of $p$ is a real number defined as $\frac{ p}{p - 1}$.

Mathlib.Basic.Real.ENatENNReal

ENat.toENNRealdefMathlib.Basic.Real.ENatENNReal, function or constant
Wording
no wording
English
Let $x$ be a natural number. Then $\operatorname{toENNReal}$ applied to $x$ is an element of $\mathrm{ENNReal}$ defined as the map of $\operatorname{toNatCast}$ and $x$.
ENat.toENNRealOrderEmbeddingdefMathlib.Basic.Real.ENatENNReal, function or constant
Wording
no wording
English
$\operatorname{toENNRealOrderEmbedding}$ is an order embedding of the set of natural numbers and $\mathrm{ENNReal}$ defined as $\operatorname{withTopMap}$ applied to the cast order embedding.
ENat.toENNRealRingHomdefMathlib.Basic.Real.ENatENNReal, function or constant
Wording
no wording
English
$\operatorname{toENNRealRingHom}$ is a ring homomorphism of the set of natural numbers and $\mathrm{ENNReal}$.

Mathlib.Basic.Real.Embedding

Archimedean.embedRealdefMathlib.Basic.Real.Embedding, function or constant
Wording
no wording
English
Let $M$ be a set. Then $\operatorname{embedReal}$ applied to $M$ is an order additive monoid homomorphism of $M$ and $\Real$.
Archimedean.embedRealFundefMathlib.Basic.Real.Embedding, function or constant
Wording
the embed real function of x3 (from the name)
English
Let $x_{3}$ be an element of $M$. Then the embed real function of $x_{3}$ is a real number defined as the supremum of $\operatorname{ratLt'}$ applied to $x_{3}$.
Archimedean.ratLtdefMathlib.Basic.Real.Embedding, function or constant
Wording
no wording
English
Let $x_{3}$ be an element of $M$. Then $\operatorname{ratLt}$ applied to $x_{3}$ is an element of $\wp \Rational$ defined as $\operatorname{ofPred}$ applied to the function that maps $r$ to $\mathrm{Lt} (\HSMulhSMulMACRoAL {\operatorname{num} (r)}{1}, \HSMulhSMulMACRoAL {\operatorname{den} (r)}{x_{3}})$.
Archimedean.ratLt'defMathlib.Basic.Real.Embedding, function or constant
Wording
no wording
English
Let $x_{3}$ be an element of $M$. Then $\operatorname{ratLt'}$ applied to $x_{3}$ is an element of $\wp \Real$ defined as the image of $\operatorname{coe}$ applied to the cast homomorphism of $\Real$ and $\operatorname{ratLt}$ applied to $x_{3}$.

Mathlib.Basic.Real.Sign

Real.signdefMathlib.Basic.Real.Sign, function or constant
Wording
the sign of r (from the name)
English
Let $r$ be a real number. Then the sign of $r$ is a real number defined as $\iteMACRoG {\mathrm{Lt} (r , 0)}{\operatorname{neg} (1)}{(\iteMACRoG {\mathrm{Lt} (0 , r)}{1}{0})}$.

Mathlib.Basic.Rel

Function.graphdefMathlib.Basic.Rel, function or constant
Wording
the graph of f (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the graph of $f$ is a set relation of $x$ and $x_{1}$.
Function.tupleGraphdefMathlib.Basic.Rel, function or constant
Wording
the tuple graph of f (from the name)
English
Let $f$ be a function from functions from elements of $x$ to elements of $x_{1}$ to elements of $x_{1}$. Then the tuple graph of $f$ is an element of $\wp (\mathrm{Elem} (\mathrm{Option} (x))\rightarrow x_{1})$ defined as $\operatorname{ofPred}$ applied to the function that maps $v$ to $\EqtMACRoH {f (\operatorname{comp} (v , \operatorname{some}))}{v (\operatorname{none})}$.
ReldefMathlib.Basic.Rel, type
Wording
relation of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then a relation of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of functions from elements of $x$ and elements of $x_{1}$ to propositions.
SetReldefMathlib.Basic.Rel, type
Wording
set relation of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then a set relation of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to $\wp \mathrm{Prod} (x , x_{1})$.
SetRel.HomdefMathlib.Basic.Rel, type
Wording
homomorphism of R and S (from the name)
English
Let $R$ be a set relation of $x$ and $x$. Let $S$ be a set relation of $x_{1}$ and $x_{1}$. Then a homomorphism of $R$ and $S$ is an element of the function that maps $R$ and $S$ to the set of relation homomorphisms of the function that maps $x_{2}$ and $x_{3}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{2}}{x_{3}})}$ and the function that maps $x_{4}$ and $x_{5}$ to $\MembershipmemMACRoT {S}{(\ProdmkMACRoU {x_{4}}{x_{5}})}$.
SetRel.IsIrrefldefMathlib.Basic.Rel, predicate
Wording
no wording
English
Let $R$ be a set relation of $x$ and $x$. Then $\operatorname{IsIrrefl}$ holds for $R$, if the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{1}}{x_{2}})}$ is irreflexive.
SetRel.IsRefldefMathlib.Basic.Rel, predicate
Wording
R is a identity (from the name)
English
Let $R$ be a set relation of $x$ and $x$. Then $R$ is an identity, if the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{1}}{x_{2}})}$ is reflexive.
SetRel.IsSymmdefMathlib.Basic.Rel, predicate
Wording
R is inverse (from the name)
English
Let $R$ be a set relation of $x$ and $x$. Then $R$ is inverse, if the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{1}}{x_{2}})}$ is symmetric.
SetRel.IsTransdefMathlib.Basic.Rel, predicate
Wording
R is a composition (from the name)
English
Let $R$ be a set relation of $x$ and $x$. Then $R$ is a composition, if the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{1}}{x_{2}})}$ is transitive.
SetRel.IsWellFoundeddefMathlib.Basic.Rel, predicate
Wording
no wording
English
Let $R$ be a set relation of $x$ and $x$. Then $\operatorname{IsWellFounded}$ holds for $R$, if $\mathrm{WellFounded}$ holds for the function that maps $x_{1}$ and $x_{2}$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {x_{1}}{x_{2}})}$.
SetRel.balldefMathlib.Basic.Rel, function or constant
Wording
the ball of R and b (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $b$ be an element of $x_{1}$. Then the ball of $R$ and $b$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to $\MembershipmemMACRoT {R}{(\ProdmkMACRoU {a}{b})}$.
SetRel.coddefMathlib.Basic.Rel, function or constant
Wording
the codomain of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the codomain of $R$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that there exists an element $a$ of $x$, such that $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.compdefMathlib.Basic.Rel, function or constant
Wording
the composition of R and S (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $S$ be a set relation of $x_{1}$ and $x_{2}$. Then the composition of $R$ and $S$ is a set relation of $x$ and $x_{2}$.
SetRel.coredefMathlib.Basic.Rel, function or constant
Wording
no wording
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $t$ be an element of $\wp x_{1}$. Then $\operatorname{core}$ 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 $\ProdmkMACRoU {a}{b}$ is an element of $R$, then $b$ is an element of $t$.
SetRel.domdefMathlib.Basic.Rel, function or constant
Wording
the domain of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the domain of $R$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that there exists an element $b$ of $x_{1}$, such that $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.iddefMathlib.Basic.Rel, function or constant
Wording
the identity relation (from the docstring)
English
The identity relation is a set relation of $x$ and $x$.
SetRel.imagedefMathlib.Basic.Rel, function or constant
Wording
the image of R and s (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then the image of $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 there exists an element $a$ of $x$, such that $a$ is an element of $s$ and $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.invdefMathlib.Basic.Rel, function or constant
Wording
the inverse of R (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Then the inverse of $R$ is a set relation of $x_{1}$ and $x$ defined as the preimage of $\operatorname{swap}$ and $R$.
SetRel.preimagedefMathlib.Basic.Rel, function or constant
Wording
the preimage of R and t (from the name)
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $t$ be an element of $\wp x_{1}$. Then the preimage of $R$ and $t$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that there exists an element $b$ of $x_{1}$, such that $b$ is an element of $t$ and $\ProdmkMACRoU {a}{b}$ is an element of $R$.
SetRel.restrictDomaindefMathlib.Basic.Rel, function or constant
Wording
no wording
English
Let $R$ be a set relation of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{restrictDomain}$ applied to $R$ and $s$ is a set relation of the set of elements of $s$ and $x_{1}$.
SetRel.symmetrizedefMathlib.Basic.Rel, function or constant
Wording
no wording
English
Let $R$ be a set relation of $x$ and $x$. Then $\operatorname{symmetrize}$ applied to $R$ is a set relation of $x$ and $x$ defined as $\operatorname{inter}$ applied to $R$ and the inverse of $R$.

Mathlib.Basic.Rel.Cover

SetRel.IsCoverdefMathlib.Basic.Rel.Cover, predicate
Wording
no wording
English
Let $U$ be a set relation of $X$ and $X$. Let $s$ and $N$ be elements of $\wp X$. Then $\operatorname{IsCover}$ holds for $U$, $s$ and $N$, if for all elements $x$ of $X$, if $x$ is an element of $s$, then there exists an element $y$ of $X$, such that $y$ is an element of $N$ and $\ProdmkMACRoU {x}{y}$ is an element of $U$.

Mathlib.Basic.Rel.Separated

SetRel.IsSeparateddefMathlib.Basic.Rel.Separated, predicate
Wording
no wording
English
Let $R$ be a set relation of $X$ and $X$. Let $s$ be an element of $\wp X$. Then $\operatorname{IsSeparated}$ holds for $R$ and $s$, if $\operatorname{Pairwise}$ holds for $s$ and the function that maps $x$ and $y$ to the proposition that $\ProdmkMACRoU {x}{y}$ is not an element of $R$.

Mathlib.Basic.SProd

SProdclassMathlib.Basic.SProd, predicate
Wording
x2 is a product (from the name)
English
Let $x$ and $x_{1}$ be sets. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $x_{2}$ is a product.
SProd.sproddefMathlib.Basic.SProd, function or constant
Wording
no wording
English
Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $x_{1}$. Then $\operatorname{sprod}$ applied to $x_{3}$ and $x_{4}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$, $x_{3}$ and $x_{4}$.

Mathlib.Basic.SetLike.Basic

IsConcreteLEclassMathlib.Basic.SetLike.Basic, predicate
Wording
no wording
English
Let $A$ be a set. Let $B$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{IsConcreteLE}$ holds for $A$ and $B$.
SetLikeclassMathlib.Basic.SetLike.Basic, predicate
Wording
no wording
English
Let $A$ be a set. Let $B$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SetLike}$ holds for $A$ and $B$.
SetLike.coedefMathlib.Basic.SetLike.Basic, function or constant
Wording
the coercion of x (from the docstring)
English
Let $x$ be an element of $A$. Then the coercion of $x$ is an element of $\wp B$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x$.

Mathlib.Basic.Sign.Basic

SignType.castHomdefMathlib.Basic.Sign.Basic, function or constant
Wording
the cast homomorphism (from the name)
English
The cast homomorphism is a monoid with zero homomorphism of the set of sign types and $x$.
signHomdefMathlib.Basic.Sign.Basic, function or constant
Wording
the sign homomorphism (from the name)
English
The sign homomorphism is a monoid with zero homomorphism of $x$ and the set of sign types.

Mathlib.Basic.Sign.Defs

SignTypeinductiveMathlib.Basic.Sign.Defs, type
Wording
sign type (from the name)
English
The sign types are a basic type.
SignType.LEinductiveMathlib.Basic.Sign.Defs, predicate
Wording
no wording
English
Let $x$ and $x_{1}$ be sign types. Then we can say that $\operatorname{LE}$ holds for $x$ and $x_{1}$.
SignType.castdefMathlib.Basic.Sign.Defs, function or constant
Wording
the cast of x4 (from the name)
English
Let $x_{4}$ be a sign type. Then the cast of $x_{4}$ is an element of $x$.
SignType.ctorElimTypedefMathlib.Basic.Sign.Defs, type
Wording
no wording
English
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{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the negation and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the positive part.
SignType.enumListdefMathlib.Basic.Sign.Defs, function or constant
Wording
no wording
English
$\operatorname{enumList}$ is a list of sign types defined as $\operatorname{cons}$ applied to the zero and $\operatorname{cons}$ applied to the negation and $\operatorname{cons}$ applied to the positive part and $\operatorname{nil}$.
SignType.fin3EquivdefMathlib.Basic.Sign.Defs, function or constant
Wording
the finite equivalence (from the name)
English
The finite equivalence is a multiplicative equivalence of the set of sign types and $\mathrm{Fin}$ applied to $3$.
SignType.negconstructorMathlib.Basic.Sign.Defs, function or constant
Wording
the negation (from the name)
English
The negation is a sign type.
SignType.ofNatdefMathlib.Basic.Sign.Defs, function or constant
Wording
the sign type of x (from the name)
English
Let $x$ be a natural number. Then the sign type of $x$ is a sign type defined as $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $0$, the zero and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $x$ and $1$, the negation and the positive part.
SignType.posconstructorMathlib.Basic.Sign.Defs, function or constant
Wording
the positive part (from the name)
English
The positive part is a sign type.
SignType.signdefMathlib.Basic.Sign.Defs, function or constant
Wording
the sign (from the docstring)
English
The sign is an order homomorphism of $x$ and the set of sign types.
SignType.zeroconstructorMathlib.Basic.Sign.Defs, function or constant
Wording
the zero (from the name)
English
The zero is a sign type.
instInhabitedSignType.defaultdefMathlib.Basic.Sign.Defs, function or constant
Wording
the default (from the name)
English
The default is a sign type defined as the zero.

Mathlib.Basic.TwoPointing

TwoPointingstructureMathlib.Basic.TwoPointing, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\mathrm{TwoPointing}$ applied to $x$ are a basic type.
TwoPointing.booldefMathlib.Basic.TwoPointing, function or constant
Wording
the bool (from the name)
English
The bool is an element of $\mathrm{TwoPointing}$ applied to $\mathrm{Bool}$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {\operatorname{false}}{\operatorname{true}}$ and $\mathrm{Bool\_\_false\_ne\_true}$.
TwoPointing.pidefMathlib.Basic.TwoPointing, function or constant
Wording
the product of x and q (from the name)
English
Let $x$ be a set. Let $q$ be an element of $\mathrm{TwoPointing}$ applied to $x_{1}$. Then the product of $x$ and $q$ is an element of $\mathrm{TwoPointing}$ applied to the set of functions from elements of $x$ to elements of $x_{1}$.
TwoPointing.proddefMathlib.Basic.TwoPointing, function or constant
Wording
the product of p and q (from the name)
English
Let $p$ be an element of $\mathrm{TwoPointing}$ applied to $x$. Let $q$ be an element of $\mathrm{TwoPointing}$ applied to $x_{1}$. Then the product of $p$ and $q$ is an element of $\mathrm{TwoPointing}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
TwoPointing.propdefMathlib.Basic.TwoPointing, function or constant
Wording
no wording
English
$\operatorname{prop}$ is an element of $\mathrm{TwoPointing}$ applied to the set of propositions defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {\mathrm{false}}{\mathrm{True}}$ and $\mathrm{false\_ne\_true}$.
TwoPointing.sumdefMathlib.Basic.TwoPointing, function or constant
Wording
the sum of p and q (from the name)
English
Let $p$ be an element of $\mathrm{TwoPointing}$ applied to $x$. Let $q$ be an element of $\mathrm{TwoPointing}$ applied to $x_{1}$. Then the sum of $p$ and $q$ is an element of $\mathrm{TwoPointing}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$.
TwoPointing.swapdefMathlib.Basic.TwoPointing, function or constant
Wording
the swap of p (from the name)
English
Let $p$ be an element of $\mathrm{TwoPointing}$ applied to $x$. Then the swap of $p$ is an element of $\mathrm{TwoPointing}$ applied to $x$ defined as $\operatorname{mk}$ applied to $\ProdmkMACRoU {\ProdsndMACRoAA {\operatorname{toProd} (p)}}{\ProdfstMACRoZ {\operatorname{toProd} (p)}}$ and $\mathrm{TwoPointing\_\_snd\_ne\_fst}$ applied to $p$.

Mathlib.Basic.Unique

UniqueclassMathlib.Basic.Unique, predicate
Wording
x is unique (from the name)
English
Let $x$ be a set. Then we can say that $x$ is unique.
uniqueElimdefMathlib.Basic.Unique, function or constant
Wording
the unique eliminator of x3 and i (from the name)
English
Let $x_{3}$ be an element of $x_{1}$ applied to $\operatorname{default}$. Let $i$ be an element of $x$. Then the unique eliminator of $x_{3}$ and $i$ is an element of $x_{1}$ applied to $i$.

Mathlib.Basic.UnivLE

UnivLEclassMathlib.Basic.UnivLE, predicate
Wording
no wording
English
We can say that $\mathrm{UnivLE}$.

‹ previous next ›