Definitions: Mathlib.MeasureTheory, part 2 of 2

365 definitions of 96 modules, Mathlib.MeasureTheory.MeasurableSpace.Embedding to Mathlib.MeasureTheory.VectorMeasure.WithDensityVec. ‹ previous next ›

Mathlib.MeasureTheory.MeasurableSpace.Embedding

MeasurableEmbeddingstructureMathlib.MeasureTheory.MeasurableSpace.Embedding, predicate
Wording
f is a measurable embedding (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then we can say that $f$ is a measurable embedding.
MeasurableEmbedding.equivImagedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the equivalence image of s and hf (from the name)
English
Let $s$ be an element of $\wp x$. Assume that $f$ is a measurable embedding. Then the equivalence image of $s$ and $\mathrm{hf}$ is a measurable equivalence of the set of elements of $s$ and the set of elements of the image of $f$ and $s$.
MeasurableEmbedding.equivRangedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the equivalence range of hf (from the name)
English
Assume that $f$ is a measurable embedding. Then the equivalence range of $\mathrm{hf}$ is a measurable equivalence of $x$ and the set of elements of the range of $f$.
MeasurableEmbedding.invFundefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the inverse function of hf and x4 (from the name)
English
Assume that $f$ is a measurable embedding. Let $x_{4}$ be an element of $x_{1}$. Then the inverse function of $\mathrm{hf}$ and $x_{4}$ is an element of $x$.
MeasurableEmbedding.schroederBernsteindefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Assume that $f$ is a measurable embedding. Assume that $g$ is a measurable embedding. Then $\operatorname{schroederBernstein}$ applied to $\mathrm{hf}$ and $\mathrm{hg}$ is a measurable equivalence of $x$ and $x_{1}$.
MeasurableEquivstructureMathlib.MeasureTheory.MeasurableSpace.Embedding, type
Wording
measurable equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the measurable equivalences of $x$ and $x_{1}$ are a basic type.
MeasurableEquiv.Set.proddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product of s and t (from the name)
English
Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{1}$. Then the product of $s$ and $t$ is a measurable equivalence of the set of elements of $\operatorname{sprod}$ applied to $s$ and $t$ and $\mathrm{Prod}$ applied to the set of elements of $s$ and the set of elements of $t$.
MeasurableEquiv.Set.rangeInldefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the range left injection (from the name)
English
The range left injection is a measurable equivalence of the set of elements of the range of $\operatorname{inl}$ and $x$.
MeasurableEquiv.Set.rangeInrdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the range right injection (from the name)
English
The range right injection is a measurable equivalence of the set of elements of the range of $\operatorname{inr}$ and $x_{1}$.
MeasurableEquiv.Set.singletondefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the singleton of a (from the name)
English
Let $a$ be an element of $x$. Then the singleton of $a$ is a measurable equivalence of the set of elements of $\operatorname{singleton}$ applied to $a$ and $\mathrm{Unit}$.
MeasurableEquiv.Set.univdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the universal set of x (from the name)
English
Let $x$ be a set. Then the universal set of $x$ is a measurable equivalence of the set of elements of the universal set and $x$.
MeasurableEquiv.arrowCongr'defMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the arrow congruence of x6 and x7 (from the name)
English
Let $x_{6}$ be an equivalence from $x$ to $x_{2}$. Let $x_{7}$ be a measurable equivalence of $x_{1}$ and $x_{3}$. Then the arrow congruence of $x_{6}$ and $x_{7}$ is a measurable equivalence of the set of functions from elements of $x$ to elements of $x_{1}$ and the set of functions from elements of $x_{2}$ to elements of $x_{3}$.
MeasurableEquiv.arrowProdEquivProdArrowdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the arrow product equivalence product arrow of x1 and x2 (from the name)
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then the arrow product equivalence product arrow of $x_{1}$ and $x_{2}$ is a measurable equivalence of the set of functions from elements of $x_{2}$ to elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to the set of functions from elements of $x_{2}$ to elements of $x$ and the set of functions from elements of $x_{2}$ to elements of $x_{1}$.
MeasurableEquiv.castdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the cast of h and hi (from the name)
English
Assume that $\EqtMACRoH {x}{x_{1}}$. Assume that $\mathrm{HEq}$ holds for $x_{2}$ and $x_{3}$. Then the cast of $h$ and $\mathrm{hi}$ is a measurable equivalence of $x$ and $x_{1}$.
MeasurableEquiv.currydefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the curry of x1 and X (from the name)
English
Let $x$, $x_{1}$ and $X$ be sets. Then the curry of $x_{1}$ and $X$ is a measurable equivalence of the set of functions from elements of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to elements of $X$ and the set of functions from elements of $x$ and elements of $x_{1}$ to elements of $X$.
MeasurableEquiv.finTwoArrowdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
$\operatorname{finTwoArrow}$ is a measurable equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $x$ and $\mathrm{Prod}$ applied to $x$ and $x$ defined as $\operatorname{piFinTwo}$ applied to the function that maps $x_{2}$ to $x$.
MeasurableEquiv.funUniquedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x$ and $x_{1}$ be sets. Then $\operatorname{funUnique}$ applied to $x$ and $x_{1}$ is a measurable equivalence of the set of functions from elements of $x$ to elements of $x_{1}$ and $x_{1}$ defined as $\operatorname{piUnique}$ applied to the function that maps $x_{4}$ to $x_{1}$.
MeasurableEquiv.ofInvolutivedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the measurable equivalence of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x$ such that $f$ is involutive and measurable. Then the measurable equivalence of $f$ is a measurable equivalence of $x$ and $x$ defined as $\operatorname{mk}$ applied to the permutation of $f$ and $\mathrm{hf}$, $\mathrm{hf'}$ and $\mathrm{hf'}$.
MeasurableEquiv.ofUniqueOfUniquedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the measurable equivalence of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be sets. Then the measurable equivalence of $x$ and $x_{1}$ is a measurable equivalence of $x$ and $x_{1}$.
MeasurableEquiv.piCongrLeftdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the left product congruence of x2 and f (from the name)
English
Let $x_{2}$ be a function from elements of $x_{1}$ to sets. Let $f$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $x_{2}$ and $f$ is a measurable equivalence of the set of functions from elements $b$ of $x$ to elements of $x_{2}$ applied to $f$ applied to $b$ and the set of functions from elements $a$ of $x_{1}$ to elements of $x_{2}$ applied to $a$.
MeasurableEquiv.piCongrRightdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the right product congruence of e (from the name)
English
Let $e$ be a function from elements $a_{2}$ of $x$ to measurable equivalences of $x_{1}$ applied to $a_{2}$ and $x_{2}$ applied to $a_{2}$. Then the right product congruence of $a_{2}$ is a measurable equivalence of the set of functions from elements $a$ of $x$ to elements of $x_{1}$ applied to $a$ and the set of functions from elements $a_{1}$ of $x$ to elements of $x_{2}$ applied to $a_{1}$.
MeasurableEquiv.piCurrydefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the currying operation of X (from the docstring)
English
Let $X$ be a function from elements $i_{2}$ of $x$ and elements of $x_{1}$ applied to $i_{2}$ to sets. Then the currying operation of $i_{2}$ is a measurable equivalence of the set of functions from elements $p$ of $\Sigma$ applied to the function that maps $i$ to $x_{1}$ applied to $i$ to elements of $X$ applied to $\operatorname{fst}$ applied to $p$ and $\operatorname{snd}$ applied to $p$ and the set of functions from elements $i_{1}$ of $x$ and elements $j$ of $x_{1}$ applied to $i_{1}$ to elements of $X$ applied to $i_{1}$ and $j$.
MeasurableEquiv.piEquivPiSubtypeProddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product equivalence product subtype product of x1 and p (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Let $p$ be a function from elements of $x$ to propositions. Then the product equivalence product subtype product of $x_{1}$ and $p$ is a measurable equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{4}}{p (x_{4})}$ to elements of $x_{1}$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {i_{3}}{\mathrm{not} (p (i_{3}))}$ to elements of $x_{1}$ applied to $i_{2}$.
MeasurableEquiv.piFinSuccAbovedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $n + 1$ to sets. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{piFinSuccAbove}$ applied to $x$ and $i$ is a measurable equivalence of the set of functions from elements $j$ of $\mathrm{Fin}$ applied to $n + 1$ to elements of $x$ applied to $j$ and $\mathrm{Prod}$ applied to $x$ applied to $i$ and the set of functions from elements $j_{1}$ of $\mathrm{Fin}$ applied to $n$ to elements of $x$ applied to $\operatorname{succAbove}$ applied to $i$ and $j_{1}$.
MeasurableEquiv.piFinTwodefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $x$ is a measurable equivalence of the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $2$ to elements of $x$ applied to $i$ and $\mathrm{Prod}$ applied to $x$ applied to $0$ and $x$ applied to $1$.
MeasurableEquiv.piFinsetUniondefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product finite set union of x1 and h (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Assume that $s$ is disjoint to $t$. Then the product finite set union of $x_{1}$ and $h$ is a measurable equivalence of $\mathrm{Prod}$ applied to the set of functions from elements $i$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ to elements of $x_{1}$ applied to $i$ and the set of functions from elements $i_{1}$ of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {t}{x_{5}})}$ to elements of $x_{1}$ applied to $i_{1}$ and the set of functions from elements $i_{2}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {(\UnionunionMACRoAB {s}{t})}{x_{6}})}$ to elements of $x_{1}$ applied to $i_{2}$ defined as the composition of the inverse of the sum product equivalence product product of the function that maps $b$ to $x_{1}$ applied to $\operatorname{union}$ applied to $s$, $t$, $h$ and $b$ and the left product congruence of the function that maps $i$ to $x_{1}$ applied to $i$ and the union of $s$ and $t$.
MeasurableEquiv.piMeasurableEquivTProddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product measurable equivalence product of hnd and h (from the name)
English
Assume that $\operatorname{Nodup}$ holds for $l$. Assume that for all elements $i_{1}$ of $x$, $i_{1}$ is an element of $l$. Then the product measurable equivalence product of $\mathrm{hnd}$ and $h$ is a measurable equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the set of products of $x_{1}$ and $l$ defined as $\operatorname{mk}$ applied to the product equivalence product of $\mathrm{hnd}$ and $h$, $\mathrm{measurable\_tProd\_mk}$ applied to $l$ and $\mathrm{measurable\_tProd\_elim'}$ applied to $h$.
MeasurableEquiv.piOptionEquivProddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product option equivalence product of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $\mathrm{Option}$ applied to $x$ to sets. Then the product option equivalence product of $x_{1}$ is a measurable equivalence of the set of functions from elements $i$ of $\mathrm{Option}$ applied to $x$ to elements of $x_{1}$ applied to $i$ and $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $\operatorname{some}$ applied to $i_{1}$ and $x_{1}$ applied to $\operatorname{none}$ defined as the composition of the inverse of the left product congruence of $x_{1}$ and the inverse of the option equivalence sum unit of $x$ and the composition of the sum product equivalence product product of the function that maps $i$ to $x_{1}$ applied to $\operatorname{symm}$ applied to the option equivalence sum unit of $x$ and $i$ and the product congruence of the identity of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $\operatorname{symm}$ applied to the option equivalence sum unit of $x$ and $\operatorname{inl}$ applied to $i_{1}$ and $\operatorname{piUnique}$ applied to the function that maps $i_{2}$ to $x_{1}$ applied to $\operatorname{symm}$ applied to the option equivalence sum unit of $x$ and $\operatorname{inr}$ applied to $i_{2}$.
MeasurableEquiv.piUniquedefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x_{1}$ be a function from elements of $x$ to sets. Then $\operatorname{piUnique}$ applied to $x_{1}$ is a measurable equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $x_{1}$ applied to $\operatorname{default}$.
MeasurableEquiv.prodAssocdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product associator (from the name)
English
The product associator is a measurable equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
MeasurableEquiv.prodCommdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
$\operatorname{prodComm}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$.
MeasurableEquiv.prodCongrdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product congruence of ab and cd (from the name)
English
Let $\mathrm{ab}$ be a measurable equivalence of $x$ and $x_{1}$. Let $\mathrm{cd}$ be a measurable equivalence of $x_{2}$ and $x_{3}$. Then the product congruence of $\mathrm{ab}$ and $\mathrm{cd}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.
MeasurableEquiv.prodPUnitdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the product unit (from the name)
English
The product unit is a measurable equivalence of $\mathrm{Prod}$ applied to $x$ and $\mathrm{PUnit}$ and $x$ defined as $\operatorname{mk}$ applied to the product unit of $x$, $\mathrm{measurable\_fst}$ and $\mathrm{measurable\_prodMk\_right}$.
MeasurableEquiv.prodSumDistribdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{prodSumDistrib}$ applied to $x$, $x_{1}$ and $x_{2}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{2}$ defined as the composition of $\operatorname{prodComm}$ and the composition of $\operatorname{sumProdDistrib}$ applied to $x_{1}$, $x_{2}$ and $x$ and the sum congruence of $\operatorname{prodComm}$ and $\operatorname{prodComm}$.
MeasurableEquiv.punitProddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
$\operatorname{punitProd}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $\mathrm{PUnit}$ and $x$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{punitProd}$ applied to $x$, $\mathrm{measurable\_snd}$ and $\mathrm{measurable\_prodMk\_left}$.
MeasurableEquiv.refldefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the identity of x (from the name)
English
Let $x$ be a set. Then the identity of $x$ is a measurable equivalence of $x$ and $x$.
MeasurableEquiv.setOfPreddefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the set (from the name)
English
The set is a measurable equivalence of the set of functions from elements of $x$ to propositions and $\wp x$.
MeasurableEquiv.subtypePiEquivPidefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the subtype product equivalence product (from the name)
English
The subtype product equivalence product is a measurable equivalence of $\SubtypeSet {f}{\mathrm{forall} (x , \lambda a . p (a , f (a)))}$ and the set of functions from elements $a_{1}$ of $x$ to elements of $\SubtypeSet {b}{p (a_{1} , b)}$.
MeasurableEquiv.sumCompldefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the sum complement of hs (from the name)
English
Assume that $s$ is a measurable set. Then the sum complement of $\mathrm{hs}$ is a measurable equivalence of $\mathrm{Sum}$ applied to the set of elements of $s$ and the set of elements of the complement of $s$ and $x$.
MeasurableEquiv.sumCongrdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the sum congruence of ab and cd (from the name)
English
Let $\mathrm{ab}$ be a measurable equivalence of $x$ and $x_{1}$. Let $\mathrm{cd}$ be a measurable equivalence of $x_{2}$ and $x_{3}$. Then the sum congruence of $\mathrm{ab}$ and $\mathrm{cd}$ is a measurable equivalence of $\mathrm{Sum}$ applied to $x$ and $x_{2}$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{3}$.
MeasurableEquiv.sumPiEquivProdPidefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the sum product equivalence product product of x2 (from the name)
English
Let $x_{2}$ be a function from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to sets. Then the sum product equivalence product product of $x_{2}$ is a measurable equivalence of the set of functions from elements $i$ of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to elements of $x_{2}$ applied to $i$ and $\mathrm{Prod}$ applied to the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $\operatorname{inl}$ applied to $i_{1}$ and the set of functions from elements $\mathrm{i'}$ of $x_{1}$ to elements of $x_{2}$ applied to $\operatorname{inr}$ applied to $\mathrm{i'}$.
MeasurableEquiv.sumProdDistribdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
no wording
English
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{sumProdDistrib}$ applied to $x$, $x_{1}$ and $x_{2}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
MeasurableEquiv.sumProdSumdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the sum product sum of x2 and x3 (from the name)
English
Let $x$, $x_{1}$, $x_{2}$ and $x_{3}$ be sets. Then the sum product sum of $x_{2}$ and $x_{3}$ is a measurable equivalence of $\mathrm{Prod}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$ and $\mathrm{Sum}$ applied to $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $x_{3}$ and $\mathrm{Sum}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$ defined as the composition of $\operatorname{sumProdDistrib}$ applied to $x$, $x_{1}$ and $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$ and the sum congruence of $\operatorname{prodSumDistrib}$ applied to $x$, $x_{2}$ and $x_{3}$ and $\operatorname{prodSumDistrib}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$.
MeasurableEquiv.symmdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the inverse of ab (from the docstring)
English
Let $\mathrm{ab}$ be a measurable equivalence of $x$ and $x_{1}$. Then the inverse of $\mathrm{ab}$ is a measurable equivalence of $x_{1}$ and $x$.
MeasurableEquiv.transdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the composition of ab and bc (from the name)
English
Let $\mathrm{ab}$ be a measurable equivalence of $x$ and $x_{1}$. Let $\mathrm{bc}$ be a measurable equivalence of $x_{1}$ and $x_{2}$. Then the composition of $\mathrm{ab}$ and $\mathrm{bc}$ is a measurable equivalence of $x$ and $x_{2}$.
MeasurableEquiv.uliftdefMathlib.MeasureTheory.MeasurableSpace.Embedding, function or constant
Wording
the lift (from the name)
English
The lift is a measurable equivalence of $\mathrm{ULift}$ applied to $x$ and $x$ defined as $\operatorname{mk}$ applied to the lift, $\mathrm{measurable\_down}$ and $\mathrm{measurable\_up}$.

Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

EventuallyMeasurabledefMathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable, predicate
Wording
f is eventually measurable with respect to l (from the name)
English
generation took over the time limit
EventuallyMeasurableSetdefMathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable, predicate
Wording
s is a eventually measurable set with respect to l (from the name)
English
generation took over the time limit

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Filter.IsMeasurablyGeneratedclassMathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated, predicate
Wording
no wording
English
Let $f$ be a filter of $x$. Then we can say that $\operatorname{IsMeasurablyGenerated}$ holds for $f$.

Mathlib.MeasureTheory.Measure.AEDisjoint

MeasureTheory.AEDisjointdefMathlib.MeasureTheory.Measure.AEDisjoint, predicate
Wording
s is almost everywhere disjoint to t (from the name)
English
Let $x_{1}$ be a measure of $x$. Let $s$ and $t$ be elements of $\wp x$. Then $s$ is almost everywhere disjoint to $t$, if $\EqtMACRoH {x_{1} (\operatorname{inter} (s , t))}{0}$.

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

MeasureTheory.Measure.AbsolutelyContinuousdefMathlib.MeasureTheory.Measure.AbsolutelyContinuous, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Then $\operatorname{AbsolutelyContinuous}$ holds for $x_{1}$ and $x_{2}$, if for all elements $s$ of $\wp x$, if $\EqtMACRoH {x_{2} (s)}{0}$, then $\EqtMACRoH {x_{1} (s)}{0}$.

Mathlib.MeasureTheory.Measure.AddContent

MeasureTheory.AddContentstructureMathlib.MeasureTheory.Measure.AddContent, type
Wording
additive content of G and C (from the name)
English
Let $G$ be a set. Let $C$ be an element of $\wp (\wp x)$. Then the additive contents of $G$ and $C$ are a basic type.
MeasureTheory.AddContent.IsSigmaSubadditivedefMathlib.MeasureTheory.Measure.AddContent, predicate
Wording
no wording
English
Let $m$ be an additive content of $\mathrm{ENNReal}$ and $C$. Then $\operatorname{IsSigmaSubadditive}$ holds for $m$, if for all functions $f$ from natural numbers to elements of $\wp x$, if for all natural numbers $i_{3}$, $\MembershipmemMACRoT {C}{f (i_{3})}$, then if the union of the function that maps $i_{2}$ to $f$ applied to $i_{2}$ is an element of $C$, then $m$ applied to the union of the function that maps $i$ to $f$ applied to $i$ is less than or equal to the sum of the function that maps $i_{1}$ to $m$ applied to $f$ applied to $i_{1}$ and $\operatorname{unconditional}$ applied to $\Natural$.
MeasureTheory.AddContent.extenddefMathlib.MeasureTheory.Measure.AddContent, function or constant
Wording
no wording
English
Assume that $C$ is a set semiring. Let $m$ be an additive content of $\mathrm{ENNReal}$ and $C$. Then $\operatorname{extend}$ applied to $\mathrm{hC}$ and $m$ is an additive content of $\mathrm{ENNReal}$ and $C$.
MeasureTheory.AddContent.onIocdefMathlib.MeasureTheory.Measure.AddContent, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $G$. Then $\operatorname{onIoc}$ applied to $f$ is an additive content of $G$ and $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exist elements $u$ and $v$ of $x$, such that $u \leq v$ and $\EqtMACRoH {s}{\operatorname{Ioc} (u , v)}$.
MeasureTheory.AddContent.supClosuredefMathlib.MeasureTheory.Measure.AddContent, function or constant
Wording
the supremum closure of m and hC (from the name)
English
Let $m$ be an additive content of $G$ and $C$. Assume that $C$ is a set semiring. Then the supremum closure of $m$ and $\mathrm{hC}$ is an additive content of $G$ and $\operatorname{supClosure}$ applied to $C$.
MeasureTheory.AddContent.toFundefMathlib.MeasureTheory.Measure.AddContent, function or constant
Wording
the value of the content of self and x2 (from the docstring)
English
Let $\mathrm{self}$ be an additive content of $G$ and $C$. Let $x_{2}$ be an element of $\wp x$. Then the value of the content of $\mathrm{self}$ and $x_{2}$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
MeasureTheory.IsSetRing.addContent_of_uniondefMathlib.MeasureTheory.Measure.AddContent, function or constant
Wording
the additive content of m (from the name)
English
Let $m$ be a function from elements of $\wp x$ to elements of $G$. Assume that $C$ is a set ring. Assume that $\EqtMACRoH {m (\operatorname{emptyCollection})}{0}$. Assume that for all elements $s$ and $t$ of $\wp x$, if $s$ is an element of $C$, then if $t$ is an element of $C$, then if $s$ is disjoint to $t$, then $\EqtMACRoH {m (\UnionunionMACRoAB {s}{t})}{m (s)+ m (t)}$. Then the additive content of $m$ is an additive content of $G$ and $C$.

Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

BoundedContinuousFunction.innerProbChardefMathlib.MeasureTheory.Measure.CharacteristicFunction.Basic, function or constant
Wording
no wording
English
Let $t$ be an element of $E$. Then $\operatorname{innerProbChar}$ applied to $t$ is a bounded continuous function of $E$ and the set of complexes defined as the characteristic of $t$.
BoundedContinuousFunction.probCharDualdefMathlib.MeasureTheory.Measure.CharacteristicFunction.Basic, function or constant
Wording
no wording
English
Let $L$ be a strong dual of $\Real$ and $F$. Then $\operatorname{probCharDual}$ applied to $L$ is a bounded continuous function of $F$ and the set of complexes.
MeasureTheory.charFundefMathlib.MeasureTheory.Measure.CharacteristicFunction.Basic, function or constant
Wording
the characteristic function of x1 and t (from the docstring)
English
Let $x_{1}$ be a measure of $E$. Let $t$ be an element of $E$. Then the characteristic function of $x_{1}$ and $t$ is a complex defined as the Bochner integral of $x_{1}$ and the function that maps $x_{2}$ to the exponential of the product of the natural inclusion of the real numbers into the complex numbers of $\operatorname{inner}$ applied to $\Real$, $x_{2}$ and $t$ and $\operatorname{I}$.
MeasureTheory.charFunDualdefMathlib.MeasureTheory.Measure.CharacteristicFunction.Basic, function or constant
Wording
the characteristic function of x2 and L (from the docstring)
English
Let $x_{2}$ be a measure of $E$. Let $L$ be a strong dual of $\Real$ and $E$. Then the characteristic function of $x_{2}$ and $L$ is a complex defined as the Bochner integral of $x_{2}$ and the function that maps $v$ to $\operatorname{probCharDual}$ applied to $L$ and $v$.

Mathlib.MeasureTheory.Measure.Comap

MeasureTheory.Measure.comapdefMathlib.MeasureTheory.Measure.Comap, function or constant
Wording
the preimage of f and x4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a measure of $x_{1}$. Then the preimage of $f$ and $x_{4}$ is a measure of $x$.
MeasureTheory.Measure.comapₗdefMathlib.MeasureTheory.Measure.Comap, function or constant
Wording
the preimage of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the preimage of $f$ is a linear map of the set of measures of $x_{1}$ and the set of measures of $x$.

Mathlib.MeasureTheory.Measure.Complex

MeasureTheory.ComplexMeasuredefMathlib.MeasureTheory.Measure.Complex, type
Wording
complex measure of x (from the name)
English
Let $x$ be a set. Then a complex measure of $x$ is an element of the function that maps $x$ to the set of vector measures of $x$ and the set of complexes.
MeasureTheory.ComplexMeasure.equivSignedMeasuredefMathlib.MeasureTheory.Measure.Complex, function or constant
Wording
the equivalence signed measure (from the name)
English
The equivalence signed measure is an equivalence from the set of complex measures of $x$ to $\mathrm{Prod}$ applied to the set of signed measures of $x$ and the set of signed measures of $x$.
MeasureTheory.ComplexMeasure.equivSignedMeasureₗdefMathlib.MeasureTheory.Measure.Complex, function or constant
Wording
the equivalence signed measure (from the name)
English
The equivalence signed measure is a linear equivalence of the set of complex measures of $x$ and $\mathrm{Prod}$ applied to the set of signed measures of $x$ and the set of signed measures of $x$.
MeasureTheory.ComplexMeasure.imdefMathlib.MeasureTheory.Measure.Complex, function or constant
Wording
the imaginary part (from the docstring)
English
The imaginary part is a linear map of the set of complex measures of $x$ and the set of signed measures of $x$ defined as the map range of the imaginary part continuous linear map.
MeasureTheory.ComplexMeasure.redefMathlib.MeasureTheory.Measure.Complex, function or constant
Wording
the real part (from the docstring)
English
The real part is a linear map of the set of complex measures of $x$ and the set of signed measures of $x$ defined as the map range of the real part continuous linear map.
MeasureTheory.SignedMeasure.toComplexMeasuredefMathlib.MeasureTheory.Measure.Complex, function or constant
Wording
the complex measure of s and t (from the name)
English
Let $s$ and $t$ be signed measures of $x$. Then the complex measure of $s$ and $t$ is a complex measure of $x$.

Mathlib.MeasureTheory.Measure.Content

MeasureTheory.ContentstructureMathlib.MeasureTheory.Measure.Content, type
Wording
content of G (from the name)
English
Let $G$ be a set. Then the contents of $G$ are a basic type.
MeasureTheory.Content.ContentRegulardefMathlib.MeasureTheory.Measure.Content, predicate
Wording
x1 is a content regular (from the name)
English
Let $x_{1}$ be a content of $G$. Then $x_{1}$ is a content regular, if for all compacts $K$ of $G$, $x_{1}$ applied to $K$ is equal to the infimum of the function that maps $\mathrm{K'}$ to the infimum of the function that maps $h$ to $x_{1}$ applied to $\mathrm{K'}$.
MeasureTheory.Content.innerContentdefMathlib.MeasureTheory.Measure.Content, function or constant
Wording
the inner content of x1 and U (from the name)
English
Let $x_{1}$ be a content of $G$. Let $U$ be an open of $G$. Then the inner content of $x_{1}$ and $U$ is an element of $\mathrm{ENNReal}$ defined as the supremum of the function that maps $K$ to the supremum of the function that maps $h$ to $x_{1}$ applied to $K$.
MeasureTheory.Content.measuredefMathlib.MeasureTheory.Measure.Content, function or constant
Wording
the measure of x1 (from the name)
English
Let $x_{1}$ be a content of $G$. Then the measure of $x_{1}$ is a measure of $G$ defined as the measure of the outer measure of $x_{1}$ and $\mathrm{MeasureTheory\_\_Content\_\_borel\_le\_caratheodory}$ applied to $x_{1}$.
MeasureTheory.Content.outerMeasuredefMathlib.MeasureTheory.Measure.Content, function or constant
Wording
the outer measure of x1 (from the name)
English
Let $x_{1}$ be a content of $G$. Then the outer measure of $x_{1}$ is an outer measure of $G$ defined as the induced outer measure of the function that maps $U$ and $\mathrm{hU}$ to the inner content of $x_{1}$ and $\operatorname{mk}$ applied to $U$ and $\mathrm{hU}$.
MeasureTheory.Content.toFundefMathlib.MeasureTheory.Measure.Content, function or constant
Wording
the content of self and x1 (from the name)
English
Let $\mathrm{self}$ be a content of $G$. Let $x_{1}$ be a compact of $G$. Then the content of $\mathrm{self}$ and $x_{1}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.

Mathlib.MeasureTheory.Measure.Count

MeasureTheory.Measure.countdefMathlib.MeasureTheory.Measure.Count, function or constant
Wording
the count (from the name)
English
The count is a measure of $x$ defined as the sum of $\operatorname{dirac}$.

Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

MeasureTheory.Measure.sigmaFiniteSetdefMathlib.MeasureTheory.Measure.Decomposition.Exhaustion, function or constant
Wording
the sigma finite set of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the sigma finite set of $x_{2}$ is an element of $\wp x$ defined as $\operatorname{sigmaFiniteSetWRT}$ applied to $x_{2}$ and $x_{2}$.
MeasureTheory.Measure.sigmaFiniteSetGEdefMathlib.MeasureTheory.Measure.Decomposition.Exhaustion, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Let $n$ be a natural number. Then $\operatorname{sigmaFiniteSetGE}$ applied to $x_{2}$, $x_{3}$ and $n$ is an element of $\wp x$ defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_exists\_isSigmaFiniteSet\_measure\_ge}$ applied to $x_{2}$, $x_{3}$ and $n$.
MeasureTheory.Measure.sigmaFiniteSetWRTdefMathlib.MeasureTheory.Measure.Decomposition.Exhaustion, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{sigmaFiniteSetWRT}$ applied to $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as $\mathrm{dite}$ applied to the proposition that there exists an element $s$ of $\wp x$, such that $s$ is a measurable set, $\operatorname{SigmaFinite}$ holds for $\operatorname{restrict}$ applied to $x_{2}$ and $s$ and for all elements $t$ of $\wp x$, if $t$ is less than or equal to the complement of $s$, then if $x_{3} (t)\neq 0$, then $x_{2}$ applied to $t$ is equal to the top, the function that maps $h_{2}$ to $\operatorname{choose}$ applied to $h_{2}$ and the function that maps $h_{3}$ to $\operatorname{emptyCollection}$.
MeasureTheory.Measure.sigmaFiniteSetWRT'defMathlib.MeasureTheory.Measure.Decomposition.Exhaustion, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{sigmaFiniteSetWRT'}$ applied to $x_{2}$ and $x_{3}$ is an element of $\wp x$ defined as the union of the function that maps $n$ to $\operatorname{sigmaFiniteSetGE}$ applied to $x_{2}$, $x_{3}$ and $n$.

Mathlib.MeasureTheory.Measure.Decomposition.Hahn

MeasureTheory.IsHahnDecompositionstructureMathlib.MeasureTheory.Measure.Decomposition.Hahn, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Let $s$ be an element of $\wp x$. Then we can say that $\operatorname{IsHahnDecomposition}$ holds for $x_{2}$, $x_{3}$ and $s$.

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

MeasureTheory.Measure.HaveLebesgueDecompositionclassMathlib.MeasureTheory.Measure.Decomposition.Lebesgue, predicate
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Then we can say that $\operatorname{HaveLebesgueDecomposition}$ holds for $x_{1}$ and $x_{2}$.
MeasureTheory.Measure.LebesgueDecomposition.measurableLEdefMathlib.MeasureTheory.Measure.Decomposition.Lebesgue, function or constant
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Then $\operatorname{measurableLE}$ applied to $x_{1}$ and $x_{2}$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow \mathrm{ENNReal})$ defined as $\operatorname{ofPred}$ applied to the function that maps $f$ to the proposition that $f$ is measurable and for all elements $A$ of $\wp x$, if $A$ is a measurable set, then $\operatorname{lintegral} (\operatorname{restrict} (x_{1} , A), \lambda x_{3} . f (x_{3}))\leq x_{2} (A)$.
MeasureTheory.Measure.LebesgueDecomposition.measurableLEEvaldefMathlib.MeasureTheory.Measure.Decomposition.Lebesgue, function or constant
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Then $\operatorname{measurableLEEval}$ applied to $x_{1}$ and $x_{2}$ is an element of $\wp \mathrm{ENNReal}$ defined as the image of the function that maps $f$ to $\operatorname{lintegral}$ applied to $x_{1}$ and the function that maps $x_{3}$ to $f$ applied to $x_{3}$ and $\operatorname{measurableLE}$ applied to $x_{1}$ and $x_{2}$.
MeasureTheory.Measure.rnDerivdefMathlib.MeasureTheory.Measure.Decomposition.Lebesgue, function or constant
Wording
no wording
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Let $x_{3}$ be an element of $x$. Then $\operatorname{rnDeriv}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Decomposition\_\_Lebesgue\_\_3676591092\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{1}$, $x_{2}$ and $x_{3}$.
MeasureTheory.Measure.singularPartdefMathlib.MeasureTheory.Measure.Decomposition.Lebesgue, function or constant
Wording
the singular part of x1 and x2 (from the name)
English
Let $x_{1}$ and $x_{2}$ be measures of $x$. Then the singular part of $x_{1}$ and $x_{2}$ is a measure of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Decomposition\_\_Lebesgue\_\_3118627775\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{1}$ and $x_{2}$.

Mathlib.MeasureTheory.Measure.Dirac.Def

MeasureTheory.Measure.diracdefMathlib.MeasureTheory.Measure.Dirac.Def, function or constant
Wording
the Dirac of a (from the name)
English
Let $a$ be an element of $x$. Then the Dirac of $a$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.DiracProba

MeasureTheory.diracProbadefMathlib.MeasureTheory.Measure.DiracProba, function or constant
Wording
the Dirac delta mass at a point of x1 (from the docstring)
English
Let $x_{1}$ be an element of $X$. Then the Dirac delta mass at a point of $x_{1}$ is a probability measure of $X$ defined as the Dirac of $x_{1}$.
MeasureTheory.diracProbaEquivdefMathlib.MeasureTheory.Measure.DiracProba, function or constant
Wording
no wording
English
$\operatorname{diracProbaEquiv}$ is an equivalence from $X$ to the set of elements of the range of $\operatorname{diracProba}$.
MeasureTheory.diracProbaHomeomorphdefMathlib.MeasureTheory.Measure.DiracProba, function or constant
Wording
no wording
English
$\operatorname{diracProbaHomeomorph}$ is a homeomorphism of $X$ and the set of elements of the range of $\operatorname{diracProba}$ defined as $\operatorname{mk}$ applied to $\operatorname{diracProbaEquiv}$, $\mathrm{MeasureTheory\_\_continuous\_diracProbaEquiv}$ and $\mathrm{MeasureTheory\_\_continuous\_diracProbaEquivSymm}$.
MeasureTheory.diracProbaInversedefMathlib.MeasureTheory.Measure.DiracProba, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of the range of $\operatorname{diracProba}$. Then $\operatorname{diracProbaInverse}$ applied to $x_{1}$ is an element of $X$.

Mathlib.MeasureTheory.Measure.Doubling

IsUnifLocDoublingMeasureclassMathlib.MeasureTheory.Measure.Doubling, predicate
Wording
no wording
English
Let $x_{3}$ be a measure of $x$. Then we can say that $\mathrm{IsUnifLocDoublingMeasure}$ holds for $x_{3}$.
IsUnifLocDoublingMeasure.doublingConstantdefMathlib.MeasureTheory.Measure.Doubling, function or constant
Wording
the doubling constant of x3 (from the name)
English
Let $x_{3}$ be a measure of $x$. Then the doubling constant of $x_{3}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{choose}$ applied to $\mathrm{IsUnifLocDoublingMeasure\_\_exists\_measure\_closedBall\_le\_mul}$ applied to $x_{3}$.
IsUnifLocDoublingMeasure.scalingConstantOfdefMathlib.MeasureTheory.Measure.Doubling, function or constant
Wording
the scaling constant of x3 and K (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $K$ be a real number. Then the scaling constant of $x_{3}$ and $K$ is an element of $\mathrm{NNReal}$ defined as $\MaxmaxMACRoAF {\operatorname{choose} (\mathrm{IsUnifLocDoublingMeasure\_\_exists\_eventually\_forall\_measure\_closedBall\_le\_mul} (x_{3} , K))}{1}$.
IsUnifLocDoublingMeasure.scalingScaleOfdefMathlib.MeasureTheory.Measure.Doubling, function or constant
Wording
the scaling scale of x3 and K (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $K$ be a real number. Then the scaling scale of $x_{3}$ and $K$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{IsUnifLocDoublingMeasure\_\_eventually\_measure\_mul\_le\_scalingConstantOf\_mul}$ applied to $x_{3}$ and $K$.

Mathlib.MeasureTheory.Measure.EverywherePos

MeasureTheory.Measure.IsEverywherePosdefMathlib.MeasureTheory.Measure.EverywherePos, predicate
Wording
s is a everywhere positive part with respect to x3 (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $s$ is an everywhere positive part with respect to $x_{3}$, if for all elements $x_{4}$ of $x$, if $x_{4}$ is an element of $s$, then for all elements $n$ of $\wp x$, if $\MembershipmemMACRoT {\mathrm{nhdsWithin} (x_{4} , s)}{n}$, then $0 < x_{3} (n)$.
MeasureTheory.Measure.everywherePosSubsetdefMathlib.MeasureTheory.Measure.EverywherePos, function or constant
Wording
the everywhere positive subset of x3 and s (from the docstring)
English
Let $x_{3}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then the everywhere positive subset of $x_{3}$ and $s$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{4}$ to the proposition that $x_{4}$ is an element of $s$ and for all elements $n$ of $\wp x$, if $\MembershipmemMACRoT {\mathrm{nhdsWithin} (x_{4} , s)}{n}$, then $0 < x_{3} (n)$.

Mathlib.MeasureTheory.Measure.Filter

MeasureTheory.Measure.cofinitedefMathlib.MeasureTheory.Measure.Filter, function or constant
Wording
the cofinite of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the cofinite of $x_{2}$ is a filter of $x$.

Mathlib.MeasureTheory.Measure.FiniteMeasure

MeasureTheory.FiniteMeasuredefMathlib.MeasureTheory.Measure.FiniteMeasure, type
Wording
finite measure of x (from the name)
English
Let $x$ be a set. Then a finite measure of $x$ is an element of the function that maps $x$ to $\SubtypeSet {x_{2}}{\operatorname{IsFiniteMeasure} (x_{2})}$.
MeasureTheory.FiniteMeasure.comapdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the preimage of f and x4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a finite measure of $x_{1}$. Then the preimage of $f$ and $x_{4}$ is a finite measure of $x$ defined as the preimage of $f$ and the measure of $x_{4}$.
MeasureTheory.FiniteMeasure.mapdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the map of x4 and f (from the name)
English
Let $x_{4}$ be a finite measure of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $x_{4}$ and $f$ is a finite measure of $x_{1}$ defined as the map of $f$ and the measure of $x_{4}$.
MeasureTheory.FiniteMeasure.mapCLMdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the map continuous linear map of f_cont (from the name)
English
Assume that $f$ is continuous. Then the map continuous linear map of $\mathrm{f\_cont}$ is a continuous linear map of the set of finite measures of $x$ and the set of finite measures of $x_{1}$.
MeasureTheory.FiniteMeasure.mapHomdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the map homomorphism of f_mble (from the name)
English
Assume that $f$ is measurable. Then the map homomorphism of $\mathrm{f\_mble}$ is a linear map of the set of finite measures of $x$ and the set of finite measures of $x_{1}$.
MeasureTheory.FiniteMeasure.massdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the mass of x2 (from the name)
English
Let $x_{2}$ be a finite measure of $x$. Then the mass of $x_{2}$ is an element of $\mathrm{NNReal}$ defined as $x_{2}$ applied to the universal set.
MeasureTheory.FiniteMeasure.restrictdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
no wording
English
Let $x_{2}$ be a finite measure of $x$. Let $A$ be an element of $\wp x$. Then $\operatorname{restrict}$ applied to $x_{2}$ and $A$ is a finite measure of $x$ defined as $\operatorname{restrict}$ applied to the measure of $x_{2}$ and $A$.
MeasureTheory.FiniteMeasure.testAgainstNNdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
no wording
English
Let $x_{3}$ be a finite measure of $x$. Let $f$ be a bounded continuous function of $x$ and $\mathrm{NNReal}$. Then $\operatorname{testAgainstNN}$ applied to $x_{3}$ and $f$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toNNReal}$ applied to $\operatorname{lintegral}$ applied to the measure of $x_{3}$ and the function that maps $x_{4}$ to $\operatorname{ofNNReal}$ applied to $f$ applied to $x_{4}$.
MeasureTheory.FiniteMeasure.toMeasuredefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the measure of x2 (from the name)
English
Let $x_{2}$ be a finite measure of $x$. Then the measure of $x_{2}$ is a measure of $x$ defined as the proposition that $x_{2}$ is a finite measure.
MeasureTheory.FiniteMeasure.toMeasureAddMonoidHomdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
the measure additive monoid homomorphism (from the name)
English
The measure additive monoid homomorphism is an additive monoid homomorphism of the set of finite measures of $x$ and the set of measures of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toMeasure}$ and $\mathrm{MeasureTheory\_\_FiniteMeasure\_\_toMeasure\_zero}$ and $\mathrm{MeasureTheory\_\_FiniteMeasure\_\_toMeasure\_add}$.
MeasureTheory.FiniteMeasure.toWeakDualBCNNdefMathlib.MeasureTheory.Measure.FiniteMeasure, function or constant
Wording
no wording
English
Let $x_{3}$ be a finite measure of $x$. Then $\operatorname{toWeakDualBCNN}$ applied to $x_{3}$ is a weak dual of $\mathrm{NNReal}$ and the set of bounded continuous functions of $x$ and $\mathrm{NNReal}$.

Mathlib.MeasureTheory.Measure.FiniteMeasurePi

MeasureTheory.FiniteMeasure.pidefMathlib.MeasureTheory.Measure.FiniteMeasurePi, function or constant
Wording
the product of x4 (from the name)
English
Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to finite measures of $x_{1}$ applied to $i_{1}$. Then the product of $i_{1}$ is a finite measure of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ defined as the function that maps $x_{4}$ to the finite product of the measures of the function that maps $i$ to the measure of $i_{1}$ applied to $i$.
MeasureTheory.ProbabilityMeasure.pidefMathlib.MeasureTheory.Measure.FiniteMeasurePi, function or constant
Wording
the product of x4 (from the name)
English
Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to probability measures of $x_{1}$ applied to $i_{1}$. Then the product of $i_{1}$ is a probability measure of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ defined as the function that maps $x_{4}$ to the finite product of the measures of the function that maps $i$ to the measure of $i_{1}$ applied to $i$.

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

MeasureTheory.FiniteMeasure.proddefMathlib.MeasureTheory.Measure.FiniteMeasureProd, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be a finite measure of $x$. Let $x_{5}$ be a finite measure of $x_{2}$. Then the product of $x_{4}$ and $x_{5}$ is a finite measure of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ defined as the product of the measure of $x_{4}$ and the measure of $x_{5}$.
MeasureTheory.ProbabilityMeasure.proddefMathlib.MeasureTheory.Measure.FiniteMeasureProd, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be a probability measure of $x$. Let $x_{5}$ be a probability measure of $x_{2}$. Then the product of $x_{4}$ and $x_{5}$ is a probability measure of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ defined as the product of the measure of $x_{4}$ and the measure of $x_{5}$.

Mathlib.MeasureTheory.Measure.GiryMonad

MeasureTheory.Measure.binddefMathlib.MeasureTheory.Measure.GiryMonad, function or constant
Wording
no wording
English
Let $m$ be a measure of $x$. Let $f$ be a function from elements of $x$ to measures of $x_{1}$. Then $\operatorname{bind}$ applied to $m$ and $f$ is a measure of $x_{1}$ defined as the join of the map of $f$ and $m$.
MeasureTheory.Measure.joindefMathlib.MeasureTheory.Measure.GiryMonad, function or constant
Wording
the join of m (from the name)
English
Let $m$ be a measure of the set of measures of $x$. Then the join of $m$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.Haar.Basic

MeasureTheory.Measure.addHaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the additive Haar (from the name)
English
generation took over the time limit
MeasureTheory.Measure.addHaarMeasuredefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the Haar measure on the locally compact additive group of x3 (from the docstring)
English
no reading
MeasureTheory.Measure.haardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the Haar (from the name)
English
generation took over the time limit
MeasureTheory.Measure.haar.addCHaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the additive Haar of x2 and K (from the name)
English
Let $x_{2}$ be a positive compact of $G$. Let $K$ be a compact of $G$. Then the additive Haar of $x_{2}$ and $K$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_haar\_\_nonempty\_iInter\_clAddPrehaar}$ applied to $x_{2}$ and $K$.
MeasureTheory.Measure.haar.addHaarContentdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the additive Haar content of x2 (from the name)
English
Let $x_{2}$ be a positive compact of $G$. Then the additive Haar content of $x_{2}$ is a content of $G$.
MeasureTheory.Measure.haar.addHaarProductdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the additive Haar product of x2 (from the name)
English
Let $x_{2}$ be an element of $\wp G$. Then the additive Haar product of $x_{2}$ is an element of $\wp (\mathrm{Elem} (\operatorname{Compacts} (G))\rightarrow \Real)$ defined as the product of the universal set and the function that maps $K$ to $\SetIccMACRoP {0}{\operatorname{addIndex} (K , x_{2})}$.
MeasureTheory.Measure.haar.addIndexdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the additive index of K and V (from the name)
English
Let $K$ and $V$ be elements of $\wp G$. Then the additive index of $K$ and $V$ is a natural number defined as the infimum of the image of $\FinsetcardMACRoM$ and $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $K$ is less than or equal to the union of the function that maps $g$ to the union of the function that maps $h$ to the preimage of the function that maps $h_{1}$ to $g + h_{1}$ and $V$.
MeasureTheory.Measure.haar.addPrehaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
no wording
English
Let $x_{2}$ and $U$ be elements of $\wp G$. Let $K$ be a compact of $G$. Then $\operatorname{addPrehaar}$ applied to $x_{2}$, $U$ and $K$ is a real number defined as the quotient of the additive index of $K$ and $U$ and the additive index of $x_{2}$ and $U$.
MeasureTheory.Measure.haar.chaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
no wording
English
Let $x_{2}$ be a positive compact of $G$. Let $K$ be a compact of $G$. Then $\operatorname{chaar}$ applied to $x_{2}$ and $K$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_haar\_\_nonempty\_iInter\_clPrehaar}$ applied to $x_{2}$ and $K$.
MeasureTheory.Measure.haar.clAddPrehaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
no wording
English
Let $x_{2}$ be an element of $\wp G$. Let $V$ be an element of $\operatorname{OpenNhdsOf}$ applied to $0$. Then $\operatorname{clAddPrehaar}$ applied to $x_{2}$ and $V$ is an element of the power set of the set of functions from compacts of $G$ to real numbers defined as the closure of the image of $\operatorname{addPrehaar}$ applied to $x_{2}$ and $\operatorname{ofPred}$ applied to the function that maps $U$ to the proposition that $U \leq \operatorname{toOpens} (V)$, $U$ is open and $0$ is an element of $U$.
MeasureTheory.Measure.haar.clPrehaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
no wording
English
Let $x_{2}$ be an element of $\wp G$. Let $V$ be an element of $\operatorname{OpenNhdsOf}$ applied to $1$. Then $\operatorname{clPrehaar}$ applied to $x_{2}$ and $V$ is an element of the power set of the set of functions from compacts of $G$ to real numbers defined as the closure of the image of $\operatorname{prehaar}$ applied to $x_{2}$ and $\operatorname{ofPred}$ applied to the function that maps $U$ to the proposition that $U \leq \operatorname{toOpens} (V)$, $U$ is open and $1$ is an element of $U$.
MeasureTheory.Measure.haar.haarContentdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the Haar content of x2 (from the name)
English
Let $x_{2}$ be a positive compact of $G$. Then the Haar content of $x_{2}$ is a content of $G$.
MeasureTheory.Measure.haar.haarProductdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the Haar product of x2 (from the name)
English
Let $x_{2}$ be an element of $\wp G$. Then the Haar product of $x_{2}$ is an element of $\wp (\mathrm{Elem} (\operatorname{Compacts} (G))\rightarrow \Real)$ defined as the product of the universal set and the function that maps $K$ to $\SetIccMACRoP {0}{\operatorname{index} (K , x_{2})}$.
MeasureTheory.Measure.haar.indexdefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the index of K and V (from the name)
English
Let $K$ and $V$ be elements of $\wp G$. Then the index of $K$ and $V$ is a natural number defined as the infimum of the image of $\FinsetcardMACRoM$ and $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $K$ is less than or equal to the union of the function that maps $g$ to the union of the function that maps $h$ to the preimage of the function that maps $h_{1}$ to $g \times h_{1}$ and $V$.
MeasureTheory.Measure.haar.prehaardefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
no wording
English
Let $x_{2}$ and $U$ be elements of $\wp G$. Let $K$ be a compact of $G$. Then $\operatorname{prehaar}$ applied to $x_{2}$, $U$ and $K$ is a real number defined as the quotient of the index of $K$ and $U$ and the index of $x_{2}$ and $U$.
MeasureTheory.Measure.haarMeasuredefMathlib.MeasureTheory.Measure.Haar.Basic, function or constant
Wording
the Haar measure on the locally compact group of x3 (from the docstring)
English
no reading

Mathlib.MeasureTheory.Measure.Haar.DistribChar

MeasureTheory.distribHaarChardefMathlib.MeasureTheory.Measure.Haar.DistribChar, function or constant
Wording
the distributive Haar character of A (from the docstring)
English
Let $A$ be a set. Then the distributive Haar character of $A$ is a monoid homomorphism of $G$ and $\mathrm{NNReal}$.

Mathlib.MeasureTheory.Measure.Haar.Extension

TopologicalAddGroup.IsSES.inducedMeasuredefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
the induced measure of x9 and x11 (from the name)
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{9}$ be a measure of $A$. Let $x_{11}$ be a measure of $C$. Then the induced measure of $x_{9}$ and $x_{11}$ is a measure of $B$ defined as the Riesz measure of $\operatorname{mk}$ applied to $\operatorname{integrate}$ applied to $H$, $x_{9}$ and $x_{11}$ and the function that maps $x_{13}$ and $x_{14}$ to $\mathrm{TopologicalAddGroup\_\_IsSES\_\_integrate\_mono}$ applied to $H$, $x_{9}$ and $x_{11}$.
TopologicalAddGroup.IsSES.integratedefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{10}$ be a measure of $A$. Let $x_{13}$ be a measure of $C$. Then $\operatorname{integrate}$ applied to $H$, $x_{10}$ and $x_{13}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$ and $E$.
TopologicalAddGroup.IsSES.pullbackdefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
the pullback of f and b (from the name)
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$. Let $b$ be an element of $B$. Then the pullback of $f$ and $b$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $A$ and $E$ defined as the pullback additive monoid homomorphism of $f$ and $b$.
TopologicalAddGroup.IsSES.pushforwarddefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{10}$ be a measure of $A$. Then $\operatorname{pushforward}$ applied to $H$ and $x_{10}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $C$ and $E$.
TopologicalGroup.IsSES.inducedMeasuredefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
the induced measure of x9 and x11 (from the name)
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{9}$ be a measure of $A$. Let $x_{11}$ be a measure of $C$. Then the induced measure of $x_{9}$ and $x_{11}$ is a measure of $B$ defined as the Riesz measure of $\operatorname{mk}$ applied to $\operatorname{integrate}$ applied to $H$, $x_{9}$ and $x_{11}$ and the function that maps $x_{13}$ and $x_{14}$ to $\mathrm{TopologicalGroup\_\_IsSES\_\_integrate\_mono}$ applied to $H$, $x_{9}$ and $x_{11}$.
TopologicalGroup.IsSES.integratedefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{10}$ be a measure of $A$. Let $x_{13}$ be a measure of $C$. Then $\operatorname{integrate}$ applied to $H$, $x_{10}$ and $x_{13}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$ and $E$.
TopologicalGroup.IsSES.pullbackdefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
the pullback of f and b (from the name)
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $f$ be an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$. Let $b$ be an element of $B$. Then the pullback of $f$ and $b$ is an element of $\mathrm{CompactlySupportedContinuousMap}$ applied to $A$ and $E$ defined as the pullback monoid homomorphism of $f$ and $b$.
TopologicalGroup.IsSES.pushforwarddefMathlib.MeasureTheory.Measure.Haar.Extension, function or constant
Wording
no wording
English
Assume that $\operatorname{IsSES}$ holds for $x_{6}$ and $x_{7}$. Let $x_{10}$ be a measure of $A$. Then $\operatorname{pushforward}$ applied to $H$ and $x_{10}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $B$ and $E$ and $\mathrm{CompactlySupportedContinuousMap}$ applied to $C$ and $E$.

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

LinearIsometryEquiv.toMeasurableEquivdefMathlib.MeasureTheory.Measure.Haar.InnerProductSpace, function or constant
Wording
the measurable equivalence of f (from the name)
English
Let $f$ be a linear isometry equivalence of $E$ and $F$. Then the measurable equivalence of $f$ is a measurable equivalence of $E$ and $F$ defined as the measurable equivalence of the homeomorphism of $f$.
OrthonormalBasis.measurableEquivdefMathlib.MeasureTheory.Measure.Haar.InnerProductSpace, function or constant
Wording
the measurable equivalence of b (from the name)
English
Let $b$ be an orthonormal basis of $\Real$ and $F$. Then the measurable equivalence of $b$ is a measurable equivalence of $F$ and the set of Euclidean spaces of $\Real$ and $x$ defined as the measurable equivalence of the homeomorphism of the representation of $b$.

Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

MeasureTheory.addEquivAddHaarChardefMathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar, function or constant
Wording
the additive equivalence additive Haar characteristic of x3 (from the name)
English
Let $x_{3}$ be a continuous additive equivalence of $G$ and $G$. Then the additive equivalence additive Haar characteristic of $x_{3}$ is an element of $\mathrm{NNReal}$ defined as the additive Haar scalar factor of the additive Haar and the map of $\operatorname{coe}$ applied to $x_{3}$ and the additive Haar.
MeasureTheory.mulEquivHaarChardefMathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar, function or constant
Wording
the multiplicative equivalence Haar characteristic of x3 (from the name)
English
Let $x_{3}$ be a continuous multiplicative equivalence of $G$ and $G$. Then the multiplicative equivalence Haar characteristic of $x_{3}$ is an element of $\mathrm{NNReal}$ defined as the Haar scalar factor of the Haar and the map of $\operatorname{coe}$ applied to $x_{3}$ and the Haar.

Mathlib.MeasureTheory.Measure.Haar.OfBasis

Module.Basis.addHaardefMathlib.MeasureTheory.Measure.Haar.OfBasis, function or constant
Wording
the additive Haar of b (from the name)
English
Let $b$ be a basis of $\Real$ and $E$. Then the additive Haar of $b$ is a measure of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{Module\_\_Basis\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Haar\_\_OfBasis\_\_29914027\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $b$.
Module.Basis.parallelepipeddefMathlib.MeasureTheory.Measure.Haar.OfBasis, function or constant
Wording
the parallelepiped of b (from the name)
English
Let $b$ be a basis of $\Real$ and $E$. Then the parallelepiped of $b$ is a positive compact of $E$.
parallelepipeddefMathlib.MeasureTheory.Measure.Haar.OfBasis, function or constant
Wording
the closed parallelepiped spanned by a finite family of vectors of v (from the docstring)
English
Let $v$ be a function from elements of $x$ to elements of $E$. Then the closed parallelepiped spanned by a finite family of vectors of $v$ is an element of $\wp E$ defined as the image of the function that maps $t$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {t (i)}{v (i)})}$ and $\SetIccMACRoP {0}{1}$.

Mathlib.MeasureTheory.Measure.Haar.Unique

MeasureTheory.Measure.addHaarScalarFactordefMathlib.MeasureTheory.Measure.Haar.Unique, function or constant
Wording
the additive Haar scalar factor of x3 and x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be measures of $G$. Then the additive Haar scalar factor of $x_{3}$ and $x_{4}$ is an element of $\mathrm{NNReal}$ defined as $\iteMACRoG {\mathrm{not} (\mathrm{LocallyCompactSpace} (G))}{1}{\operatorname{choose} (\mathrm{MeasureTheory\_\_Measure\_\_exists\_integral\_isAddLeftInvariant\_eq\_smul\_of\_hasCompactSupport} (x_{3} , x_{4}))}$.
MeasureTheory.Measure.haarScalarFactordefMathlib.MeasureTheory.Measure.Haar.Unique, function or constant
Wording
the Haar scalar factor of x3 and x4 (from the name)
English
Let $x_{3}$ and $x_{4}$ be measures of $G$. Then the Haar scalar factor of $x_{3}$ and $x_{4}$ is an element of $\mathrm{NNReal}$ defined as $\iteMACRoG {\mathrm{not} (\mathrm{LocallyCompactSpace} (G))}{1}{\operatorname{choose} (\mathrm{MeasureTheory\_\_Measure\_\_exists\_integral\_isMulLeftInvariant\_eq\_smul\_of\_hasCompactSupport} (x_{3} , x_{4}))}$.

Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

HasOuterApproxClosedclassMathlib.MeasureTheory.Measure.HasOuterApproxClosed, predicate
Wording
no wording
English
Let $X$ be a set. Then we can say that $\mathrm{HasOuterApproxClosed}$ holds for $X$.
IsClosed.apprSeqdefMathlib.MeasureTheory.Measure.HasOuterApproxClosed, function or constant
Wording
no wording
English
Assume that $F$ is closed. Let $x_{1}$ be a natural number. Then $\operatorname{apprSeq}$ applied to $\mathrm{hF}$ and $x_{1}$ is a bounded continuous function of $X$ and $\mathrm{NNReal}$ defined as $\operatorname{choose}$ applied to $\operatorname{exAppr}$ applied to $F$ and $\mathrm{hF}$ and $x_{1}$.

Mathlib.MeasureTheory.Measure.Hausdorff

MeasureTheory.Measure.hausdorffMeasuredefMathlib.MeasureTheory.Measure.Hausdorff, function or constant
Wording
the Hausdorff measure of d (from the name)
English
Let $d$ be a real number. Then the Hausdorff measure of $d$ is a measure of $X$ defined as $\operatorname{mkMetric}$ applied to the function that maps $r$ to $r ^ {d}$.
MeasureTheory.Measure.mkMetricdefMathlib.MeasureTheory.Measure.Hausdorff, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\mathrm{ENNReal}$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{mkMetric}$ applied to $m$ is a measure of $X$.
MeasureTheory.Measure.mkMetric'defMathlib.MeasureTheory.Measure.Hausdorff, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{mkMetric'}$ applied to $m$ is a measure of $X$.
MeasureTheory.OuterMeasure.IsMetricdefMathlib.MeasureTheory.Measure.Hausdorff, predicate
Wording
x1 is metric (from the name)
English
Let $x_{1}$ be an outer measure of $X$. Then $x_{1}$ is metric, if for all elements $s$ and $t$ of $\wp X$, if $\operatorname{AreSeparated}$ holds for $s$ and $t$, then $\EqtMACRoH {x_{1} (\UnionunionMACRoAB {s}{t})}{x_{1} (s)+ x_{1} (t)}$.
MeasureTheory.OuterMeasure.mkMetricdefMathlib.MeasureTheory.Measure.Hausdorff, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\mathrm{ENNReal}$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{mkMetric}$ applied to $m$ is an outer measure of $X$ defined as $\operatorname{mkMetric'}$ applied to the function that maps $s$ to $m$ applied to $\operatorname{ediam}$ applied to $s$.
MeasureTheory.OuterMeasure.mkMetric'defMathlib.MeasureTheory.Measure.Hausdorff, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{mkMetric'}$ applied to $m$ is an outer measure of $X$ defined as the supremum of the function that maps $r$ to the supremum of the function that maps $h$ to $\operatorname{pre}$ applied to $m$ and $r$.

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

regionBetweendefMathlib.MeasureTheory.Measure.Lebesgue.Basic, function or constant
Wording
no wording
English
Let $f$ and $g$ be functions from elements of $x$ to real numbers. Let $s$ be an element of $\wp x$. Then $\mathrm{regionBetween}$ applied to $f$, $g$ and $s$ is an element of $\wp \mathrm{Prod} (x , \Real)$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that $\MembershipmemMACRoT {s}{\ProdfstMACRoZ {p}}$ and $\ProdsndMACRoAA {p}$ is an element of the open interval of $f$ applied to $\ProdfstMACRoZ {p}$ and $g$ applied to $\ProdfstMACRoZ {p}$.

Mathlib.MeasureTheory.Measure.Lebesgue.Complex

Complex.measurableEquivPidefMathlib.MeasureTheory.Measure.Lebesgue.Complex, function or constant
Wording
the measurable equivalence product (from the name)
English
The measurable equivalence product is a measurable equivalence of the set of complexes and the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to real numbers defined as the measurable equivalence of the homeomorphism of the continuous linear equivalence of the equivalence function of the basis one.
Complex.measurableEquivRealProddefMathlib.MeasureTheory.Measure.Lebesgue.Complex, function or constant
Wording
the measurable equivalence real product (from the name)
English
The measurable equivalence real product is a measurable equivalence of the set of complexes and $\mathrm{Prod}$ applied to $\Real$ and $\Real$ defined as the measurable equivalence of the homeomorphism of the equivalence real product continuous linear map.

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

AlternatingMap.measuredefMathlib.MeasureTheory.Measure.Lebesgue.EqHaar, function or constant
Wording
the measure of x3 (from the name)
English
Let $x_{3}$ be an alternating map of $\Real$ and $\mathrm{Fin}$ applied to $n$. Then the measure of $x_{3}$ is a measure of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Lebesgue\_\_EqHaar\_\_3071773250\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{3}$.
TopologicalSpace.PositiveCompacts.Icc01defMathlib.MeasureTheory.Measure.Lebesgue.EqHaar, function or constant
Wording
the interval (from the docstring)
English
The interval is a positive compact of $\Real$.
TopologicalSpace.PositiveCompacts.piIcc01defMathlib.MeasureTheory.Measure.Lebesgue.EqHaar, function or constant
Wording
no wording
English
Let $x$ be a set. Then $\operatorname{piIcc01}$ applied to $x$ is a positive compact of the set of functions from elements of $x$ to real numbers.

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

MeasureTheory.LevyProkhorovstructureMathlib.MeasureTheory.Measure.LevyProkhorovMetric, type
Wording
no wording
English
Let $x$ be a set. Then the elements of $\operatorname{LevyProkhorov}$ applied to $x$ are a basic type.
MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorphdefMathlib.MeasureTheory.Measure.LevyProkhorovMetric, function or constant
Wording
the probability measure homeomorphism (from the name)
English
The probability measure homeomorphism is a homeomorphism of the set of probability measures of $x$ and $\operatorname{LevyProkhorov}$ applied to the set of probability measures of $x$.
MeasureTheory.LevyProkhorov.toMeasuredefMathlib.MeasureTheory.Measure.LevyProkhorovMetric, function or constant
Wording
the measure of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{LevyProkhorov}$ applied to $x$. Then the measure of $\mathrm{self}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
MeasureTheory.LevyProkhorov.toMeasureEquivdefMathlib.MeasureTheory.Measure.LevyProkhorovMetric, function or constant
Wording
the measure equivalence (from the name)
English
The measure equivalence is an element of $\EquivMACRoAE {\operatorname{LevyProkhorov} (x)}{x}$.
MeasureTheory.levyProkhorovDistdefMathlib.MeasureTheory.Measure.LevyProkhorovMetric, function or constant
Wording
no wording
English
Let $x_{3}$ and $x_{4}$ be measures of $x$. Then $\operatorname{levyProkhorovDist}$ applied to $x_{3}$ and $x_{4}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{levyProkhorovEDist}$ applied to $x_{3}$ and $x_{4}$.
MeasureTheory.levyProkhorovEDistdefMathlib.MeasureTheory.Measure.LevyProkhorovMetric, function or constant
Wording
no wording
English
Let $x_{3}$ and $x_{4}$ be measures of $x$. Then $\operatorname{levyProkhorovEDist}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $x_{5}$ to the proposition that for all elements $B$ of $\wp x$, if $B$ is a measurable set, then $x_{3}$ applied to $B$ is less than or equal to the sum of $x_{4}$ applied to the thickening of $\operatorname{toReal}$ applied to $x_{5}$ and $B$ and $x_{5}$ and $x_{4}$ applied to $B$ is less than or equal to the sum of $x_{3}$ applied to the thickening of $\operatorname{toReal}$ applied to $x_{5}$ and $B$ and $x_{5}$.

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

MeasureTheory.llrdefMathlib.MeasureTheory.Measure.LogLikelihoodRatio, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Let $x_{4}$ be an element of $x$. Then $\operatorname{llr}$ applied to $x_{2}$, $x_{3}$ and $x_{4}$ is a real number defined as the logarithm of $\operatorname{toReal}$ applied to $\operatorname{rnDeriv}$ applied to $x_{2}$, $x_{3}$ and $x_{4}$.

Mathlib.MeasureTheory.Measure.Map

MeasureTheory.Measure.liftLineardefMathlib.MeasureTheory.Measure.Map, function or constant
Wording
no wording
English
Let $f$ be a linear map of the set of outer measures of $x$ and the set of outer measures of $x_{1}$ such that for all measures $x_{4}$ of $x$, $x_{3} \leq \operatorname{caratheodory} (f (\operatorname{toOuterMeasure} (x_{4})))$. Then $\operatorname{liftLinear}$ applied to $f$ and $\mathrm{hf}$ is a linear map of the set of measures of $x$ and the set of measures of $x_{1}$.
MeasureTheory.Measure.mapdefMathlib.MeasureTheory.Measure.Map, function or constant
Wording
the map of f and x4 (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be a measure of $x$. Then the map of $f$ and $x_{4}$ is a measure of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Map\_\_2681718712\_\_\_hygCtx\_\_\_hyg\_\_8}$, $f$ and $x_{4}$.
MeasureTheory.Measure.mapₗdefMathlib.MeasureTheory.Measure.Map, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a linear map of the set of measures of $x$ and the set of measures of $x_{1}$.

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

AEMeasurabledefMathlib.MeasureTheory.Measure.MeasureSpaceDef, predicate
Wording
f is almost everywhere measurable (from the docstring)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{AEMeasurable\_\_\_auto\_1}$. Then $f$ is almost everywhere measurable, if there exists a function $g$ from elements of $x$ to elements of $x_{1}$, such that $g$ is measurable and $\operatorname{EventuallyEq}$ holds for $\operatorname{ae}$ applied to $x_{3}$, $f$ and $g$.
AEMeasurable.mkdefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
no wording
English
Let $f$ be an almost everywhere measurable function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{mk}$ applied to $f$, $h$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $h$ and $x_{4}$.
MeasureTheory.MeasurestructureMathlib.MeasureTheory.Measure.MeasureSpaceDef, type
Wording
measure of x (from the name)
English
Let $x$ be a set. Then the measures of $x$ are a basic type.
MeasureTheory.Measure.ofMeasurabledefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
the measure of m (from the name)
English
Let $m$ be a function from elements $s$ of $\wp x$ and elements of $\mathrm{Proof}$ applied to the proposition that $s$ is a measurable set to elements of $\mathrm{ENNReal}$ such that $\EqtMACRoH {m (\operatorname{emptyCollection} , \operatorname{empty})}{0}$ and for all functions $f$ from natural numbers to elements of $\wp x$, for all elements $h$ of $\mathrm{Proof}$ applied to the proposition that for all natural numbers $i_{2}$, $f$ applied to $i_{2}$ is a measurable set, if $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $f$ is pairwise, then $m$ applied to the union of the function that maps $i$ to $f$ applied to $i$ and $\operatorname{iUnion}$ applied to $h$ is equal to the sum of the function that maps $i_{1}$ to $m$ applied to $f$ applied to $i_{1}$ and $h$ applied to $i_{1}$ and $\operatorname{unconditional}$ applied to $\Natural$. Then the measure of $s$ is a measure of $x$.
MeasureTheory.Measure.realdefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{real}$ applied to $x_{1}$ and $s$ is a real number defined as $\operatorname{toReal}$ applied to $x_{1}$ applied to $s$.
MeasureTheory.MeasureSpaceclassMathlib.MeasureTheory.Measure.MeasureSpaceDef, predicate
Wording
x is a measure space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a measure space.
MeasureTheory.MeasureSpace.volumedefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
the volume (from the name)
English
The volume is a measure of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
MeasureTheory.tacticVolume_tacdefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
no wording
English
generation took over the time limit
MeasureTheory.toMeasurabledefMathlib.MeasureTheory.Measure.MeasureSpaceDef, function or constant
Wording
no wording
English
Let $x_{2}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{toMeasurable}$ applied to $x_{2}$ and $s$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_MeasureSpaceDef\_\_1555446310\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{2}$ and $s$.

Mathlib.MeasureTheory.Measure.MeasuredSets

MeasureTheory.MeasuredSetsdefMathlib.MeasureTheory.Measure.MeasuredSets, type
Wording
measured set of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then a measured set of $x_{2}$ is an element of the function that maps $x_{2}$ to $\SubtypeSet {s}{\mathrm{MeasurableSet} (s)}$.

Mathlib.MeasureTheory.Measure.Module

MeasureTheory.Measure.coeAddHomdefMathlib.MeasureTheory.Measure.Module, function or constant
Wording
the coercion additive homomorphism (from the name)
English
The coercion additive homomorphism is an additive monoid homomorphism of the set of measures of $x$ and the set of functions from elements of $\wp x$ to elements of $\mathrm{ENNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{MeasureTheory\_\_Measure\_\_coe\_zero}$ and $\mathrm{MeasureTheory\_\_Measure\_\_coe\_add}$.

Mathlib.MeasureTheory.Measure.MutuallySingular

MeasureTheory.Measure.MutuallySingulardefMathlib.MeasureTheory.Measure.MutuallySingular, predicate
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{MutuallySingular}$ holds for $x_{2}$ and $x_{3}$, if there exists an element $s$ of $\wp x$, such that $s$ is a measurable set, $\EqtMACRoH {x_{2} (s)}{0}$ and $x_{3}$ applied to the complement of $s$ is equal to $0$.
MeasureTheory.Measure.MutuallySingular.nullSetdefMathlib.MeasureTheory.Measure.MutuallySingular, function or constant
Wording
the null set of h (from the name)
English
Assume that $\operatorname{MutuallySingular}$ holds for $x_{1}$ and $x_{2}$. Then the null set of $h$ is an element of $\wp x$ defined as $\operatorname{choose}$ applied to $h$.

Mathlib.MeasureTheory.Measure.NullMeasurable

MeasureTheory.Measure.IsCompleteclassMathlib.MeasureTheory.Measure.NullMeasurable, predicate
Wording
x2 is complete (from the docstring)
English
Let $x_{2}$ be a measure of $x$. Then we can say that $x_{2}$ is complete.
MeasureTheory.Measure.completiondefMathlib.MeasureTheory.Measure.NullMeasurable, function or constant
Wording
the completion of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the completion of $x_{2}$ is a measure of the set of null measurable spaces of $x$ and $x_{2}$.
MeasureTheory.NullMeasurabledefMathlib.MeasureTheory.Measure.NullMeasurable, predicate
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_NullMeasurable\_\_\_auto\_1}$. Then $\operatorname{NullMeasurable}$ holds for $f$ and $x_{3}$, if for all elements $s$ of $\wp x_{1}$, if $s$ is a measurable set, then $\operatorname{NullMeasurableSet}$ holds for the preimage of $f$ and $s$ and $x_{3}$.
MeasureTheory.NullMeasurableSetdefMathlib.MeasureTheory.Measure.NullMeasurable, predicate
Wording
no wording
English
Let $s$ be an element of $\wp x$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_NullMeasurableSet\_\_\_auto\_1}$. Then $\operatorname{NullMeasurableSet}$ holds for $s$ and $x_{2}$, if $s$ is a measurable set.
MeasureTheory.NullMeasurableSpacedefMathlib.MeasureTheory.Measure.NullMeasurable, type
Wording
null measurable space of x and x2 (from the name)
English
Let $x$ be a set. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_NullMeasurableSpace\_\_\_auto\_1}$. Then a null measurable space of $x$ and $x_{2}$ is an element of the function that maps $x$ and $x_{2}$ to $x$.

Mathlib.MeasureTheory.Measure.OpenPos

MeasureTheory.Measure.IsOpenPosMeasureclassMathlib.MeasureTheory.Measure.OpenPos, predicate
Wording
x1 is a open positive part measure (from the name)
English
Let $x_{1}$ be a measure of $X$. Then we can say that $x_{1}$ is an open positive part measure.

Mathlib.MeasureTheory.Measure.OuterMeasure

MeasureTheory.OuterMeasure.toMeasuredefMathlib.MeasureTheory.Measure.OuterMeasure, function or constant
Wording
the measure of m and h (from the name)
English
Let $m$ be an outer measure of $x$ such that $\mathrm{ms} \leq \operatorname{caratheodory} (m)$. Then the measure of $m$ and $h$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.PreVariation

Finpartition.toMeasurableSetdefMathlib.MeasureTheory.Measure.PreVariation, function or constant
Wording
the measurable set of P (from the name)
English
Let $P$ be a finpartition of $s$. Assume that $s$ is a measurable set. Assume that for all elements $p$ of $\wp X$, if $p$ is an element of the set of parts of $P$, then $p$ is a measurable set. Then the measurable set of $P$ is a finpartition of $s$.
MeasureTheory.IsSigmaSubadditiveSetFundefMathlib.MeasureTheory.Measure.PreVariation, predicate
Wording
f is a sigma subadditive set function (from the name)
English
Let $f$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$. Then $f$ is a sigma subadditive set function, if for all functions $s$ from elements of $\Natural$ to elements of $\SubtypeSet {t_{1}}{\mathrm{MeasurableSet} (t_{1})}$, if $\operatorname{onFun}$ applied to the proposition that $\mathrm{Disjoint}$ and $\operatorname{comp}$ applied to the function that maps $t$ to the proposition that $t$ is a measurable set and $s$ is pairwise, then $f (\operatorname{iUnion} (\lambda i . s (i)))\leq \mathrm{tsum} (\lambda i_{1} . f (s (i_{1})), \operatorname{unconditional} (\Natural))$.
MeasureTheory.ennrealPreVariationdefMathlib.MeasureTheory.Measure.PreVariation, function or constant
Wording
the extended nonnegative real number variation of f (from the name)
English
Let $f$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$ such that $f$ is a sigma subadditive set function and $\EqtMACRoH {f (\operatorname{emptyCollection})}{0}$. Then the extended nonnegative real number variation of $f$ is a vector measure of $X$ and $\mathrm{ENNReal}$.
MeasureTheory.preVariationdefMathlib.MeasureTheory.Measure.PreVariation, function or constant
Wording
the variation of f (from the name)
English
Let $f$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$ such that $f$ is a sigma subadditive set function and $\EqtMACRoH {f (\operatorname{emptyCollection})}{0}$. Then the variation of $f$ is a measure of $X$ defined as the extended nonnegative real number to measure of the extended nonnegative real number variation of $f$.
MeasureTheory.preVariationFundefMathlib.MeasureTheory.Measure.PreVariation, function or constant
Wording
the variation function of f and s (from the name)
English
Let $f$ be a function from elements of $\wp X$ to elements of $\mathrm{ENNReal}$. Let $s$ be an element of $\wp X$. Then the variation function of $f$ and $s$ is an element of $\mathrm{ENNReal}$ defined as $\mathrm{dite}$ applied to the proposition that $s$ is a measurable set, the function that maps $h$ to the supremum of the function that maps $P$ to $\FinsetSum {\operatorname{parts} (P)}{p}{f (p)}$ and the function that maps $h_{1}$ to $0$.

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

MeasureTheory.FiniteMeasure.normalizedefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
no wording
English
Let $x_{1}$ be a finite measure of $x$. Then $\operatorname{normalize}$ applied to $x_{1}$ is a probability measure of $x$ defined as $\mathrm{dite}$ applied to $\EqtMACRoH {\operatorname{mass} (x_{1})}{0}$, the function that maps $\mathrm{zero}$ to the Dirac of $\operatorname{some}$ applied to $h$ and the function that maps $\mathrm{zero1}$ to $\HSMulhSMulMACRoAL {\operatorname{inv} (\operatorname{mass} (x_{1}))}{\operatorname{toMeasure} (x_{1})}$.
MeasureTheory.Measure.toProbabilityMeasuredefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
the probability measure of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the probability measure of $x_{2}$ is a probability measure of $x$ defined as $x_{2}$.
MeasureTheory.ProbabilityMeasuredefMathlib.MeasureTheory.Measure.ProbabilityMeasure, type
Wording
probability measure of x (from the name)
English
Let $x$ be a set. Then a probability measure of $x$ is an element of the function that maps $x$ to $\SubtypeSet {x_{2}}{\operatorname{IsProbabilityMeasure} (x_{2})}$.
MeasureTheory.ProbabilityMeasure.mapdefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
the map of x4 and f (from the name)
English
Let $x_{4}$ be a probability measure of $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $x_{4}$ and $f$ is a probability measure of $x_{1}$ defined as the map of $f$ and the measure of $x_{4}$.
MeasureTheory.ProbabilityMeasure.toFiniteMeasuredefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
the finite measure of x2 (from the name)
English
Let $x_{2}$ be a probability measure of $x$. Then the finite measure of $x_{2}$ is a finite measure of $x$ defined as the measure of $x_{2}$.
MeasureTheory.ProbabilityMeasure.toMeasuredefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
the measure of x2 (from the name)
English
Let $x_{2}$ be a probability measure of $x$. Then the measure of $x_{2}$ is a measure of $x$ defined as the proposition that $x_{2}$ is a probability measure.
MeasureTheory.ProbabilityMeasure.toWeakDualBCNNdefMathlib.MeasureTheory.Measure.ProbabilityMeasure, function or constant
Wording
no wording
English
Let $x_{3}$ be a probability measure of $x$. Then $\operatorname{toWeakDualBCNN}$ applied to $x_{3}$ is a weak dual of $\mathrm{NNReal}$ and the set of bounded continuous functions of $x$ and $\mathrm{NNReal}$ defined as $\operatorname{comp}$ applied to $\operatorname{toWeakDualBCNN}$, $\operatorname{toFiniteMeasure}$ and $x_{3}$.

Mathlib.MeasureTheory.Measure.Prod

MeasureTheory.Measure.FiniteSpanningSetsIn.proddefMathlib.MeasureTheory.Measure.Prod, function or constant
Wording
the product of x6 and x7 (from the name)
English
Let $x_{6}$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{4}$ and $C$. Let $x_{7}$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{5}$ and $D$. Then the product of $x_{6}$ and $x_{7}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to the product of $x_{4}$ and $x_{5}$ and the image of $C$ and $D$.
MeasureTheory.Measure.fstdefMathlib.MeasureTheory.Measure.Prod, function or constant
Wording
the first component of x4 (from the name)
English
Let $x_{4}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the first component of $x_{4}$ is a measure of $x$ defined as the map of $\ProdfstMACRoZ$ and $x_{4}$.
MeasureTheory.Measure.proddefMathlib.MeasureTheory.Measure.Prod, function or constant
Wording
the product of x4 and x5 (from the name)
English
Let $x_{4}$ be a measure of $x$. Let $x_{5}$ be a measure of $x_{1}$. Then the product of $x_{4}$ and $x_{5}$ is a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Prod\_\_473312173\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{4}$ and $x_{5}$.
MeasureTheory.Measure.snddefMathlib.MeasureTheory.Measure.Prod, function or constant
Wording
the second component of x4 (from the name)
English
Let $x_{4}$ be a measure of $\mathrm{Prod}$ applied to $x$ and $x_{1}$. Then the second component of $x_{4}$ is a measure of $x_{1}$ defined as the map of $\ProdsndMACRoAA$ and $x_{4}$.

Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

MeasureTheory.QuasiMeasurePreservingstructureMathlib.MeasureTheory.Measure.QuasiMeasurePreserving, predicate
Wording
no wording
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_QuasiMeasurePreserving\_\_\_auto\_1}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{MeasureTheory\_\_QuasiMeasurePreserving\_\_\_auto\_3}$. Then we can say that $\operatorname{QuasiMeasurePreserving}$ holds for $f$, $x_{3}$ and $x_{4}$.

Mathlib.MeasureTheory.Measure.Regular

MeasureTheory.Measure.InnerRegularclassMathlib.MeasureTheory.Measure.Regular, predicate
Wording
x3 is a inner regular (from the name)
English
Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is an inner regular.
MeasureTheory.Measure.InnerRegularCompactLTTopclassMathlib.MeasureTheory.Measure.Regular, predicate
Wording
no wording
English
Let $x_{3}$ be a measure of $x$. Then we can say that $\operatorname{InnerRegularCompactLTTop}$ holds for $x_{3}$.
MeasureTheory.Measure.InnerRegularWRTdefMathlib.MeasureTheory.Measure.Regular, predicate
Wording
no wording
English
Let $x_{2}$ be a measure of $x$. Let $p$ and $q$ be functions from elements of $\wp x$ to propositions. Then $\operatorname{InnerRegularWRT}$ holds for $x_{2}$, $p$ and $q$, if for all elements $U$ of $\wp x$, if $q$ holds for $U$, then for all elements $r$ of $\mathrm{ENNReal}$, if $r < x_{2} (U)$, then there exists an element $K$ of $\wp x$, such that $K \leq U$, $p$ holds for $K$ and $r < x_{2} (K)$.
MeasureTheory.Measure.OuterRegularclassMathlib.MeasureTheory.Measure.Regular, predicate
Wording
x3 is a outer regular (from the name)
English
Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is an outer regular.
MeasureTheory.Measure.RegularclassMathlib.MeasureTheory.Measure.Regular, predicate
Wording
x3 is regular (from the name)
English
Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is regular.
MeasureTheory.Measure.WeaklyRegularclassMathlib.MeasureTheory.Measure.Regular, predicate
Wording
x3 is weakly regular (from the name)
English
generation took over the time limit

Mathlib.MeasureTheory.Measure.ResolventTransform

MeasureTheory.resolventTransformdefMathlib.MeasureTheory.Measure.ResolventTransform, function or constant
Wording
the resolvent transform of x6 and a (from the docstring)
English
Let $x_{6}$ be a measure of $x$. Let $a$ be an element of $A$. Then the resolvent transform of $x_{6}$ and $a$ is an element of $A$ defined as the Bochner integral of $x_{6}$ and the function that maps $x_{7}$ to $\mathrm{resolvent}$ applied to $a$ and $x_{7}$.

Mathlib.MeasureTheory.Measure.Restrict

MeasureTheory.Measure.restrictdefMathlib.MeasureTheory.Measure.Restrict, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{restrict}$ applied to $x_{1}$ and $s$ is a measure of $x$ defined as $\mathrm{MeasureTheory\_\_Measure\_\_restrict\_u2097\_\_\_app}$ applied to $s$ and $x_{1}$.
MeasureTheory.Measure.restrictₗdefMathlib.MeasureTheory.Measure.Restrict, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\mathrm{MeasureTheory\_\_Measure\_\_restrict\_u2097\_}$ applied to $s$ is a linear map of the set of measures of $x$ and the set of measures of $x$.

Mathlib.MeasureTheory.Measure.SeparableMeasure

MeasureTheory.IsSeparableclassMathlib.MeasureTheory.Measure.SeparableMeasure, predicate
Wording
x is separable (from the name)
English
Let $x$ be a measure of $X$. Then we can say that $x$ is separable.
MeasureTheory.Measure.MeasureDensestructureMathlib.MeasureTheory.Measure.SeparableMeasure, predicate
Wording
x1 is a measure dense with respect to x (from the name)
English
Let $x$ be a measure of $X$. Let $x_{1}$ be an element of $\wp (\wp X)$. Then we can say that $x_{1}$ is a measure dense with respect to $x$.

Mathlib.MeasureTheory.Measure.Stieltjes

IotopdefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
no wording
English
Let $a$ and $b$ be elements of $R$. Then $\mathrm{Iotop}$ applied to $a$ and $b$ is an element of $\wp R$ defined as $\iteMACRoG {\mathrm{IsTop} (b)}{\operatorname{Ioc} (a , b)}{\operatorname{Ioo} (a , b)}$.
Monotone.stieltjesFunctiondefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the Stieltjes function of hf (from the name)
English
Assume that $f$ is monotone. Then the Stieltjes function of $\mathrm{hf}$ is a Stieltjes function of $R$.
StieltjesFunctionstructureMathlib.MeasureTheory.Measure.Stieltjes, type
Wording
Stieltjes function of R (from the name)
English
Let $R$ be a set. Then the Stieltjes functions of $R$ are a basic type.
StieltjesFunction.adddefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the sum of f and g (from the name)
English
Let $f$ and $g$ be Stieltjes functions of $R$. Then the sum of $f$ and $g$ is a Stieltjes function of $R$.
StieltjesFunction.constdefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the constant of R and c (from the name)
English
Let $R$ be a set. Let $c$ be a real number. Then the constant of $R$ and $c$ is a Stieltjes function of $R$.
StieltjesFunction.iddefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the identity (from the name)
English
The identity is a Stieltjes function of $\Real$.
StieltjesFunction.lengthdefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the length of f and s (from the name)
English
Let $f$ be a Stieltjes function of $R$. Let $s$ be an element of $\wp R$. Then the length of $f$ and $s$ is an element of $\mathrm{ENNReal}$ defined as $\iteMACRoG {\mathrm{IsEmpty} (R)}{0}{\mathrm{iInf} (\lambda a . \mathrm{iInf} (\lambda b . \mathrm{iInf} (\lambda h . \operatorname{ofReal} (\operatorname{toFun} (f , b)- \operatorname{toFun} (f , a)))))}$.
StieltjesFunction.measuredefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the measure of f (from the name)
English
Let $f$ be a Stieltjes function of $R$. Then the measure of $f$ is a measure of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{StieltjesFunction\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Stieltjes\_\_1973370438\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $f$.
StieltjesFunction.outerdefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
no wording
English
Let $f$ be a Stieltjes function of $R$. Then $\operatorname{outer}$ applied to $f$ is an outer measure of $R$ defined as the outer measure of $\operatorname{length}$ applied to $f$ and $\mathrm{StieltjesFunction\_\_length\_empty}$ applied to $f$.
StieltjesFunction.toFundefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the underlying function of self and x2 (from the docstring)
English
Let $\mathrm{self}$ be a Stieltjes function of $R$. Let $x_{2}$ be an element of $R$. Then the underlying function of $\mathrm{self}$ and $x_{2}$ is a real number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
botSetdefMathlib.MeasureTheory.Measure.Stieltjes, function or constant
Wording
the set of all bottom elements (from the docstring)
English
The set of all bottom elements is an element of $\wp R$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{1}$ to the proposition that $x_{1}$ is a bottom.

Mathlib.MeasureTheory.Measure.Sum

MeasureTheory.Measure.sumdefMathlib.MeasureTheory.Measure.Sum, function or constant
Wording
the sum of x3 (from the name)
English
Let $x_{3}$ be a function from elements of $x_{1}$ to measures of $x$. Then the sum of $x_{3}$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.Support

MeasureTheory.Measure.supportdefMathlib.MeasureTheory.Measure.Support, function or constant
Wording
the support of x2 (from the name)
English
Let $x_{2}$ be a measure of $X$. Then the support of $x_{2}$ is an element of $\wp X$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to $\operatorname{Frequently}$ applied to the function that maps $u$ to $\mathrm{Lt} (0 , x_{2} (u))$ and the small set of the neighbourhood filter of $x_{3}$.

Mathlib.MeasureTheory.Measure.Tight

MeasureTheory.IsTightMeasureSetdefMathlib.MeasureTheory.Measure.Tight, predicate
Wording
S is a tight measure set (from the name)
English
Let $S$ be an element of the power set of the set of measures of $x$. Then $S$ is a tight measure set, if $\operatorname{Tendsto}$ holds for the supremum of the function that maps $x_{3}$ to the supremum of the function that maps $h$ to $\operatorname{coe}$ applied to $x_{3}$, the small set of the cocompact of $x$ and the neighbourhood filter of $0$.

Mathlib.MeasureTheory.Measure.Tilted

MeasureTheory.Measure.tilteddefMathlib.MeasureTheory.Measure.Tilted, function or constant
Wording
no wording
English
Let $x_{2}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to real numbers. Then $\operatorname{tilted}$ applied to $x_{2}$ and $f$ is a measure of $x$ defined as $\operatorname{withDensity}$ applied to $x_{2}$ and the function that maps $x_{3}$ to $\operatorname{ofReal}$ applied to the quotient of the exponential of $f$ applied to $x_{3}$ and the Bochner integral of $x_{2}$ and the function that maps $x_{4}$ to the exponential of $f$ applied to $x_{4}$.

Mathlib.MeasureTheory.Measure.TotalVariation.Defs

MeasureTheory.etvDistdefMathlib.MeasureTheory.Measure.TotalVariation.Defs, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{etvDist}$ applied to $x_{2}$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\mathrm{dite}$ applied to the proposition that $x_{2}$ is a finite measure and $x_{3}$ is a finite measure, the function that maps $h$ to $\operatorname{etvDist}$ applied to the signed measure of $x_{2}$ and the signed measure of $x_{3}$ and the function that maps $h_{1}$ to the top.
MeasureTheory.tvDistdefMathlib.MeasureTheory.Measure.TotalVariation.Defs, function or constant
Wording
no wording
English
Let $x_{2}$ and $x_{3}$ be measures of $x$. Then $\operatorname{tvDist}$ applied to $x_{2}$ and $x_{3}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{etvDist}$ applied to $x_{2}$ and $x_{3}$.

Mathlib.MeasureTheory.Measure.Trim

MeasureTheory.Measure.trimdefMathlib.MeasureTheory.Measure.Trim, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Assume that $m \leq m_{0}$. Then $\operatorname{trim}$ applied to $x_{1}$ and $\mathrm{hm}$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

MeasureTheory.IsFiniteMeasureclassMathlib.MeasureTheory.Measure.Typeclasses.Finite, predicate
Wording
x1 is a finite measure (from the name)
English
Let $x_{1}$ be a measure of $x$. Then we can say that $x_{1}$ is a finite measure.
MeasureTheory.IsFiniteMeasureOnCompactsclassMathlib.MeasureTheory.Measure.Typeclasses.Finite, predicate
Wording
no wording
English
Let $x_{2}$ be a measure of $x$. Then we can say that $\operatorname{IsFiniteMeasureOnCompacts}$ holds for $x_{2}$.
MeasureTheory.IsLocallyFiniteMeasureclassMathlib.MeasureTheory.Measure.Typeclasses.Finite, predicate
Wording
x2 is locally finite (from the docstring)
English
generation took over the time limit
MeasureTheory.Measure.FiniteAtFilterdefMathlib.MeasureTheory.Measure.Typeclasses.Finite, predicate
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $f$ be a filter of $x$. Then $\operatorname{FiniteAtFilter}$ holds for $x_{1}$ and $f$, if there exists an element $s$ of $\wp x$, such that $s$ is an element of $f$ and $x_{1}$ applied to $s$ is less than the top.
MeasureTheory.Measure.FiniteSpanningSetsInstructureMathlib.MeasureTheory.Measure.Typeclasses.Finite, type
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $C$ be an element of $\wp (\wp x)$. Then the elements of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $C$ are a basic type.
MeasureTheory.Measure.FiniteSpanningSetsIn.setdefMathlib.MeasureTheory.Measure.Typeclasses.Finite, function or constant
Wording
the set of self and x2 (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $C$. Let $x_{2}$ be a natural number. Then the set of $\mathrm{self}$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
MeasureTheory.Measure.finiteSpanningSetsInCompactdefMathlib.MeasureTheory.Measure.Typeclasses.Finite, function or constant
Wording
the finite spanning set in compact of x3 (from the name)
English
Let $x_{3}$ be a measure of $x$. Then the finite spanning set in compact of $x_{3}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{3}$ and $\operatorname{ofPred}$ applied to the function that maps $K$ to the proposition that $K$ is compact.
MeasureTheory.Measure.finiteSpanningSetsInOpendefMathlib.MeasureTheory.Measure.Typeclasses.Finite, function or constant
Wording
the finite spanning set in open of x3 (from the name)
English
Let $x_{3}$ be a measure of $x$. Then the finite spanning set in open of $x_{3}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{3}$ and $\operatorname{ofPred}$ applied to the function that maps $K$ to the proposition that $K$ is open.
MeasureTheory.Measure.finiteSpanningSetsInOpen'defMathlib.MeasureTheory.Measure.Typeclasses.Finite, function or constant
Wording
the finite spanning set in open of x2 (from the name)
English
Let $x_{2}$ be a measure of $x$. Then the finite spanning set in open of $x_{2}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{2}$ and $\operatorname{ofPred}$ applied to the function that maps $K$ to the proposition that $K$ is open defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Measure\_\_Typeclasses\_\_Finite\_\_1878421158\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{2}$.
MeasureTheory.measureUnivNNRealdefMathlib.MeasureTheory.Measure.Typeclasses.Finite, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Then $\operatorname{measureUnivNNReal}$ applied to $x_{1}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toNNReal}$ applied to $x_{1}$ applied to the universal set.

Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

MeasureTheory.NullSingletonClassclassMathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass, predicate
Wording
x1 is a null singleton class (from the name)
English
Let $x_{1}$ be a measure of $x$. Then we can say that $x_{1}$ is a null singleton class.

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

MeasureTheory.IsProbabilityMeasureclassMathlib.MeasureTheory.Measure.Typeclasses.Probability, predicate
Wording
x1 is a probability measure (from the name)
English
Let $x_{1}$ be a measure of $x$. Then we can say that $x_{1}$ is a probability measure.
MeasureTheory.IsZeroOrProbabilityMeasureclassMathlib.MeasureTheory.Measure.Typeclasses.Probability, predicate
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Then we can say that $\operatorname{IsZeroOrProbabilityMeasure}$ holds for $x_{1}$.

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

MeasureTheory.Measure.FiniteSpanningSetsIn.disjointeddefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Let $S$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $s_{1}$ to the proposition that $s_{1}$ is a measurable set. Then $\operatorname{disjointed}$ applied to $S$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set.
MeasureTheory.Measure.FiniteSpanningSetsIn.monodefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Let $h$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $C$. Assume that $C \leq D$. Then $\operatorname{mono}$ applied to $h$ and $\mathrm{hC}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $D$.
MeasureTheory.Measure.FiniteSpanningSetsIn.mono'defMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Let $h$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $C$. Assume that $\operatorname{inter}$ applied to $C$ and $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $x_{1}$ applied to $s$ is less than the top is less than or equal to $D$. Then $\operatorname{mono'}$ applied to $h$ and $\mathrm{hC}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $D$.
MeasureTheory.Measure.FiniteSpanningSetsIn.ofLEdefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Assume that $x_{2} \leq x_{1}$. Let $S$ be an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $C$. Then $\operatorname{ofLE}$ applied to $h$ and $S$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{2}$ and $C$.
MeasureTheory.Measure.toFiniteSpanningSetsIndefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Then $\operatorname{toFiniteSpanningSetsIn}$ applied to $x_{1}$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{1}$ and $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set.
MeasureTheory.SFiniteclassMathlib.MeasureTheory.Measure.Typeclasses.SFinite, predicate
Wording
x1 is finite (from the name)
English
Let $x_{1}$ be a measure of $x$. Then we can say that $x_{1}$ is finite.
MeasureTheory.SigmaFiniteclassMathlib.MeasureTheory.Measure.Typeclasses.SFinite, predicate
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Then we can say that $\operatorname{SigmaFinite}$ holds for $x_{1}$.
MeasureTheory.sfiniteSeqdefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $x_{2}$ be a natural number. Then $\operatorname{sfiniteSeq}$ applied to $x_{1}$ and $x_{2}$ is a measure of $x$ defined as $\operatorname{choose}$ applied to $\operatorname{out'}$ and $x_{2}$.
MeasureTheory.spanningSetsdefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
the spanning set of x1 and i (from the name)
English
Let $x_{1}$ be a measure of $x$. Let $i$ be a natural number. Then the spanning set of $x_{1}$ and $i$ is an element of $\wp x$ defined as $\operatorname{accumulate}$ applied to $\operatorname{set}$ applied to $\operatorname{toFiniteSpanningSetsIn}$ applied to $x_{1}$ and $i$.
MeasureTheory.spanningSetsIndexdefMathlib.MeasureTheory.Measure.Typeclasses.SFinite, function or constant
Wording
the spanning set index of x1 and x2 (from the name)
English
Let $x_{1}$ be a measure of $x$. Let $x_{2}$ be an element of $x$. Then the spanning set index of $x_{1}$ and $x_{2}$ is a natural number.

Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

MeasureTheory.IsZeroOneMeasureclassMathlib.MeasureTheory.Measure.Typeclasses.ZeroOne, predicate
Wording
x2 is a zero one measure (from the name)
English
Let $x_{2}$ be a measure of $x$. Then we can say that $x_{2}$ is a zero one measure.

Mathlib.MeasureTheory.Measure.WithDensity

MeasureTheory.Measure.withDensitydefMathlib.MeasureTheory.Measure.WithDensity, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{withDensity}$ applied to $x_{1}$ and $f$ is a measure of $x$.

Mathlib.MeasureTheory.Measure.WithDensityFinite

MeasureTheory.Measure.toFinitedefMathlib.MeasureTheory.Measure.WithDensityFinite, function or constant
Wording
no wording
English
Let $x_{2}$ be a measure of $x$. Then $\operatorname{toFinite}$ applied to $x_{2}$ is a measure of $x$ defined as the conditional probability measure of measure of $\operatorname{toFiniteAux}$ applied to $x_{2}$ and the universal set.

Mathlib.MeasureTheory.Order.Lattice

MeasurableInfclassMathlib.MeasureTheory.Order.Lattice, predicate
Wording
M is a measurable infimum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable infimum.
MeasurableInf₂classMathlib.MeasureTheory.Order.Lattice, predicate
Wording
M is a measurable infimum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable infimum.
MeasurableSupclassMathlib.MeasureTheory.Order.Lattice, predicate
Wording
M is a measurable supremum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable supremum.
MeasurableSup₂classMathlib.MeasureTheory.Order.Lattice, predicate
Wording
M is a measurable supremum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable supremum.

Mathlib.MeasureTheory.OuterMeasure.AE

MeasureTheory.aedefMathlib.MeasureTheory.OuterMeasure.AE, function or constant
Wording
no wording
English
Let $x_{2}$ be an element of $F$. Then $\operatorname{ae}$ applied to $x_{2}$ is a filter of $x$.

Mathlib.MeasureTheory.OuterMeasure.Caratheodory

MeasureTheory.OuterMeasure.IsCaratheodorydefMathlib.MeasureTheory.OuterMeasure.Caratheodory, predicate
Wording
no wording
English
Let $m$ be an outer measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{IsCaratheodory}$ holds for $m$ and $s$, if for all elements $t$ of $\wp x$, $\EqtMACRoH {m (t)}{m (\operatorname{inter} (t , s))+ m (\operatorname{sdiff} (t , s))}$.
MeasureTheory.OuterMeasure.caratheodoryDynkindefMathlib.MeasureTheory.OuterMeasure.Caratheodory, function or constant
Wording
no wording
English
Let $m$ be an outer measure of $x$. Then $\operatorname{caratheodoryDynkin}$ applied to $m$ is a Dynkin system of $x$.

Mathlib.MeasureTheory.OuterMeasure.Defs

MeasureTheory.OuterMeasurestructureMathlib.MeasureTheory.OuterMeasure.Defs, type
Wording
outer measure of x (from the name)
English
Let $x$ be a set. Then the outer measures of $x$ are a basic type.
MeasureTheory.OuterMeasure.measureOfdefMathlib.MeasureTheory.OuterMeasure.Defs, function or constant
Wording
the measure of self and x1 (from the name)
English
Let $\mathrm{self}$ be an outer measure of $x$. Let $x_{1}$ be an element of $\wp x$. Then the measure of $\mathrm{self}$ and $x_{1}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{1}$.
MeasureTheory.OuterMeasureClassclassMathlib.MeasureTheory.OuterMeasure.Defs, predicate
Wording
x is a outer measure class (from the name)
English
Let $F$ be a set. Let $x$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $x$ is an outer measure class.

Mathlib.MeasureTheory.OuterMeasure.Induced

MeasureTheory.OuterMeasure.trimdefMathlib.MeasureTheory.OuterMeasure.Induced, function or constant
Wording
no wording
English
Let $m$ be an outer measure of $x$. Then $\operatorname{trim}$ applied to $m$ is an outer measure of $x$ defined as the induced outer measure of the function that maps $s$ and $h$ to $m$ applied to $s$.
MeasureTheory.extenddefMathlib.MeasureTheory.OuterMeasure.Induced, function or constant
Wording
no wording
English
Let $m$ be a function from elements $s_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $P$ applied to $s_{1}$ to elements of $\mathrm{ENNReal}$. Let $s$ be an element of $x$. Then $\operatorname{extend}$ applied to $s_{1}$, $m$ and $s$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $s$ to the infimum of the function that maps $h$ to $s_{1}$ applied to $m$ and $h$.
MeasureTheory.inducedOuterMeasuredefMathlib.MeasureTheory.OuterMeasure.Induced, function or constant
Wording
the induced outer measure of m (from the name)
English
Let $m$ be a function from elements $s$ of $\wp x$ and elements of $\mathrm{Proof}$ applied to $P$ applied to $s$ to elements of $\mathrm{ENNReal}$. Assume that $P$ holds for $\operatorname{emptyCollection}$. Assume that $\EqtMACRoH {m (\operatorname{emptyCollection} , P_{0})}{0}$. Then the induced outer measure of $s$ is an outer measure of $x$ defined as the function that maps $m_{0}$ to the outer measure of $\operatorname{extend}$ applied to $s$ and $\mathrm{MeasureTheory\_\_extend\_empty}$ applied to $m$ and $P_{0}$.

Mathlib.MeasureTheory.OuterMeasure.OfAddContent

MeasureTheory.AddContent.measuredefMathlib.MeasureTheory.OuterMeasure.OfAddContent, function or constant
Wording
the measure of m (from the name)
English
Let $m$ be an additive content of $\mathrm{ENNReal}$ and $C$. Assume that $C$ is a set semiring. Assume that $x_{1} \leq \operatorname{generateFrom} (C)$. Assume that $\operatorname{IsSigmaSubadditive}$ holds for $m$. Then the measure of $m$ is a measure of $x$.
MeasureTheory.AddContent.measureCaratheodorydefMathlib.MeasureTheory.OuterMeasure.OfAddContent, function or constant
Wording
no wording
English
Let $m$ be an additive content of $\mathrm{ENNReal}$ and $C$. Assume that $C$ is a set semiring. Assume that $\operatorname{IsSigmaSubadditive}$ holds for $m$. Then $\operatorname{measureCaratheodory}$ applied to $m$, $\mathrm{hC}$ and $\mathrm{m\_sigma\_subadd}$ is a measure of $x$.

Mathlib.MeasureTheory.OuterMeasure.OfFunction

MeasureTheory.OuterMeasure.boundedBydefMathlib.MeasureTheory.OuterMeasure.OfFunction, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\wp x$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{boundedBy}$ applied to $m$ is an outer measure of $x$.
MeasureTheory.OuterMeasure.ofFunctiondefMathlib.MeasureTheory.OuterMeasure.OfFunction, function or constant
Wording
the outer measure of m and m_empty (from the name)
English
Let $m$ be a function from elements of $\wp x$ to elements of $\mathrm{ENNReal}$ such that $\EqtMACRoH {m (\operatorname{emptyCollection})}{0}$. Then the outer measure of $m$ and $\mathrm{m\_empty}$ is an outer measure of $x$.
MeasureTheory.OuterMeasure.sInfGendefMathlib.MeasureTheory.OuterMeasure.OfFunction, function or constant
Wording
the infimum generator of m and s (from the name)
English
Let $m$ be an element of the power set of the set of outer measures of $x$. Let $s$ be an element of $\wp x$. Then the infimum generator of $m$ and $s$ is an element of $\mathrm{ENNReal}$ defined as the infimum of the function that maps $x_{1}$ to the infimum of the function that maps $h$ to $x_{1}$ applied to $s$.

Mathlib.MeasureTheory.OuterMeasure.Operations

MeasureTheory.OuterMeasure.comapdefMathlib.MeasureTheory.OuterMeasure.Operations, function or constant
Wording
the preimage of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the preimage of $f$ is a linear map of the set of outer measures of $x_{1}$ and the set of outer measures of $x$.
MeasureTheory.OuterMeasure.diracdefMathlib.MeasureTheory.OuterMeasure.Operations, function or constant
Wording
the Dirac of a (from the name)
English
Let $a$ be an element of $x$. Then the Dirac of $a$ is an outer measure of $x$.
MeasureTheory.OuterMeasure.mapdefMathlib.MeasureTheory.OuterMeasure.Operations, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a linear map of the set of outer measures of $x$ and the set of outer measures of $x_{1}$.
MeasureTheory.OuterMeasure.restrictdefMathlib.MeasureTheory.OuterMeasure.Operations, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp x$. Then $\operatorname{restrict}$ applied to $s$ is a linear map of the set of outer measures of $x$ and the set of outer measures of $x$ defined as the composition of the map of the function that maps $x_{1}$ to $\MembershipmemMACRoT {s}{x_{1}}$ and the preimage of the function that maps $x_{2}$ to $\MembershipmemMACRoT {s}{x_{2}}$.
MeasureTheory.OuterMeasure.sumdefMathlib.MeasureTheory.OuterMeasure.Operations, function or constant
Wording
the sum of f (from the docstring)
English
Let $f$ be a function from elements of $x_{1}$ to outer measures of $x$. Then the sum of $f$ is an outer measure of $x$.

Mathlib.MeasureTheory.PiSystem

IsPiSystemdefMathlib.MeasureTheory.PiSystem, predicate
Wording
C is a product system (from the name)
English
Let $C$ be an element of $\wp (\wp x)$. Then $C$ is a product system, if for all elements $s$ of $\wp x$, if $s$ is an element of $C$, then for all elements $t$ of $\wp x$, if $t$ is an element of $C$, then if $\operatorname{inter}$ applied to $s$ and $t$ is nonempty, then $\MembershipmemMACRoT {C}{\operatorname{inter} (s , t)}$.
MeasurableSpace.DynkinSystemstructureMathlib.MeasureTheory.PiSystem, type
Wording
Dynkin system of x (from the name)
English
Let $x$ be a set. Then the Dynkin systems of $x$ are a basic type.
MeasurableSpace.DynkinSystem.GenerateHasinductiveMathlib.MeasureTheory.PiSystem, predicate
Wording
no wording
English
Let $s$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{GenerateHas}$ holds for $s$ and $x_{1}$.
MeasurableSpace.DynkinSystem.GenerateHas.belowinductiveMathlib.MeasureTheory.PiSystem, predicate
Wording
no wording
English
Assume that $\operatorname{GenerateHas}$ holds for $s$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
MeasurableSpace.DynkinSystem.HasdefMathlib.MeasureTheory.PiSystem, predicate
Wording
no wording
English
Let $\mathrm{self}$ be a Dynkin system of $x$. Let $x_{1}$ be an element of $\wp x$. Then $\operatorname{Has}$ holds for $\mathrm{self}$ and $x_{1}$, if $\operatorname{proj0}$ holds for $\mathrm{self}$ and $x_{1}$.
MeasurableSpace.DynkinSystem.generatedefMathlib.MeasureTheory.PiSystem, function or constant
Wording
no wording
English
Let $s$ be an element of $\wp (\wp x)$. Then $\operatorname{generate}$ applied to $s$ is a Dynkin system of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{GenerateHas}$ applied to $s$, $\operatorname{empty}$, the function that maps $x_{1}$ to $\operatorname{compl}$ and the function that maps $x_{2}$ to $\operatorname{iUnion}$.
MeasurableSpace.DynkinSystem.ofMeasurableSpacedefMathlib.MeasureTheory.PiSystem, function or constant
Wording
the Dynkin system of m (from the name)
English
Assume that $x$ is a measurable space. Then the Dynkin system of $m$ is a Dynkin system of $x$ defined as $\operatorname{mk}$ applied to the proposition that $\operatorname{MeasurableSet'}$, $\mathrm{MeasurableSpace\_\_measurableSet\_empty}$ applied to $m$, the function that maps $a$ to $\mathrm{MeasurableSpace\_\_measurableSet\_compl}$ applied to $m$ and $a$ and the function that maps $f$, $h$ and $\mathrm{hf}$ to $\mathrm{MeasurableSpace\_\_measurableSet\_iUnion}$ applied to $m$, $f$ and $\mathrm{hf}$.
MeasurableSpace.DynkinSystem.restrictOndefMathlib.MeasureTheory.PiSystem, function or constant
Wording
no wording
English
Let $d$ be a Dynkin system of $x$ such that $\operatorname{Has}$ holds for $d$ and $s$. Then $\operatorname{restrictOn}$ applied to $d$ and $h$ is a Dynkin system of $x$.
generatePiSystemdefMathlib.MeasureTheory.PiSystem, function or constant
Wording
no wording
English
Let $S$ be an element of $\wp (\wp x)$. Then $\mathrm{generatePiSystem}$ applied to $S$ is an element of $\wp (\wp x)$.
piiUnionInterdefMathlib.MeasureTheory.PiSystem, function or constant
Wording
no wording
English
Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $\wp (\wp x)$. Let $S$ be an element of $\wp x_{1}$. Then $\mathrm{piiUnionInter}$ applied to $x_{2}$ and $S$ is an element of $\wp (\wp x)$ defined as $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that there exists a finite set $t$ of $x_{1}$, such that there exists an element $h$ of $\mathrm{Leq} (t , S)$, such that there exists a function $f$ from elements of $x_{1}$ to elements of $\wp x$, such that there exists an element $h_{1}$ of $\mathrm{forall}$ applied to $x_{1}$ and the function that maps $x_{4}$ to the proposition that if $x_{4}$ is an element of $t$, then $\MembershipmemMACRoT {x_{2} (x_{4})}{f (x_{4})}$, such that $s$ is equal to the intersection of the function that maps $x_{3}$ to the intersection of the function that maps $h_{2}$ to $f$ applied to $x_{3}$.

Mathlib.MeasureTheory.SetAlgebra

MeasureTheory.IsSetAlgebrastructureMathlib.MeasureTheory.SetAlgebra, predicate
Wording
x1 is a set algebra (from the name)
English
Let $x_{1}$ be an element of $\wp (\wp x)$. Then we can say that $x_{1}$ is a set algebra.
MeasureTheory.generateSetAlgebradefMathlib.MeasureTheory.SetAlgebra, function or constant
Wording
no wording
English
Let $x_{1}$ be an element of $\wp (\wp x)$. Then $\operatorname{generateSetAlgebra}$ applied to $x_{1}$ is an element of $\wp (\wp x)$.

Mathlib.MeasureTheory.SetSemiring

MeasureTheory.IsSetRingstructureMathlib.MeasureTheory.SetSemiring, predicate
Wording
C is a set ring (from the name)
English
Let $C$ be an element of $\wp (\wp x)$. Then we can say that $C$ is a set ring.
MeasureTheory.IsSetSemiringstructureMathlib.MeasureTheory.SetSemiring, predicate
Wording
C is a set semiring (from the name)
English
Let $C$ be an element of $\wp (\wp x)$. Then we can say that $C$ is a set semiring.
MeasureTheory.IsSetSemiring.disjointOfDiffdefMathlib.MeasureTheory.SetSemiring, function or constant
Wording
no wording
English
Assume that $C$ is a set semiring. Assume that $s$ is an element of $C$. Assume that $t$ is an element of $C$. Then $\operatorname{disjointOfDiff}$ applied to $\mathrm{hC}$, $\mathrm{hs}$ and $\mathrm{ht}$ is a finite set of $\wp x$ defined as the set of parts of $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_IsSetSemiring\_\_exists\_finpartition\_sdiff}$ applied to $\mathrm{hC}$, $\mathrm{hs}$ and $\mathrm{ht}$.
MeasureTheory.IsSetSemiring.disjointOfDiffUniondefMathlib.MeasureTheory.SetSemiring, function or constant
Wording
no wording
English
Assume that $C$ is a set semiring. Assume that $s$ is an element of $C$. Assume that $I \leq C$. Then $\operatorname{disjointOfDiffUnion}$ applied to $\mathrm{hC}$, $\mathrm{hs}$ and $\mathrm{hI}$ is a finite set of $\wp x$.
MeasureTheory.IsSetSemiring.disjointOfUniondefMathlib.MeasureTheory.SetSemiring, function or constant
Wording
no wording
English
Assume that $C$ is a set semiring. Assume that $J \leq C$. Let $j$ be an element of $\wp x$. Then $\operatorname{disjointOfUnion}$ applied to $\mathrm{hC}$, $\mathrm{hJ}$ and $j$ is a finite set of $\wp x$.

Mathlib.MeasureTheory.VectorMeasure.AddContent

MeasureTheory.VectorMeasure.of_additive_of_le_measuredefMathlib.MeasureTheory.VectorMeasure.AddContent, function or constant
Wording
no wording
English
Let $m$ be a function from elements of $\wp x$ to elements of $E$ such that for all elements $s_{2}$ of $\wp x$, the extended norm of $m$ applied to $s_{2}$ is less than or equal to $x_{3}$ applied to $s_{2}$, for all elements $s_{1}$ of $\wp x$, for all elements $t$ of $\wp x$, if $s_{1}$ is a measurable set, then if $t$ is a measurable set, then if $s_{1}$ is disjoint to $t$, then $\EqtMACRoH {m (\UnionunionMACRoAB {s_{1}}{t})}{m (s_{1})+ m (t)}$ and for all elements $s$ of $\wp x$, if $s$ is not a measurable set, then $\EqtMACRoH {m (s)}{0}$. Then $\mathrm{MeasureTheory\_\_VectorMeasure\_\_of\_additive\_of\_le\_measure}$ applied to $m$, $\mathrm{hm}$, $\mathrm{h'm}$ and $\mathrm{h''m}$ is a vector measure of $x$ and $E$.

Mathlib.MeasureTheory.VectorMeasure.Basic

MeasureTheory.VectorMeasure.adddefMathlib.MeasureTheory.VectorMeasure.Basic, function or constant
Wording
the sum of two vector measure of v and w (from the docstring)
English
Let $v$ and $w$ be vector measures of $x$ and $M$. Then the sum of two vector measure of $v$ and $w$ is a vector measure of $x$ and $M$.
MeasureTheory.VectorMeasure.diracdefMathlib.MeasureTheory.VectorMeasure.Basic, function or constant
Wording
the Dirac of x4 and v (from the name)
English
Let $x_{4}$ be an element of $x$. Let $v$ be an element of $M$. Then the Dirac of $x_{4}$ and $v$ is a vector measure of $x$ and $M$.
MeasureTheory.VectorMeasure.negdefMathlib.MeasureTheory.VectorMeasure.Basic, function or constant
Wording
the negative of v (from the docstring)
English
Let $v$ be a vector measure of $x$ and $M$. Then the negative of $v$ is a vector measure of $x$ and $M$.
MeasureTheory.VectorMeasure.smuldefMathlib.MeasureTheory.VectorMeasure.Basic, function or constant
Wording
the scalar multiple of r and v (from the name)
English
Let $r$ be an element of $R$. Let $v$ be a vector measure of $x$ and $M$. Then the scalar multiple of $r$ and $v$ is a vector measure of $x$ and $M$.
MeasureTheory.VectorMeasure.subdefMathlib.MeasureTheory.VectorMeasure.Basic, function or constant
Wording
the difference of two vector measure of v and w (from the docstring)
English
Let $v$ and $w$ be vector measures of $x$ and $M$. Then the difference of two vector measure of $v$ and $w$ is a vector measure of $x$ and $M$.

Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

BoundedVariationOn.stieltjesFunctionRightLimdefMathlib.MeasureTheory.VectorMeasure.BoundedVariation, function or constant
Wording
the Stieltjes function right limit of hf and x4 (from the name)
English
Assume that $\mathrm{BoundedVariationOn}$ holds for $f$ and the universal set. Let $x_{4}$ be an element of $x$. Then the Stieltjes function right limit of $\mathrm{hf}$ and $x_{4}$ is a Stieltjes function of $x$.
BoundedVariationOn.vectorMeasuredefMathlib.MeasureTheory.VectorMeasure.BoundedVariation, function or constant
Wording
the vector measure of hf (from the name)
English
Assume that $\mathrm{BoundedVariationOn}$ holds for $f$ and the universal set. Then the vector measure of $\mathrm{hf}$ is a vector measure of $x$ and $E$.

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

MeasureTheory.SignedMeasure.measureOfNegativesdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn, function or constant
Wording
the measure of s (from the name)
English
Let $s$ be a signed measure of $x$. Then the measure of $s$ is an element of $\wp \Real$ defined as the image of $\operatorname{coe}$ applied to $s$ and $\operatorname{ofPred}$ applied to the function that maps $B$ to the proposition that $B$ is a measurable set and the restriction of $s$ and $B$ is less than or equal to the restriction of $0$ and $B$.

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

MeasureTheory.JordanDecompositionstructureMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, type
Wording
Jordan decomposition of x (from the name)
English
Let $x$ be a set. Then the Jordan decompositions of $x$ are a basic type.
MeasureTheory.JordanDecomposition.negPartdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the negation part of self (from the name)
English
Let $\mathrm{self}$ be a Jordan decomposition of $x$. Then the negation part of $\mathrm{self}$ is a measure of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
MeasureTheory.JordanDecomposition.posPartdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the positive part part of self (from the name)
English
Let $\mathrm{self}$ be a Jordan decomposition of $x$. Then the positive part part of $\mathrm{self}$ is a measure of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
MeasureTheory.JordanDecomposition.toSignedMeasuredefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the signed measure associated with a Jordan decomposition of j (from the docstring)
English
Let $j$ be a Jordan decomposition of $x$. Then the signed measure associated with a Jordan decomposition of $j$ is a signed measure of $x$ defined as the difference between the signed measure of the positive part part of $j$ and the signed measure of the negation part of $j$.
MeasureTheory.SignedMeasure.toJordanDecompositiondefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the Jordan decomposition of s (from the name)
English
Let $s$ be a signed measure of $x$. Then the Jordan decomposition of $s$ is a Jordan decomposition of $x$.
MeasureTheory.SignedMeasure.toJordanDecompositionEquivdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the Jordan decomposition equivalence of x (from the name)
English
Let $x$ be a set. Then the Jordan decomposition equivalence of $x$ is an equivalence from the set of signed measures of $x$ to the set of Jordan decompositions of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{toJordanDecomposition}$, $\operatorname{toSignedMeasure}$, $\mathrm{MeasureTheory\_\_SignedMeasure\_\_toSignedMeasure\_toJordanDecomposition}$ and $\mathrm{MeasureTheory\_\_JordanDecomposition\_\_toJordanDecomposition\_toSignedMeasure}$.
MeasureTheory.SignedMeasure.totalVariationdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan, function or constant
Wording
the total variation of s (from the docstring)
English
Let $s$ be a signed measure of $x$. Then the total variation of $s$ is a measure of $x$ defined as the sum of the positive part part of the Jordan decomposition of $s$ and the negation part of the Jordan decomposition of $s$.

Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSubdefMathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub, function or constant
Wording
the Jordan decomposition of x and x1 (from the name)
English
Let $x$ and $x_{1}$ be measures of $X$. Then the Jordan decomposition of $x$ and $x_{1}$ is a Jordan decomposition of $X$ defined as $\operatorname{mk}$ applied to $x - x_{1}$, $x_{1} - x$ and $\mathrm{MeasureTheory\_\_Measure\_\_mutually\_singular\_measure\_sub}$.

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

MeasureTheory.ComplexMeasure.HaveLebesgueDecompositionclassMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, predicate
Wording
no wording
English
Let $c$ be a complex measure of $x$. Let $x_{1}$ be a measure of $x$. Then we can say that $\operatorname{HaveLebesgueDecomposition}$ holds for $c$ and $x_{1}$.
MeasureTheory.ComplexMeasure.rnDerivdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, function or constant
Wording
no wording
English
Let $c$ be a complex measure of $x$. Let $x_{1}$ be a measure of $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{rnDeriv}$ applied to $c$, $x_{1}$ and $x_{2}$ is a complex defined as $\operatorname{mk}$ applied to $\operatorname{rnDeriv}$ applied to $\operatorname{re}$ applied to $c$, $x_{1}$ and $x_{2}$ and $\operatorname{rnDeriv}$ applied to $\operatorname{im}$ applied to $c$, $x_{1}$ and $x_{2}$.
MeasureTheory.ComplexMeasure.singularPartdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, function or constant
Wording
the singular part of c and x1 (from the name)
English
Let $c$ be a complex measure of $x$. Let $x_{1}$ be a measure of $x$. Then the singular part of $c$ and $x_{1}$ is a complex measure of $x$ defined as the complex measure of the singular part of $\operatorname{re}$ applied to $c$ and $x_{1}$ and the singular part of $\operatorname{im}$ applied to $c$ and $x_{1}$.
MeasureTheory.SignedMeasure.HaveLebesgueDecompositionclassMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, predicate
Wording
no wording
English
Let $s$ be a signed measure of $x$. Let $x_{1}$ be a measure of $x$. Then we can say that $\operatorname{HaveLebesgueDecomposition}$ holds for $s$ and $x_{1}$.
MeasureTheory.SignedMeasure.rnDerivdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, function or constant
Wording
no wording
English
Let $s$ be a signed measure of $x$. Let $x_{1}$ be a measure of $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{rnDeriv}$ applied to $s$, $x_{1}$ and $x_{2}$ is a real number defined as the difference between $\operatorname{toReal}$ applied to $\operatorname{rnDeriv}$ applied to the positive part part of the Jordan decomposition of $s$, $x_{1}$ and $x_{2}$ and $\operatorname{toReal}$ applied to $\operatorname{rnDeriv}$ applied to the negation part of the Jordan decomposition of $s$, $x_{1}$ and $x_{2}$.
MeasureTheory.SignedMeasure.singularPartdefMathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue, function or constant
Wording
the singular part of s and x1 (from the name)
English
Let $s$ be a signed measure of $x$. Let $x_{1}$ be a measure of $x$. Then the singular part of $s$ and $x_{1}$ is a signed measure of $x$ defined as the difference between the signed measure of the singular part of the positive part part of the Jordan decomposition of $s$ and $x_{1}$ and the signed measure of the singular part of the negation part of the Jordan decomposition of $s$ and $x_{1}$.

Mathlib.MeasureTheory.VectorMeasure.Defs

MeasureTheory.SignedMeasuredefMathlib.MeasureTheory.VectorMeasure.Defs, type
Wording
signed measure of x (from the name)
English
Let $x$ be a set. Then a signed measure of $x$ is an element of the function that maps $x$ to the set of vector measures of $x$ and $\Real$.
MeasureTheory.VectorMeasurestructureMathlib.MeasureTheory.VectorMeasure.Defs, type
Wording
vector measure of x and M (from the name)
English
Let $x$ and $M$ be sets. Then the vector measures of $x$ and $M$ are a basic type.
MeasureTheory.VectorMeasure.measureOf'defMathlib.MeasureTheory.VectorMeasure.Defs, function or constant
Wording
the measure of self and x4 (from the name)
English
Let $\mathrm{self}$ be a vector measure of $x$ and $M$. Let $x_{4}$ be an element of $\wp x$. Then the measure of $\mathrm{self}$ and $x_{4}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

Mathlib.MeasureTheory.VectorMeasure.Integral

MeasureTheory.VectorMeasure.IntegrabledefMathlib.MeasureTheory.VectorMeasure.Integral, predicate
Wording
no wording
English
Let $x_{2}$ be a vector measure of $X$ and $F$. Let $f$ be a function from elements of $X$ to elements of $E$. Then $\operatorname{Integrable}$ holds for $x_{2}$ and $f$, if $\operatorname{Integrable}$ holds for $f$ and the variation of $x_{2}$.
MeasureTheory.VectorMeasure.IntegrableOndefMathlib.MeasureTheory.VectorMeasure.Integral, predicate
Wording
no wording
English
Let $x_{2}$ be a vector measure of $X$ and $F$. Let $f$ be a function from elements of $X$ to elements of $E$. Let $s$ be an element of $\wp X$. Then $\operatorname{IntegrableOn}$ holds for $x_{2}$, $f$ and $s$, if $\operatorname{Integrable}$ holds for the restriction of $x_{2}$ and $s$ and $f$.
MeasureTheory.VectorMeasure.integraldefMathlib.MeasureTheory.VectorMeasure.Integral, function or constant
Wording
the integral of f and B (from the name)
English
Let $x_{6}$ be a vector measure of $X$ and $F$. Let $f$ be a function from elements of $X$ to elements of $E$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the integral of $f$ and $B$ is an element of $G$ defined as the set to function of $\operatorname{coe}$ applied to the transpose of $x_{6}$ and $B$ and $f$.
MeasureTheory.VectorMeasure.transposedefMathlib.MeasureTheory.VectorMeasure.Integral, function or constant
Wording
the transpose of x6 and B (from the name)
English
Let $x_{6}$ be a vector measure of $X$ and $F$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the transpose of $x_{6}$ and $B$ is a vector measure of $X$ and the set of continuous linear maps of $E$ and $G$.
MeasureTheory.cbmApplyMeasuredefMathlib.MeasureTheory.VectorMeasure.Integral, function or constant
Wording
no wording
English
Let $x_{6}$ be a vector measure of $X$ and $F$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Let $s$ be an element of $\wp X$. Then $\operatorname{cbmApplyMeasure}$ applied to $x_{6}$, $B$ and $s$ is a continuous linear map of $E$ and $G$.

Mathlib.MeasureTheory.VectorMeasure.Operations

MeasureTheory.Measure.toENNRealVectorMeasuredefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
no wording
English
Let $x_{1}$ be a measure of $x$. Then $\operatorname{toENNRealVectorMeasure}$ applied to $x_{1}$ is a vector measure of $x$ and $\mathrm{ENNReal}$.
MeasureTheory.Measure.toSignedMeasuredefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the signed measure of x1 (from the name)
English
Let $x_{1}$ be a measure of $x$. Then the signed measure of $x_{1}$ is a signed measure of $x$.
MeasureTheory.VectorMeasure.ennrealToMeasuredefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the extended nonnegative real number to measure of v (from the name)
English
Let $v$ be a vector measure of $x$ and $\mathrm{ENNReal}$. Then the extended nonnegative real number to measure of $v$ is a measure of $x$ defined as the measure of the function that maps $s$ and $h$ to $v$ applied to $s$.
MeasureTheory.VectorMeasure.equivMeasuredefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the equivalence measure (from the name)
English
The equivalence measure is an equivalence from the set of vector measures of $x$ and $\mathrm{ENNReal}$ to the set of measures of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{ennrealToMeasure}$, $\operatorname{toENNRealVectorMeasure}$, $\mathrm{MeasureTheory\_\_Measure\_\_toENNRealVectorMeasure\_ennrealToMeasure}$ and $\mathrm{MeasureTheory\_\_VectorMeasure\_\_ennrealToMeasure\_toENNRealVectorMeasure}$.
MeasureTheory.VectorMeasure.mapdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the map of v and f (from the name)
English
Let $v$ be a vector measure of $x$ and $M$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $v$ and $f$ is a vector measure of $x_{1}$ and $M$.
MeasureTheory.VectorMeasure.mapGmdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
no wording
English
Let $f$ be a function from elements of $x_{4}$ to elements of $x$. Then $\operatorname{mapGm}$ applied to $f$ is an additive monoid homomorphism of the set of vector measures of $x_{4}$ and $M$ and the set of vector measures of $x$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $v$ to the map of $v$ and $f$ and $\mathrm{MeasureTheory\_\_VectorMeasure\_\_map\_zero}$ applied to $f$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{MeasureTheory\_\_VectorMeasure\_\_map\_add}$ applied to $x_{6}$, $x_{7}$ and $f$.
MeasureTheory.VectorMeasure.mapRangedefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the map range of v and f (from the name)
English
Let $v$ be a vector measure of $x$ and $M$. Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the map range of $v$ and $f$ is a vector measure of $x$ and $N$.
MeasureTheory.VectorMeasure.mapRangeHomdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the map range homomorphism of f and hf (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and $N$ such that $\operatorname{coe}$ applied to $f$ is continuous. Then the map range homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of vector measures of $x_{4}$ and $M$ and the set of vector measures of $x_{4}$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $v$ to the map range of $v$ and $f$ and $\mathrm{MeasureTheory\_\_VectorMeasure\_\_mapRange\_zero}$ applied to $\mathrm{hf}$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{MeasureTheory\_\_VectorMeasure\_\_mapRange\_add}$ applied to $\mathrm{hf}$.
MeasureTheory.VectorMeasure.mapRangeLdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the map range of f (from the name)
English
Let $f$ be a continuous linear map of $M$ and $N$. Then the map range of $f$ is a linear map of the set of vector measures of $x_{7}$ and $M$ and the set of vector measures of $x_{7}$ and $N$.
MeasureTheory.VectorMeasure.mapₗdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the map of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $f$ is a linear map of the set of vector measures of $x$ and $M$ and the set of vector measures of $x_{1}$ and $M$.
MeasureTheory.VectorMeasure.restrictdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
the restriction of v and i (from the docstring)
English
Let $v$ be a vector measure of $x$ and $M$. Let $i$ be an element of $\wp x$. Then the restriction of $v$ and $i$ is a vector measure of $x$ and $M$.
MeasureTheory.VectorMeasure.restrictGmdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
no wording
English
Let $i$ be an element of $\wp x_{2}$. Then $\operatorname{restrictGm}$ applied to $i$ is an additive monoid homomorphism of the set of vector measures of $x_{2}$ and $M$ and the set of vector measures of $x_{2}$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $v$ to the restriction of $v$ and $i$ and $\mathrm{MeasureTheory\_\_VectorMeasure\_\_restrict\_zero}$ and the function that maps $x_{4}$ and $x_{5}$ to $\mathrm{MeasureTheory\_\_VectorMeasure\_\_restrict\_add}$ applied to $x_{4}$, $x_{5}$ and $i$.
MeasureTheory.VectorMeasure.restrictₗdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
no wording
English
Let $i$ be an element of $\wp x$. Then $\mathrm{MeasureTheory\_\_VectorMeasure\_\_restrict\_u2097\_}$ applied to $i$ is a linear map of the set of vector measures of $x$ and $M$ and the set of vector measures of $x$ and $M$.
MeasureTheory.VectorMeasure.trimdefMathlib.MeasureTheory.VectorMeasure.Operations, function or constant
Wording
no wording
English
Let $v$ be a vector measure of $x$ and $M$. Assume that $m \leq n$. Then $\operatorname{trim}$ applied to $v$ and $\mathrm{hle}$ is a vector measure of $x$ and $M$.

Mathlib.MeasureTheory.VectorMeasure.Order

MeasureTheory.SignedMeasure.toMeasureOfLEZerodefMathlib.MeasureTheory.VectorMeasure.Order, function or constant
Wording
the measure of s and i (from the name)
English
Let $s$ be a signed measure of $x$. Let $i$ be an element of $\wp x$ such that $i$ is a measurable set and the restriction of $s$ and $i$ is less than or equal to the restriction of $0$ and $i$. Then the measure of $s$ and $i$ is a measure of $x$.
MeasureTheory.SignedMeasure.toMeasureOfZeroLEdefMathlib.MeasureTheory.VectorMeasure.Order, function or constant
Wording
the measure of s and i (from the name)
English
Let $s$ be a signed measure of $x$. Let $i$ be an element of $\wp x$ such that $i$ is a measurable set and the restriction of $0$ and $i$ is less than or equal to the restriction of $s$ and $i$. Then the measure of $s$ and $i$ is a measure of $x$.
MeasureTheory.SignedMeasure.toMeasureOfZeroLE'defMathlib.MeasureTheory.VectorMeasure.Order, function or constant
Wording
the measure of i and j (from the name)
English
Let $s$ be a signed measure of $x$. Let $i$ and $j$ be elements of $\wp x$ such that the restriction of $0$ and $i$ is less than or equal to the restriction of $s$ and $i$ and $j$ is a measurable set. Then the measure of $i$ and $j$ is an element of $\mathrm{ENNReal}$.

Mathlib.MeasureTheory.VectorMeasure.Prod

MeasureTheory.VectorMeasure.HasProdclassMathlib.MeasureTheory.VectorMeasure.Prod, predicate
Wording
no wording
English
Let $x_{6}$ be a vector measure of $X$ and $E$. Let $x_{7}$ be a vector measure of $Y$ and $F$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then we can say that $\operatorname{HasProd}$ holds for $x_{6}$, $x_{7}$ and $B$.
MeasureTheory.VectorMeasure.proddefMathlib.MeasureTheory.VectorMeasure.Prod, function or constant
Wording
the product of x7 and B (from the name)
English
Let $x_{6}$ be a vector measure of $X$ and $E$. Let $x_{7}$ be a vector measure of $Y$ and $F$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the product of $x_{7}$ and $B$ is a vector measure of $\mathrm{Prod}$ applied to $X$ and $Y$ and $G$ defined as $\mathrm{dite}$ applied to $\operatorname{HasProd}$ applied to $x_{6}$, $x_{7}$ and $B$, the function that maps $h$ to $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_VectorMeasure\_\_HasProd\_\_exists\_prod}$ and the function that maps $h_{1}$ to $0$.

Mathlib.MeasureTheory.VectorMeasure.Relations

MeasureTheory.VectorMeasure.AbsolutelyContinuousdefMathlib.MeasureTheory.VectorMeasure.Relations, predicate
Wording
no wording
English
Let $v$ be a vector measure of $x$ and $M$. Let $w$ be a vector measure of $x$ and $N$. Then $\operatorname{AbsolutelyContinuous}$ holds for $v$ and $w$, if for all elements $s$ of $\wp x$, if $\EqtMACRoH {w (s)}{0}$, then $\EqtMACRoH {v (s)}{0}$.
MeasureTheory.VectorMeasure.MutuallySingulardefMathlib.MeasureTheory.VectorMeasure.Relations, predicate
Wording
no wording
English
Let $v$ be a vector measure of $x$ and $M$. Let $w$ be a vector measure of $x$ and $N$. Then $\operatorname{MutuallySingular}$ holds for $v$ and $w$, if there exists an element $s$ of $\wp x$, such that $s$ is a measurable set, for all elements $t$ of $\wp x$, if $t \leq s$, then $\EqtMACRoH {v (t)}{0}$ and for all elements $t_{1}$ of $\wp x$, if $t_{1}$ is less than or equal to the complement of $s$, then $\EqtMACRoH {w (t_{1})}{0}$.

Mathlib.MeasureTheory.VectorMeasure.TotalVariation

MeasureTheory.VectorMeasure.etvDistdefMathlib.MeasureTheory.VectorMeasure.TotalVariation, function or constant
Wording
no wording
English
Let $x_{3}$ and $x_{4}$ be vector measures of $x$ and $M$. Then $\operatorname{etvDist}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{variation}$ applied to $x_{3} - x_{4}$ and the universal set.

Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

MeasureTheory.VectorMeasure.ennrealVariationdefMathlib.MeasureTheory.VectorMeasure.Variation.Defs, function or constant
Wording
the variation of x2 (from the docstring)
English
Let $x_{2}$ be a vector measure of $X$ and $V$. Then the variation of $x_{2}$ is a vector measure of $X$ and $\mathrm{ENNReal}$ defined as $\operatorname{toENNRealVectorMeasure}$ applied to the variation of $x_{2}$.
MeasureTheory.VectorMeasure.variationdefMathlib.MeasureTheory.VectorMeasure.Variation.Defs, function or constant
Wording
the variation of x2 (from the docstring)
English
Let $x_{2}$ be a vector measure of $X$ and $V$. Then the variation of $x_{2}$ is a measure of $X$.

Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

MeasureTheory.VectorMeasure.bounddefMathlib.MeasureTheory.VectorMeasure.Variation.Semivariation, function or constant
Wording
the bound of x2 (from the name)
English
Let $x_{2}$ be a vector measure of $X$ and $E$. Then the bound of $x_{2}$ is an element of $\mathrm{NNReal}$ defined as $\operatorname{toNNReal}$ applied to $\operatorname{semivariation}$ applied to $x_{2}$ and the universal set.
MeasureTheory.VectorMeasure.semivariationdefMathlib.MeasureTheory.VectorMeasure.Variation.Semivariation, function or constant
Wording
no wording
English
Let $x_{2}$ be a vector measure of $X$ and $E$. Let $s$ be an element of $\wp X$. Then $\operatorname{semivariation}$ applied to $x_{2}$ and $s$ is an element of $\mathrm{ENNReal}$.

Mathlib.MeasureTheory.VectorMeasure.WithDensity

MeasureTheory.Measure.withDensityᵥdefMathlib.MeasureTheory.VectorMeasure.WithDensity, function or constant
Wording
no wording
English
Let $x_{3}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Then $\mathrm{MeasureTheory\_\_Measure\_\_withDensity\_u1d65\_}$ applied to $x_{3}$ and $f$ is a vector measure of $x$ and $E$.

Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

MeasureTheory.VectorMeasure.withDensitydefMathlib.MeasureTheory.VectorMeasure.WithDensityVec, function or constant
Wording
no wording
English
Let $x_{6}$ be a vector measure of $X$ and $F$. Let $f$ be a function from elements of $X$ to elements of $E$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then $\operatorname{withDensity}$ applied to $x_{6}$, $f$ and $B$ is a vector measure of $X$ and $G$.

‹ previous next ›