![]() |
Metamath
Proof Explorer Theorem List (p. 459 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | unisalgen2 45801 | The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β π) & β’ π = (SalGenβπ΄) β β’ (π β βͺ π = βͺ π΄) | ||
Theorem | bor1sal 45802 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ π΅ β SAlg | ||
Theorem | iocborel 45803 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β (π΄(,]πΆ) β π΅) | ||
Theorem | subsaliuncllem 45804* | A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²π¦π & β’ (π β π β π) & β’ πΊ = (π β β β¦ {π₯ β π β£ (πΉβπ) = (π₯ β© π·)}) & β’ πΈ = (π» β πΊ) & β’ (π β π» Fn ran πΊ) & β’ (π β βπ¦ β ran πΊ(π»βπ¦) β π¦) β β’ (π β βπ β (π βm β)βπ β β (πΉβπ) = ((πβπ) β© π·)) | ||
Theorem | subsaliuncl 45805* | A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π· β π) & β’ π = (π βΎt π·) & β’ (π β πΉ:ββΆπ) β β’ (π β βͺ π β β (πΉβπ) β π) | ||
Theorem | subsalsal 45806 | A subspace sigma-algebra is a sigma algebra. This is Lemma 121A of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π· β π) & β’ π = (π βΎt π·) β β’ (π β π β SAlg) | ||
Theorem | subsaluni 45807 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) β β’ (π β π΄ β (π βΎt π΄)) | ||
Theorem | salrestss 45808 | A sigma-algebra restricted to one of its elements is a subset of the original sigma-algebra. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) β β’ (π β (π βΎt πΈ) β π) | ||
Syntax | csumge0 45809 | Extend class notation to include the sum of nonnegative extended reals. |
class Ξ£^ | ||
Definition | df-sumge0 45810* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
β’ Ξ£^ = (π₯ β V β¦ if(+β β ran π₯, +β, sup(ran (π¦ β (π« dom π₯ β© Fin) β¦ Ξ£π€ β π¦ (π₯βπ€)), β*, < ))) | ||
Theorem | sge0rnre 45811* | When Ξ£^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)) β β) | ||
Theorem | fge0icoicc 45812 | If πΉ maps to nonnegative reals, then πΉ maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β πΉ:πβΆ(0[,]+β)) | ||
Theorem | sge0val 45813* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β π β§ πΉ:πβΆ(0[,]+β)) β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π¦ β (π« π β© Fin) β¦ Ξ£π€ β π¦ (πΉβπ€)), β*, < ))) | ||
Theorem | fge0npnf 45814 | If πΉ maps to nonnegative reals, then +β is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0rnn0 45815* | The range used in the definition of Ξ£^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)) β β | ||
Theorem | sge0vald 45816* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β*, < ))) | ||
Theorem | fge0iccico 45817 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆ(0[,)+β)) | ||
Theorem | gsumge0cl 45818 | Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΉ finSupp 0) β β’ (π β (πΊ Ξ£g πΉ) β (0[,]+β)) | ||
Theorem | sge0reval 45819* | Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β*, < )) | ||
Theorem | sge0pnfval 45820 | If a term in the sum of nonnegative extended reals is +β, then the value of the sum is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β +β β ran πΉ) β β’ (π β (Ξ£^βπΉ) = +β) | ||
Theorem | fge0iccre 45821 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆβ) | ||
Theorem | sge0z 45822* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) β β’ (π β (Ξ£^β(π β π΄ β¦ 0)) = 0) | ||
Theorem | sge00 45823 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (Ξ£^ββ ) = 0 | ||
Theorem | fsumlesge0 45824* | Every finite subsum of nonnegative reals is less than or equal to the extended sum over the whole (possibly infinite) domain. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,)+β)) & β’ (π β π β π) & β’ (π β π β Fin) β β’ (π β Ξ£π₯ β π (πΉβπ₯) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0revalmpt 45825* | Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = sup(ran (π¦ β (π« π΄ β© Fin) β¦ Ξ£π₯ β π¦ π΅), β*, < )) | ||
Theorem | sge0sn 45826 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:{π΄}βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = (πΉβπ΄)) | ||
Theorem | sge0tsms 45827 | Ξ£^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β (πΊ tsums πΉ)) | ||
Theorem | sge0cl 45828 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β (0[,]+β)) | ||
Theorem | sge0f1o 45829* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0snmpt 45830* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0 45831 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β 0 β€ (Ξ£^βπΉ)) | ||
Theorem | sge0xrcl 45832 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 45833 | 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 45834* | 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 45835 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 45836* | 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 45838, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 45837* | 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 45838* | 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 45839 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 45840* | 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 45841* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 45842* | 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 45843* | 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 45844 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 45845* | 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 45846* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 45847* | 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 45848* | 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 45841. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 45849* | 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 45850 | 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 45851 | 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 45852* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 45853 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 45856. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0le 45854* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΊ:πβΆ(0[,]+β)) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (Ξ£^βπΉ) β€ (Ξ£^βπΊ)) | ||
Theorem | sge0ltfirpmpt 45855* | 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 45856 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) +π (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0lempt 45857* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ πΆ))) | ||
Theorem | sge0splitmpt 45858* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β (π΄ βͺ π΅) β¦ πΆ)) = ((Ξ£^β(π₯ β π΄ β¦ πΆ)) +π (Ξ£^β(π₯ β π΅ β¦ πΆ)))) | ||
Theorem | sge0ss 45859* | 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 45860* | 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 45861* | 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 45862* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) & β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) β β*) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) β β*) & β’ (π β (π β βͺ π₯ β π΄ π΅ β¦ πΆ):βͺ π₯ β π΄ π΅βΆ(0[,]+β)) & β’ (π β βͺ π₯ β π΄ π΅ β V) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0fodjrnlem 45863* | 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 45864* | 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 45865* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0iun 45866* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ π = βͺ π₯ β π΄ π΅ & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (Ξ£^βπΉ) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(πΉ βΎ π΅))))) | ||
Theorem | sge0nemnf 45867 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β -β) | ||
Theorem | sge0rpcpnf 45868* | The sum of an infinite number of a positive constant, is +β (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β Fin) & β’ (π β π΅ β β+) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0rernmpt 45869* | If the sum of nonnegative extended reals is not +β then no term is +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) | ||
Theorem | sge0lefimpt 45870* | 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 45871 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β0 β (0[,)+β) | ||
Theorem | sge0clmpt 45872* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β (0[,]+β)) | ||
Theorem | sge0ltfirpmpt2 45873* | 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 45874 | 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 45875* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β*) | ||
Theorem | sge0xp 45876* | 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 45877* | 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 45878* | 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 45879* | 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 45880* | 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 45881* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0xadd 45882* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0fsummptf 45883* | 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 45884* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0mpt 45885* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β 0 β€ (Ξ£^β(π β π΄ β¦ π΅))) | ||
Theorem | sge0repnfmpt 45886* | 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 45887* | 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 45888* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β (0[,]+β)) β β’ (π β (Ξ£^β(π β (π΄ βͺ {π΅}) β¦ πΆ)) = ((Ξ£^β(π β π΄ β¦ πΆ)) +π π·)) | ||
Theorem | sge0pnffsumgt 45889* | 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 45890* | 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 45891* | 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 45892* | 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 45893 | 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 45894* | 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 45895* | 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 45896 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 45897* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ Meas = {π₯ β£ (((π₯:dom π₯βΆ(0[,]+β) β§ dom π₯ β SAlg) β§ (π₯ββ ) = 0) β§ βπ¦ β π« dom π₯((π¦ βΌ Ο β§ Disj π€ β π¦ π€) β (π₯ββͺ π¦) = (Ξ£^β(π₯ βΎ π¦))))} | ||
Theorem | ismea 45898* | 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 45899 | The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π β SAlg) | ||
Theorem | meaf 45900 | A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β Meas) & β’ π = dom π β β’ (π β π:πβΆ(0[,]+β)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |