Home | Metamath
Proof Explorer Theorem List (p. 444 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | salincld 44301 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ β© πΉ) β π) | ||
Theorem | salunid 44302 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) β β’ (π β βͺ π β π) | ||
Theorem | unisalgen2 44303 | 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 44304 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ π΅ β SAlg | ||
Theorem | iocborel 44305 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β (π΄(,]πΆ) β π΅) | ||
Theorem | subsaliuncllem 44306* | 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 44307* | 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 44308 | 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 44309 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) β β’ (π β π΄ β (π βΎt π΄)) | ||
Theorem | salrestss 44310 | 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 44311 | Extend class notation to include the sum of nonnegative extended reals. |
class Ξ£^ | ||
Definition | df-sumge0 44312* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
β’ Ξ£^ = (π₯ β V β¦ if(+β β ran π₯, +β, sup(ran (π¦ β (π« dom π₯ β© Fin) β¦ Ξ£π€ β π¦ (π₯βπ€)), β*, < ))) | ||
Theorem | sge0rnre 44313* | 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 44314 | If πΉ maps to nonnegative reals, then πΉ maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β πΉ:πβΆ(0[,]+β)) | ||
Theorem | sge0val 44315* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β π β§ πΉ:πβΆ(0[,]+β)) β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π¦ β (π« π β© Fin) β¦ Ξ£π€ β π¦ (πΉβπ€)), β*, < ))) | ||
Theorem | fge0npnf 44316 | If πΉ maps to nonnegative reals, then +β is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0rnn0 44317* | The range used in the definition of Ξ£^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)) β β | ||
Theorem | sge0vald 44318* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β*, < ))) | ||
Theorem | fge0iccico 44319 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆ(0[,)+β)) | ||
Theorem | gsumge0cl 44320 | 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 44321* | 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 44322 | 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 44323 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆβ) | ||
Theorem | sge0z 44324* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) β β’ (π β (Ξ£^β(π β π΄ β¦ 0)) = 0) | ||
Theorem | sge00 44325 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (Ξ£^ββ ) = 0 | ||
Theorem | fsumlesge0 44326* | 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 44327* | 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 44328 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:{π΄}βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = (πΉβπ΄)) | ||
Theorem | sge0tsms 44329 | Ξ£^ 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 44330 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β (0[,]+β)) | ||
Theorem | sge0f1o 44331* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0snmpt 44332* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0 44333 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β 0 β€ (Ξ£^βπΉ)) | ||
Theorem | sge0xrcl 44334 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 44335 | 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 44336* | 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 44337 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 44338* | 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 44340, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 44339* | 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 44340* | 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 44341 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 44342* | 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 44343* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 44344* | 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 44345* | 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 44346 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 44347* | 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 44348* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 44349* | 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 44350* | 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 44343. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 44351* | 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 44352 | 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 44353 | 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 44354* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 44355 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 44358. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0le 44356* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΊ:πβΆ(0[,]+β)) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (Ξ£^βπΉ) β€ (Ξ£^βπΊ)) | ||
Theorem | sge0ltfirpmpt 44357* | 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 44358 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) +π (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0lempt 44359* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ πΆ))) | ||
Theorem | sge0splitmpt 44360* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β (π΄ βͺ π΅) β¦ πΆ)) = ((Ξ£^β(π₯ β π΄ β¦ πΆ)) +π (Ξ£^β(π₯ β π΅ β¦ πΆ)))) | ||
Theorem | sge0ss 44361* | 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 44362* | 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 44363* | 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 44364* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) & β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) β β*) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) β β*) & β’ (π β (π β βͺ π₯ β π΄ π΅ β¦ πΆ):βͺ π₯ β π΄ π΅βΆ(0[,]+β)) & β’ (π β βͺ π₯ β π΄ π΅ β V) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0fodjrnlem 44365* | 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 44366* | 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 44367* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0iun 44368* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ π = βͺ π₯ β π΄ π΅ & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (Ξ£^βπΉ) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(πΉ βΎ π΅))))) | ||
Theorem | sge0nemnf 44369 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β -β) | ||
Theorem | sge0rpcpnf 44370* | The sum of an infinite number of a positive constant, is +β (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β Fin) & β’ (π β π΅ β β+) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0rernmpt 44371* | If the sum of nonnegative extended reals is not +β then no term is +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) | ||
Theorem | sge0lefimpt 44372* | 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 44373 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β0 β (0[,)+β) | ||
Theorem | sge0clmpt 44374* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β (0[,]+β)) | ||
Theorem | sge0ltfirpmpt2 44375* | 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 44376 | 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 44377* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β*) | ||
Theorem | sge0xp 44378* | 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 44379* | 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 44380* | 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 44381* | 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 44382* | 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 44383* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0xadd 44384* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0fsummptf 44385* | 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 44386* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0mpt 44387* | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β 0 β€ (Ξ£^β(π β π΄ β¦ π΅))) | ||
Theorem | sge0repnfmpt 44388* | 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 44389* | 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 44390* | Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β (0[,]+β)) β β’ (π β (Ξ£^β(π β (π΄ βͺ {π΅}) β¦ πΆ)) = ((Ξ£^β(π β π΄ β¦ πΆ)) +π π·)) | ||
Theorem | sge0pnffsumgt 44391* | 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 44392* | 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 44393* | 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 44394* | 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 44395 | 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 44396* | 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 44397* | 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 44398 | Extend class notation with the class of measures. |
class Meas | ||
Definition | df-mea 44399* | Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ Meas = {π₯ β£ (((π₯:dom π₯βΆ(0[,]+β) β§ dom π₯ β SAlg) β§ (π₯ββ ) = 0) β§ βπ¦ β π« dom π₯((π¦ βΌ Ο β§ Disj π€ β π¦ π€) β (π₯ββͺ π¦) = (Ξ£^β(π₯ βΎ π¦))))} | ||
Theorem | ismea 44400* | 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 π¦ β π₯ π¦) β (πββͺ π₯) = (Ξ£^β(π βΎ π₯))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |