![]() |
Metamath
Proof Explorer Theorem List (p. 455 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sge0xrcl 45401 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 45402 | 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 45403* | 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 45404 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 45405* | 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 45407, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 45406* | 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 45407* | 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 45408 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 45409* | 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 45410* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 45411* | 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 45412* | 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 45413 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 45414* | 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 45415* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 45416* | 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 45417* | 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 45410. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 45418* | 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 45419 | 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 45420 | 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 45421* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 45422 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 45425. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0le 45423* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΊ:πβΆ(0[,]+β)) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (Ξ£^βπΉ) β€ (Ξ£^βπΊ)) | ||
Theorem | sge0ltfirpmpt 45424* | 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 45425 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) +π (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0lempt 45426* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ πΆ))) | ||
Theorem | sge0splitmpt 45427* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β (π΄ βͺ π΅) β¦ πΆ)) = ((Ξ£^β(π₯ β π΄ β¦ πΆ)) +π (Ξ£^β(π₯ β π΅ β¦ πΆ)))) | ||
Theorem | sge0ss 45428* | 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 45429* | 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 45430* | 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 45431* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) & β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) β β*) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) β β*) & β’ (π β (π β βͺ π₯ β π΄ π΅ β¦ πΆ):βͺ π₯ β π΄ π΅βΆ(0[,]+β)) & β’ (π β βͺ π₯ β π΄ π΅ β V) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0fodjrnlem 45432* | 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 45433* | 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 45434* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0iun 45435* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ π = βͺ π₯ β π΄ π΅ & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (Ξ£^βπΉ) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(πΉ βΎ π΅))))) | ||
Theorem | sge0nemnf 45436 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β -β) | ||
Theorem | sge0rpcpnf 45437* | The sum of an infinite number of a positive constant, is +β (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β Fin) & β’ (π β π΅ β β+) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0rernmpt 45438* | If the sum of nonnegative extended reals is not +β then no term is +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) | ||
Theorem | sge0lefimpt 45439* | 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 45440 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β0 β (0[,)+β) | ||
Theorem | sge0clmpt 45441* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β (0[,]+β)) | ||
Theorem | sge0ltfirpmpt2 45442* | 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 45443 | 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 45444* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β*) | ||
Theorem | sge0xp 45445* | 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 45446* | 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 45447* | 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 45448* | 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 45449* | 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 45450* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0xadd 45451* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0fsummptf 45452* | 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 45453* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0mpt 45454* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β 0 β€ (Ξ£^β(π β π΄ β¦ π΅))) | ||
Theorem | sge0repnfmpt 45455* | 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 45456* | 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 45457* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β (0[,]+β)) β β’ (π β (Ξ£^β(π β (π΄ βͺ {π΅}) β¦ πΆ)) = ((Ξ£^β(π β π΄ β¦ πΆ)) +π π·)) | ||
Theorem | sge0pnffsumgt 45458* | 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 45459* | 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 45460* | 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 45461* | 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 45462 | 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 45463* | 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 45464* | 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 45465 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 45466* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ Meas = {π₯ β£ (((π₯:dom π₯βΆ(0[,]+β) β§ dom π₯ β SAlg) β§ (π₯ββ ) = 0) β§ βπ¦ β π« dom π₯((π¦ βΌ Ο β§ Disj π€ β π¦ π€) β (π₯ββͺ π¦) = (Ξ£^β(π₯ βΎ π¦))))} | ||
Theorem | ismea 45467* | 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 45468 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π β SAlg) | ||
Theorem | meaf 45469 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π:πβΆ(0[,]+β)) | ||
Theorem | mea0 45470 | The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) β β’ (π β (πββ ) = 0) | ||
Theorem | nnfoctbdjlem 45471* | 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 45472* | 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 45473* | 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 45474 | The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β (0[,]+β)) | ||
Theorem | iundjiunlem 45475* | The sets in the sequence πΉ are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (β€β₯βπ) & β’ πΉ = (π β π β¦ ((πΈβπ) β βͺ π β (π..^π)(πΈβπ))) & β’ (π β π½ β π) & β’ (π β πΎ β π) & β’ (π β π½ < πΎ) β β’ (π β ((πΉβπ½) β© (πΉβπΎ)) = β ) | ||
Theorem | iundjiun 45476* | 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 45477 | The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π & β’ (π β π΄ β π) β β’ (π β (πβπ΄) β β*) | ||
Theorem | meadjun 45478 | 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 45479 | 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 45480 | 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 45481* | 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 45482* | 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 45483* | Sufficient condition to prove that π is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β SAlg) & β’ (π β π:πβΆ(0[,]+β)) & β’ (π β (πββ ) = 0) & β’ ((π β§ π:ββΆπ β§ Disj π β β (πβπ)) β (πββͺ π β β (πβπ)) = (Ξ£^β(π β β β¦ (πβ(πβπ))))) β β’ (π β π β Meas) | ||
Theorem | meaiunlelem 45484* | 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 45485* | 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 45486* | π 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 45487* | Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β π»:πβΆ(0[,]+β)) & β’ π = (π₯ β π« π β¦ (Ξ£^β(π» βΎ π₯))) β β’ (π β π β Meas) | ||
Theorem | voliunsge0lem 45488* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ π = seq1( + , πΊ) & β’ πΊ = (π β β β¦ (volβ(πΈβπ))) & β’ (π β πΈ:ββΆdom vol) & β’ (π β Disj π β β (πΈβπ)) β β’ (π β (volββͺ π β β (πΈβπ)) = (Ξ£^β(π β β β¦ (volβ(πΈβπ))))) | ||
Theorem | voliunsge0 45489* | The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β πΈ:ββΆdom vol) & β’ (π β Disj π β β (πΈβπ)) β β’ (π β (volββͺ π β β (πΈβπ)) = (Ξ£^β(π β β β¦ (volβ(πΈβπ))))) | ||
Theorem | volmea 45490 | The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β vol β Meas) | ||
Theorem | meage0 45491 | 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 45492 | 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 45493 | 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 45494 | 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 45495 | The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Meas) & β’ (π β π΄ β dom π) & β’ (π β (πβπ΄) β β) & β’ (π β π΅ β dom π) & β’ (π β π΅ β π΄) β β’ (π β (πβ(π΄ β π΅)) = ((πβπ΄) β (πβπ΅))) | ||
Theorem | meaiuninclem 45496* | 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 45497* | 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 45498* | 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 45499* | 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 45500* | 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 45497 and meaiuninc2 45498 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 > |