BoreldefMathlib.MeasureTheory.Category.MeasCat, function or constantEnglish
$\mathrm{Borel}$ is a functor of the set of topological categories and the set of measurable categories defined as the forgetful functor of the set of topological categories and the set of measurable categories.
MeasCatstructureMathlib.MeasureTheory.Category.MeasCat, typeWording
measurable category (from the name)
English
The measurable categories are a basic type.
MeasCat.GirydefMathlib.MeasureTheory.Category.MeasCat, function or constantEnglish
$\operatorname{Giry}$ is a monad of the set of measurable categories.
MeasCat.IntegraldefMathlib.MeasureTheory.Category.MeasCat, function or constantWording
the integral (from the name)
English
The integral is an algebra of $\operatorname{Giry}$.
MeasCat.MeasuredefMathlib.MeasureTheory.Category.MeasCat, function or constantWording
the measure (from the name)
English
The measure is a functor of the set of measurable categories and the set of measurable categories.
MeasCat.carrierdefMathlib.MeasureTheory.Category.MeasCat, typeWording
carrier of self (from the name)
English
Let $\mathrm{self}$ be a measurable category. Then a carrier of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
BorelSpaceclassMathlib.MeasureTheory.Constructions.BorelSpace.Basic, predicateWording
x is a Borel space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a Borel space.
Homeomorph.toMeasurableEquivdefMathlib.MeasureTheory.Constructions.BorelSpace.Basic, function or constantWording
the measurable equivalence of h2 (from the name)
English
Let $h_{2}$ be a homeomorphism of $x$ and $x_{1}$. Then the measurable equivalence of $h_{2}$ is a measurable equivalence of $x$ and $x_{1}$.
OpensMeasurableSpaceclassMathlib.MeasureTheory.Constructions.BorelSpace.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{OpensMeasurableSpace}$ holds for $x$.
SecondCountableTopologyEitherclassMathlib.MeasureTheory.Constructions.BorelSpace.Basic, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{SecondCountableTopologyEither}$ holds for $x$ and $x_{1}$.
MeasurableEquiv.continuousMapToFundefMathlib.MeasureTheory.Constructions.BorelSpace.ContinuousMap, function or constantWording
the continuous map to function of X and Y (from the name)
English
Let $X$ and $Y$ be sets. Then the continuous map to function of $X$ and $Y$ is a measurable equivalence of the set of continuous maps of $X$ and $Y$ and $\SubtypeSet {f}{\mathrm{Continuous} (f)}$.
ENNReal.ennrealEquivSumdefMathlib.MeasureTheory.Constructions.BorelSpace.Real, function or constantWording
the extended nonnegative real number equivalence sum (from the name)
English
The extended nonnegative real number equivalence sum is a measurable equivalence of $\mathrm{ENNReal}$ and $\mathrm{Sum}$ applied to $\mathrm{NNReal}$ and $\mathrm{Unit}$.
MeasurableEquiv.ennrealEquivNNRealdefMathlib.MeasureTheory.Constructions.BorelSpace.Real, function or constantEnglish
$\operatorname{ennrealEquivNNReal}$ is a measurable equivalence of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that $r$ is distinct from the top and $\mathrm{NNReal}$ defined as the measurable equivalence of $\operatorname{neTopHomeomorphNNReal}$.
MeasurableEquiv.erealEquivRealdefMathlib.MeasureTheory.Constructions.BorelSpace.Real, function or constantEnglish
$\operatorname{erealEquivReal}$ is a measurable equivalence of the set of elements of the complement of $\operatorname{insert}$ applied to the bottom and $\operatorname{singleton}$ applied to the top and $\Real$ defined as the measurable equivalence of $\operatorname{neBotTopHomeomorphReal}$.
Real.finiteSpanningSetsInIooRatdefMathlib.MeasureTheory.Constructions.BorelSpace.Real, function or constantWording
the finite spanning set in open interval rational number of x (from the name)
English
Let $x$ be a measure of $\Real$. Then the finite spanning set in open interval rational number of $x$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $x$ and the union of the function that maps $a$ to the union of the function that maps $b$ to the union of the function that maps $h_{1}$ to $\operatorname{singleton}$ applied to the open interval of $\operatorname{cast}$ applied to $a$ and $\operatorname{cast}$ applied to $b$.
WithTop.MeasurableEquiv.neTopEquivdefMathlib.MeasureTheory.Constructions.BorelSpace.WithTop, function or constantEnglish
$\operatorname{neTopEquiv}$ is a measurable equivalence of the set of elements of $\operatorname{ofPred}$ applied to the function that maps $r$ to the proposition that $r$ is distinct from the top and $x$ defined as the measurable equivalence of $\operatorname{neTopHomeomorph}$ applied to $x$.
WithTop.measurableEquivSumdefMathlib.MeasureTheory.Constructions.BorelSpace.WithTop, function or constantWording
the measurable equivalence sum (from the name)
English
The measurable equivalence sum is a measurable equivalence of $\mathrm{WithTop}$ applied to $x$ and $\mathrm{Sum}$ applied to $x$ and $\mathrm{Unit}$.
MeasureTheory.closedCompactCylindersdefMathlib.MeasureTheory.Constructions.ClosedCompactCylinders, function or constantWording
the closed compact cylinder of X (from the name)
English
Let $X$ be a function from elements of $x$ to sets. Then the closed compact cylinder of $X$ is an element of $\wp (\wp (\mathrm{Elem} (x)\rightarrow X (i)))$ defined as the union of the function that maps $s$ to the union of the function that maps $S$ to the union of the function that maps $h$ to the union of the function that maps $h_{1}$ to $\operatorname{singleton}$ applied to the cylinder of $s$ and $S$.
MeasureTheory.closedCompactCylinders.finsetdefMathlib.MeasureTheory.Constructions.ClosedCompactCylinders, function or constantWording
the finite set of ht (from the name)
English
Assume that $t$ is an element of the closed compact cylinder of $X$. Then the finite set of $\mathrm{ht}$ is a finite set of $x$.
MeasureTheory.closedCompactCylinders.setdefMathlib.MeasureTheory.Constructions.ClosedCompactCylinders, function or constantWording
the set of ht (from the name)
English
Assume that $\MembershipmemMACRoT {\operatorname{closedCompactCylinders} (X)}{t}$. Then the set of $\mathrm{ht}$ is an element of $\wp (\mathrm{Elem} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{finset} (\mathrm{ht})}{x_{2}})})\rightarrow X (i))$.
MeasureTheory.cylinderdefMathlib.MeasureTheory.Constructions.Cylinders, function or constantWording
the cylinder of s and S (from the name)
English
Let $s$ be a finite set of $x$. Let $S$ be an element of $\wp (\mathrm{Elem} (\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {s}{x_{2}})})\rightarrow x_{1} (i_{1}))$. Then the cylinder of $s$ and $S$ is an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i))$ defined as the preimage of $\operatorname{restrict}$ applied to $s$ and $S$.
MeasureTheory.measurableCylindersdefMathlib.MeasureTheory.Constructions.Cylinders, function or constantWording
the measurable cylinder of x1 (from the name)
English
Let $x_{1}$ be a function from elements of $x$ to sets. Then the measurable cylinder of $x_{1}$ is an element of $\wp (\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i)))$ defined as the union of the function that maps $s$ to the union of the function that maps $S$ to the union of the function that maps $h$ to $\operatorname{singleton}$ applied to the cylinder of $s$ and $S$.
MeasureTheory.measurableCylinders.finsetdefMathlib.MeasureTheory.Constructions.Cylinders, function or constantWording
the finite set of ht (from the name)
English
Assume that $t$ is an element of the measurable cylinder of $x_{1}$. Then the finite set of $\mathrm{ht}$ is a finite set of $x$.
MeasureTheory.measurableCylinders.setdefMathlib.MeasureTheory.Constructions.Cylinders, function or constantWording
the set of ht (from the name)
English
Assume that $\MembershipmemMACRoT {\operatorname{measurableCylinders} (x_{1})}{t}$. Then the set of $\mathrm{ht}$ is an element of $\wp (\mathrm{Elem} (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{finset} (\mathrm{ht})}{x_{3}})})\rightarrow x_{1} (i))$.
MeasureTheory.squareCylindersdefMathlib.MeasureTheory.Constructions.Cylinders, function or constantWording
the square cylinder of C (from the name)
English
Let $C$ be a function from elements $i_{1}$ of $x$ to elements of $\wp (\wp x_{1} (i_{1}))$. Then the square cylinder of $i_{1}$ is an element of $\wp (\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i)))$ defined as the function that maps $C$ to $\operatorname{ofPred}$ applied to the function that maps $S$ to the proposition that there exists a finite set $s$ of $x$, such that there exists a function $t$ from elements $i_{1}$ of $x$ to elements of $\wp x_{1} (i_{1})$, such that $t$ is an element of the product of the universal set and $i_{1}$ and $S$ is equal to the product of $s$ and $t$ and $C$.
MeasureTheory.Measure.finiteSpanningSetsIn_volumeIoiPow_range_IiodefMathlib.MeasureTheory.Constructions.HaarToSphere, function or constantEnglish
Let $n$ be a natural number. Then $\mathrm{MeasureTheory\_\_Measure\_\_finiteSpanningSetsIn\_volumeIoiPow\_range\_Iio}$ applied to $n$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to $\operatorname{volumeIoiPow}$ applied to $n$ and the range of $\operatorname{Iio}$.
MeasureTheory.Measure.toSpheredefMathlib.MeasureTheory.Constructions.HaarToSphere, function or constantWording
the sphere of x3 (from the name)
English
Let $x_{3}$ be a measure of $E$. Then the sphere of $x_{3}$ is a measure of the set of elements of the sphere of $0$ and $1$ defined as $\HSMulhSMulMACRoAL {\operatorname{finrank} (\Real , E)}{\operatorname{fst} (\operatorname{restrict} (\operatorname{comap} (\operatorname{comp} (\lambda x_{4} . \MembershipmemMACRoT {\operatorname{compl} (\operatorname{singleton} (0))}{x_{4}}, \operatorname{coe} (\operatorname{symm} (\mathrm{homeomorphUnitSphereProd} (E)))), x_{3}), \operatorname{sprod} (\operatorname{univ} , \operatorname{Iio} (1))))}$.
MeasureTheory.Measure.toSphereBallBounddefMathlib.MeasureTheory.Constructions.HaarToSphere, function or constantWording
the sphere ball bound of n and x (from the name)
English
Let $n$ be a natural number. Let $x$ be a real number. Then the sphere ball bound of $n$ and $x$ is an element of $\mathrm{NNReal}$ defined as $\iteMACRoG {\mathrm{and} (\mathrm{Neq} (n , 0), \mathrm{Lt} (0 , x))}{(n \times (\frac{ \MinminMACRoAG {\operatorname{toNNReal} (x)}{2}}{4})^ {n})}{1}$.
MeasureTheory.Measure.volumeIoiPowdefMathlib.MeasureTheory.Constructions.HaarToSphere, function or constantEnglish
Let $n$ be a natural number. Then $\operatorname{volumeIoiPow}$ applied to $n$ is a measure of the set of elements of $\operatorname{Ioi}$ applied to $0$ defined as $\operatorname{withDensity}$ applied to the preimage of the function that maps $x$ to $\MembershipmemMACRoT {\operatorname{Ioi} (0)}{x}$ and the volume and the function that maps $r$ to $\operatorname{ofReal}$ applied to $r ^ {n}$.
MeasureTheory.Measure.FiniteSpanningSetsIn.pidefMathlib.MeasureTheory.Constructions.Pi, function or constantWording
the product of x5 (from the name)
English
Let $x_{5}$ be a function from elements $i$ of $x$ to elements of $\operatorname{FiniteSpanningSetsIn}$ applied to $x_{4}$ applied to $i$ and $C$ applied to $i$. Then the product of $i$ is an element of $\operatorname{FiniteSpanningSetsIn}$ applied to the finite product of the measures of $x_{4}$ and the image of $\operatorname{pi}$ applied to the universal set and the product of the universal set and $C$.
MeasureTheory.Measure.pidefMathlib.MeasureTheory.Constructions.Pi, function or constantWording
the finite product of the measures of x4 (from the docstring)
English
Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to measures of $x_{1}$ applied to $i_{1}$. Then the finite product of the measures of $i_{1}$ is a 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 $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_Measure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Constructions\_\_Pi\_\_668077722\_\_\_hygCtx\_\_\_hyg\_\_2}$, $i_{1}$ and $x_{4}$.
MeasureTheory.Measure.pi'defMathlib.MeasureTheory.Constructions.Pi, function or constantWording
the product of x4 (from the name)
English
Let $x_{4}$ be a function from elements $i_{1}$ of $x$ to measures of $x_{1}$ applied to $i_{1}$. Then the product of $i_{1}$ is a 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 map of $\operatorname{elim'}$ and $\operatorname{tprod}$ applied to $\operatorname{sortedUniv}$ applied to $x$ and $i_{1}$.
MeasureTheory.Measure.tproddefMathlib.MeasureTheory.Constructions.Pi, function or constantEnglish
Let $l$ be a list of elements of $x$. Let $x_{2}$ be a function from elements $i$ of $x$ to measures of $X$ applied to $i$. Then $\operatorname{tprod}$ applied to $l$, $i$ and $x_{2}$ is a measure of the set of products of $X$ and $l$.
MeasureTheory.OuterMeasure.pidefMathlib.MeasureTheory.Constructions.Pi, function or constantWording
the finite product of the outer measures of m (from the docstring)
English
Let $m$ be a function from elements $i_{1}$ of $x$ to outer measures of $x_{1}$ applied to $i_{1}$. Then the finite product of the outer measures of $i_{1}$ is an outer 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 $m$ to $\operatorname{boundedBy}$ applied to $\operatorname{piPremeasure}$ applied to $i_{1}$ and $m$.
MeasureTheory.piPremeasuredefMathlib.MeasureTheory.Constructions.Pi, function or constantEnglish
Let $m$ be a function from elements $i_{1}$ of $x$ to outer measures of $x_{1}$ applied to $i_{1}$. Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i))$. Then $\operatorname{piPremeasure}$ applied to $i_{1}$, $m$ and $s$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $s$ to $\FinsetProd {\FinsetunivMACRoAC}{i}{i_{1} (i , \operatorname{image} (\operatorname{eval} (i), m))}{s}$.
MeasureTheory.AnalyticSetdefMathlib.MeasureTheory.Constructions.Polish.Basic, predicateWording
s is a analytic set (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is an analytic set, if $\operatorname{proj0}$ holds for $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Constructions\_\_Polish\_\_Basic\_\_3011411360\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $s$.
MeasureTheory.MeasurablySeparabledefMathlib.MeasureTheory.Constructions.Polish.Basic, predicateEnglish
Let $s$ and $t$ be elements of $\wp x$. Then $\operatorname{MeasurablySeparable}$ holds for $s$ and $t$, if there exists an element $u$ of $\wp x$, such that $s \leq u$, $t$ is disjoint to $u$ and $u$ is a measurable set.
PolishSpace.Equiv.measurableEquivdefMathlib.MeasureTheory.Constructions.Polish.Basic, function or constantWording
the measurable equivalence of e (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{1}$. Then the measurable equivalence of $e$ is a measurable equivalence of $x$ and $x_{1}$.
PolishSpace.borelSchroederBernsteindefMathlib.MeasureTheory.Constructions.Polish.Basic, function or constantEnglish
Assume that $f$ is measurable. Assume that $f$ is injective. Assume that $g$ is measurable. Assume that $g$ is injective. Then $\operatorname{borelSchroederBernstein}$ applied to $\mathrm{fmeas}$, $\mathrm{finj}$, $\mathrm{gmeas}$ and $\mathrm{ginj}$ is a measurable equivalence of $x$ and $x_{1}$.
PolishSpace.measurableEquivNatBoolOfNotCountabledefMathlib.MeasureTheory.Constructions.Polish.Basic, function or constantWording
the measurable equivalence natural bool of h1 (from the name)
English
Assume that $x$ is not countable. Then the measurable equivalence natural bool of $h_{1}$ is a measurable equivalence of $x$ and the set of functions from natural numbers to elements of $\mathrm{Bool}$.
PolishSpace.measurableEquivOfNotCountabledefMathlib.MeasureTheory.Constructions.Polish.Basic, function or constantWording
the measurable equivalence of h2 and h3 (from the name)
English
Assume that $x$ is not countable. Assume that $x_{1}$ is not countable. Then the measurable equivalence of $h_{2}$ and $h_{3}$ is a measurable equivalence of $x$ and $x_{1}$ defined as the composition of the measurable equivalence natural bool of $h_{2}$ and the inverse of the measurable equivalence natural bool of $h_{3}$.
StandardBorelSpaceclassMathlib.MeasureTheory.Constructions.Polish.Basic, predicateWording
x is a standard Borel space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a standard Borel space.
UpgradedStandardBorelclassMathlib.MeasureTheory.Constructions.Polish.Basic, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{UpgradedStandardBorel}$ holds for $x$.
MeasureTheory.embeddingRealdefMathlib.MeasureTheory.Constructions.Polish.EmbeddingReal, function or constantEnglish
Let $x$ be a set. Let $x_{2}$ be an element of $x$. Then $\operatorname{embeddingReal}$ applied to $x$ and $x_{2}$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_exists\_measurableEmbedding\_real}$ applied to $x$ and $x_{2}$.
MeasureTheory.IsProjectiveLimitdefMathlib.MeasureTheory.Constructions.Projective, predicateEnglish
Let $x_{3}$ be a measure of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Let $P$ be a function from finite sets $J$ of $x$ to measures of the set of functions from elements $j$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {J}{x_{4}})}$ to elements of $x_{1}$ applied to $j$. Then $\operatorname{IsProjectiveLimit}$ holds for $x_{3}$, $J$ and $P$, if for all finite sets $I$ of $x$, the map of $\operatorname{restrict}$ applied to $I$ and $x_{3}$ is equal to $J$ applied to $I$.
MeasureTheory.IsProjectiveMeasureFamilydefMathlib.MeasureTheory.Constructions.Projective, predicateWording
P is a projective measure family (from the name)
English
Let $P$ be a function from finite sets $J$ of $x$ to measures of the set of functions from elements $j$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {J}{x_{3}})}$ to elements of $x_{1}$ applied to $j$. Then $J$ is a projective measure family, if for all finite sets $I$ and $J$ of $x$, for all elements $\mathrm{hJI}$ of $\mathrm{Proof}$ applied to $\mathrm{Leq} (J , I)$, $J$ applied to $J$ is equal to the map of $\mathrm{Finset\_\_restrict\_u2082\_}$ applied to $\mathrm{hJI}$ and $J$ applied to $I$.
MeasureTheory.projectiveFamilyContentdefMathlib.MeasureTheory.Constructions.ProjectiveFamilyContent, function or constantWording
the projective family content of hP (from the name)
English
Assume that $P$ is a projective measure family. Then the projective family content of $\mathrm{hP}$ is an additive content of $\mathrm{ENNReal}$ and the measurable cylinder of $x_{1}$ defined as the additive content of $\operatorname{projectiveFamilyFun}$ applied to $P$.
MeasureTheory.projectiveFamilyFundefMathlib.MeasureTheory.Constructions.ProjectiveFamilyContent, function or constantWording
the projective family function of P and J (from the name)
English
Let $P$ be a function from finite sets $J$ of $x$ to measures of the set of functions from elements $j$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {J}{x_{3}})}$ to elements of $x_{1}$ applied to $j$. Let $s$ be an element of $\wp (\mathrm{Elem} (x)\rightarrow x_{1} (i))$. Then the projective family function of $J$ and $P$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $s$ to $\mathrm{dite}$ applied to the proposition that $P$ is an element of the measurable cylinder of $x_{1}$, the function that maps $\mathrm{hs}$ to $J$ applied to the finite set of $\mathrm{hs}$ and the set of $\mathrm{hs}$, the function that maps $\mathrm{hs1}$ to $0$ and $s$.
unitInterval.symmMeasurableEquivdefMathlib.MeasureTheory.Constructions.UnitInterval, function or constantWording
the inverse measurable equivalence (from the name)
English
The inverse measurable equivalence is a measurable equivalence of the set of elements of the unit interval and the set of elements of the unit interval.
Besicovitch.BallPackagestructureMathlib.MeasureTheory.Covering.Besicovitch, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\operatorname{BallPackage}$ applied to $x$ and $x_{1}$ are a basic type.
Besicovitch.BallPackage.cdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{BallPackage}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{c}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
Besicovitch.BallPackage.rdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{BallPackage}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{r}$ applied to $\mathrm{self}$ and $x_{2}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{2}$.
Besicovitch.BallPackage.r_bounddefMathlib.MeasureTheory.Covering.Besicovitch, function or constantWording
the bound of self (from the name)
English
Let $\mathrm{self}$ be an element of $\operatorname{BallPackage}$ applied to $x$ and $x_{1}$. Then the bound of $\mathrm{self}$ is a real number defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
Besicovitch.SatelliteConfigstructureMathlib.MeasureTheory.Covering.Besicovitch, typeWording
satellite configuration of N and x2 (from the name)
English
Let $x$ be a set. Let $N$ be a natural number. Let $x_{2}$ be a real number. Then the satellite configurations of $N$ and $x_{2}$ are a basic type.
Besicovitch.SatelliteConfig.cdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $\mathrm{self}$ be a satellite configuration of $N$ and $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Fin}$ applied to the successor of $N$. Then $\operatorname{c}$ applied to $\mathrm{self}$ and $x_{3}$ is an element of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
Besicovitch.SatelliteConfig.rdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $\mathrm{self}$ be a satellite configuration of $N$ and $x_{2}$. Let $x_{3}$ be an element of $\mathrm{Fin}$ applied to the successor of $N$. Then $\operatorname{r}$ applied to $\mathrm{self}$ and $x_{3}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{3}$.
Besicovitch.TauPackagestructureMathlib.MeasureTheory.Covering.Besicovitch, typeEnglish
Let $x$ and $x_{1}$ be sets. Then the elements of $\operatorname{TauPackage}$ applied to $x$ and $x_{1}$ are a basic type.
Besicovitch.TauPackage.RdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $p$ be an element of $\operatorname{TauPackage}$ applied to $x_{2}$ and $x$. Let $i$ be an ordinal. Then $\operatorname{R}$ applied to $p$ and $i$ is a real number defined as the supremum of the function that maps $b$ to $\operatorname{r}$ applied to $\operatorname{toBallPackage}$ applied to $p$ and $b$.
Besicovitch.TauPackage.colordefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $p$ be an element of $\operatorname{TauPackage}$ applied to $x_{2}$ and $x$. Let $x_{3}$ be an ordinal. Then $\operatorname{color}$ applied to $p$ and $x_{3}$ is a natural number.
Besicovitch.TauPackage.iUnionUpTodefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $p$ be an element of $\operatorname{TauPackage}$ applied to $x_{2}$ and $x$. Let $i$ be an ordinal. Then $\operatorname{iUnionUpTo}$ applied to $p$ and $i$ is an element of $\wp x$ defined as the union of the function that maps $j$ to the ball of $\operatorname{c}$ applied to $\operatorname{toBallPackage}$ applied to $p$ and the index of $p$ and $j$ and $\operatorname{r}$ applied to $\operatorname{toBallPackage}$ applied to $p$ and the index of $p$ and $j$.
Besicovitch.TauPackage.indexdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantWording
the index of p and x3 (from the name)
English
Let $p$ be an element of $\operatorname{TauPackage}$ applied to $x_{2}$ and $x$. Let $x_{3}$ be an ordinal. Then the index of $p$ and $x_{3}$ is an element of $x_{2}$.
Besicovitch.TauPackage.lastStepdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantWording
the last step of p (from the name)
English
Let $p$ be an element of $\operatorname{TauPackage}$ applied to $x_{2}$ and $x$. Then the last step of $p$ is an ordinal defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $i$ to the proposition that it is not the case that there exists an element $b$ of $x_{2}$, such that it is not the case that $\MembershipmemMACRoT {\operatorname{iUnionUpTo} (p , i)}{\operatorname{c} (\operatorname{toBallPackage} (p), b)}$ and $\operatorname{R} (p , i)\leq \mathrm{Besicovitch\_\_TauPackage\_\_\_u3c4\_} (p)\times \operatorname{r} (\operatorname{toBallPackage} (p), b)$.
Besicovitch.TauPackage.τdefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{TauPackage}$ applied to $x$ and $x_{1}$. Then $\mathrm{Besicovitch\_\_TauPackage\_\_\_u3c4\_}$ applied to $\mathrm{self}$ is a real number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Besicovitch.unitBallPackagedefMathlib.MeasureTheory.Covering.Besicovitch, function or constantEnglish
Let $x$ be a set. Then $\operatorname{unitBallPackage}$ applied to $x$ is an element of $\operatorname{BallPackage}$ applied to $x$ and $x$.
Besicovitch.vitaliFamilydefMathlib.MeasureTheory.Covering.Besicovitch, function or constantWording
the Vitali family of x3 (from the name)
English
Let $x_{3}$ be a measure of $x$. Then the Vitali family of $x_{3}$ is a Vitali family of $x_{3}$.
HasBesicovitchCoveringclassMathlib.MeasureTheory.Covering.Besicovitch, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{HasBesicovitchCovering}$ holds for $x$.
Besicovitch.SatelliteConfig.centerAndRescaledefMathlib.MeasureTheory.Covering.BesicovitchVectorSpace, function or constantEnglish
Let $a$ be a satellite configuration of $N$ and $x_{2}$. Then $\operatorname{centerAndRescale}$ applied to $a$ is a satellite configuration of $N$ and $x_{2}$.
Besicovitch.goodδdefMathlib.MeasureTheory.Covering.BesicovitchVectorSpace, function or constantEnglish
Let $E$ be a set. Then $\mathrm{Besicovitch\_\_good\_u3b4\_}$ applied to $E$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{Besicovitch\_\_exists\_good\_u3b4\_}$ applied to $E$.
Besicovitch.goodτdefMathlib.MeasureTheory.Covering.BesicovitchVectorSpace, function or constantEnglish
Let $E$ be a set. Then $\mathrm{Besicovitch\_\_good\_u3c4\_}$ applied to $E$ is a real number defined as $1 + \frac{ \mathrm{Besicovitch\_\_good\_u3b4\_} (E)}{4}$.
Besicovitch.multiplicitydefMathlib.MeasureTheory.Covering.BesicovitchVectorSpace, function or constantWording
the multiplicity of E (from the name)
English
Let $E$ be a set. Then the multiplicity of $E$ is a natural number defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $N$ to the proposition that there exists a finite set $s$ of $E$, such that $\FinsetcardMACRoM {s}= N$, for all elements $c$ of $E$, if $c$ is an element of $s$, then the norm of $c$ is less than or equal to $2$ and for all elements $c_{1}$ of $E$, if $c_{1}$ is an element of $s$, then for all elements $d$ of $E$, if $d$ is an element of $s$, then if $c_{1} \neq d$, then $1$ is less than or equal to the norm of $c_{1} - d$.
IsUnifLocDoublingMeasure.vitaliFamilydefMathlib.MeasureTheory.Covering.DensityTheorem, function or constantWording
the Vitali family of x3 and K (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $K$ be a real number. Then the Vitali family of $x_{3}$ and $K$ is a Vitali family of $x_{3}$ defined as $\operatorname{proj0}$ applied to $\mathrm{IsUnifLocDoublingMeasure\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Covering\_\_DensityTheorem\_\_1554790178\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{3}$ and $K$.
VitaliFamily.limRatiodefMathlib.MeasureTheory.Covering.Differentiation, function or constantWording
the limit ratio of x3 and x4 (from the name)
English
Let $v$ be a Vitali family of $x_{2}$. Let $x_{3}$ be a measure of $x$. Let $x_{4}$ be an element of $x$. Then the limit ratio of $x_{3}$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{limUnder}$ applied to $\operatorname{filterAt}$ applied to $v$ and $x_{4}$ and the function that maps $a$ to $\frac{ x_{3} (a)}{x_{2} (a)}$.
VitaliFamily.limRatioMeasdefMathlib.MeasureTheory.Covering.Differentiation, function or constantEnglish
Let $v$ be a Vitali family of $x_{2}$. Assume that $\operatorname{AbsolutelyContinuous}$ holds for $x_{3}$ and $x_{2}$. Let $x_{4}$ be an element of $x$. Then $\operatorname{limRatioMeas}$ applied to $v$, $h_{4}$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{limRatio}$ applied to $x_{3}$, $\mathrm{VitaliFamily\_\_aemeasurable\_limRatio}$ applied to $v$ and $h_{4}$ and $x_{4}$.
Vitali.vitaliFamilydefMathlib.MeasureTheory.Covering.Vitali, function or constantWording
the Vitali family of x3 and C (from the name)
English
Let $x_{3}$ be a measure of $x$. Let $C$ be an element of $\mathrm{NNReal}$ such that for all elements $x_{4}$ of $x$, $\operatorname{Frequently}$ holds for the function that maps $r$ to the proposition that $x_{3}$ applied to the closed ball of $x_{4}$ and $3 \times r$ is less than or equal to the product of $\operatorname{ofNNReal}$ applied to $C$ and $x_{3}$ applied to the closed ball of $x_{4}$ and $r$ and $\mathrm{nhdsWithin}$ applied to $0$ and $\operatorname{Ioi}$ applied to $0$. Then the Vitali family of $x_{3}$ and $C$ is a Vitali family of $x_{3}$.
VitaliFamilystructureMathlib.MeasureTheory.Covering.VitaliFamily, typeWording
Vitali family of x1 (from the name)
English
Let $x_{1}$ be a measure of $X$. Then the Vitali families of $x_{1}$ are a basic type.
VitaliFamily.FineSubfamilyOndefMathlib.MeasureTheory.Covering.VitaliFamily, predicateEnglish
Let $v$ be a Vitali family of $x_{1}$. Let $f$ be a function from elements of $X$ to elements of $\wp (\wp X)$. Let $s$ be an element of $\wp X$. Then $\operatorname{FineSubfamilyOn}$ holds for $v$, $f$ and $s$, if for all elements $x_{2}$ of $X$, if $x_{2}$ is an element of $s$, then for all real numbers $x_{3}$, if $x_{3} > 0$, then there exists an element $t$ of $\wp X$, such that $\MembershipmemMACRoT {\operatorname{inter} (\operatorname{setsAt} (v , x_{2}), f (x_{2}))}{t}$ and $t$ is less than or equal to the closed ball of $x_{2}$ and $x_{3}$.
VitaliFamily.FineSubfamilyOn.coveringdefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantWording
the covering of _h and x2 (from the name)
English
Assume that $\operatorname{FineSubfamilyOn}$ holds for $v$, $f$ and $s$. Let $x_{2}$ be an element of $\mathrm{Prod}$ applied to $X$ and $\wp X$. Then the covering of $\mathrm{\_h}$ and $x_{2}$ is an element of $\wp X$ defined as $\ProdsndMACRoAA {x_{2}}$.
VitaliFamily.FineSubfamilyOn.indexdefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantWording
the index of h (from the name)
English
Assume that $\operatorname{FineSubfamilyOn}$ holds for $v$, $f$ and $s$. Then the index of $h$ is an element of $\wp \mathrm{Prod} (X , \wp X)$ defined as $\operatorname{choose}$ applied to $\mathrm{VitaliFamily\_\_FineSubfamilyOn\_\_exists\_disjoint\_covering\_ae}$ applied to $h$.
VitaliFamily.enlargedefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantEnglish
Let $v$ be a Vitali family of $x_{1}$. Let $x_{2}$ be a real number such that $0 < x_{2}$. Then $\operatorname{enlarge}$ applied to $v$, $x_{2}$ and $h$ is a Vitali family of $x_{1}$.
VitaliFamily.filterAtdefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantEnglish
Let $v$ be a Vitali family of $x_{1}$. Let $x_{2}$ be an element of $X$. Then $\operatorname{filterAt}$ applied to $v$ and $x_{2}$ is a filter of $\wp X$ defined as the minimum of the small set of the neighbourhood filter of $x_{2}$ and the principal filter of $\operatorname{setsAt}$ applied to $v$ and $x_{2}$.
VitaliFamily.monodefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantEnglish
Let $v$ be a Vitali family of $x_{1}$. Let $x_{2}$ be a measure of $X$ such that $\operatorname{AbsolutelyContinuous}$ holds for $x_{2}$ and $x_{1}$. Then $\operatorname{mono}$ applied to $v$, $x_{2}$ and $h$ is a Vitali family of $x_{2}$.
VitaliFamily.setsAtdefMathlib.MeasureTheory.Covering.VitaliFamily, function or constantEnglish
Let $\mathrm{self}$ be a Vitali family of $x_{1}$. Let $x_{2}$ be an element of $X$. Then $\operatorname{setsAt}$ applied to $\mathrm{self}$ and $x_{2}$ is an element of $\wp (\wp X)$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{2}$.
ContinuousMap.toAEEqFundefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $x_{3}$ be a measure of $x$. Let $f$ be a continuous map of $x$ and $x_{1}$. Then $\operatorname{toAEEqFun}$ applied to $x_{3}$ and $f$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$.
ContinuousMap.toAEEqFunAddHomdefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $x_{3}$ be a measure of $x$. Then $\operatorname{toAEEqFunAddHom}$ applied to $x_{3}$ is an additive monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$.
ContinuousMap.toAEEqFunLinearMapdefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $x_{3}$ be a measure of $x$. Then $\operatorname{toAEEqFunLinearMap}$ applied to $x_{3}$ is a linear map of the set of continuous maps of $x$ and $x_{1}$ and $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$.
ContinuousMap.toAEEqFunMulHomdefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $x_{3}$ be a measure of $x$. Then $\operatorname{toAEEqFunMulHom}$ applied to $x_{3}$ is a monoid homomorphism of the set of continuous maps of $x$ and $x_{1}$ and $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$.
MeasureTheory.AEEqFundefMathlib.MeasureTheory.Function.AEEqFun, typeEnglish
Let $x$ and $x_{1}$ be sets. Let $x_{4}$ be a measure of $x$. Then an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{4}$ is an element of the function that maps $x$, $x_{1}$ and $x_{4}$ to $\mathrm{Quotient}$ applied to $\operatorname{aeEqSetoid}$ applied to $x_{1}$ and $x_{4}$.
MeasureTheory.AEEqFun.LiftPreddefMathlib.MeasureTheory.Function.AEEqFun, predicateEnglish
Let $p$ be a function from elements of $x_{1}$ to propositions. Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$. Then $\operatorname{LiftPred}$ holds for $p$ and $f$, if $\operatorname{LiftPred}$ holds for $p$ and the germ of $f$.
MeasureTheory.AEEqFun.LiftReldefMathlib.MeasureTheory.Function.AEEqFun, predicateEnglish
Let $r$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to propositions. Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{4}$. Let $g$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$. Then $\operatorname{LiftRel}$ holds for $r$, $f$ and $g$, if $\operatorname{LiftRel}$ holds for $r$, the germ of $f$ and the germ of $g$.
MeasureTheory.AEEqFun.castdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the cast of f and x5 (from the name)
English
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$. Let $x_{5}$ be an element of $x$. Then the cast of $f$ and $x_{5}$ is an element of $x_{1}$.
MeasureTheory.AEEqFun.compdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a continuous function from elements of $x_{1}$ to elements of $x_{2}$. Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{4}$. Then the composition of $g$ and $f$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$.
MeasureTheory.AEEqFun.compMeasurabledefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $g$ be a measurable function from elements of $x_{1}$ to elements of $x_{2}$. Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{4}$. Then $\operatorname{compMeasurable}$ applied to $g$, $\mathrm{hg}$ and $f$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$.
MeasureTheory.AEEqFun.compMeasurePreservingdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the composition measure preserving of g and f (from the name)
English
Let $g$ be an element of $\operatorname{AEEqFun}$ applied to $x_{1}$, $x_{2}$ and $x_{7}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{MeasurePreserving}$ holds for $f$, $x_{4}$ and $x_{7}$. Then the composition measure preserving of $g$ and $f$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$ defined as $\operatorname{compQuasiMeasurePreserving}$ applied to $g$, $f$ and $\operatorname{quasiMeasurePreserving}$ applied to $\mathrm{hf}$.
MeasureTheory.AEEqFun.compQuasiMeasurePreservingdefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $g$ be an element of $\operatorname{AEEqFun}$ applied to $x_{1}$, $x_{2}$ and $x_{7}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{QuasiMeasurePreserving}$ holds for $f$, $x_{4}$ and $x_{7}$. Then $\operatorname{compQuasiMeasurePreserving}$ applied to $g$, $f$ and $\mathrm{hf}$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$.
MeasureTheory.AEEqFun.comp₂defMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the composition of x9 and x10 (from the name)
English
Let $g$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to elements of $x_{3}$ such that $\operatorname{uncurry}$ applied to $g$ is continuous. Let $x_{9}$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{5}$. Let $x_{10}$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{5}$. Then the composition of $x_{9}$ and $x_{10}$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{3}$ and $x_{5}$ defined as the composition of $\operatorname{uncurry}$ applied to $g$ and the pair of $x_{9}$ and $x_{10}$.
MeasureTheory.AEEqFun.comp₂MeasurabledefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $g$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to elements of $x_{3}$ such that $\operatorname{uncurry}$ applied to $g$ is measurable. Let $x_{12}$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{5}$. Let $x_{13}$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{5}$. Then $\mathrm{MeasureTheory\_\_AEEqFun\_\_comp\_u2082\_Measurable}$ applied to $g$, $\mathrm{hg}$, $x_{12}$ and $x_{13}$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{3}$ and $x_{5}$ defined as $\operatorname{compMeasurable}$ applied to $\operatorname{uncurry}$ applied to $g$, $\mathrm{hg}$ and the pair of $x_{12}$ and $x_{13}$.
MeasureTheory.AEEqFun.constdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the constant of x and b (from the name)
English
Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant of $x$ and $b$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$ defined as $\operatorname{mk}$ applied to the function that maps $x_{5}$ to $b$ and $\mathrm{MeasureTheory\_\_aestronglyMeasurable\_const}$.
MeasureTheory.AEEqFun.lintegraldefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $\mathrm{ENNReal}$ and $x_{2}$. Then $\operatorname{lintegral}$ applied to $f$ is an element of $\mathrm{ENNReal}$.
MeasureTheory.AEEqFun.mkdefMathlib.MeasureTheory.Function.AEEqFun, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{3}$ such that $\operatorname{AEStronglyMeasurable}$ holds for $f$ and $x_{2}$. Then $\operatorname{mk}$ applied to $f$ and $\mathrm{hf}$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{3}$ and $x_{2}$ defined as $\operatorname{mk''}$ applied to $f$.
MeasureTheory.AEEqFun.pairdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the pair of f and g (from the name)
English
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{4}$. Let $g$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{2}$ and $x_{4}$. Then the pair of $f$ and $g$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $x_{4}$.
MeasureTheory.AEEqFun.posPartdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the positive part part of f (from the name)
English
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$. Then the positive part part of $f$ is an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$.
MeasureTheory.AEEqFun.toGermdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the germ of f (from the name)
English
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$. Then the germ of $f$ is a germ of $\operatorname{ae}$ applied to $x_{3}$ and $x_{1}$.
MeasureTheory.AEEqFun.toGermAddMonoidHomdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the germ additive monoid homomorphism (from the name)
English
The germ additive monoid homomorphism is an additive monoid homomorphism of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$ and the set of germs of $\operatorname{ae}$ applied to $x_{3}$ and $x_{1}$.
MeasureTheory.AEEqFun.toGermMonoidHomdefMathlib.MeasureTheory.Function.AEEqFun, function or constantWording
the germ monoid homomorphism (from the name)
English
The germ monoid homomorphism is a monoid homomorphism of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{3}$ and the set of germs of $\operatorname{ae}$ applied to $x_{3}$ and $x_{1}$.
aeSeqdefMathlib.MeasureTheory.Function.AEMeasurableSequence, function or constantEnglish
Assume that for all elements $i$ of $x$, $f$ applied to $i$ is almost everywhere measurable. Let $p$ be a function from elements of $x_{1}$ and functions from elements of $x$ to elements of $x_{2}$ to propositions. Let $x_{6}$ be an element of $x$. Let $x_{7}$ be an element of $x_{1}$. Then $\mathrm{aeSeq}$ applied to $\mathrm{hf}$, $p$, $x_{6}$ and $x_{7}$ is an element of $x_{2}$.
aeSeqSetdefMathlib.MeasureTheory.Function.AEMeasurableSequence, function or constantEnglish
Assume that for all elements $i$ of $x$, $f$ applied to $i$ is almost everywhere measurable. Let $p$ be a function from elements of $x_{1}$ and functions from elements of $x$ to elements of $x_{2}$ to propositions. Then $\mathrm{aeSeqSet}$ applied to $\mathrm{hf}$ and $p$ is an element of $\wp x_{1}$ defined as the complement of $\operatorname{toMeasurable}$ applied to $x_{5}$ and the complement of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that for all elements $i$ of $x$, $\EqtMACRoH {f (i , x_{6})}{\operatorname{mk} (f (i), \mathrm{hf} (i), x_{6})}$ and $p$ holds for $x_{6}$ and the function that maps $n$ to $f$ applied to $n$ and $x_{6}$.
AbsolutelyContinuousOnIntervaldefMathlib.MeasureTheory.Function.AbsolutelyContinuous, predicateEnglish
Let $f$ be a function from elements of $\Real$ to elements of $X$. Let $a$ and $b$ be elements of $\Real$. Then $\mathrm{AbsolutelyContinuousOnInterval}$ holds for $f$, $a$ and $b$, if $\operatorname{Tendsto}$ holds for the function that maps $E$ to $\FinsetSum {\FinsetrangeMACRoN {\ProdfstMACRoZ {E}}}{i}{\operatorname{dist} (f (\ProdfstMACRoZ {\ProdsndMACRoAA {E}}), f (\ProdsndMACRoAA {\ProdsndMACRoAA {E}}))}$, $\MinminMACRoAG {\operatorname{totalLengthFilter}}{\operatorname{principal} (\operatorname{disjWithin} (a , b))}$ and the neighbourhood filter of $0$.
AbsolutelyContinuousOnInterval.disjWithindefMathlib.MeasureTheory.Function.AbsolutelyContinuous, function or constantEnglish
Let $a$ and $b$ be elements of $\Real$. Then $\operatorname{disjWithin}$ applied to $a$ and $b$ is an element of $\wp \mathrm{Prod} (\Natural , \mathrm{Elem} (\Natural)\rightarrow \mathrm{Prod} (\Real , \Real))$ defined as $\operatorname{ofPred}$ applied to the function that maps $E$ to the proposition that for all elements $i$ of $\Natural$, if $\MembershipmemMACRoT {\FinsetrangeMACRoN {\ProdfstMACRoZ {E}}}{i}$, then $\ProdfstMACRoZ {\ProdsndMACRoAA {E}}$ is an element of the closed interval of $a$ and $b$ and $\ProdsndMACRoAA {\ProdsndMACRoAA {E}}$ is an element of the closed interval of $a$ and $b$ and $\FinsetrangeMACRoN {\ProdfstMACRoZ {E}}$ is a pairwise disjoint with respect to the function that maps $i_{1}$ to $\operatorname{uIoc}$ applied to $\ProdfstMACRoZ {\ProdsndMACRoAA {E}}$ and $\ProdsndMACRoAA {\ProdsndMACRoAA {E}}$.
AbsolutelyContinuousOnInterval.totalLengthFilterdefMathlib.MeasureTheory.Function.AbsolutelyContinuous, function or constantWording
the total length filter (from the name)
English
The total length filter is a filter of $\mathrm{Prod}$ applied to $\Natural$ and the set of functions from elements of $\Natural$ to elements of $\mathrm{Prod}$ applied to $X$ and $X$ defined as the preimage of the function that maps $E$ to $\FinsetSum {\FinsetrangeMACRoN {\ProdfstMACRoZ {E}}}{i}{\operatorname{dist} (\ProdfstMACRoZ {\ProdsndMACRoAA {E}}, \ProdsndMACRoAA {\ProdsndMACRoAA {E}})}$ and the neighbourhood filter of $0$.
MeasureTheory.lpMeasdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ and $x_{1}$ be sets. Assume that $x$ is a measurable space. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{6}$ be a measure of $x$. Then $\operatorname{lpMeas}$ applied to $F$, $x_{1}$, $m$, $p$ and $x_{6}$ is a submodule of $x_{1}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{6})}{x_{7}})}$.
MeasureTheory.lpMeasSubgroupdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ be a set. Assume that $x$ is a measurable space. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{3}$ be a measure of $x$. Then $\operatorname{lpMeasSubgroup}$ applied to $F$, $m$, $p$ and $x_{3}$ is an additive subgroup of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{3})}{x_{4}})}$.
MeasureTheory.lpMeasSubgroupToLpMeasIsodefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ and $x_{1}$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Then $\operatorname{lpMeasSubgroupToLpMeasIso}$ applied to $F$, $x_{1}$, $p$ and $x_{5}$ is an isometry equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{lpMeasSubgroup} (F , m , p , x_{5})}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{lpMeas} (F , x_{1} , m , p , x_{5})}{x_{7}})}$ defined as the identity isometry of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{lpMeasSubgroup} (F , m , p , x_{5})}{x_{6}})}$.
MeasureTheory.lpMeasSubgroupToLpTrimdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Assume that $m \leq m_{0}$. Let $f$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{lpMeasSubgroup} (F , m , p , x_{2})}{x_{4}})}$. Then $\operatorname{lpMeasSubgroupToLpTrim}$ applied to $F$, $p$, $x_{2}$, $\mathrm{hm}$ and $f$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{2} , \mathrm{hm}))}{x_{3}})}$.
MeasureTheory.lpMeasSubgroupToLpTrimIsodefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Assume that $m \leq m_{0}$. Then $\operatorname{lpMeasSubgroupToLpTrimIso}$ applied to $F$, $p$, $x_{2}$ and $\mathrm{hm}$ is an isometry equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{lpMeasSubgroup} (F , m , p , x_{2})}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{2} , \mathrm{hm}))}{x_{4}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{lpMeasSubgroupToLpTrim}$ applied to $F$, $p$, $x_{2}$ and $\mathrm{hm}$, $\operatorname{lpTrimToLpMeasSubgroup}$ applied to $F$, $p$, $x_{2}$ and $\mathrm{hm}$, $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_left\_inv}$ applied to $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_right\_inv}$ applied to $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_isometry\_lpMeasSubgroupToLpTrim}$ applied to $\mathrm{hm}$.
MeasureTheory.lpMeasToLpTrimdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ and $x_{1}$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Assume that $m \leq m_{0}$. Let $f$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{lpMeas} (F , x_{1} , m , p , x_{5})}{x_{7}})}$. Then $\operatorname{lpMeasToLpTrim}$ applied to $F$, $x_{1}$, $p$, $x_{5}$, $\mathrm{hm}$ and $f$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{5} , \mathrm{hm}))}{x_{6}})}$.
MeasureTheory.lpMeasToLpTrimLiedefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ and $x_{1}$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Assume that $m \leq m_{0}$. Then $\operatorname{lpMeasToLpTrimLie}$ applied to $F$, $x_{1}$, $p$, $x_{5}$ and $\mathrm{hm}$ is a linear isometry equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{lpMeas} (F , x_{1} , m , p , x_{5})}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{5} , \mathrm{hm}))}{x_{7}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{lpMeasToLpTrim}$ applied to $F$, $x_{1}$, $p$, $x_{5}$ and $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_add}$ applied to $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_lpMeasToLpTrim\_smul}$ applied to $\mathrm{hm}$, $\operatorname{lpTrimToLpMeas}$ applied to $F$, $x_{1}$, $p$, $x_{5}$ and $\mathrm{hm}$, $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_left\_inv}$ applied to $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_right\_inv}$ applied to $\mathrm{hm}$ and $\mathrm{MeasureTheory\_\_lpMeasSubgroupToLpTrim\_norm\_map}$ applied to $\mathrm{hm}$.
MeasureTheory.lpTrimToLpMeasdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ and $x_{1}$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Assume that $m \leq m_{0}$. Let $f$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{5} , \mathrm{hm}))}{x_{7}})}$. Then $\operatorname{lpTrimToLpMeas}$ applied to $F$, $x_{1}$, $p$, $x_{5}$, $\mathrm{hm}$ and $f$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{lpMeas} (F , x_{1} , m , p , x_{5})}{x_{6}})}$.
MeasureTheory.lpTrimToLpMeasSubgroupdefMathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable, function or constantEnglish
Let $F$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Assume that $m \leq m_{0}$. Let $f$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{trim} (x_{2} , \mathrm{hm}))}{x_{4}})}$. Then $\operatorname{lpTrimToLpMeasSubgroup}$ applied to $F$, $p$, $x_{2}$, $\mathrm{hm}$ and $f$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{lpMeasSubgroup} (F , m , p , x_{2})}{x_{3}})}$.
MeasureTheory.condExpdefMathlib.MeasureTheory.Function.ConditionalExpectation.Basic, function or constantWording
the conditional exponential of f and x5 (from the name)
English
Assume that $x$ is a measurable space. Let $x_{4}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Let $x_{5}$ be an element of $x$. Then the conditional exponential of $f$ and $x_{5}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Function\_\_ConditionalExpectation\_\_Basic\_\_3200634613\_\_\_hygCtx\_\_\_hyg\_\_44}$, $m$, $x_{4}$, $f$ and $x_{5}$.
MeasureTheory.condExpInddefMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1, function or constantWording
the conditional exponential ind of x3 and s (from the name)
English
Let $G$ be a set. Assume that $m \leq m_{0}$. Let $x_{3}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then the conditional exponential ind of $x_{3}$ and $s$ is a continuous linear map of $G$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , 1 , x_{3})}{x_{4}})}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{condExpIndL1}$ applied to $s$ and $\mathrm{MeasureTheory\_\_condExpIndL1\_add}$ and $\mathrm{MeasureTheory\_\_condExpIndL1\_smul}$ and $\mathrm{MeasureTheory\_\_continuous\_condExpIndL1}$.
MeasureTheory.condExpIndL1defMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1, function or constantWording
the conditional exponential ind of s and x4 (from the name)
English
Assume that $m \leq m_{0}$. Let $x_{3}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $G$. Then the conditional exponential ind of $s$ and $x_{4}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , 1 , x_{3})}{x_{5}})}$.
MeasureTheory.condExpIndL1FindefMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1, function or constantEnglish
Assume that $m \leq m_{0}$. Assume that $s$ is a measurable set. Assume that $x_{2}$ applied to $s$ is distinct from the top. Let $x_{4}$ be an element of $G$. Then $\operatorname{condExpIndL1Fin}$ applied to $\mathrm{hm}$, $\mathrm{hs}$, $h_{1}$ and $x_{4}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , 1 , x_{2})}{x_{5}})}$ defined as $\operatorname{toL1}$ applied to $\operatorname{cast}$ applied to the conditional exponential ind product of $x_{4}$ and $\mathrm{MeasureTheory\_\_integrable\_condExpIndSMul}$ applied to $\mathrm{hm}$, $\mathrm{hs}$, $h_{1}$ and $x_{4}$.
MeasureTheory.condExpL1defMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1, function or constantWording
the conditional exponential of x3 and f (from the name)
English
Assume that $m \leq m_{0}$. Let $x_{3}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{F'}$. Then the conditional exponential of $x_{3}$ and $f$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{F'} , 1 , x_{3})}{x_{4}})}$ defined as the set to function of $\operatorname{condExpInd}$ applied to $x_{3}$ and $f$.
MeasureTheory.condExpL1CLMdefMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1, function or constantWording
the conditional exponential continuous linear map of #3 (from the name)
English
Let $\mathrm{F'}$ be a set. Assume that $m \leq m_{0}$. Let $x_{3}$ be a measure of $x$. Then the conditional exponential continuous linear map of $x_{3}$ is a continuous linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{F'} , 1 , x_{3})}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (\mathrm{F'} , 1 , x_{3})}{x_{5}})}$ defined as $\operatorname{setToL1}$ applied to $\mathrm{MeasureTheory\_\_dominatedFinMeasAdditive\_condExpInd}$ applied to $\mathrm{F'}$, $\mathrm{hm}$ and $x_{3}$.
MeasureTheory.condExpIndSMuldefMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2, function or constantWording
the conditional exponential ind product of x4 (from the name)
English
Assume that $m \leq m_{0}$. Assume that $s$ is a measurable set. Assume that $x_{2}$ applied to $s$ is distinct from the top. Let $x_{4}$ be an element of $G$. Then the conditional exponential ind product of $x_{4}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , 2 , x_{2})}{x_{5}})}$ defined as $\operatorname{compLpL}$ applied to $2$, $x_{2}$, the span singleton of $\Real$ and $x_{4}$ and $\operatorname{condExpL2}$ applied to $\Real$, $\Real$, $\mathrm{hm}$ and $\operatorname{indicatorConstLp}$ applied to $2$, $\mathrm{hs}$, $h$ and $1$.
MeasureTheory.condExpL2defMathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2, function or constantWording
the conditional exponential of x1 and hm (from the name)
English
Let $E$ and $x_{1}$ be sets. Assume that $m \leq m_{0}$. Then the conditional exponential of $x_{1}$ and $\mathrm{hm}$ is a continuous linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 2 , x_{5})}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{lpMeas} (E , x_{1} , m , 2 , x_{5})}{x_{7}})}$ defined as the orthogonal projection onto a subspace of $\operatorname{lpMeas}$ applied to $E$, $x_{1}$, $m$, $2$ and $x_{5}$.
MeasureTheory.condLExpdefMathlib.MeasureTheory.Function.ConditionalLExpectation, function or constantWording
the conditional exponential of X and x3 (from the name)
English
Assume that $x$ is a measurable space. Let $P$ be a measure of $x$. Let $X$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Let $x_{3}$ be an element of $x$. Then the conditional exponential of $X$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Function\_\_ConditionalLExpectation\_\_1764629072\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{2}$, $P$, $X$ and $x_{3}$.
MeasureTheory.TendstoInDistributionstructureMathlib.MeasureTheory.Function.ConvergenceInDistribution, predicateEnglish
Let $X$ be a function from elements $i_{1}$ of $x$ and elements of $x_{2}$ applied to $i_{1}$ to elements of $E$. Let $l$ be a filter of $x$. Let $Z$ be a function from elements of $x_{1}$ to elements of $E$. Let $x_{4}$ be a function from elements $i$ of $x$ to measures of $x_{2}$ applied to $i$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{1}$ and $\mathrm{MeasureTheory\_\_TendstoInDistribution\_\_\_auto\_1}$. Then we can say that $\operatorname{TendstoInDistribution}$ holds for $i_{1}$, $X$, $l$, $Z$, $i$, $x_{4}$ and $x_{5}$.
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeqdefMathlib.MeasureTheory.Function.ConvergenceInMeasure, function or constantEnglish
Assume that $g$ is a limit in measure with respect to $\operatorname{atTop}$. Let $x_{3}$ be a natural number. Then $\operatorname{seqTendstoAeSeq}$ applied to $\mathrm{hfg}$ and $x_{3}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{MeasureTheory\_\_ExistsSeqTendstoAe\_\_seqTendstoAeSeq\_\_\_f}$ applied to $\mathrm{hfg}$.
MeasureTheory.TendstoInMeasuredefMathlib.MeasureTheory.Function.ConvergenceInMeasure, predicateWording
g is a limit in measure with respect to l (from the name)
English
Let $x_{4}$ be a measure of $x$. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $E$. Let $l$ be a filter of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $E$. Then $g$ is a limit in measure with respect to $l$, if for all elements $x_{5}$ of $\mathrm{ENNReal}$, if $0 < x_{5}$, then $\operatorname{Tendsto}$ holds for the function that maps $i$ to $x_{4}$ applied to $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $x_{5}$ is less than or equal to the extended distance of $f$ applied to $i$ and $x_{6}$ and $g$ applied to $x_{6}$, $l$ and the neighbourhood filter of $0$.
MeasureTheory.Egorov.iUnionNotConvergentSeqdefMathlib.MeasureTheory.Function.Egorov, function or constantWording
the union not convergent sequence of hs and hfg (from the name)
English
Assume that $0 < x_{5}$. Assume that for all elements $n_{1}$ of $x_{2}$, the function that maps $a$ to the extended distance of $f$ applied to $n_{1}$ and $a$ and $g$ applied to $a$ is almost everywhere measurable. Assume that $\operatorname{NullMeasurableSet}$ holds for $s$ and $x_{4}$. Assume that $x_{4}$ applied to $s$ is distinct from the top. Assume that $\operatorname{Eventually}$ holds for the function that maps $x_{7}$ to the proposition that if $x_{7}$ is an element of $s$, then $\operatorname{Tendsto}$ holds for the function that maps $n$ to $f$ applied to $n$ and $x_{7}$, $\operatorname{atTop}$ and the neighbourhood filter of $g$ applied to $x_{7}$ and $\operatorname{ae}$ applied to $x_{4}$. Then the union not convergent sequence of $\mathrm{hs}$ and $\mathrm{hfg}$ is an element of $\wp x$.
MeasureTheory.Egorov.notConvergentSeqdefMathlib.MeasureTheory.Function.Egorov, function or constantWording
the not convergent sequence of n and j (from the name)
English
Let $f$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $g$ be a function from elements of $x$ to elements of $x_{1}$. Let $n$ be a natural number. Let $j$ be an element of $x_{2}$. Then the not convergent sequence of $n$ and $j$ is an element of $\wp x$ defined as the union of the function that maps $k$ to the union of the function that maps $h$ to $\operatorname{ofPred}$ applied to the function that maps $x_{5}$ to the proposition that $\operatorname{inv}$ applied to $n$ is less than the extended distance of $f$ applied to $k$ and $x_{5}$ and $g$ applied to $x_{5}$.
MeasureTheory.Egorov.notConvergentSeqLTIndexdefMathlib.MeasureTheory.Function.Egorov, function or constantEnglish
Assume that $0 < x_{5}$. Assume that for all elements $n_{2}$ of $x_{2}$, the function that maps $a$ to the extended distance of $f$ applied to $n_{2}$ and $a$ and $g$ applied to $a$ is almost everywhere measurable. Assume that $\operatorname{NullMeasurableSet}$ holds for $s$ and $x_{4}$. Assume that $x_{4}$ applied to $s$ is distinct from the top. Assume that $\operatorname{Eventually}$ holds for the function that maps $x_{7}$ to the proposition that if $x_{7}$ is an element of $s$, then $\operatorname{Tendsto}$ holds for the function that maps $n_{1}$ to $f$ applied to $n_{1}$ and $x_{7}$, $\operatorname{atTop}$ and the neighbourhood filter of $g$ applied to $x_{7}$ and $\operatorname{ae}$ applied to $x_{4}$. Let $n$ be a natural number. Then $\operatorname{notConvergentSeqLTIndex}$ applied to $h_{2}$, $\mathrm{hf}$, $\mathrm{hsm}$, $\mathrm{hs}$, $\mathrm{hfg}$ and $n$ is an element of $x_{2}$ defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_Egorov\_\_exists\_notConvergentSeq\_lt}$ applied to $h_{2}$, $\mathrm{hf}$, $\mathrm{hsm}$, $\mathrm{hs}$, $\mathrm{hfg}$ and $n$.
essInfdefMathlib.MeasureTheory.Function.EssSup, function or constantWording
the essential infimum 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 essential infimum of $f$ and $x_{4}$ is an element of $x_{1}$ defined as $\operatorname{liminf}$ applied to $f$ and $\operatorname{ae}$ applied to $x_{4}$.
essSupdefMathlib.MeasureTheory.Function.EssSup, function or constantWording
the essential supremum 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 essential supremum of $f$ and $x_{4}$ is an element of $x_{1}$ defined as the limsup of $f$ and $\operatorname{ae}$ applied to $x_{4}$.
ContinuousLinearMap.holderdefMathlib.MeasureTheory.Function.Holder, function or constantWording
the Holder of f and g (from the name)
English
Let $r$ be an element of $\mathrm{ENNReal}$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Let $f$ be an element of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{2})}{x_{12}})}$. Let $g$ be an element of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , q , x_{2})}{x_{11}})}$. Then the Holder of $f$ and $g$ is an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , r , x_{2})}{x_{10}})}$.
ContinuousLinearMap.holderLdefMathlib.MeasureTheory.Function.Holder, function or constantWording
the Holder of r and B (from the name)
English
Let $x_{2}$ be a measure of $x$. Let $p$, $q$ and $r$ be elements of $\mathrm{ENNReal}$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the Holder of $r$ and $B$ is a continuous linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{2})}{x_{10}})}$ and the set of continuous linear maps of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , q , x_{2})}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , r , x_{2})}{x_{12}})}$ defined as $\mathrm{LinearMap\_\_mkContinuous\_u2082\_}$ applied to the Holder of $r$ and $B$, the norm of $B$ and $\mathrm{ContinuousLinearMap\_\_norm\_holder\_apply\_apply\_le}$ applied to $B$.
ContinuousLinearMap.holderₗdefMathlib.MeasureTheory.Function.Holder, function or constantWording
the Holder of r and B (from the name)
English
Let $x_{2}$ be a measure of $x$. Let $p$, $q$ and $r$ be elements of $\mathrm{ENNReal}$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then the Holder of $r$ and $B$ is a linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{2})}{x_{10}})}$ and the set of linear maps of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , q , x_{2})}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , r , x_{2})}{x_{12}})}$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $x_{1}$, $\operatorname{holder}$, $\mathrm{ContinuousLinearMap\_\_holder\_add\_left}$ applied to $B$, $\mathrm{ContinuousLinearMap\_\_holder\_smul\_left}$ applied to $B$, $\mathrm{ContinuousLinearMap\_\_holder\_add\_right}$ applied to $B$ and $\mathrm{ContinuousLinearMap\_\_holder\_smul\_right}$ applied to $B$.
ContinuousLinearMap.lpPairingdefMathlib.MeasureTheory.Function.Holder, function or constantEnglish
Let $x_{2}$ be a measure of $x$. Let $p$ and $q$ be elements of $\mathrm{ENNReal}$. Let $B$ be a continuous linear map of $E$ and the set of continuous linear maps of $F$ and $G$. Then $\operatorname{lpPairing}$ applied to $x_{2}$, $p$, $q$ and $B$ is a continuous linear map of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{2})}{x_{11}})}$ and the set of continuous linear maps of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , q , x_{2})}{x_{12}})}$ and $G$ defined as the composition of the postcomposition of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , q , x_{2})}{x_{11}})}$ and the integral continuous linear map of $x_{1}$ and the Holder of $1$ and $B$.
MeasureTheory.AEEqFun.IntegrabledefMathlib.MeasureTheory.Function.L1Space.AEEqFun, predicateWording
f is integrable (from the name)
English
Let $f$ be an element of $\operatorname{AEEqFun}$ applied to $x$, $x_{1}$ and $x_{2}$. Then $f$ is integrable, if $\operatorname{Integrable}$ holds for $\operatorname{cast}$ applied to $f$ and $x_{2}$.
MeasureTheory.Integrable.toL1defMathlib.MeasureTheory.Function.L1Space.AEEqFun, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{Integrable}$ holds for $f$ and $x_{2}$. Then $\operatorname{toL1}$ applied to $f$ and $\mathrm{hf}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (x_{1} , 1 , x_{2})}{x_{4}})}$.
MeasureTheory.HasFiniteIntegraldefMathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_HasFiniteIntegral\_\_\_auto\_1}$. Then $\operatorname{HasFiniteIntegral}$ holds for $f$ and $x_{4}$, if $\operatorname{lintegral}$ applied to $x_{4}$ and the function that maps $a$ to the extended norm of $f$ applied to $a$ is less than the top.
MeasureTheory.IntegrabledefMathlib.MeasureTheory.Function.L1Space.Integrable, predicateEnglish
Let $f$ be a function from elements of $x_{3}$ to elements of $x$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x_{3}$ and $\mathrm{MeasureTheory\_\_Integrable\_\_\_auto\_1}$. Then $\operatorname{Integrable}$ holds for $f$ and $x_{5}$, if $\operatorname{AEStronglyMeasurable}$ holds for $f$ and $x_{5}$ and $\operatorname{HasFiniteIntegral}$ holds for $f$ and $x_{5}$.
MeasureTheory.withDensitySMulLIdefMathlib.MeasureTheory.Function.L1Space.Integrable, function or constantEnglish
Let $x_{1}$ be a measure of $x$. Assume that $f$ is measurable. Then $\operatorname{withDensitySMulLI}$ applied to $x_{1}$ and $\mathrm{f\_meas}$ is a linear isometry of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , \operatorname{withDensity} (x_{1} , \lambda x_{5} . \operatorname{ofNNReal} (f (x_{5}))))}{x_{4}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{1})}{x_{6}})}$.
MeasureTheory.LocallyIntegrabledefMathlib.MeasureTheory.Function.LocallyIntegrable, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $x$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $X$ and $\mathrm{MeasureTheory\_\_LocallyIntegrable\_\_\_auto\_1}$. Then $\operatorname{LocallyIntegrable}$ holds for $f$ and $x_{5}$, if for all elements $x_{6}$ of $X$, $\operatorname{IntegrableAtFilter}$ holds for $f$, the neighbourhood filter of $x_{6}$ and $x_{5}$.
MeasureTheory.LocallyIntegrableOndefMathlib.MeasureTheory.Function.LocallyIntegrable, predicateEnglish
Let $f$ be a function from elements of $X$ to elements of $x$. Let $s$ be an element of $\wp X$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $X$ and $\mathrm{MeasureTheory\_\_LocallyIntegrableOn\_\_\_auto\_1}$. Then $\operatorname{LocallyIntegrableOn}$ holds for $f$, $s$ and $x_{5}$, if for all elements $x_{6}$ of $X$, if $x_{6}$ is an element of $s$, then $\operatorname{IntegrableAtFilter}$ holds for $f$, $\mathrm{nhdsWithin}$ applied to $x_{6}$ and $s$ and $x_{5}$.
MeasureTheory.MemLpdefMathlib.MeasureTheory.Function.LpSeminorm.Defs, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_MemLp\_\_\_auto\_1}$. Then $\operatorname{MemLp}$ holds for $f$, $p$ and $x_{4}$, if $\operatorname{eLpNorm}$ applied to $f$, $p$ and $x_{4}$ is less than the top.
MeasureTheory.eLpNormdefMathlib.MeasureTheory.Function.LpSeminorm.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_eLpNorm\_\_\_auto\_1}$. Then $\operatorname{eLpNorm}$ applied to $f$, $p$ and $x_{5}$ is an element of $\mathrm{ENNReal}$ defined as $\iteMACRoG {\operatorname{AEStronglyMeasurable} (f , x_{5})}{(\iteMACRoG {(\EqtMACRoH {p}{0})}{0}{(\iteMACRoG {(\EqtMACRoH {p}{\operatorname{top}})}{\operatorname{eLpNormEssSup} (f , x_{5})}{\operatorname{eLpNorm'} (f , \operatorname{toReal} (p), x_{5})})})}{\operatorname{top}}$.
MeasureTheory.eLpNorm'defMathlib.MeasureTheory.Function.LpSeminorm.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $q$ be a real number. Let $x_{4}$ be a measure of $x$. Then $\operatorname{eLpNorm'}$ applied to $f$, $q$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as the exponentiation of $\operatorname{lintegral}$ applied to $x_{4}$ and the function that maps $a$ to the exponentiation of the extended norm of $f$ applied to $a$ to $q$ to $\frac{ 1}{q}$.
MeasureTheory.eLpNormEssSupdefMathlib.MeasureTheory.Function.LpSeminorm.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{3}$ be a measure of $x$. Then $\operatorname{eLpNormEssSup}$ applied to $f$ and $x_{3}$ is an element of $\mathrm{ENNReal}$ defined as the essential supremum of the function that maps $x_{4}$ to the extended norm of $f$ applied to $x_{4}$ and $x_{3}$.
MeasureTheory.inhmgELpNormdefMathlib.MeasureTheory.Function.LpSeminorm.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_inhmgELpNorm\_\_\_auto\_1}$. Then $\operatorname{inhmgELpNorm}$ applied to $f$, $p$ and $x_{5}$ is an element of $\mathrm{ENNReal}$ defined as $\iteMACRoG {\operatorname{AEStronglyMeasurable} (f , x_{5})}{(\iteMACRoG {(\EqtMACRoH {p}{0})}{x_{5} (\operatorname{support} (\lambda x_{6} . \operatorname{enorm} (f (x_{6}))))}{(\iteMACRoG {\mathrm{Lt} (p , 1)}{\operatorname{lintegral} (x_{5} , \lambda a . \operatorname{enorm} (f (a))^ {\operatorname{toReal} (p)})}{\operatorname{eLpNorm} (f , p , x_{5})})})}{\operatorname{top}}$.
MeasureTheory.lpNormdefMathlib.MeasureTheory.Function.LpSeminorm.Defs, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $E$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Then $\operatorname{lpNorm}$ applied to $f$, $p$ and $x_{2}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{eLpNorm}$ applied to $f$, $p$ and $x_{2}$.
ContinuousLinearMap.compLpdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $L$ be a continuous linear map of $E$ and $F$. Let $f$ be an element of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{12}})}$. Then $\operatorname{compLp}$ applied to $L$ and $f$ is an element of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{11}})}$.
ContinuousLinearMap.compLpLdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $L$ be a continuous linear map of $E$ and $F$. Then $\operatorname{compLpL}$ applied to $p$, $x_{1}$ and $L$ is a continuous linear map of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{12}})}$ defined as $\operatorname{mkContinuous}$ applied to $\mathrm{ContinuousLinearMap\_\_compLp\_u2097\_}$ applied to $p$, $x_{1}$ and $L$, the norm of $L$ and $\mathrm{ContinuousLinearMap\_\_norm\_compLp\_le}$ applied to $L$.
ContinuousLinearMap.compLpL₂defMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $B$ be a continuous linear map of $G$ and the set of continuous linear maps of $E$ and $F$. Then $\mathrm{ContinuousLinearMap\_\_compLpL\_u2082\_}$ applied to $p$, $x_{1}$ and $B$ is a continuous linear map of $G$ and the set of continuous linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{11}})}$.
ContinuousLinearMap.compLpₗdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $L$ be a continuous linear map of $E$ and $F$. Then $\mathrm{ContinuousLinearMap\_\_compLp\_u2097\_}$ applied to $p$, $x_{1}$ and $L$ is a linear map of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{12}})}$.
ContinuousLinearMap.compLpₗ₂defMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $B$ be a continuous linear map of $G$ and the set of continuous linear maps of $E$ and $F$. Then $\mathrm{ContinuousLinearMap\_\_compLp\_u2097\_\_u2082\_}$ applied to $p$, $x_{1}$ and $B$ is a linear map of $G$ and the set of linear maps of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{11}})}$.
LipschitzWith.compLpdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Assume that $\mathrm{LipschitzWith}$ holds for $c$ and $g$. Assume that $\EqtMACRoH {g (0)}{0}$. Let $f$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{5}})}$. Then $\operatorname{compLp}$ applied to $\mathrm{hg}$, $g_{0}$ and $f$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{1})}{x_{4}})}$.
MeasureTheory.LpdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $E$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_Lp\_\_\_auto\_1}$. Then $\operatorname{Lp}$ applied to $E$, $p$ and $x_{2}$ is an additive subgroup of $\operatorname{AEEqFun}$ applied to $x$, $E$ and $x_{2}$.
MeasureTheory.Lp.LpSubmoduledefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $x_{1}$ and $E$ be sets. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Then $\operatorname{LpSubmodule}$ applied to $x_{1}$, $E$, $p$ and $x_{2}$ is a submodule of $x_{1}$ and $\operatorname{AEEqFun}$ applied to $x$, $E$ and $x_{2}$.
MeasureTheory.Lp.LpToLpOfMeasureLeSMuldefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Assume that $c$ is distinct from the top. Assume that $x_{1} \leq \HSMulhSMulMACRoAL {c}{x_{4}}$. Then $\operatorname{LpToLpOfMeasureLeSMul}$ applied to $\mathrm{hc}$ and $h_{1}$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{4})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{6}})}$.
MeasureTheory.Lp.compMeasurePreservingdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantWording
the composition measure preserving of f and hf (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{3}$ such that $\operatorname{MeasurePreserving}$ holds for $f$, $x_{1}$ and $x_{5}$. Then the composition measure preserving of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{5})}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{7}})}$.
MeasureTheory.Lp.compMeasurePreservingₗdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantWording
the composition measure preserving of f (from the name)
English
Let $x_{6}$ be a set. Let $f$ be a function from elements of $x$ to elements of $x_{3}$ such that $\operatorname{MeasurePreserving}$ holds for $f$, $x_{1}$ and $x_{5}$. Then the composition measure preserving of $f$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{5})}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{10}})}$.
MeasureTheory.Lp.compMeasurePreservingₗᵢdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantWording
the composition measure preserving of f (from the name)
English
Let $x_{6}$ be a set. Let $f$ be a function from elements of $x$ to elements of $x_{3}$ such that $\operatorname{MeasurePreserving}$ holds for $f$, $x_{1}$ and $x_{5}$. Then the composition measure preserving of $f$ is a linear isometry of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{5})}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{10}})}$ defined as $\operatorname{mk}$ applied to the composition measure preserving of $f$ and the function that maps $x_{9}$ to $\mathrm{MeasureTheory\_\_Lp\_\_norm\_compMeasurePreserving}$ applied to $x_{9}$ and $\mathrm{hf}$.
MeasureTheory.Lp.negPartdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantWording
the negation part of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (\Real , p , x_{1})}{x_{3}})}$. Then the negation part of $f$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{Lp} (\Real , p , x_{1})}{x_{2}})}$ defined as the positive part part of $\operatorname{neg}$ applied to $f$.
MeasureTheory.Lp.posPartdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantWording
the positive part part of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (\Real , p , x_{1})}{x_{3}})}$. Then the positive part part of $f$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{Lp} (\Real , p , x_{1})}{x_{2}})}$.
MeasureTheory.MemLp.toLpdefMathlib.MeasureTheory.Function.LpSpace.Basic, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $E$ such that $\operatorname{MemLp}$ holds for $f$, $p$ and $x_{1}$. Then $\operatorname{toLp}$ applied to $f$ and $h$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{3}})}$.
BoundedContinuousFunction.toLpdefMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $x_{4}$ be a set. Then $\operatorname{toLp}$ applied to $p$, $x_{1}$ and $x_{4}$ is a continuous linear map of the set of bounded continuous functions of $x$ and $E$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{7}})}$ defined as $\operatorname{mkContinuous}$ applied to $\operatorname{codRestrict}$ applied to $\operatorname{LpSubmodule}$ applied to $x_{4}$, $E$, $p$ and $x_{1}$, the composition of $\operatorname{toAEEqFunLinearMap}$ applied to $x_{1}$ and the continuous map linear map of $E$ and $x_{4}$ and $\mathrm{BoundedContinuousFunction\_\_mem\_Lp}$, $\operatorname{toReal} (\operatorname{measureUnivNNReal} (x_{1}))^ {\operatorname{inv} (\operatorname{toReal} (p))}$ and $\mathrm{BoundedContinuousFunction\_\_Lp\_norm\_le}$.
BoundedContinuousFunction.toLpHomdefMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Then $\operatorname{toLpHom}$ applied to $p$ and $x_{1}$ is a normed additive group homomorphism of the set of bounded continuous functions of $x$ and $E$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{4}})}$.
ContinuousMap.toLpdefMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $x_{4}$ be a set. Then $\operatorname{toLp}$ applied to $p$, $x_{1}$ and $x_{4}$ is a continuous linear map of the set of continuous maps of $x$ and $E$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{7}})}$ defined as the composition of $\operatorname{toLp}$ applied to $p$, $x_{1}$ and $x_{4}$ and the continuous linear map of the continuous linear equivalence of $\operatorname{linearIsometryBoundedOfCompact}$ applied to $x$, $E$ and $x_{4}$.
MeasureTheory.Lp.boundedContinuousFunctiondefMathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions, function or constantWording
the bounded continuous function of p and x1 (from the name)
English
Let $E$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Then the bounded continuous function of $p$ and $x_{1}$ is an additive subgroup of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{4}})}$ defined as the additive subgroup of the range of the composition of $\operatorname{toAEEqFunAddHom}$ applied to $x_{1}$ and the continuous map additive monoid homomorphism of $x$ and $E$ and $\operatorname{Lp}$ applied to $E$, $p$ and $x_{1}$.
MeasureTheory.Lp.constdefMathlib.MeasureTheory.Function.LpSpace.Indicator, function or constantWording
the constant of p and x1 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Then the constant of $p$ and $x_{1}$ is an additive monoid homomorphism of $E$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{3}})}$.
MeasureTheory.Lp.constLdefMathlib.MeasureTheory.Function.LpSpace.Indicator, function or constantWording
the constant of p and x1 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $x_{3}$ be a set. Then the constant of $p$ and $x_{1}$ is a continuous linear map of $E$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{6}})}$.
MeasureTheory.Lp.constₗdefMathlib.MeasureTheory.Function.LpSpace.Indicator, function or constantWording
the constant of p and x1 (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Let $x_{3}$ be a set. Then the constant of $p$ and $x_{1}$ is a linear map of $E$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{6}})}$.
MeasureTheory.indicatorConstLpdefMathlib.MeasureTheory.Function.LpSpace.Indicator, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Assume that $s$ is a measurable set. Assume that $x_{1}$ applied to $s$ is distinct from the top. Let $c$ be an element of $E$. Then $\operatorname{indicatorConstLp}$ applied to $p$, $\mathrm{hs}$, $h$ and $c$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{1})}{x_{3}})}$.
IndexedPartition.simpleFunc_piecewisedefMathlib.MeasureTheory.Function.Piecewise, function or constantEnglish
Let $\mathrm{hs}$ be an indexed partition of $s$. Assume that for all elements $i$ of $x$, $s$ applied to $i$ is a measurable set. Let $f$ be a function from elements of $x$ to simple functions of $x_{1}$ and $x_{2}$. Then $\mathrm{IndexedPartition\_\_simpleFunc\_piecewise}$ applied to $\mathrm{hs}$, $\mathrm{hm}$ and $f$ is a simple function of $x_{1}$ and $x_{2}$.
MeasureTheory.SimpleFuncstructureMathlib.MeasureTheory.Function.SimpleFunc, typeWording
simple function of x and x2 (from the name)
English
Let $x$ and $x_{2}$ be sets. Then the simple functions of $x$ and $x_{2}$ are a basic type.
MeasureTheory.SimpleFunc.FinMeasSuppdefMathlib.MeasureTheory.Function.SimpleFunc, predicateEnglish
Let $f$ be a simple function of $x$ and $x_{1}$. Let $x_{3}$ be a measure of $x$. Then $\operatorname{FinMeasSupp}$ holds for $f$ and $x_{3}$, if $\operatorname{EventuallyEq}$ holds for the cofinite of $x_{3}$, $\operatorname{coe}$ applied to $f$ and $0$.
MeasureTheory.SimpleFunc.approxdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $i$ be a function from natural numbers to elements of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $n$ be a natural number. Then $\operatorname{approx}$ applied to $i$, $f$ and $n$ is a simple function of $x$ and $x_{1}$ defined as the supremum of the range of $n$ and the function that maps $k$ to $\operatorname{restrict}$ applied to the constant of $x$ and $i$ applied to $k$ and $\operatorname{ofPred}$ applied to the function that maps $a$ to $\mathrm{Leq} (i (k), f (a))$.
MeasureTheory.SimpleFunc.binddefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $f$ be a simple function of $x$ and $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to simple functions of $x$ and $x_{2}$. Then $\operatorname{bind}$ applied to $f$ and $g$ is a simple function of $x$ and $x_{2}$.
MeasureTheory.SimpleFunc.compdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be a simple function of $x_{1}$ and $x_{2}$. Let $g$ be a measurable function from elements of $x$ to elements of $x_{1}$. Then the composition of $f$ and $g$ is a simple function of $x$ and $x_{2}$.
MeasureTheory.SimpleFunc.constdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the constant of x and b (from the name)
English
Let $x$ be a set. Let $b$ be an element of $x_{1}$. Then the constant of $x$ and $b$ is a simple function of $x$ and $x_{1}$.
MeasureTheory.SimpleFunc.ditedefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $s$ be an element of $\wp x$ such that $s$ is a measurable set. Let $f$ be a simple function of the set of elements of $s$ and $x_{1}$. Let $g$ be a simple function of the set of elements of the complement of $s$ and $x_{1}$. Then $\operatorname{dite}$ applied to $s$, $\mathrm{hs}$, $f$ and $g$ is a simple function of $x$ and $x_{1}$.
MeasureTheory.SimpleFunc.eapproxdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $x_{2}$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Let $x_{3}$ be a natural number. Then $\operatorname{eapprox}$ applied to $x_{2}$ and $x_{3}$ is a simple function of $x$ and $\mathrm{ENNReal}$ defined as $\operatorname{approx}$ applied to $\operatorname{ennrealRatEmbed}$, $x_{2}$ and $x_{3}$.
MeasureTheory.SimpleFunc.eapproxDiffdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Let $x_{2}$ be a natural number. Then $\operatorname{eapproxDiff}$ applied to $f$ and $x_{2}$ is a simple function of $x$ and $\mathrm{NNReal}$.
MeasureTheory.SimpleFunc.ennrealRatEmbeddefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the extended nonnegative real number rational number embed of n (from the name)
English
Let $n$ be a natural number. Then the extended nonnegative real number rational number embed of $n$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{ofReal}$ applied to $\operatorname{cast}$ applied to $\operatorname{getD}$ applied to the decode of $n$ and $0$.
MeasureTheory.SimpleFunc.extenddefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $x_{5}$ be a simple function of $x$ and $x_{2}$. Let $g$ be a function from elements of $x$ to elements of $x_{1}$ such that $g$ is a measurable embedding. Let $x_{6}$ be a simple function of $x_{1}$ and $x_{2}$. Then $\operatorname{extend}$ applied to $x_{5}$, $g$, $\mathrm{hg}$ and $x_{6}$ is a simple function of $x_{1}$ and $x_{2}$.
MeasureTheory.SimpleFunc.lintegraldefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $f$ be a simple function of $x$ and $\mathrm{ENNReal}$. Let $x_{1}$ be a measure of $x$. Then $\operatorname{lintegral}$ applied to $f$ and $x_{1}$ is an element of $\mathrm{ENNReal}$ defined as $\FinsetSum {\operatorname{range} (f)}{x_{2}}{(x_{2} \times x_{1} (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (x_{2}))))}$.
MeasureTheory.SimpleFunc.lintegralₗdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
$\mathrm{MeasureTheory\_\_SimpleFunc\_\_lintegral\_u2097\_}$ is a linear map of the set of simple functions of $x$ and $\mathrm{ENNReal}$ and the set of linear maps of the set of measures of $x$ and $\mathrm{ENNReal}$.
MeasureTheory.SimpleFunc.mapdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the map of g and f (from the name)
English
Let $g$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Let $f$ be a simple function of $x$ and $x_{1}$. Then the map of $g$ and $f$ is a simple function of $x$ and $x_{2}$ defined as $\operatorname{bind}$ applied to $f$ and $\operatorname{comp}$ applied to $\operatorname{const}$ applied to $x$ and $g$.
MeasureTheory.SimpleFunc.ofFinitedefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the simple function of f (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the simple function of $f$ is a simple function of $x$ and $x_{1}$.
MeasureTheory.SimpleFunc.ofIsEmptydefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the simple function (from the name)
English
The simple function is a simple function of $x$ and $x_{1}$ defined as the simple function of the function that maps $a$ to $\mathrm{isEmptyElim}$ applied to $a$.
MeasureTheory.SimpleFunc.pairdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the pair of f and g (from the name)
English
Let $f$ be a simple function of $x$ and $x_{1}$. Let $g$ be a simple function of $x$ and $x_{2}$. Then the pair of $f$ and $g$ is a simple function of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as the sequence of the map of $\ProdmkMACRoU$ and $f$ and $g$.
MeasureTheory.SimpleFunc.piecewisedefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $s$ be an element of $\wp x$ such that $s$ is a measurable set. Let $f$ and $g$ be simple functions of $x$ and $x_{1}$. Then $\operatorname{piecewise}$ applied to $s$, $\mathrm{hs}$, $f$ and $g$ is a simple function of $x$ and $x_{1}$.
MeasureTheory.SimpleFunc.rangedefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the range of f (from the name)
English
Let $f$ be a simple function of $x$ and $x_{1}$. Then the range of $f$ is a finite set of $x_{1}$ defined as the finite set of $\mathrm{MeasureTheory\_\_SimpleFunc\_\_finite\_range}$ applied to $f$.
MeasureTheory.SimpleFunc.restrictdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantEnglish
Let $f$ be a simple function of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then $\operatorname{restrict}$ applied to $f$ and $s$ is a simple function of $x$ and $x_{1}$ defined as $\mathrm{dite}$ applied to the proposition that $s$ is a measurable set, the function that maps $\mathrm{hs}$ to $\operatorname{piecewise}$ applied to $s$, $\mathrm{hs}$, $f$ and $0$ and the function that maps $\mathrm{hs1}$ to $0$.
MeasureTheory.SimpleFunc.seqdefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the sequence of f and g (from the name)
English
Let $f$ be a simple function of $x$ and the set of functions from elements of $x_{1}$ to elements of $x_{2}$. Let $g$ be a simple function of $x$ and $x_{1}$. Then the sequence of $f$ and $g$ is a simple function of $x$ and $x_{2}$ defined as $\operatorname{bind}$ applied to $f$ and the function that maps $f_{1}$ to the map of $f_{1}$ and $g$.
MeasureTheory.SimpleFunc.toFundefMathlib.MeasureTheory.Function.SimpleFunc, function or constantWording
the underlying function of self and x3 (from the docstring)
English
Let $\mathrm{self}$ be a simple function of $x$ and $x_{2}$. Let $x_{3}$ be an element of $x$. Then the underlying function of $\mathrm{self}$ and $x_{3}$ is an element of $x_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{3}$.
MeasureTheory.SimpleFunc.approxOndefMathlib.MeasureTheory.Function.SimpleFuncDense, function or constantEnglish
Let $f$ be a measurable function from elements of $x_{1}$ to elements of $x$. Let $s$ be an element of $\wp x$. Let $x_{5}$ be an element of $x$ such that $x_{5}$ is an element of $s$. Let $n$ be a natural number. Then $\operatorname{approxOn}$ applied to $f$, $\mathrm{hf}$, $s$, $x_{5}$, $h_{1}$ and $n$ is a simple function of $x_{1}$ and $x$.
MeasureTheory.SimpleFunc.nearestPtdefMathlib.MeasureTheory.Function.SimpleFuncDense, function or constantEnglish
Let $e$ be a function from natural numbers to elements of $x$. Let $N$ be a natural number. Then $\operatorname{nearestPt}$ applied to $e$ and $N$ is a simple function of $x$ and $x$ defined as the map of $e$ and $\operatorname{nearestPtInd}$ applied to $e$ and $N$.
MeasureTheory.SimpleFunc.nearestPtInddefMathlib.MeasureTheory.Function.SimpleFuncDense, function or constantEnglish
Let $e$ be a function from natural numbers to elements of $x$. Let $x_{3}$ be a natural number. Then $\operatorname{nearestPtInd}$ applied to $e$ and $x_{3}$ is a simple function of $x$ and $\Natural$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{MeasureTheory\_\_SimpleFunc\_\_nearestPtInd\_\_\_f}$ applied to $e$.
MeasureTheory.Lp.simpleFuncdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantWording
the simple function of p and x3 (from the name)
English
Let $E$ be a set. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{3}$ be a measure of $x$. Then the simple function of $p$ and $x_{3}$ is an additive subgroup of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{3})}{x_{4}})}$.
MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonnegdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantEnglish
Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{2}$ be a measure of $x$. Let $G$ be a set. Let $x_{5}$ be an element of $\mathrm{Nonneg}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (p , x_{2})}{x_{7}})}$. Then $\operatorname{coeSimpleFuncNonnegToLpNonneg}$ applied to $p$, $x_{2}$, $G$ and $x_{5}$ is an element of $\mathrm{Nonneg}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (G , p , x_{2})}{x_{6}})}$ defined as $x_{5}$.
MeasureTheory.Lp.simpleFunc.coeToLpdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantEnglish
Let $x$, $E$ and $x_{1}$ be sets. Then $\operatorname{coeToLp}$ applied to $x$, $E$ and $x_{1}$ is a continuous linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (p , x_{4})}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , p , x_{4})}{x_{8}})}$.
MeasureTheory.Lp.simpleFunc.indicatorConstdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantWording
the indicator constant of p and c (from the name)
English
Let $p$ be an element of $\mathrm{ENNReal}$. Assume that $s$ is a measurable set. Assume that $x_{3} (s)\neq \operatorname{top}$. Let $c$ be an element of $E$. Then the indicator constant of $p$ and $c$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (p , x_{3})}{x_{4}})}$.
MeasureTheory.Lp.simpleFunc.toSimpleFuncdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantWording
the simple function of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (p , x_{3})}{x_{4}})}$. Then the simple function of $f$ is a simple function of $x$ and $E$.
MeasureTheory.SimpleFunc.toLpdefMathlib.MeasureTheory.Function.SimpleFuncDenseLp, function or constantEnglish
Let $f$ be a simple function of $x$ and $E$ such that $\operatorname{MemLp}$ holds for $\operatorname{coe}$ applied to $f$, $p$ and $x_{3}$. Then $\operatorname{toLp}$ applied to $f$ and $\mathrm{hf}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (p , x_{3})}{x_{4}})}$ defined as $\operatorname{toLp}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$.
MeasureTheory.AEFinStronglyMeasurabledefMathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_AEFinStronglyMeasurable\_\_\_auto\_1}$. Then $\operatorname{AEFinStronglyMeasurable}$ holds for $f$ and $x_{5}$, if there exists a function $g$ from elements of $x$ to elements of $x_{1}$, such that $\operatorname{FinStronglyMeasurable}$ holds for $g$ and $x_{5}$ and $\operatorname{EventuallyEq}$ holds for $\operatorname{ae}$ applied to $x_{5}$, $f$ and $g$.
MeasureTheory.AEFinStronglyMeasurable.mkdefMathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{AEFinStronglyMeasurable}$ holds for $f$ and $x_{2}$. Let $x_{5}$ be an element of $x$. Then $\operatorname{mk}$ applied to $f$, $\mathrm{hf}$ and $x_{5}$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$ and $x_{5}$.
MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSetdefMathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable, function or constantWording
the sigma finite set of hf (from the name)
English
Assume that $\operatorname{AEFinStronglyMeasurable}$ holds for $f$ and $x_{2}$. Then the sigma finite set of $\mathrm{hf}$ is an element of $\wp x$ defined as $\operatorname{choose}$ applied to $\mathrm{MeasureTheory\_\_AEFinStronglyMeasurable\_\_exists\_set\_sigmaFinite}$ applied to $\mathrm{hf}$.
MeasureTheory.AEStronglyMeasurabledefMathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_AEStronglyMeasurable\_\_\_auto\_1}$. Then $\operatorname{AEStronglyMeasurable}$ holds for $f$ and $x_{4}$, if there exists a function $g$ from elements of $x$ to elements of $x_{1}$, such that $\operatorname{StronglyMeasurable}$ holds for $g$ and $\operatorname{EventuallyEq}$ holds for $\operatorname{ae}$ applied to $x_{4}$, $f$ and $g$.
MeasureTheory.AEStronglyMeasurable.mkdefMathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable, function or constantEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$ such that $\operatorname{AEStronglyMeasurable}$ holds for $f$ and $x_{4}$. Let $x_{5}$ be an element of $x$. Then $\operatorname{mk}$ applied to $f$, $\mathrm{hf}$ and $x_{5}$ is an element of $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$ and $x_{5}$.
MeasureTheory.FinStronglyMeasurabledefMathlib.MeasureTheory.Function.StronglyMeasurable.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_FinStronglyMeasurable\_\_\_auto\_1}$. Then $\operatorname{FinStronglyMeasurable}$ holds for $f$ and $x_{5}$, if there exists a function $\mathrm{fs}$ from natural numbers to simple functions of $x$ and $x_{1}$, such that for all natural numbers $n$, $x_{5}$ applied to the support of $\operatorname{coe}$ applied to $\mathrm{fs}$ applied to $n$ is less than the top and for all elements $x_{6}$ of $x$, $\operatorname{Tendsto}$ holds for the function that maps $n_{1}$ to $\mathrm{fs}$ applied to $n_{1}$ and $x_{6}$, $\operatorname{atTop}$ and the neighbourhood filter of $f$ applied to $x_{6}$.
MeasureTheory.FinStronglyMeasurable.approxdefMathlib.MeasureTheory.Function.StronglyMeasurable.Basic, function or constantEnglish
Assume that $\operatorname{FinStronglyMeasurable}$ holds for $f$ and $x_{2}$. Let $x_{5}$ be a natural number. Then $\operatorname{approx}$ applied to $\mathrm{hf}$ and $x_{5}$ is a simple function of $x$ and $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$ and $x_{5}$.
MeasureTheory.StronglyMeasurabledefMathlib.MeasureTheory.Function.StronglyMeasurable.Basic, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{StronglyMeasurable}$ holds for $f$, if there exists a function $\mathrm{fs}$ from natural numbers to simple functions of $x$ and $x_{1}$, such that for all elements $x_{4}$ of $x$, $\operatorname{Tendsto}$ holds for the function that maps $n$ to $\mathrm{fs}$ applied to $n$ and $x_{4}$, $\operatorname{atTop}$ and the neighbourhood filter of $f$ applied to $x_{4}$.
MeasureTheory.StronglyMeasurable.approxdefMathlib.MeasureTheory.Function.StronglyMeasurable.Basic, function or constantEnglish
Assume that $\operatorname{StronglyMeasurable}$ holds for $f$. Let $x_{4}$ be a natural number. Then $\operatorname{approx}$ applied to $\mathrm{hf}$ and $x_{4}$ is a simple function of $x$ and $x_{1}$ defined as $\operatorname{choose}$ applied to $\mathrm{hf}$ and $x_{4}$.
MeasureTheory.StronglyMeasurable.approxBoundeddefMathlib.MeasureTheory.Function.StronglyMeasurable.Basic, function or constantEnglish
Assume that $\operatorname{StronglyMeasurable}$ holds for $f$. Let $c$ be an element of $\Real$. Let $x_{6}$ be an element of $\Natural$. Then $\operatorname{approxBounded}$ applied to $\mathrm{hf}$, $c$ and $x_{6}$ is a simple function of $x$ and $x_{1}$ defined as the map of the function that maps $x_{7}$ to $\HSMulhSMulMACRoAL {(\MinminMACRoAG {1}{(\frac{ c}{\operatorname{norm} (x_{7})})})}{x_{7}}$ and $\operatorname{approx}$ applied to $\mathrm{hf}$ and $x_{6}$.
MeasureTheory.UnifTightdefMathlib.MeasureTheory.Function.UnifTight, predicateEnglish
Let $f$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Then $\operatorname{UnifTight}$ holds for $f$, $p$ and $x_{5}$, if for all elements $x_{6}$ of $\mathrm{ENNReal}$, if $x_{6} > 0$, then there exists an element $s$ of $\wp x$, such that $x_{5}$ applied to $s$ is distinct from the top and for all elements $i$ of $x_{2}$, $\operatorname{eLpNorm}$ applied to $\operatorname{indicator}$ applied to $f$ applied to $i$, $p$ and $x_{5}$ is less than or equal to $x_{6}$.
MeasureTheory.UnifIntegrabledefMathlib.MeasureTheory.Function.UniformIntegrable, predicateEnglish
Let $f$ be a function from elements of $x_{2}$ and elements of $x$ to elements of $x_{1}$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $x_{5}$ be a measure of $x$. Then $\operatorname{UnifIntegrable}$ holds for $f$, $p$ and $x_{5}$, if $\operatorname{Tendsto}$ holds for the function that maps $x_{6}$ to the supremum of the function that maps $i$ to the supremum of the function that maps $s$ to the supremum of the function that maps $h$ to $\operatorname{eLpNorm}$ applied to $f$ applied to $i$, $p$ and $\operatorname{restrict}$ applied to $x_{5}$ and $s$, the neighbourhood filter of $0$ and the neighbourhood filter of $0$.
AddAction.aestabilizerdefMathlib.MeasureTheory.Group.AEStabilizer, function or constantEnglish
Let $G$ be a set. Let $x_{4}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{aestabilizer}$ applied to $G$, $x_{4}$ and $s$ is an additive subgroup of $G$.
MulAction.aestabilizerdefMathlib.MeasureTheory.Group.AEStabilizer, function or constantEnglish
Let $G$ be a set. Let $x_{4}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then $\operatorname{aestabilizer}$ applied to $G$, $x_{4}$ and $s$ is a subgroup of $G$.
MeasurableAddclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
M is a measurable sum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable sum.
MeasurableAdd₂classMathlib.MeasureTheory.Group.Arithmetic, predicateWording
M is a measurable sum (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable sum.
MeasurableConstSMulclassMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableConstSMul}$ holds for $M$ and $x$.
MeasurableConstVAddclassMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableConstVAdd}$ holds for $M$ and $x$.
MeasurableDivclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
x is a measurable quotient (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a measurable quotient.
MeasurableDiv₂classMathlib.MeasureTheory.Group.Arithmetic, predicateWording
x is a measurable quotient (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a measurable quotient.
MeasurableInvclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
G is a measurable inverse (from the name)
English
Let $G$ be a set. Then we can say that $G$ is a measurable inverse.
MeasurableMulclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
M is a measurable product (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable product.
MeasurableMul₂classMathlib.MeasureTheory.Group.Arithmetic, predicateWording
M is a measurable product (from the name)
English
Let $M$ be a set. Then we can say that $M$ is a measurable product.
MeasurableNegclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
G is a measurable negation (from the name)
English
Let $G$ be a set. Then we can say that $G$ is a measurable negation.
MeasurablePowclassMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\mathrm{MeasurablePow}$ holds for $x$ and $x_{1}$.
MeasurableSMulclassMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableSMul}$ holds for $M$ and $x$.
MeasurableSMul₂classMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableSMul\_u2082\_}$ holds for $M$ and $x$.
MeasurableSubclassMathlib.MeasureTheory.Group.Arithmetic, predicateWording
G is a measurable difference (from the name)
English
Let $G$ be a set. Then we can say that $G$ is a measurable difference.
MeasurableSub₂classMathlib.MeasureTheory.Group.Arithmetic, predicateWording
G is a measurable difference (from the name)
English
Let $G$ be a set. Then we can say that $G$ is a measurable difference.
MeasurableVAddclassMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableVAdd}$ holds for $M$ and $x$.
MeasurableVAdd₂classMathlib.MeasureTheory.Group.Arithmetic, predicateEnglish
Let $M$ and $x$ be sets. Then we can say that $\mathrm{MeasurableVAdd\_u2082\_}$ holds for $M$ and $x$.
MeasureTheory.Measure.convdefMathlib.MeasureTheory.Group.Convolution, function or constantEnglish
Let $x_{2}$ and $x_{3}$ be measures of $M$. Then $\operatorname{conv}$ applied to $x_{2}$ and $x_{3}$ is a measure of $M$ defined as the map of the function that maps $x_{4}$ to $\ProdfstMACRoZ {x_{4}}+ \ProdsndMACRoAA {x_{4}}$ and the product of $x_{2}$ and $x_{3}$.
MeasureTheory.Measure.mconvdefMathlib.MeasureTheory.Group.Convolution, function or constantEnglish
Let $x_{2}$ and $x_{3}$ be measures of $M$. Then $\operatorname{mconv}$ applied to $x_{2}$ and $x_{3}$ is a measure of $M$ defined as the map of the function that maps $x_{4}$ to $\ProdfstMACRoZ {x_{4}}\times \ProdsndMACRoAA {x_{4}}$ and the product of $x_{2}$ and $x_{3}$.
MeasureTheory.Measure.IsAddLeftInvariantclassMathlib.MeasureTheory.Group.Defs, predicateWording
x2 is a additive left invariant (from the name)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is an additive left invariant.
MeasureTheory.Measure.IsAddRightInvariantclassMathlib.MeasureTheory.Group.Defs, predicateWording
x2 is a additive right invariant (from the name)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is an additive right invariant.
MeasureTheory.Measure.IsMulLeftInvariantclassMathlib.MeasureTheory.Group.Defs, predicateWording
x2 is a multiplicative left invariant (from the name)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is a multiplicative left invariant.
MeasureTheory.Measure.IsMulRightInvariantclassMathlib.MeasureTheory.Group.Defs, predicateWording
x2 is a multiplicative right invariant (from the name)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is a multiplicative right invariant.
MeasureTheory.SMulInvariantMeasureclassMathlib.MeasureTheory.Group.Defs, predicateWording
x3 is a multiplicative invariant measure (from the name)
English
Let $M$ and $x$ be sets. Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is a multiplicative invariant measure.
MeasureTheory.VAddInvariantMeasureclassMathlib.MeasureTheory.Group.Defs, predicateWording
x3 is a additive invariant measure (from the name)
English
Let $M$ and $x$ be sets. Let $x_{3}$ be a measure of $x$. Then we can say that $x_{3}$ is an additive invariant measure.
IsAddFoelnerstructureMathlib.MeasureTheory.Group.FoelnerFilter, predicateEnglish
Let $G$ be a set. Let $x_{1}$ be a measure of $X$. Let $l$ be a filter of $x_{4}$. Let $F$ be a function from elements of $x_{4}$ to elements of $\wp X$. Then we can say that $\mathrm{IsAddFoelner}$ holds for $G$, $x_{1}$, $l$ and $F$.
IsAddFoelner.meandefMathlib.MeasureTheory.Group.FoelnerFilter, function or constantEnglish
Let $x_{1}$ be a measure of $X$. Let $u$ be a ultrafilter of $x_{2}$. Let $F$ be a function from elements of $x_{2}$ to elements of $\wp X$. Let $s$ be an element of $\wp X$. Then $\operatorname{mean}$ applied to $x_{1}$, $u$, $F$ and $s$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{limUnder}$ applied to $\operatorname{toFilter}$ applied to $u$ and the function that maps $i$ to $\frac{ x_{1} (\operatorname{inter} (s , F (i)))}{x_{1} (F (i))}$.
IsFoelnerstructureMathlib.MeasureTheory.Group.FoelnerFilter, predicateEnglish
Let $G$ be a set. Let $x_{1}$ be a measure of $X$. Let $l$ be a filter of $x_{4}$. Let $F$ be a function from elements of $x_{4}$ to elements of $\wp X$. Then we can say that $\mathrm{IsFoelner}$ holds for $G$, $x_{1}$, $l$ and $F$.
IsFoelner.meandefMathlib.MeasureTheory.Group.FoelnerFilter, function or constantEnglish
Let $x_{1}$ be a measure of $X$. Let $u$ be a ultrafilter of $x_{2}$. Let $F$ be a function from elements of $x_{2}$ to elements of $\wp X$. Let $s$ be an element of $\wp X$. Then $\operatorname{mean}$ applied to $x_{1}$, $u$, $F$ and $s$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{limUnder}$ applied to $\operatorname{toFilter}$ applied to $u$ and the function that maps $i$ to $\frac{ x_{1} (\operatorname{inter} (s , F (i)))}{x_{1} (F (i))}$.
maxAddFoelnerdefMathlib.MeasureTheory.Group.FoelnerFilter, function or constantEnglish
Let $G$ be a set. Let $x_{1}$ be a measure of $X$. Then $\mathrm{maxAddFoelner}$ applied to $G$ and $x_{1}$ is a filter of $\wp X$ defined as the minimum of the principal filter of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set, $x_{1} (s)\neq 0$ and $x_{1}$ applied to $s$ is distinct from the top and the infimum of the function that maps $g$ to the preimage of the function that maps $s_{1}$ to the quotient of $x_{1}$ applied to the symmetric difference operator of the sum of $g$ and $s_{1}$ and $s_{1}$ and $x_{1}$ applied to $s_{1}$ and the neighbourhood filter of $0$.
maxFoelnerdefMathlib.MeasureTheory.Group.FoelnerFilter, function or constantEnglish
Let $G$ be a set. Let $x_{1}$ be a measure of $X$. Then $\mathrm{maxFoelner}$ applied to $G$ and $x_{1}$ is a filter of $\wp X$ defined as the minimum of the principal filter of $\operatorname{ofPred}$ applied to the function that maps $s$ to the proposition that $s$ is a measurable set, $x_{1} (s)\neq 0$ and $x_{1}$ applied to $s$ is distinct from the top and the infimum of the function that maps $g$ to the preimage of the function that maps $s_{1}$ to the quotient of $x_{1}$ applied to the symmetric difference operator of $\HSMulhSMulMACRoAL {g}{s_{1}}$ and $s_{1}$ and $x_{1}$ applied to $s_{1}$ and the neighbourhood filter of $0$.
MeasureTheory.AddQuotientMeasureEqMeasurePreimageclassMathlib.MeasureTheory.Group.FundamentalDomain, predicateEnglish
Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_AddQuotientMeasureEqMeasurePreimage\_\_\_auto\_1}$. Let $x_{5}$ be a measure of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $x$. Then we can say that $\operatorname{AddQuotientMeasureEqMeasurePreimage}$ holds for $x_{4}$ and $x_{5}$.
MeasureTheory.HasAddFundamentalDomainclassMathlib.MeasureTheory.Group.FundamentalDomain, predicateWording
x4 has additive fundamental domains (from the name)
English
Let $G$ and $x$ be sets. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_HasAddFundamentalDomain\_\_\_auto\_1}$. Then we can say that $x_{4}$ has additive fundamental domains.
MeasureTheory.HasFundamentalDomainclassMathlib.MeasureTheory.Group.FundamentalDomain, predicateWording
x4 has fundamental domains (from the name)
English
Let $G$ and $x$ be sets. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_HasFundamentalDomain\_\_\_auto\_1}$. Then we can say that $x_{4}$ has fundamental domains.
MeasureTheory.IsAddFundamentalDomainstructureMathlib.MeasureTheory.Group.FundamentalDomain, predicateEnglish
Let $G$ be a set. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_IsAddFundamentalDomain\_\_\_auto\_1}$. Then we can say that $\operatorname{IsAddFundamentalDomain}$ holds for $G$, $s$ and $x_{4}$.
MeasureTheory.IsFundamentalDomainstructureMathlib.MeasureTheory.Group.FundamentalDomain, predicateEnglish
Let $G$ be a set. Let $s$ be an element of $\wp x$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_IsFundamentalDomain\_\_\_auto\_1}$. Then we can say that $\operatorname{IsFundamentalDomain}$ holds for $G$, $s$ and $x_{4}$.
MeasureTheory.QuotientMeasureEqMeasurePreimageclassMathlib.MeasureTheory.Group.FundamentalDomain, predicateEnglish
Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_QuotientMeasureEqMeasurePreimage\_\_\_auto\_1}$. Let $x_{5}$ be a measure of $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $G$ and $x$. Then we can say that $\operatorname{QuotientMeasureEqMeasurePreimage}$ holds for $x_{4}$ and $x_{5}$.
MeasureTheory.addCovolumedefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantEnglish
Let $G$ and $x$ be sets. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_addCovolume\_\_\_auto\_1}$. Then $\operatorname{addCovolume}$ applied to $G$, $x$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as $\mathrm{dite}$ applied to the proposition that $x_{4}$ has additive fundamental domains, the function that maps $\mathrm{funDom}$ to $x_{4}$ applied to $\operatorname{choose}$ applied to $\operatorname{ExistsIsAddFundamentalDomain}$ and the function that maps $\mathrm{funDom1}$ to $0$.
MeasureTheory.addFundamentalFrontierdefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantWording
the additive fundamental frontier of G and s (from the name)
English
Let $G$ be a set. Let $s$ be an element of $\wp x$. Then the additive fundamental frontier of $G$ and $s$ is an element of $\wp x$ defined as $\operatorname{inter}$ applied to $s$ and the union of the function that maps $g$ to the union of the function that maps $h$ to the sum of $g$ and $s$.
MeasureTheory.addFundamentalInteriordefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantWording
the interior of G and s (from the docstring)
English
Let $G$ be a set. Let $s$ be an element of $\wp x$. Then the interior of $G$ and $s$ is an element of $\wp x$ defined as $\operatorname{sdiff}$ applied to $s$ and the union of the function that maps $g$ to the union of the function that maps $h$ to the sum of $g$ and $s$.
MeasureTheory.covolumedefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantEnglish
Let $G$ and $x$ be sets. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_covolume\_\_\_auto\_1}$. Then $\operatorname{covolume}$ applied to $G$, $x$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as $\mathrm{dite}$ applied to the proposition that $x_{4}$ has fundamental domains, the function that maps $\mathrm{funDom}$ to $x_{4}$ applied to $\operatorname{choose}$ applied to $\operatorname{ExistsIsFundamentalDomain}$ and the function that maps $\mathrm{funDom1}$ to $0$.
MeasureTheory.fundamentalFrontierdefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantWording
the fundamental frontier of G and s (from the name)
English
Let $G$ be a set. Let $s$ be an element of $\wp x$. Then the fundamental frontier of $G$ and $s$ is an element of $\wp x$ defined as $\operatorname{inter}$ applied to $s$ and the union of the function that maps $g$ to the union of the function that maps $h$ to $\HSMulhSMulMACRoAL {g}{s}$.
MeasureTheory.fundamentalInteriordefMathlib.MeasureTheory.Group.FundamentalDomain, function or constantWording
the interior of G and s (from the docstring)
English
Let $G$ be a set. Let $s$ be an element of $\wp x$. Then the interior of $G$ and $s$ is an element of $\wp x$ defined as $\operatorname{sdiff}$ applied to $s$ and the union of the function that maps $g$ to the union of the function that maps $h$ to $\HSMulhSMulMACRoAL {g}{s}$.
MeasurableEquiv.addLeftdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantEnglish
Let $g$ be an element of $G$. Then $\operatorname{addLeft}$ applied to $g$ is a measurable equivalence of $G$ and $G$ defined as the vector sum of $g$.
MeasurableEquiv.addRightdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantEnglish
Let $g$ be an element of $G$. Then $\operatorname{addRight}$ applied to $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.divLeftdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the left quotient of g (from the name)
English
Let $g$ be an element of $G$. Then the left quotient of $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.divRightdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the right quotient of g (from the name)
English
Let $g$ be an element of $G$. Then the right quotient of $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.invdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the inverse of G (from the name)
English
Let $G$ be a set. Then the inverse of $G$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.mulLeftdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the left multiplicative of g (from the name)
English
Let $g$ be an element of $G$. Then the left multiplicative of $g$ is a measurable equivalence of $G$ and $G$ defined as the scalar multiple of $g$.
MeasurableEquiv.mulLeft₀defMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the left multiplicative of g and hg (from the name)
English
Let $g$ be an element of $x$ such that $g \neq 0$. Then the left multiplicative of $g$ and $\mathrm{hg}$ is a measurable equivalence of $x$ and $x$ defined as the scalar multiple of $g$ and $\mathrm{hg}$.
MeasurableEquiv.mulRightdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the right multiplicative of g (from the name)
English
Let $g$ be an element of $G$. Then the right multiplicative of $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.mulRight₀defMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the right multiplicative of g and hg (from the name)
English
Let $g$ be an element of $x$ such that $g \neq 0$. Then the right multiplicative of $g$ and $\mathrm{hg}$ is a measurable equivalence of $x$ and $x$.
MeasurableEquiv.negdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the negation of G (from the name)
English
Let $G$ be a set. Then the negation of $G$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.smuldefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the scalar multiple of c (from the name)
English
Let $c$ be an element of $G$. Then the scalar multiple of $c$ is a measurable equivalence of $x$ and $x$.
MeasurableEquiv.smul₀defMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the scalar multiple of c and hc (from the name)
English
Let $c$ be an element of $x$ such that $c \neq 0$. Then the scalar multiple of $c$ and $\mathrm{hc}$ is a measurable equivalence of $x_{1}$ and $x_{1}$ defined as the scalar multiple of $\operatorname{mk0}$ applied to $c$ and $\mathrm{hc}$.
MeasurableEquiv.subLeftdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the left difference of g (from the name)
English
Let $g$ be an element of $G$. Then the left difference of $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.subRightdefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the right difference of g (from the name)
English
Let $g$ be an element of $G$. Then the right difference of $g$ is a measurable equivalence of $G$ and $G$.
MeasurableEquiv.vadddefMathlib.MeasureTheory.Group.MeasurableEquiv, function or constantWording
the vector sum of c (from the name)
English
Let $c$ be an element of $G$. Then the vector sum of $c$ is a measurable equivalence of $x$ and $x$.
MeasureTheory.Measure.IsAddHaarMeasureclassMathlib.MeasureTheory.Group.Measure, predicateWording
x3 is a additive Haar measure (from the name)
English
Let $x_{3}$ be a measure of $G$. Then we can say that $x_{3}$ is an additive Haar measure.
MeasureTheory.Measure.IsHaarMeasureclassMathlib.MeasureTheory.Group.Measure, predicateWording
x3 is a Haar measure (from the name)
English
Let $x_{3}$ be a measure of $G$. Then we can say that $x_{3}$ is a Haar measure.
MeasureTheory.Measure.IsInvInvariantclassMathlib.MeasureTheory.Group.Measure, predicateWording
x2 is invariant under inversion (from the docstring)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is invariant under inversion.
MeasureTheory.Measure.IsNegInvariantclassMathlib.MeasureTheory.Group.Measure, predicateWording
x2 is invariant under negation (from the docstring)
English
Let $x_{2}$ be a measure of $G$. Then we can say that $x_{2}$ is invariant under negation.
MeasureTheory.Measure.invdefMathlib.MeasureTheory.Group.Measure, function or constantWording
the inverse of x2 (from the name)
English
Let $x_{2}$ be a measure of $G$. Then the inverse of $x_{2}$ is a measure of $G$ defined as the map of $\operatorname{inv}$ and $x_{2}$.
MeasureTheory.Measure.negdefMathlib.MeasureTheory.Group.Measure, function or constantWording
the negation of x2 (from the name)
English
Let $x_{2}$ be a measure of $G$. Then the negation of $x_{2}$ is a measure of $G$ defined as the map of $\operatorname{neg}$ and $x_{2}$.
MeasureTheory.Measure.addModularCharacterFundefMathlib.MeasureTheory.Group.ModularCharacter, function or constantWording
the additive modular character of g (from the docstring)
English
Let $g$ be an element of $G$. Then the additive modular character of $g$ is an element of $\mathrm{NNReal}$ defined as the additive Haar scalar factor of the map of the function that maps $x_{2}$ to $x_{2} + g$ and the additive Haar and the additive Haar.
MeasureTheory.Measure.modularCharacterdefMathlib.MeasureTheory.Group.ModularCharacter, function or constantWording
the modular character homomorphism (from the docstring)
English
The modular character homomorphism is a monoid homomorphism of $G$ and $\mathrm{NNReal}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{modularCharacterFun}$ and $\mathrm{MeasureTheory\_\_Measure\_\_modularCharacterFun\_map\_one}$ and $\mathrm{MeasureTheory\_\_Measure\_\_modularCharacterFun\_map\_mul}$.
MeasureTheory.Measure.modularCharacterFundefMathlib.MeasureTheory.Group.ModularCharacter, function or constantWording
the modular character of g (from the docstring)
English
Let $g$ be an element of $G$. Then the modular character of $g$ is an element of $\mathrm{NNReal}$ defined as the Haar scalar factor of the map of the function that maps $x_{2}$ to $x_{2} \times g$ and the Haar and the Haar.
MeasurableEquiv.shearAddRightdefMathlib.MeasureTheory.Group.Prod, function or constantEnglish
Let $G$ be a set. Then $\operatorname{shearAddRight}$ applied to $G$ is a measurable equivalence of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.
MeasurableEquiv.shearDivRightdefMathlib.MeasureTheory.Group.Prod, function or constantWording
the right shear quotient of G (from the name)
English
Let $G$ be a set. Then the right shear quotient of $G$ is a measurable equivalence of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.
MeasurableEquiv.shearMulRightdefMathlib.MeasureTheory.Group.Prod, function or constantWording
the right shear multiplicative of G (from the name)
English
Let $G$ be a set. Then the right shear multiplicative of $G$ is a measurable equivalence of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.
MeasurableEquiv.shearSubRightdefMathlib.MeasureTheory.Group.Prod, function or constantWording
the right shear difference of G (from the name)
English
Let $G$ be a set. Then the right shear difference of $G$ is a measurable equivalence of $\mathrm{Prod}$ applied to $G$ and $G$ and $\mathrm{Prod}$ applied to $G$ and $G$.
MeasureTheory.averagedefMathlib.MeasureTheory.Integral.Average, function or constantEnglish
Let $x_{3}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $E$. Then $\operatorname{average}$ applied to $x_{3}$ and $f$ is an element of $E$ defined as the Bochner integral of $\HSMulhSMulMACRoAL {\operatorname{inv} (x_{3} (\operatorname{univ}))}{x_{3}}$ and the function that maps $x_{4}$ to $f$ applied to $x_{4}$.
MeasureTheory.laveragedefMathlib.MeasureTheory.Integral.Average, function or constantEnglish
Let $x_{1}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{laverage}$ applied to $x_{1}$ and $f$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{lintegral}$ applied to $\HSMulhSMulMACRoAL {\operatorname{inv} (x_{1} (\operatorname{univ}))}{x_{1}}$ and the function that maps $x_{2}$ to $f$ applied to $x_{2}$.
MeasureTheory.SimpleFunc.toLargerSpacedefMathlib.MeasureTheory.Integral.Bochner.Basic, function or constantEnglish
Assume that $m \leq m_{0}$. Let $f$ be a simple function of $x$ and $x_{1}$. Then $\operatorname{toLargerSpace}$ applied to $\mathrm{hm}$ and $f$ is a simple function of $x$ and $x_{1}$.
MeasureTheory.integraldefMathlib.MeasureTheory.Integral.Bochner.Basic, function or constantWording
the Bochner integral of x4 and f (from the docstring)
English
Let $x_{4}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $G$. Then the Bochner integral of $x_{4}$ and $f$ is an element of $G$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Integral\_\_Bochner\_\_Basic\_\_266965040\_\_\_hygCtx\_\_\_hyg\_\_8}$, $x_{4}$ and $f$.
MeasureTheory.L1.SimpleFunc.integraldefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{2})}{x_{4}})}$. Then the integral of $f$ is an element of $E$ defined as the integral of $x_{2}$ and the simple function of $f$.
MeasureTheory.L1.SimpleFunc.integralCLMdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral continuous linear map of x2 (from the name)
English
Let $x$ and $E$ be sets. Let $x_{2}$ be a measure of $x$. Then the integral continuous linear map of $x_{2}$ is a continuous linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{2})}{x_{4}})}$ and $E$ defined as the integral continuous linear map of $x_{2}$.
MeasureTheory.L1.SimpleFunc.integralCLM'defMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral continuous linear map of x3 (from the name)
English
Let $x$, $E$ and $x_{1}$ be sets. Let $x_{3}$ be a measure of $x$. Then the integral continuous linear map of $x_{3}$ is a continuous linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{3})}{x_{7}})}$ and $E$.
MeasureTheory.L1.SimpleFunc.negPartdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the negation part of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{1})}{x_{3}})}$. Then the negation part of $f$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{1})}{x_{2}})}$ defined as the positive part part of $\operatorname{neg}$ applied to $f$.
MeasureTheory.L1.SimpleFunc.posPartdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the positive part part of f (from the name)
English
Let $f$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{1})}{x_{3}})}$. Then the positive part part of $f$ is an element of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{1})}{x_{2}})}$ defined as the positive part part of $f$.
MeasureTheory.L1.integraldefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral of x4 (from the name)
English
Let $x_{4}$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{2})}{x_{5}})}$. Then the integral of $x_{4}$ is an element of $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_L1\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Integral\_\_Bochner\_\_L1\_\_1479606858\_\_\_hygCtx\_\_\_hyg\_\_2}$ and $x_{4}$.
MeasureTheory.L1.integralCLMdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral continuous linear map (from the name)
English
The integral continuous linear map is a continuous linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{2})}{x_{4}})}$ and $E$ defined as the integral continuous linear map of $\Real$.
MeasureTheory.L1.integralCLM'defMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral continuous linear map of x1 (from the name)
English
Let $x_{1}$ be a set. Then the integral continuous linear map of $x_{1}$ is a continuous linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{3})}{x_{7}})}$ and $E$ defined as $\operatorname{extend}$ applied to the integral continuous linear map of $x_{3}$ and $\operatorname{coeToLp}$ applied to $x$, $E$ and $x_{1}$.
MeasureTheory.SimpleFunc.integraldefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the integral of x4 and f (from the name)
English
Let $x_{4}$ be a measure of $x$. Let $f$ be a simple function of $x$ and $F$. Then the integral of $x_{4}$ and $f$ is an element of $F$ defined as the set to simple function of $\operatorname{weightedSMul}$ applied to $x_{4}$ and $f$.
MeasureTheory.SimpleFunc.negPartdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the negation part of f (from the name)
English
Let $f$ be a simple function of $x$ and $E$. Then the negation part of $f$ is a simple function of $x$ and $E$ defined as the positive part part of $\operatorname{neg}$ applied to $f$.
MeasureTheory.SimpleFunc.posPartdefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the positive part part of f (from the name)
English
Let $f$ be a simple function of $x$ and $E$. Then the positive part part of $f$ is a simple function of $x$ and $E$ defined as the map of the function that maps $b$ to $\MaxmaxMACRoAF {b}{0}$ and $f$.
MeasureTheory.weightedSMuldefMathlib.MeasureTheory.Integral.Bochner.L1, function or constantWording
the weighted product of x4 and s (from the name)
English
Let $x_{4}$ be a measure of $x$. Let $s$ be an element of $\wp x$. Then the weighted product of $x_{4}$ and $s$ is a continuous linear map of $F$ and $F$ defined as $\HSMulhSMulMACRoAL {\operatorname{real} (x_{4} , s)}{\operatorname{id} (\Real , F)}$.
MeasureTheory.LpToLpRestrictCLMdefMathlib.MeasureTheory.Integral.Bochner.Set, function or constantEnglish
Let $X$, $F$ and $x$ be sets. Let $x_{4}$ be a measure of $X$. Let $p$ be an element of $\mathrm{ENNReal}$. Let $s$ be an element of $\wp X$. Then $\operatorname{LpToLpRestrictCLM}$ applied to $X$, $F$, $x$, $x_{4}$, $p$ and $s$ is a continuous linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , x_{4})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (F , p , \operatorname{restrict} (x_{4} , s))}{x_{6}})}$.
Real.circleAveragedefMathlib.MeasureTheory.Integral.CircleAverage, function or constantEnglish
Let $f$ be a function from complexes to elements of $E$. Let $c$ be a complex. Let $R$ be an element of $\Real$. Then $\operatorname{circleAverage}$ applied to $f$, $c$ and $R$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (2 \times \operatorname{pi})}{\mathrm{intervalIntegral} (2 \times \operatorname{pi} , \operatorname{volume})}$.
CircleIntegrabledefMathlib.MeasureTheory.Integral.CircleIntegral, predicateEnglish
Let $f$ be a function from complexes to elements of $E$. Let $c$ be a complex. Let $R$ be a real number. Then $\mathrm{CircleIntegrable}$ holds for $f$, $c$ and $R$, if $\mathrm{IntervalIntegrable}$ holds for the function that maps $x_{1}$ to $f$ applied to the circle map of $R$ and $x_{1}$, the volume, $0$ and the product of $2$ and the product.
cauchyPowerSeriesdefMathlib.MeasureTheory.Integral.CircleIntegral, function or constantWording
the Cauchy power series of c and R (from the name)
English
Let $f$ be a function from complexes to elements of $E$. Let $c$ be a complex. Let $R$ be an element of $\Real$. Then the Cauchy power series of $c$ and $R$ is a formal multilinear series of the set of complexes and $E$ defined as the function that maps $n$ to the product ring of $\HSMulhSMulMACRoAL {\operatorname{inv} (2 \times \operatorname{ofReal} (\operatorname{pi})\times \operatorname{I})}{\mathrm{circleIntegral} (c , R)}$.
circleIntegraldefMathlib.MeasureTheory.Integral.CircleIntegral, function or constantWording
the circle integral of c and R (from the name)
English
Let $f$ be a function from complexes to elements of $E$. Let $c$ be a complex. Let $R$ be a real number. Then the circle integral of $c$ and $R$ is an element of $E$ defined as the interval integral of the product of $2$ and the product and the volume.
CompactlySupportedContinuousMap.integralLinearMapdefMathlib.MeasureTheory.Integral.CompactlySupported, function or constantWording
the integral linear map of x2 (from the name)
English
Let $x_{2}$ be a measure of $X$. Then the integral linear map of $x_{2}$ is a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $X$ and $\mathrm{NNReal}$ and $\mathrm{NNReal}$ defined as $\operatorname{toNNRealLinear}$ applied to the integral positive linear map of $x_{2}$.
CompactlySupportedContinuousMap.integralPositiveLinearMapdefMathlib.MeasureTheory.Integral.CompactlySupported, function or constantWording
the integral positive linear map of x2 (from the name)
English
Let $x_{2}$ be a measure of $X$. Then the integral positive linear map of $x_{2}$ is a positive linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $X$ and $\Real$ and $\Real$.
CurveIntegrabledefMathlib.MeasureTheory.Integral.CurveIntegral.Basic, predicateWording
x6 is a curve integrable with respect to x7 (from the name)
English
Let $x_{6}$ be a function from elements of $E$ to continuous linear maps of $E$ and $F$. Let $x_{7}$ be a path of $a$ and $b$. Then $x_{6}$ is a curve integrable with respect to $x_{7}$, if $\mathrm{IntervalIntegrable}$ holds for $\mathrm{curveIntegralFun}$ applied to $x_{7}$, the volume, $0$ and $1$.
curveIntegraldefMathlib.MeasureTheory.Integral.CurveIntegral.Basic, function or constantWording
the curve integral of x6 and x7 (from the name)
English
Let $x_{6}$ be a function from elements of $E$ to continuous linear maps of $E$ and $F$. Let $x_{7}$ be a path of $a$ and $b$. Then the curve integral of $x_{6}$ and $x_{7}$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Integral\_\_CurveIntegral\_\_Basic\_\_4243001254\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{6}$ and $x_{7}$.
curveIntegralFundefMathlib.MeasureTheory.Integral.CurveIntegral.Basic, function or constantWording
the curve integral function of x7 and t (from the name)
English
Let $x_{6}$ be a function from elements of $E$ to continuous linear maps of $E$ and $F$. Let $x_{7}$ be a path of $a$ and $b$. Let $t$ be a real number. Then the curve integral function of $x_{7}$ and $t$ is an element of $F$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Integral\_\_CurveIntegral\_\_Basic\_\_4195796962\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{6}$, $x_{7}$ and $t$.
MeasureTheory.DominatedFinMeasAdditivedefMathlib.MeasureTheory.Integral.FinMeasAdditive, predicateEnglish
Let $x_{4}$ be a measure of $x$. Let $T$ be a function from elements of $\wp x$ to elements of $x_{1}$. Let $C$ be a real number. Then $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{4}$, $T$ and $C$, if $\operatorname{FinMeasAdditive}$ holds for $x_{4}$ and $T$ and for all elements $s$ of $\wp x$, if $s$ is a measurable set, then if $x_{4}$ applied to $s$ is less than the top, then the norm of $T$ applied to $s$ is less than or equal to $C \times \operatorname{real} (x_{4} , s)$.
MeasureTheory.FinMeasAdditivedefMathlib.MeasureTheory.Integral.FinMeasAdditive, predicateEnglish
Let $x_{4}$ be a measure of $x$. Let $T$ be a function from elements of $\wp x$ to elements of $x_{1}$. Then $\operatorname{FinMeasAdditive}$ holds for $x_{4}$ and $T$, if for all elements $s$ and $t$ of $\wp x$, if $s$ is a measurable set, then if $t$ is a measurable set, then if $x_{4}$ applied to $s$ is distinct from the top, then if $x_{4}$ applied to $t$ is distinct from the top, then if $s$ is disjoint to $t$, then $\EqtMACRoH {T (\UnionunionMACRoAB {s}{t})}{T (s)+ T (t)}$.
MeasureTheory.SimpleFunc.setToSimpleFuncdefMathlib.MeasureTheory.Integral.FinMeasAdditive, function or constantWording
the set to simple function of T and f (from the name)
English
Let $T$ be a function from elements of $\wp x$ to continuous linear maps of $F$ and $\mathrm{F'}$. Let $f$ be a simple function of $x$ and $F$. Then the set to simple function of $T$ and $f$ is an element of $\mathrm{F'}$ defined as $\FinsetSum {\operatorname{range} (f)}{x_{6}}{T (\operatorname{preimage} (\operatorname{coe} (f), \operatorname{singleton} (x_{6})), x_{6})}$.
MeasureTheory.IntegrableAtFilterdefMathlib.MeasureTheory.Integral.IntegrableOn, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a filter of $x$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_IntegrableAtFilter\_\_\_auto\_1}$. Then $\operatorname{IntegrableAtFilter}$ holds for $f$, $l$ and $x_{5}$, if there exists an element $s$ of $\wp x$, such that $s$ is an element of $l$ and $\operatorname{IntegrableOn}$ holds for $f$, $s$ and $x_{5}$.
MeasureTheory.IntegrableOndefMathlib.MeasureTheory.Integral.IntegrableOn, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Let $x_{5}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{MeasureTheory\_\_IntegrableOn\_\_\_auto\_1}$. Then $\operatorname{IntegrableOn}$ holds for $f$, $s$ and $x_{5}$, if $\operatorname{Integrable}$ holds for $f$ and $\operatorname{restrict}$ applied to $x_{5}$ and $s$.
StronglyMeasurableAtFilterdefMathlib.MeasureTheory.Integral.IntegrableOn, predicateEnglish
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $l$ be a filter of $x$. Let $x_{4}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $x$ and $\mathrm{StronglyMeasurableAtFilter\_\_\_auto\_1}$. Then $\mathrm{StronglyMeasurableAtFilter}$ holds for $f$, $l$ and $x_{4}$, if there exists an element $s$ of $\wp x$, such that $s$ is an element of $l$ and $\operatorname{AEStronglyMeasurable}$ holds for $f$ and $\operatorname{restrict}$ applied to $x_{4}$ and $s$.
MeasureTheory.AECoverstructureMathlib.MeasureTheory.Integral.IntegralEqImproper, predicateEnglish
Let $x_{3}$ be a measure of $x$. Let $l$ be a filter of $x_{1}$. Let $x_{4}$ be a function from elements of $x_{1}$ to elements of $\wp x$. Then we can say that $\operatorname{AECover}$ holds for $x_{3}$, $l$ and $x_{4}$.
IntervalIntegrabledefMathlib.MeasureTheory.Integral.IntervalIntegral.Basic, predicateEnglish
Let $f$ be a function from real numbers to elements of $x$. Let $x_{3}$ be a measure of $\Real$. Let $a$ and $b$ be real numbers. Then $\mathrm{IntervalIntegrable}$ holds for $f$, $x_{3}$, $a$ and $b$, if $\operatorname{IntegrableOn}$ holds for $f$, $\operatorname{Ioc}$ applied to $a$ and $b$ and $x_{3}$ and $\operatorname{IntegrableOn}$ holds for $f$, $\operatorname{Ioc}$ applied to $b$ and $a$ and $x_{3}$.
intervalIntegraldefMathlib.MeasureTheory.Integral.IntervalIntegral.Basic, function or constantWording
the interval integral of b and x2 (from the name)
English
Let $f$ be a function from real numbers to elements of $E$. Let $a$ and $b$ be real numbers. Let $x_{2}$ be a measure of $\Real$. Then the interval integral of $b$ and $x_{2}$ is an element of $E$ defined as the difference between the Bochner integral of $\operatorname{restrict}$ applied to $x_{2}$ and $\operatorname{Ioc}$ applied to $a$ and $b$ and the function that maps $x_{3}$ to $f$ applied to $x_{3}$ and the Bochner integral of $\operatorname{restrict}$ applied to $x_{2}$ and $\operatorname{Ioc}$ applied to $b$ and $a$ and the function that maps $x_{4}$ to $f$ applied to $x_{4}$.
AddCircle.measurableEquivIcodefMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic, function or constantEnglish
Let $T$ and $a$ be real numbers. Then $\operatorname{measurableEquivIco}$ applied to $T$ and $a$ is a measurable equivalence of the set of additive circles of $T$ and the set of elements of $\operatorname{Ico}$ applied to $a$ and $a + T$.
AddCircle.measurableEquivIocdefMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic, function or constantEnglish
Let $T$ and $a$ be real numbers. Then $\operatorname{measurableEquivIoc}$ applied to $T$ and $a$ is a measurable equivalence of the set of additive circles of $T$ and the set of elements of $\operatorname{Ioc}$ applied to $a$ and $a + T$.
trapezoidal_errordefMathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule, function or constantWording
the trapezoidal error of a and b (from the name)
English
Let $f$ be a function from real numbers to real numbers. Let $N$ be a natural number. Let $a$ and $b$ be real numbers. Then the trapezoidal error of $a$ and $b$ is a real number defined as the difference between the trapezoidal integral of $a$ and $b$ and the interval integral of $b$ and the volume.
trapezoidal_integraldefMathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule, function or constantWording
the trapezoidal integral of a and b (from the name)
English
Let $f$ be a function from elements of $\Real$ to real numbers. Let $N$ be a natural number. Let $a$ and $b$ be elements of $\Real$. Then the trapezoidal integral of $a$ and $b$ is a real number defined as $\frac{ b - a}{N}\times (\frac{ f (a)+ f (b)}{2}+ \FinsetSum {\FinsetrangeMACRoN {(N - 1)}}{k}{f (a + \frac{ (k + 1)\times (b - a)}{N})})$.
MeasureTheory.lintegraldefMathlib.MeasureTheory.Integral.Lebesgue.Basic, function or constantEnglish
Let $x_{1}$ be a measure of $x$. Let $f$ be a function from elements of $x$ to elements of $\mathrm{ENNReal}$. Then $\operatorname{lintegral}$ applied to $x_{1}$ and $f$ is an element of $\mathrm{ENNReal}$ defined as $\operatorname{proj0}$ applied to $\mathrm{MeasureTheory\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_MeasureTheory\_\_Integral\_\_Lebesgue\_\_Basic\_\_3365958504\_\_\_hygCtx\_\_\_hyg\_\_2}$, $x_{1}$ and $f$.
MeasureTheory.lmarginaldefMathlib.MeasureTheory.Integral.Marginal, function or constantEnglish
Let $x_{3}$ be a function from elements $i_{2}$ of $x$ to measures of $X$ applied to $i_{2}$. Let $s$ be a finite set of $x$. Let $f$ be a function from functions from elements $i_{1}$ of $x$ to elements of $X$ applied to $i_{1}$ to elements of $\mathrm{ENNReal}$. Let $x_{4}$ be a function from elements $i$ of $x$ to elements of $X$ applied to $i$. Then $\operatorname{lmarginal}$ applied to $i_{2}$, $x_{3}$, $s$, $f$, $i$ and $x_{4}$ is an element of $\mathrm{ENNReal}$ defined as the function that maps $i$ and $x_{4}$ to $\operatorname{lintegral}$ applied to the finite product of the measures of the function that maps $i$ to $i_{2}$ applied to $i$, the function that maps $y$ to $s$ applied to $\operatorname{updateFinset}$ applied to $f$, $x_{3}$ and $y$, $i$ and $x_{4}$.
NNRealRMK.rieszMeasuredefMathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic, function or constantWording
the Riesz measure of x1 (from the name)
English
Let $x_{1}$ be a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $X$ and $\mathrm{NNReal}$ and $\mathrm{NNReal}$. Then the Riesz measure of $x_{1}$ is a measure of $X$ defined as the measure of the Riesz content of $x_{1}$.
rieszContentdefMathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic, function or constantWording
the Riesz content of x1 (from the name)
English
Let $x_{1}$ be a linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $X$ and $\mathrm{NNReal}$ and $\mathrm{NNReal}$. Then the Riesz content of $x_{1}$ is a content of $X$ defined as $\operatorname{mk}$ applied to $\mathrm{rieszContentAux}$ applied to $x_{1}$, the function that maps $x_{2}$ and $x_{3}$ to $\mathrm{rieszContentAux\_mono}$ applied to $x_{1}$, the function that maps $x_{4}$, $x_{5}$, $\mathrm{disj}$, $h_{2}$ and $h_{3}$ to $\mathrm{rieszContentAux\_union}$ applied to $x_{1}$ and $\mathrm{disj}$ and $\mathrm{rieszContentAux\_sup\_le}$ applied to $x_{1}$.
RealRMK.rieszMeasuredefMathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real, function or constantWording
the Riesz measure of x2 (from the name)
English
Let $x_{2}$ be a positive linear map of $\mathrm{CompactlySupportedContinuousMap}$ applied to $X$ and $\Real$ and $\Real$. Then the Riesz measure of $x_{2}$ is a measure of $X$ defined as the measure of the Riesz content of $\operatorname{toNNRealLinear}$ applied to $x_{2}$.
MeasureTheory.setToFundefMathlib.MeasureTheory.Integral.SetToL1.Function, function or constantWording
the set to function of T and f (from the name)
English
Let $x_{5}$ be a measure of $x$. Let $T$ be a function from elements of $\wp x$ to continuous linear maps of $E$ and $F$ such that $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{5}$, $T$ and $C$. Let $f$ be a function from elements of $x$ to elements of $E$. Then the set to function of $T$ and $f$ is an element of $F$ defined as $\mathrm{dite}$ applied to the proposition that $F$ is a complete space, the function that maps $\mathrm{\_hF}$ to $\mathrm{dite}$ applied to $\operatorname{Integrable}$ applied to $f$ and $x_{5}$, the function that maps $\mathrm{hf}$ to $\operatorname{setToL1}$ applied to $\mathrm{hT}$ and $\operatorname{toL1}$ applied to $f$ and $\mathrm{hf}$ and the function that maps $\mathrm{hf1}$ to $0$ and the function that maps $\mathrm{\_hF1}$ to $0$.
MeasureTheory.L1.setToL1defMathlib.MeasureTheory.Integral.SetToL1.L1, function or constantEnglish
Assume that $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{5}$, $T$ and $C$. Then $\operatorname{setToL1}$ applied to $\mathrm{hT}$ is a continuous linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{5})}{x_{6}})}$ and $F$ defined as $\operatorname{extend}$ applied to $\operatorname{setToL1SCLM}$ applied to $x$, $E$, $x_{5}$ and $\mathrm{hT}$ and $\operatorname{coeToLp}$ applied to $x$, $E$ and $\Real$.
MeasureTheory.L1.setToL1'defMathlib.MeasureTheory.Integral.SetToL1.L1, function or constantEnglish
Let $x_{1}$ be a set. Assume that $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{6}$, $T$ and $C$. Assume that for all elements $c$ of $x_{1}$, for all elements $s$ of $\wp x$, for all elements $x_{11}$ of $E$, $\EqtMACRoH {T (s , \HSMulhSMulMACRoAL {c}{x_{11}})}{\HSMulhSMulMACRoAL {c}{T (s , x_{11})}}$. Then $\operatorname{setToL1'}$ applied to $x_{1}$, $\mathrm{hT}$ and $\mathrm{h\_smul}$ is a continuous linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{Lp} (E , 1 , x_{6})}{x_{10}})}$ and $F$ defined as $\operatorname{extend}$ applied to $\operatorname{setToL1SCLM'}$ applied to $x$, $E$, $x_{1}$, $x_{6}$, $\mathrm{hT}$ and $\mathrm{h\_smul}$ and $\operatorname{coeToLp}$ applied to $x$, $E$ and $x_{1}$.
MeasureTheory.L1.SimpleFunc.setToL1SdefMathlib.MeasureTheory.Integral.SetToL1.SimpleFunc, function or constantEnglish
Let $T$ be a function from elements of $\wp x$ to continuous linear maps of $E$ and $F$. Let $f$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{5})}{x_{6}})}$. Then $\operatorname{setToL1S}$ applied to $T$ and $f$ is an element of $F$ defined as the set to simple function of $T$ and the simple function of $f$.
MeasureTheory.L1.SimpleFunc.setToL1SCLMdefMathlib.MeasureTheory.Integral.SetToL1.SimpleFunc, function or constantEnglish
Let $x$ and $E$ be sets. Let $x_{5}$ be a measure of $x$ such that $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{5}$, $T$ and $C$. Then $\operatorname{setToL1SCLM}$ applied to $x$, $E$, $x_{5}$ and $\mathrm{hT}$ is a continuous linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{5})}{x_{6}})}$ and $F$.
MeasureTheory.L1.SimpleFunc.setToL1SCLM'defMathlib.MeasureTheory.Integral.SetToL1.SimpleFunc, function or constantEnglish
Let $x$, $E$ and $x_{1}$ be sets. Let $x_{6}$ be a measure of $x$ such that $\operatorname{DominatedFinMeasAdditive}$ holds for $x_{6}$, $T$ and $C$. Assume that for all elements $c$ of $x_{1}$, for all elements $s$ of $\wp x$, for all elements $x_{11}$ of $E$, $\EqtMACRoH {T (s , \HSMulhSMulMACRoAL {c}{x_{11}})}{\HSMulhSMulMACRoAL {c}{T (s , x_{11})}}$. Then $\operatorname{setToL1SCLM'}$ applied to $x$, $E$, $x_{1}$, $x_{6}$, $\mathrm{hT}$ and $\mathrm{h\_smul}$ is a continuous linear map of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{simpleFunc} (1 , x_{6})}{x_{10}})}$ and $F$.
TorusIntegrabledefMathlib.MeasureTheory.Integral.TorusIntegral, predicateEnglish
Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to complexes to elements of $E$. Let $c$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to complexes. Let $R$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\Real$. Then $\mathrm{TorusIntegrable}$ holds for $f$, $c$ and $R$, if $\operatorname{IntegrableOn}$ holds for the function that maps $x_{1}$ to $f$ applied to $\mathrm{torusMap}$ applied to $x_{1}$, $\SetIccMACRoP {0}{x_{2}}{(2 \times \operatorname{pi})}$ and the volume.
torusIntegraldefMathlib.MeasureTheory.Integral.TorusIntegral, function or constantWording
the torus integral of c and R (from the name)
English
Let $f$ be a function from functions from elements of $\mathrm{Fin}$ applied to $n$ to complexes to elements of $E$. Let $c$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to complexes. Let $R$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $\Real$. Then the torus integral of $c$ and $R$ is an element of $E$ defined as the Bochner integral of $\operatorname{restrict}$ applied to the volume and $\SetIccMACRoP {0}{x_{2}}{(2 \times \operatorname{pi})}$ and the function that maps $x_{3}$ to $\HSMulhSMulMACRoAL {(\FinsetProd {\FinsetunivMACRoAC}{i}{(\operatorname{ofReal} (R (i))\times \operatorname{exp} (\operatorname{ofReal} (x_{3} (i))\times \operatorname{I})\times \operatorname{I})})}{f (\mathrm{torusMap} (x_{3}))}$.
torusMapdefMathlib.MeasureTheory.Integral.TorusIntegral, function or constantWording
the torus map of x and x1 (from the name)
English
Let $c$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to complexes. Let $R$ and $x$ be functions from elements of $\mathrm{Fin}$ applied to $n$ to real numbers. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to $n$. Then the torus map of $x$ and $x_{1}$ is a complex defined as the sum of $c$ applied to $x_{1}$ and the product of the natural inclusion of the real numbers into the complex numbers of $R$ applied to $x_{1}$ and the exponential of the product of the natural inclusion of the real numbers into the complex numbers of $x$ applied to $x_{1}$ and $\operatorname{I}$.
IsCountablySpanningdefMathlib.MeasureTheory.MeasurableSpace.Basic, predicateEnglish
Let $C$ be an element of $\wp (\wp x)$. Then $\mathrm{IsCountablySpanning}$ holds for $C$, if there exists a function $s$ from natural numbers to elements of $\wp x$, such that for all natural numbers $n$, $\MembershipmemMACRoT {C}{s (n)}$ and the union of the function that maps $n_{1}$ to $s$ applied to $n_{1}$ is equal to the universal set.
MeasurableSpace.generateMeasurableRecdefMathlib.MeasureTheory.MeasurableSpace.Card, function or constantEnglish
Let $s$ be an element of $\wp (\wp x)$. Let $i$ be an ordinal. Then $\operatorname{generateMeasurableRec}$ applied to $s$ and $i$ is an element of $\wp (\wp x)$.
MeasurableEqclassMathlib.MeasureTheory.MeasurableSpace.Constructions, predicateEnglish
Let $x$ be a set. Then we can say that $\mathrm{MeasurableEq}$ holds for $x$.
measurableAtomdefMathlib.MeasureTheory.MeasurableSpace.Constructions, function or constantWording
the measurable atom of x2 (from the name)
English
Let $x_{2}$ be an element of $x$. Then the measurable atom of $x_{2}$ is an element of $\wp x$ defined as the intersection of the function that maps $s$ to the intersection of the function that maps $\mathrm{\_h's}$ to the intersection of the function that maps $\mathrm{\_hs}$ to $s$.
MeasurableSpace.CountableOrCountablyGeneratedclassMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, predicateEnglish
Let $x$ and $x_{1}$ be sets. Then we can say that $\operatorname{CountableOrCountablyGenerated}$ holds for $x$ and $x_{1}$.
MeasurableSpace.CountablyGeneratedclassMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{CountablyGenerated}$ holds for $x$.
MeasurableSpace.CountablySeparatedclassMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, predicateWording
x is countably separated (from the name)
English
generation took over the time limit
MeasurableSpace.SeparatesPointsclassMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, predicateEnglish
Let $x$ be a set. Then we can say that $\operatorname{SeparatesPoints}$ holds for $x$.
MeasurableSpace.countableGeneratingSetdefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantWording
the countable generating set of x (from the name)
English
Let $x$ be a set. Then the countable generating set of $x$ is an element of $\wp (\wp x)$ defined as $\operatorname{insert}$ applied to $\operatorname{emptyCollection}$ and $\operatorname{choose}$ applied to $\operatorname{isCountablyGenerated}$.
MeasurableSpace.countablePartitiondefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantWording
the countable partition of x and x2 (from the name)
English
Let $x$ be a set. Let $x_{2}$ be a natural number. Then the countable partition of $x$ and $x_{2}$ is an element of $\wp (\wp x)$ defined as the membership partition of $\operatorname{enumerateCountable}$ applied to $\mathrm{MeasurableSpace\_\_countable\_countableGeneratingSet}$ and $\operatorname{emptyCollection}$ and $x_{2}$.
MeasurableSpace.countablePartitionSetdefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantWording
the countable partition set of n and a (from the name)
English
Let $n$ be a natural number. Let $a$ be an element of $x$. Then the countable partition set of $n$ and $a$ is an element of $\wp x$ defined as the set in $\operatorname{enumerateCountable}$ applied to $\mathrm{MeasurableSpace\_\_countable\_countableGeneratingSet}$ and $\operatorname{emptyCollection}$.
MeasurableSpace.countablyGeneratedAtomdefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantEnglish
Let $x$ be a set. Let $x_{2}$ be a function from elements of $\Natural$ to propositions. Then $\operatorname{countablyGeneratedAtom}$ applied to $x$ and $x_{2}$ is an element of $\wp x$ defined as the intersection of the function that maps $n$ to $\iteMACRoG {x_{2} (n)}{\operatorname{natGeneratingSequence} (x , n)}{\operatorname{compl} (\operatorname{natGeneratingSequence} (x , n))}$.
MeasurableSpace.mapNatBooldefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantWording
the map natural bool of x2 and n (from the name)
English
Let $x$ be a set. Let $x_{2}$ be an element of $x$. Let $n$ be a natural number. Then the map natural bool of $x_{2}$ and $n$ is an element of $\mathrm{Bool}$ defined as $\operatorname{decide}$ applied to the proposition that $x_{2}$ is an element of the natural generating sequence of $x$ and $n$.
MeasurableSpace.natGeneratingSequencedefMathlib.MeasureTheory.MeasurableSpace.CountablyGenerated, function or constantWording
the natural generating sequence of x and x2 (from the name)
English
Let $x$ be a set. Let $x_{2}$ be a natural number. Then the natural generating sequence of $x$ and $x_{2}$ is an element of $\wp x$ defined as $\operatorname{enumerateCountable}$ applied to $\mathrm{MeasurableSpace\_\_countable\_countableGeneratingSet}$, $\operatorname{emptyCollection}$ and $x_{2}$.
DiscreteMeasurableSpaceclassMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
x is a discrete measurable space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a discrete measurable space.
MeasurabledefMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
f is measurable (from the name)
English
Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then $f$ is measurable, if for all elements $t$ of $\wp x_{1}$, if $t$ is a measurable set, then the preimage of $f$ and $t$ is a measurable set.
MeasurableSetdefMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
s is a measurable set (from the name)
English
Let $s$ be an element of $\wp x$. Then $s$ is a measurable set, if $s$ is a measurable set.
MeasurableSingletonClassclassMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
x is a measurable singleton class (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a measurable singleton class.
MeasurableSpaceclassMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
x is a measurable space (from the name)
English
Let $x$ be a set. Then we can say that $x$ is a measurable space.
MeasurableSpace.GenerateMeasurableinductiveMathlib.MeasureTheory.MeasurableSpace.Defs, predicateEnglish
Let $s$ be an element of $\wp (\wp x)$. Let $x_{1}$ be an element of $\wp x$. Then we can say that $\operatorname{GenerateMeasurable}$ holds for $s$ and $x_{1}$.
MeasurableSpace.GenerateMeasurable.belowinductiveMathlib.MeasureTheory.MeasurableSpace.Defs, predicateEnglish
Assume that $\operatorname{GenerateMeasurable}$ holds for $s$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.
MeasurableSpace.MeasurableSet'defMathlib.MeasureTheory.MeasurableSpace.Defs, predicateWording
x1 is a measurable set (from the name)
English
Assume that $x$ is a measurable space. Let $x_{1}$ be an element of $\wp x$. Then $x_{1}$ is a measurable set, if $\operatorname{proj0}$ holds for $\mathrm{self}$ and $x_{1}$.
MeasurableSpace.giGenerateFromdefMathlib.MeasureTheory.MeasurableSpace.Defs, function or constantEnglish
$\operatorname{giGenerateFrom}$ is a Galois insertion of $\operatorname{generateFrom}$ and the function that maps $m$ to $\operatorname{ofPred}$ applied to the function that maps $t$ to the proposition that $t$ is a measurable set.