HomeTheorem List (p. 227 of 411)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 227 of 411) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-26652) |
Hilbert Space Explorer
(26653-28175) |
Users' Mathboxes
(28176-41046) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ioovolcl 22601 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
     ![/\](wedge.gif "/\"){kind=small}       | ||
| Theorem | ovolfs2 22602 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
           
 | ||
| Theorem | ioorcl2 22603 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
 
| ||
| Theorem | ioorf 22604 | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
 
 
    inf    | ||
| Theorem | ioorval 22605* | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.) |
|
inf
inf | ||
| Theorem | ioorinv2 22606* |
The function is an
"inverse" of sorts to the open interval
function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by
AV, 13-Sep-2020.)
|
|
inf | ||
| Theorem | ioorinv 22607* |
The function is an
"inverse" of sorts to the open interval
function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by
AV, 13-Sep-2020.)
|
|
inf | ||
| Theorem | ioorcl 22608* |
The function does not
always return real numbers, but it does on
intervals of finite volume. (Contributed by Mario Carneiro,
26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
|
|
inf
| ||
| Theorem | ioorfOLD 22609 | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) Obsolete version of ioorf 22604 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
 | ||
| Theorem | ioorvalOLD 22610* | Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) Obsolete version of ioorval 22605 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | ioorinv2OLD 22611* |
The function is an
"inverse" of sorts to the open interval
function. (Contributed by Mario Carneiro, 26-Mar-2015.) Obsolete
version of ioorinv2 22606 as of 13-Sep-2020. (New usage is
discouraged.)
(Proof modification is discouraged.)
|
|
| ||
| Theorem | ioorinvOLD 22612* |
The function is an
"inverse" of sorts to the open interval
function. (Contributed by Mario Carneiro, 26-Mar-2015.) Obsolete
version of ioorinv 22607 as of 13-Sep-2020. (New usage is
discouraged.)
(Proof modification is discouraged.)
|
|
| ||
| Theorem | ioorclOLD 22613* |
The function does not
always return real numbers, but it does on
intervals of finite volume. (Contributed by Mario Carneiro,
26-Mar-2015.) Obsolete version of ioorcl 22608 as of 13-Sep-2020.
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | uniiccdif 22614 | A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015.) |
 ![[,]](_icc.gif "[,]"){kind=small} ![\](setminus.gif "\"){kind=small} | ||
| Theorem | uniioovol 22615* | A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 22586.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
 Disj   
| ||
| Theorem | uniiccvol 22616* | An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 22586.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
|
Disj
| ||
| Theorem | uniioombllem1 22617* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 25-Mar-2015.) |
Disj
   
| ||
| Theorem | uniioombllem2a 22618* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 7-May-2015.) |
Disj
 
| ||
| Theorem | uniioombllem2 22619* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by AV, 13-Sep-2020.) |
Disj
  inf
 | ||
| Theorem | uniioombllem2OLD 22620* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) Obsolete version of uniioombllem2 22619 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
Disj
| ||
| Theorem | uniioombllem3a 22621* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 8-May-2015.) |
Disj
    | ||
| Theorem | uniioombllem3 22622* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 26-Mar-2015.) |
|
Disj
| ||
| Theorem | uniioombllem4 22623* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 26-Mar-2015.) |
Disj
     
| ||
| Theorem | uniioombllem5 22624* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 25-Aug-2014.) |
Disj
  | ||
| Theorem | uniioombllem6 22625* | Lemma for uniioombl 22626. (Contributed by Mario Carneiro, 26-Mar-2015.) |
|
Disj
| ||
| Theorem | uniioombl 22626* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 22585.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
Disj
 | ||
| Theorem | uniiccmbl 22627* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 22585.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
|
Disj
| ||
| Theorem | dyadf 22628* |
The function returns
the endpoints of a dyadic rational covering
of the real line. (Contributed by Mario Carneiro, 26-Mar-2015.)
|
     | ||
| Theorem | dyadval 22629* |
Value of the dyadic rational function . (Contributed by Mario
Carneiro, 26-Mar-2015.)
|
|
| ||
| Theorem | dyadovol 22630* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| | ||
| Theorem | dyadss 22631* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) (Proof shortened by Mario Carneiro, 26-Apr-2016.) |
| ||
| Theorem | dyaddisjlem 22632* | Lemma for dyaddisj 22633. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ||
| Theorem | dyaddisj 22633* | Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) |
|
| ||
| Theorem | dyadmaxlem 22634* | Lemma for dyadmax 22635. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ||
| Theorem | dyadmax 22635* | Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015.) |
 
| ||
| Theorem | dyadmbllem 22636* | Lemma for dyadmbl 22637. (Contributed by Mario Carneiro, 26-Mar-2015.) |
 
 | ||
| Theorem | dyadmbl 22637* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
|
| ||
| Theorem | opnmbllem 22638* | Lemma for opnmbl 22639. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ||
| Theorem | opnmbl 22639 | All open sets are measurable. This proof, via dyadmbl 22637 and uniioombl 22626, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.) |
|
| ||
| Theorem | opnmblALT 22640 | All open sets are measurable. This alternative proof of opnmbl 22639 is significantly shorter, at the expense of invoking countable choice ax-cc 8883. (This was also the original proof before the current opnmbl 22639 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | subopnmbl 22641 | Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ↾t | ||
| Theorem | volsup2 22642* |
The volume of is the
supremum of the sequence
  of volumes of bounded sets.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
|
| ||
| Theorem | volcn 22643* | The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.) |
 | ||
| Theorem | volivth 22644* |
The Intermediate Value Theorem for the Lebesgue volume function. For
any positive
, there is a
measurable subset of
whose volume
is . (Contributed by
Mario Carneiro,
30-Aug-2014.)
|
|
| ||
| Theorem | vitalilem1 22645* | Lemma for vitali 22650. (Contributed by Mario Carneiro, 16-Jun-2014.) |
 
| ||
| Theorem | vitalilem2 22646* | Lemma for vitali 22650. (Contributed by Mario Carneiro, 16-Jun-2014.) |
 
| ||
| Theorem | vitalilem3 22647* | Lemma for vitali 22650. (Contributed by Mario Carneiro, 16-Jun-2014.) |
|
Disj | ||
| Theorem | vitalilem4 22648* | Lemma for vitali 22650. (Contributed by Mario Carneiro, 16-Jun-2014.) |
|
| ||
| Theorem | vitalilem5 22649* | Lemma for vitali 22650. (Contributed by Mario Carneiro, 16-Jun-2014.) |
|
| ||
| Theorem | vitali 22650 | If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014.) |
 | ||
| Syntax | cmbf 22651 | Extend class notation with the class of measurable functions. |
 MblFn | ||
| Syntax | citg1 22652 | Extend class notation with the Lebesgue integral for simple functions. |
 | ||
| Syntax | citg2 22653 | Extend class notation with the Lebesgue integral for nonnegative functions. |
 | ||
| Syntax | cibl 22654 | Extend class notation with the class of integrable functions. |
  | ||
| Syntax | citg 22655 | Extend class notation with the general Lebesgue integral. |
  | ||
| Definition | df-mbf 22656* | Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 22558) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
MblFn    
| ||
| Definition | df-itg1 22657* | Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.) |
 MblFn 
| ||
| Definition | df-itg2 22658* |
Define the Lebesgue integral for nonnegative functions. A nonnegative
function's integral is the supremum of the integrals of all simple
functions that are less than the input function. Note that this may be
 for
functions that take the value on a set of positive
measure or functions that are bounded below by a positive number on a
set of infinite measure. (Contributed by Mario Carneiro,
28-Jun-2014.)
|
 
| ||
| Definition | df-ibl 22659* | Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.) |
MblFn
 
  ![]_](_urbrack.gif "]_"){kind=small}
| ||
| Definition | df-itg 22660* |
Define the full Lebesgue integral, for complex-valued functions to
. The syntax
is designed to be suggestive of the standard
notation for integrals. For example, our notation for the integral of
from to is
. The only real function
of this definition is to break the integral up into nonnegative real
parts and send it off to df-itg2 22658 for further processing. Note that
this definition cannot handle integrals which evaluate to infinity,
because addition and multiplication are not currently defined on
extended reals. (You can use df-itg2 22658 directly for this use-case.)
(Contributed by Mario Carneiro, 28-Jun-2014.)
|
|
| ||
| Theorem | ismbf1 22661* |
The predicate "
is a measurable function". This is more naturally
stated for functions on the reals, see ismbf 22665 and ismbfcn 22666 for the
decomposition of the real and imaginary parts. (Contributed by Mario
Carneiro, 17-Jun-2014.)
|
MblFn 
| ||
| Theorem | mbff 22662 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| MblFn | ||
| Theorem | mbfdm 22663 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| MblFn | ||
| Theorem | mbfconstlem 22664 | Lemma for mbfconst 22670. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| | ||
| Theorem | ismbf 22665* |
The predicate "
is a measurable function". A function is
measurable iff the preimages of all open intervals are measurable sets
in the sense of ismbl 22558. (Contributed by Mario Carneiro,
17-Jun-2014.)
|
| MblFn
| ||
| Theorem | ismbfcn 22666 | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| MblFn
MblFn MblFn | ||
| Theorem | mbfima 22667 | Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| MblFn
| ||
| Theorem | mbfimaicc 22668 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| MblFn
| ||
| Theorem | mbfimasn 22669 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| MblFn
| ||
| Theorem | mbfconst 22670 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| MblFn | ||
| Theorem | mbfid 22671 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
  MblFn | ||
| Theorem | mbfmptcl 22672* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
MblFn  | ||
| Theorem | mbfdm2 22673* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
|
MblFn
| ||
| Theorem | ismbfcn2 22674* | A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 13-Aug-2014.) |
|
MblFn MblFn MblFn | ||
| Theorem | ismbfd 22675* | Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d 22689. (Contributed by Mario Carneiro, 18-Jun-2014.) |
 MblFn | ||
| Theorem | ismbf2d 22676* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
|
MblFn | ||
| Theorem | mbfeqalem 22677* | Lemma for mbfeqa 22678. (Contributed by Mario Carneiro, 2-Sep-2014.) |
|
MblFn MblFn | ||
| Theorem | mbfeqa 22678* | If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 2-Sep-2014.) |
|
MblFn MblFn | ||
| Theorem | mbfres 22679 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| MblFn MblFn | ||
| Theorem | mbfres2 22680 |
Measurability of a piecewise function: if is measurable on subsets
and of its domain, and these
pieces make up all of ,
then is
measurable on the whole domain. (Contributed by Mario
Carneiro, 18-Jun-2014.)
|
MblFn
MblFn  MblFn | ||
| Theorem | mbfss 22681* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
|
MblFn
MblFn | ||
| Theorem | mbfmulc2lem 22682 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
MblFn  MblFn | ||
| Theorem | mbfmulc2re 22683 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| MblFn MblFn | ||
| Theorem | mbfmax 22684* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| MblFn MblFn
MblFn | ||
| Theorem | mbfneg 22685* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
|
MblFn
MblFn | ||
| Theorem | mbfpos 22686* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
|
MblFn
MblFn | ||
| Theorem | mbfposr 22687* | Converse to mbfpos 22686. (Contributed by Mario Carneiro, 11-Aug-2014.) |
|
MblFn MblFn MblFn | ||
| Theorem | mbfposb 22688* | A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.) |
|
MblFn
MblFn
MblFn | ||
| Theorem | ismbf3d 22689* | Simplified form of ismbfd 22675. (Contributed by Mario Carneiro, 18-Jun-2014.) |
|
MblFn | ||
| Theorem | mbfimaopnlem 22690* | Lemma for mbfimaopn 22691. (Contributed by Mario Carneiro, 25-Aug-2014.) |
 ℂfld
MblFn | ||
| Theorem | mbfimaopn 22691 |
The preimage of any open set (in the complex topology) under a
measurable function is measurable. (See also cncombf 22693, which explains
why is too weak a condition for this theorem.)
(Contributed by Mario Carneiro, 25-Aug-2014.)
|
| ℂfld MblFn
| ||
| Theorem | mbfimaopn2 22692 | The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| ℂfld
↾t MblFn | ||
| Theorem | cncombf 22693 |
The composition of a continuous function with a measurable function is
measurable. (More generally, can be a Borel-measurable function,
but notably the condition that be only measurable is too weak, the
usual counterexample taking to be the Cantor function and
the indicator function of the -image of a nonmeasurable set, which
is a subset of the Cantor set and hence null and measurable.)
(Contributed by Mario Carneiro, 25-Aug-2014.)
|
| MblFn
MblFn | ||
| Theorem | cnmbf 22694 | A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.) |
|
MblFn | ||
| Theorem | mbfaddlem 22695 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| MblFn MblFn
MblFn | ||
| Theorem | mbfadd 22696 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| MblFn MblFn
MblFn | ||
| Theorem | mbfsub 22697 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
| MblFn MblFn
MblFn | ||
| Theorem | mbfmulc2 22698* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
|
MblFn
MblFn | ||
| Theorem | mbfsup 22699* |
The supremum of a sequence of measurable, real-valued functions is
measurable. Note that in this and related theorems, is
a function of both and , since
it is an -indexed
sequence of functions on . (Contributed by Mario Carneiro,
14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)
|
 
MblFn
MblFn | ||
| Theorem | mbfinf 22700* | The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.) |
| inf
MblFn
MblFn | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |