![]() |
Metamath
Proof Explorer Theorem List (p. 452 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sge0xrcl 45101 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 45102 | The of nonnegative extended reals is a real number if and only if it is not +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β ((Ξ£^βπΉ) β β β Β¬ (Ξ£^βπΉ) = +β)) | ||
Theorem | sge0fsum 45103* | 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.) |
β’ (π β π β Fin) & β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β (Ξ£^βπΉ) = Ξ£π₯ β π (πΉβπ₯)) | ||
Theorem | sge0rern 45104 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 45105* | 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 45107, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 45106* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = Ξ£π β π΄ π΅) | ||
Theorem | sge0sup 45107* | The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ (Ξ£^β(πΉ βΎ π₯))), β*, < )) | ||
Theorem | sge0less 45108 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 45109* | The range used in the definition of Ξ£^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β βπ§ β β βπ€ β ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦))π€ β€ π§) | ||
Theorem | sge0pr 45110* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 45111* | The arbitrary sum of nonnegative extended reals is greater than 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.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β π΄ β β*) & β’ ((π β§ π₯ β β+) β βπ§ β (π« π β© Fin)π΄ β€ ((Ξ£^β(πΉ βΎ π§)) +π π₯)) β β’ (π β π΄ β€ (Ξ£^βπΉ)) | ||
Theorem | sge0pnffigt 45112* | 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.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) = +β) & β’ (π β π β β) β β’ (π β βπ₯ β (π« π β© Fin)π < (Ξ£^β(πΉ βΎ π₯))) | ||
Theorem | sge0ssre 45113 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 45114* | 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.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β π΄ β β*) β β’ (π β ((Ξ£^βπΉ) β€ π΄ β βπ₯ β (π« π β© Fin)(Ξ£^β(πΉ βΎ π₯)) β€ π΄)) | ||
Theorem | sge0lessmpt 45115* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 45116* | 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.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β π β β+) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β βπ₯ β (π« π β© Fin)(Ξ£^βπΉ) < ((Ξ£^β(πΉ βΎ π₯)) + π)) | ||
Theorem | sge0prle 45117* | 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 45110. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 45118* | The arbitrary sum of nonnegative extended reals is greater than 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.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β β*) & β’ ((π β§ π¦ β β+) β βπ§ β (π« π΄ β© Fin)πΆ β€ ((Ξ£^β(π₯ β π§ β¦ π΅)) +π π¦)) β β’ (π β πΆ β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0resrnlem 45119 | The sum of nonnegative extended reals restricted to the range of a function is less than or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΅βΆ(0[,]+β)) & β’ (π β πΊ:π΄βΆπ΅) & β’ (π β π β π« π΄) & β’ (π β (πΊ βΎ π):πβ1-1-ontoβran πΊ) β β’ (π β (Ξ£^β(πΉ βΎ ran πΊ)) β€ (Ξ£^β(πΉ β πΊ))) | ||
Theorem | sge0resrn 45120 | The sum of nonnegative extended reals restricted to the range of a function is less than 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.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΅βΆ(0[,]+β)) & β’ (π β πΊ:π΄βΆπ΅) & β’ (π β π We π΄) β β’ (π β (Ξ£^β(πΉ βΎ ran πΊ)) β€ (Ξ£^β(πΉ β πΊ))) | ||
Theorem | sge0ssrempt 45121* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 45122 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 45125. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0le 45123* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΊ:πβΆ(0[,]+β)) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (Ξ£^βπΉ) β€ (Ξ£^βπΊ)) | ||
Theorem | sge0ltfirpmpt 45124* | 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.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β π β β+) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ (π β βπ¦ β (π« π΄ β© Fin)(Ξ£^β(π₯ β π΄ β¦ π΅)) < ((Ξ£^β(π₯ β π¦ β¦ π΅)) + π)) | ||
Theorem | sge0split 45125 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) +π (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0lempt 45126* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ πΆ))) | ||
Theorem | sge0splitmpt 45127* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β (π΄ βͺ π΅) β¦ πΆ)) = ((Ξ£^β(π₯ β π΄ β¦ πΆ)) +π (Ξ£^β(π₯ β π΅ β¦ πΆ)))) | ||
Theorem | sge0ss 45128* | Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) β β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) = (Ξ£^β(π β π΅ β¦ πΆ))) | ||
Theorem | sge0iunmptlemfi 45129* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0p1 45130* | The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β (0[,]+β)) & β’ (π = (π + 1) β π΄ = π΅) β β’ (π β (Ξ£^β(π β (π...(π + 1)) β¦ π΄)) = ((Ξ£^β(π β (π...π) β¦ π΄)) +π π΅)) | ||
Theorem | sge0iunmptlemre 45131* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) & β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) β β*) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) β β*) & β’ (π β (π β βͺ π₯ β π΄ π΅ β¦ πΆ):βͺ π₯ β π΄ π΅βΆ(0[,]+β)) & β’ (π β βͺ π₯ β π΄ π΅ β V) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0fodjrnlem 45132* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβontoβπ΄) & β’ (π β Disj π β πΆ (πΉβπ)) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π = β ) β π΅ = 0) & β’ π = (β‘πΉ β {β }) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0fodjrn 45133* | Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβontoβπ΄) & β’ (π β Disj π β πΆ (πΉβπ)) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π = β ) β π΅ = 0) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0iunmpt 45134* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0iun 45135* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ π = βͺ π₯ β π΄ π΅ & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (Ξ£^βπΉ) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(πΉ βΎ π΅))))) | ||
Theorem | sge0nemnf 45136 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β -β) | ||
Theorem | sge0rpcpnf 45137* | The sum of an infinite number of a positive constant, is +β (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β Fin) & β’ (π β π΅ β β+) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0rernmpt 45138* | If the sum of nonnegative extended reals is not +β then no term is +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) | ||
Theorem | sge0lefimpt 45139* | 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.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β β*) β β’ (π β ((Ξ£^β(π₯ β π΄ β¦ π΅)) β€ πΆ β βπ¦ β (π« π΄ β© Fin)(Ξ£^β(π₯ β π¦ β¦ π΅)) β€ πΆ)) | ||
Theorem | nn0ssge0 45140 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β0 β (0[,)+β) | ||
Theorem | sge0clmpt 45141* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β (0[,]+β)) | ||
Theorem | sge0ltfirpmpt2 45142* | 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.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β π β β+) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ (π β βπ¦ β (π« π΄ β© Fin)(Ξ£^β(π₯ β π΄ β¦ π΅)) < (Ξ£π₯ β π¦ π΅ + π)) | ||
Theorem | sge0isum 45143 | 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.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆ(0[,)+β)) & β’ πΊ = seqπ( + , πΉ) & β’ (π β πΊ β π΅) β β’ (π β (Ξ£^βπΉ) = π΅) | ||
Theorem | sge0xrclmpt 45144* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β*) | ||
Theorem | sge0xp 45145* | Combine two generalized sums of nonnegative extended reals into a single generalized sum over the cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π§ = β¨π, πβ© β π· = πΆ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ ((π β§ π β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) = (Ξ£^β(π§ β (π΄ Γ π΅) β¦ π·))) | ||
Theorem | sge0isummpt 45146* | 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.) |
β’ β²ππ & β’ ((π β§ π β π) β π΄ β (0[,)+β)) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β seqπ( + , (π β π β¦ π΄)) β π΅) β β’ (π β (Ξ£^β(π β π β¦ π΄)) = π΅) | ||
Theorem | sge0ad2en 45147* | The value of the infinite geometric series 2β-1 + 2β-2 +... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β (0[,)+β)) β β’ (π β (Ξ£^β(π β β β¦ (π΄ / (2βπ)))) = π΄) | ||
Theorem | sge0isummpt2 45148* | 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.) |
β’ β²ππ & β’ ((π β§ π β π) β π΄ β (0[,)+β)) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β seqπ( + , (π β π β¦ π΄)) β π΅) β β’ (π β (Ξ£^β(π β π β¦ π΄)) = Ξ£π β π π΄) | ||
Theorem | sge0xaddlem1 45149* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β πΈ β β+) & β’ (π β π β π΄) & β’ (π β π β Fin) & β’ (π β π β π΄) & β’ (π β π β Fin) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) < (Ξ£π β π π΅ + (πΈ / 2))) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) < (Ξ£π β π πΆ + (πΈ / 2))) & β’ (π β sup(ran (π₯ β (π« π΄ β© Fin) β¦ Ξ£π β π₯ (π΅ + πΆ)), β*, < ) β (0[,]+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β ((Ξ£^β(π β π΄ β¦ π΅)) + (Ξ£^β(π β π΄ β¦ πΆ))) β€ (sup(ran (π₯ β (π« π΄ β© Fin) β¦ Ξ£π β π₯ (π΅ + πΆ)), β*, < ) +π πΈ)) | ||
Theorem | sge0xaddlem2 45150* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0xadd 45151* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0fsummptf 45152* | 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.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = Ξ£π β π΄ π΅) | ||
Theorem | sge0snmptf 45153* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0mpt 45154* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β 0 β€ (Ξ£^β(π β π΄ β¦ π΅))) | ||
Theorem | sge0repnfmpt 45155* | The of nonnegative extended reals is a real number if and only if it is not +β. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β ((Ξ£^β(π β π΄ β¦ π΅)) β β β Β¬ (Ξ£^β(π β π΄ β¦ π΅)) = +β)) | ||
Theorem | sge0pnffigtmpt 45156* | 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.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = +β) & β’ (π β π β β) β β’ (π β βπ₯ β (π« π΄ β© Fin)π < (Ξ£^β(π β π₯ β¦ π΅))) | ||
Theorem | sge0splitsn 45157* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β (0[,]+β)) β β’ (π β (Ξ£^β(π β (π΄ βͺ {π΅}) β¦ πΆ)) = ((Ξ£^β(π β π΄ β¦ πΆ)) +π π·)) | ||
Theorem | sge0pnffsumgt 45158* | 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.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = +β) & β’ (π β π β β) β β’ (π β βπ₯ β (π« π΄ β© Fin)π < Ξ£π β π₯ π΅) | ||
Theorem | sge0gtfsumgt 45159* | 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.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ (π β πΆ β β) & β’ (π β πΆ < (Ξ£^β(π β π΄ β¦ π΅))) β β’ (π β βπ¦ β (π« π΄ β© Fin)πΆ < Ξ£π β π¦ π΅) | ||
Theorem | sge0uzfsumgt 45160* | 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.) |
β’ β²ππ & β’ (π β πΎ β β€) & β’ π = (β€β₯βπΎ) & β’ ((π β§ π β π) β π΅ β (0[,)+β)) & β’ (π β πΆ β β) & β’ (π β πΆ < (Ξ£^β(π β π β¦ π΅))) β β’ (π β βπ β π πΆ < Ξ£π β (πΎ...π)π΅) | ||
Theorem | sge0pnfmpt 45161* | 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.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ (π β βπ β π΄ π΅ = +β) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0seq 45162 | A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆ(0[,)+β)) & β’ πΊ = seqπ( + , πΉ) β β’ (π β (Ξ£^βπΉ) = sup(ran πΊ, β*, < )) | ||
Theorem | sge0reuz 45163* | Value of the generalized sum of nonnegative reals, when the domain is a set of upper integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β (0[,)+β)) β β’ (π β (Ξ£^β(π β π β¦ π΅)) = sup(ran (π β π β¦ Ξ£π β (π...π)π΅), β*, < )) | ||
Theorem | sge0reuzb 45164* | 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.) |
β’ β²ππ & β’ β²π₯π & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΅ β (0[,)+β)) & β’ (π β βπ₯ β β βπ β π Ξ£π β (π...π)π΅ β€ π₯) β β’ (π β (Ξ£^β(π β π β¦ π΅)) = sup(ran (π β π β¦ Ξ£π β (π...π)π΅), β, < )) | ||
Proofs for most of the theorems in section 112 of [Fremlin1] | ||
Syntax | cmea 45165 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 45166* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ Meas = {π₯ β£ (((π₯:dom π₯βΆ(0[,]+β) β§ dom π₯ β SAlg) β§ (π₯ββ ) = 0) β§ βπ¦ β π« dom π₯((π¦ βΌ Ο β§ Disj π€ β π¦ π€) β (π₯ββͺ π¦) = (Ξ£^β(π₯ βΎ π¦))))} | ||
Theorem | ismea 45167* | Express the predicate "π is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β Meas β (((π:dom πβΆ(0[,]+β) β§ dom π β SAlg) β§ (πββ ) = 0) β§ βπ₯ β π« dom π((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (πββͺ π₯) = (Ξ£^β(π βΎ π₯))))) | ||
Theorem | dmmeasal 45168 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π β SAlg) | ||
Theorem | meaf 45169 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π:πβΆ(0[,]+β)) | ||
Theorem | mea0 45170 | The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) β β’ (π β (πββ ) = 0) | ||
Theorem | nnfoctbdjlem 45171* | 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.) |
β’ (π β π΄ β β) & β’ (π β πΊ:π΄β1-1-ontoβπ) & β’ (π β Disj π¦ β π π¦) & β’ πΉ = (π β β β¦ if((π = 1 β¨ Β¬ (π β 1) β π΄), β , (πΊβ(π β 1)))) β β’ (π β βπ(π:ββontoβ(π βͺ {β }) β§ Disj π β β (πβπ))) | ||
Theorem | nnfoctbdj 45172* | 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 π¦ β π π¦) β β’ (π β βπ(π:ββontoβ(π βͺ {β }) β§ Disj π β β (πβπ))) | ||
Theorem | meadjuni 45173* | 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) & β’ π = dom π & β’ (π β π β π) & β’ (π β π βΌ Ο) & β’ (π β Disj π₯ β π π₯) β β’ (π β (πββͺ π) = (Ξ£^β(π βΎ π))) | ||
Theorem | meacl 45174 | The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β (0[,]+β)) | ||
Theorem | iundjiunlem 45175* | The sets in the sequence πΉ are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (β€β₯βπ) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) & β’ (π β π½ β π) & β’ (π β πΎ β π) & β’ (π β π½ < πΎ) β β’ (π β ((πΉβπ½) β© (πΉβπΎ)) = β ) | ||
Theorem | iundjiun 45176* | 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 45177 | The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β β*) | ||
Theorem | meadjun 45178 | 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) & β’ π = dom π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) β β’ (π β (πβ(π΄ βͺ π΅)) = ((πβπ΄) +π (πβπ΅))) | ||
Theorem | meassle 45179 | The measure of a set is greater than or equal to the measure of a subset, Property 112C (b) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) β β’ (π β (πβπ΄) β€ (πβπ΅)) | ||
Theorem | meaunle 45180 | The measure of the union of two sets is less than or equal to the sum of the measures, Property 112C (c) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (πβ(π΄ βͺ π΅)) β€ ((πβπ΄) +π (πβπ΅))) | ||
Theorem | meadjiunlem 45181* | The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π β π) & β’ (π β πΊ:πβΆπ) & β’ π = {π β π β£ (πΊβπ) β β } & β’ (π β Disj π β π (πΊβπ)) β β’ (π β (Ξ£^β(π βΎ ran πΊ)) = (Ξ£^β(π β πΊ))) | ||
Theorem | meadjiun 45182* | 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) & β’ π = dom π & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β π΄ βΌ Ο) & β’ (π β Disj π β π΄ π΅) β β’ (π β (πββͺ π β π΄ π΅) = (Ξ£^β(π β π΄ β¦ (πβπ΅)))) | ||
Theorem | ismeannd 45183* | Sufficient condition to prove that π is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β SAlg) & β’ (π β π:πβΆ(0[,]+β)) & β’ (π β (πββ ) = 0) & β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β (πββͺ π β β (πβπ)) = (Ξ£^β(π β β β¦ (πβ(πβπ))))) β β’ (π β π β Meas) | ||
Theorem | meaiunlelem 45184* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π β Meas) & β’ π = dom π & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) β β’ (π β (πββͺ π β π (πΈβπ)) β€ (Ξ£^β(π β π β¦ (πβ(πΈβπ))))) | ||
Theorem | meaiunle 45185* | The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π β Meas) & β’ π = dom π & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆπ) β β’ (π β (πββͺ π β π (πΈβπ)) β€ (Ξ£^β(π β π β¦ (πβ(πΈβπ))))) | ||
Theorem | psmeasurelem 45186* | π 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.) |
β’ (π β π β π) & β’ (π β π»:πβΆ(0[,]+β)) & β’ π = (π₯ β π« π β¦ (Ξ£^β(π» βΎ π₯))) & β’ (π β π:π« πβΆ(0[,]+β)) & β’ (π β π β π« π) & β’ (π β Disj π¦ β π π¦) β β’ (π β (πββͺ π) = (Ξ£^β(π βΎ π))) | ||
Theorem | psmeasure 45187* | Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β π»:πβΆ(0[,]+β)) & β’ π = (π₯ β π« π β¦ (Ξ£^β(π» βΎ π₯))) β β’ (π β π β Meas) | ||
Theorem | voliunsge0lem 45188* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πΈβπ))) & β’ (π β πΈ:ββΆdom vol) & β’ (π β Disj π β β (πΈβπ)) β β’ (π β (volββͺ π β β (πΈβπ)) = (Ξ£^β(π β β β¦ (volβ(πΈβπ))))) | ||
Theorem | voliunsge0 45189* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΈ:ββΆdom vol) & β’ (π β Disj π β β (πΈβπ)) β β’ (π β (volββͺ π β β (πΈβπ)) = (Ξ£^β(π β β β¦ (volβ(πΈβπ))))) | ||
Theorem | volmea 45190 | The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β vol β Meas) | ||
Theorem | meage0 45191 | If the measure of a measurable set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Meas) & β’ (π β π΄ β dom π) β β’ (π β 0 β€ (πβπ΄)) | ||
Theorem | meadjunre 45192 | 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) & β’ π = dom π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β (πβπ΄) β β) & β’ (π β (πβπ΅) β β) β β’ (π β (πβ(π΄ βͺ π΅)) = ((πβπ΄) + (πβπ΅))) | ||
Theorem | meassre 45193 | 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) & β’ (π β π΄ β dom π) & β’ (π β (πβπ΄) β β) & β’ (π β π΅ β π΄) & β’ (π β π΅ β dom π) β β’ (π β (πβπ΅) β β) | ||
Theorem | meale0eq0 45194 | A measure that is less than or equal to 0 is 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Meas) & β’ (π β π΄ β dom π) & β’ (π β (πβπ΄) β€ 0) β β’ (π β (πβπ΄) = 0) | ||
Theorem | meadif 45195 | The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Meas) & β’ (π β π΄ β dom π) & β’ (π β (πβπ΄) β β) & β’ (π β π΅ β dom π) & β’ (π β π΅ β π΄) β β’ (π β (πβ(π΄ β π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | meaiuninclem 45196* | 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) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβπ) β (πΈβ(π + 1))) & β’ (π β βπ₯ β β βπ β π (πβ(πΈβπ)) β€ π₯) & β’ π = (π β π β¦ (πβ(πΈβπ))) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) β β’ (π β π β (πββͺ π β π (πΈβπ))) | ||
Theorem | meaiuninc 45197* | Measures are continuous from below (bounded case): if πΈ is a sequence of nondecreasing 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) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβπ) β (πΈβ(π + 1))) & β’ (π β βπ₯ β β βπ β π (πβ(πΈβπ)) β€ π₯) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π β (πββͺ π β π (πΈβπ))) | ||
Theorem | meaiuninc2 45198* | Measures are continuous from below (bounded case): if πΈ is a sequence of nondecreasing 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) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβπ) β (πΈβ(π + 1))) & β’ (π β π΅ β β) & β’ ((π β§ π β π) β (πβ(πΈβπ)) β€ π΅) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π β (πββͺ π β π (πΈβπ))) | ||
Theorem | meaiunincf 45199* | Measures are continuous from below (bounded case): if πΈ is a sequence of nondecreasing 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, 13-Feb-2022.) |
β’ β²ππ & β’ β²ππΈ & β’ (π β π β Meas) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβπ) β (πΈβ(π + 1))) & β’ (π β βπ₯ β β βπ β π (πβ(πΈβπ)) β€ π₯) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π β (πββͺ π β π (πΈβπ))) | ||
Theorem | meaiuninc3v 45200* | Measures are continuous from below: if πΈ is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 45197 and meaiuninc2 45198 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ (π β π β Meas) & β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β πΈ:πβΆdom π) & β’ ((π β§ π β π) β (πΈβπ) β (πΈβ(π + 1))) & β’ π = (π β π β¦ (πβ(πΈβπ))) β β’ (π β π~~>*(πββͺ π β π (πΈβπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |