Home | Metamath
Proof Explorer Theorem List (p. 407 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sge0ge0 40601 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0xrcl 40602 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0repnf 40603 | The of nonnegative extended reals is a real number if and only if it is not . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0fsum 40604* | The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0rern 40605 | If the sum of nonnegative extended reals is not then no terms is . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0supre 40606* | If the arbitrary sum of nonnegative extended reals is real, then it is the supremum (in the real numbers) of finite subsums. Similar to sge0sup 40608, but here we can use with respect to instead of (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0fsummpt 40607* | The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0sup 40608* | The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0less 40609 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0rnbnd 40610* | The range used in the definition of Σ^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0pr 40611* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0gerp 40612* | The arbitrary sum of nonnegative extended reals is larger or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0pnffigt 40613* | If the sum of nonnegative extended reals is , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0ssre 40614 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0lefi 40615* | A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0lessmpt 40616* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0ltfirp 40617* | If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0prle 40618* | The sum of a pair of nonnegative extended reals is less than or equal their extended addition. When it is a distinct pair, than equality holds, see sge0pr 40611. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0gerpmpt 40619* | The arbitrary sum of nonnegative extended reals is larger or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0resrnlem 40620 | The sum of nonnegative extended reals restricted to the range of a function is less or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0resrn 40621 | The sum of nonnegative extended reals restricted to the range of a function is less or equal to the sum of the composition of the two functions (well order hypothesis allows to avoid using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0ssrempt 40622* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0resplit 40623 | Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 40626. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ Σ^ Σ^ | ||
Theorem | sge0le 40624* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0ltfirpmpt 40625* | If the extended sum of nonnegative reals is not , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0split 40626 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0lempt 40627* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0splitmpt 40628* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0ss 40629* | Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0iunmptlemfi 40630* | Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ Σ^ Σ^ | ||
Theorem | sge0p1 40631* | The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0iunmptlemre 40632* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ Σ^ Σ^ Σ^ Σ^ Σ^ | ||
Theorem | sge0fodjrnlem 40633* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ | ||
Theorem | sge0fodjrn 40634* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ | ||
Theorem | sge0iunmpt 40635* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ Σ^ | ||
Theorem | sge0iun 40636* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Σ^ Σ^ Σ^ | ||
Theorem | sge0nemnf 40637 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0rpcpnf 40638* | The sum of an infinite number of a positive constant, is (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0rernmpt 40639* | If the sum of nonnegative extended reals is not then no term is . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0lefimpt 40640* | A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ Σ^ | ||
Theorem | nn0ssge0 40641 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Theorem | sge0clmpt 40642* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0ltfirpmpt2 40643* | If the extended sum of nonnegative reals is not , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Σ^ | ||
Theorem | sge0isum 40644 | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0xrclmpt 40645* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0xp 40646* | Combine two generalized sums of nonnegative extended reals into a single generalized sum over the cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0isummpt 40647* | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0ad2en 40648* | The value of the infinite geometric series ... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0isummpt2 40649* | If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ | ||
Theorem | sge0xaddlem1 40650* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ Σ^ Σ^ Σ^ Σ^ Σ^ | ||
Theorem | sge0xaddlem2 40651* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ Σ^ Σ^ Σ^ Σ^ | ||
Theorem | sge0xadd 40652* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Σ^ Σ^ Σ^ | ||
Theorem | sge0fsummptf 40653* | The generalized sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ | ||
Theorem | sge0snmptf 40654* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ | ||
Theorem | sge0ge0mpt 40655* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ | ||
Theorem | sge0repnfmpt 40656* | The of nonnegative extended reals is a real number if and only if it is not . (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ | ||
Theorem | sge0pnffigtmpt 40657* | If the generalized sum of nonnegative reals is , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ | ||
Theorem | sge0splitsn 40658* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ Σ^ | ||
Theorem | sge0pnffsumgt 40659* | If the sum of nonnegative extended reals is , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ | ||
Theorem | sge0gtfsumgt 40660* | If the generalized sum of nonnegative reals is larger than a given number, then that number can be dominated by a finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ | ||
Theorem | sge0uzfsumgt 40661* | If a real number is smaller than a generalized sum of nonnegative reals, then it is smaller than some finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
Σ^ | ||
Theorem | sge0pnfmpt 40662* | If a term in the sum of nonnegative extended reals is , then the value of the sum is (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ | ||
Theorem | sge0seq 40663 | A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Σ^ | ||
Theorem | sge0reuz 40664* | Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Σ^ | ||
Theorem | sge0reuzb 40665* | Value of the generalized sum of uniformly bounded nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Σ^ | ||
Proofs for most of the theorems in section 112 of [Fremlin1] | ||
Syntax | cmea 40666 | Extend class notation with the class of measures. |
Meas | ||
Definition | df-mea 40667* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas SAlg Disj Σ^ | ||
Theorem | ismea 40668* | Express the predicate " is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas SAlg Disj Σ^ | ||
Theorem | dmmeasal 40669 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas SAlg | ||
Theorem | meaf 40670 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | mea0 40671 | The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | nnfoctbdjlem 40672* | There exists a mapping from onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Disj | ||
Theorem | nnfoctbdj 40673* | There exists a mapping from onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Disj Disj | ||
Theorem | meadjuni 40674* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas Disj Σ^ | ||
Theorem | meacl 40675 | The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | iundjiunlem 40676* | The sets in the sequence are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
..^ | ||
Theorem | iundjiun 40677* | Given a sequence of sets, a sequence of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
..^ Disj | ||
Theorem | meaxrcl 40678 | The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | meadjun 40679 | The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | meassle 40680 | The measure of a set is larger or equal to the measure of a subset, Property 112C (b) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | meaunle 40681 | The measure of the union of two sets is less or equal to the sum of the measures, Property 112C (c) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas | ||
Theorem | meadjiunlem 40682* | The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas Disj Σ^ Σ^ | ||
Theorem | meadjiun 40683* | The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas Disj Σ^ | ||
Theorem | ismeannd 40684* | Sufficient condition to prove that is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
SAlg Disj Σ^ Meas | ||
Theorem | meaiunlelem 40685* | The measure of the union of countable sets is less or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas ..^ Σ^ | ||
Theorem | meaiunle 40686* | The measure of the union of countable sets is less or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Meas Σ^ | ||
Theorem | psmeasurelem 40687* | applied to a disjoint union of subsets of its domain is the sum of applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Disj Σ^ | ||
Theorem | psmeasure 40688* | Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Σ^ Meas | ||
Theorem | voliunsge0lem 40689* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Disj Σ^ | ||
Theorem | voliunsge0 40690* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Disj Σ^ | ||
Theorem | volmea 40691 | The Lebeasgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Meas | ||
Theorem | meage0 40692 | If the measure of a measurable set is greater than or equal to . (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meadjunre 40693 | The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meassre 40694 | If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meale0eq0 40695 | A measure that is smaller or equal to is . (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meadif 40696 | The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meaiuninclem 40697* | Measures are continuous from below (bounded case): if is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas ..^ | ||
Theorem | meaiuninc 40698* | Measures are continuous from below (bounded case): if is a sequence of non-decreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meaiuninc2 40699* | Measures are continuous from below (bounded case): if is a sequence of non-decreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas | ||
Theorem | meaiininclem 40700* | Measures are continuous from above: if is a non-increasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
Meas |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |