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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issalgend 44301* | One side of dfsalgen2 44304. If a sigma-algebra on βͺ π includes π and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by π. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ (π β π β SAlg) & β’ (π β βͺ π = βͺ π) & β’ (π β π β π) & β’ ((π β§ (π¦ β SAlg β§ βͺ π¦ = βͺ π β§ π β π¦)) β π β π¦) β β’ (π β (SalGenβπ) = π) | ||
Theorem | salexct2 44302* | An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 44297. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (0[,]2) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} & β’ π΅ = (0[,]1) β β’ Β¬ π΅ β π | ||
Theorem | unisalgen 44303 | The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ π = (SalGenβπ) & β’ π = βͺ π β β’ (π β π β π) | ||
Theorem | dfsalgen2 44304* | Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) β β’ (π β ((SalGenβπ) = π β ((π β SAlg β§ βͺ π = βͺ π β§ π β π) β§ βπ¦ β SAlg ((βͺ π¦ = βͺ π β§ π β π¦) β π β π¦)))) | ||
Theorem | salexct3 44305* | An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (0[,]2) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} & β’ π = ran (π¦ β (0[,]1) β¦ {π¦}) β β’ (π β SAlg β§ π β π β§ Β¬ βͺ π β π) | ||
Theorem | salgencntex 44306* | This counterexample shows that df-salgen 44276 needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (0[,]2) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} & β’ π΅ = (0[,]1) & β’ π = π« π΅ & β’ πΆ = (π β© π) & β’ π = β© {π β SAlg β£ πΆ β π } β β’ Β¬ π β SAlg | ||
Theorem | salgensscntex 44307* | This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (0[,]2) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} & β’ π = ran (π¦ β (0[,]1) β¦ {π¦}) & β’ πΊ = (SalGenβπ) β β’ (π β π β§ π β SAlg β§ Β¬ πΊ β π) | ||
Theorem | issalnnd 44308* | Sufficient condition to prove that π is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β π) & β’ (π β β β π) & β’ π = βͺ π & β’ ((π β§ π¦ β π) β (π β π¦) β π) & β’ ((π β§ π:ββΆπ) β βͺ π β β (πβπ) β π) β β’ (π β π β SAlg) | ||
Theorem | dmvolsal 44309 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β SAlg | ||
Theorem | saldifcld 44310 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) β β’ (π β (βͺ π β πΈ) β π) | ||
Theorem | saluncld 44311 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ βͺ πΉ) β π) | ||
Theorem | salgencld 44312 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β π) & β’ π = (SalGenβπ) β β’ (π β π β SAlg) | ||
Theorem | 0sald 44313 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) β β’ (π β β β π) | ||
Theorem | iooborel 44314 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π΄(,)πΆ) β π΅ | ||
Theorem | salincld 44315 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ β© πΉ) β π) | ||
Theorem | salunid 44316 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) β β’ (π β βͺ π β π) | ||
Theorem | unisalgen2 44317 | 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 44318 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ π΅ β SAlg | ||
Theorem | iocborel 44319 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β (π΄(,]πΆ) β π΅) | ||
Theorem | subsaliuncllem 44320* | 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 44321* | 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 44322 | 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 44323 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) β β’ (π β π΄ β (π βΎt π΄)) | ||
Theorem | salrestss 44324 | 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 44325 | Extend class notation to include the sum of nonnegative extended reals. |
class Ξ£^ | ||
Definition | df-sumge0 44326* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
β’ Ξ£^ = (π₯ β V β¦ if(+β β ran π₯, +β, sup(ran (π¦ β (π« dom π₯ β© Fin) β¦ Ξ£π€ β π¦ (π₯βπ€)), β*, < ))) | ||
Theorem | sge0rnre 44327* | 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 44328 | If πΉ maps to nonnegative reals, then πΉ maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β πΉ:πβΆ(0[,]+β)) | ||
Theorem | sge0val 44329* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β π β§ πΉ:πβΆ(0[,]+β)) β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π¦ β (π« π β© Fin) β¦ Ξ£π€ β π¦ (πΉβπ€)), β*, < ))) | ||
Theorem | fge0npnf 44330 | If πΉ maps to nonnegative reals, then +β is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0rnn0 44331* | The range used in the definition of Ξ£^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)) β β | ||
Theorem | sge0vald 44332* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β*, < ))) | ||
Theorem | fge0iccico 44333 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆ(0[,)+β)) | ||
Theorem | gsumge0cl 44334 | 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 44335* | 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 44336 | 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 44337 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆβ) | ||
Theorem | sge0z 44338* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) β β’ (π β (Ξ£^β(π β π΄ β¦ 0)) = 0) | ||
Theorem | sge00 44339 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (Ξ£^ββ ) = 0 | ||
Theorem | fsumlesge0 44340* | 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 44341* | 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 44342 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:{π΄}βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = (πΉβπ΄)) | ||
Theorem | sge0tsms 44343 | Ξ£^ 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 44344 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β (0[,]+β)) | ||
Theorem | sge0f1o 44345* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0snmpt 44346* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0 44347 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β 0 β€ (Ξ£^βπΉ)) | ||
Theorem | sge0xrcl 44348 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 44349 | 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 44350* | 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 44351 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 44352* | 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 44354, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 44353* | 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 44354* | 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 44355 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 44356* | 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 44357* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 44358* | 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 44359* | 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 44360 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 44361* | 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 44362* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 44363* | 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 44364* | 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 44357. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 44365* | 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 44366 | 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 44367 | 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 44368* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 44369 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 44372. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0le 44370* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β πΊ:πβΆ(0[,]+β)) & β’ ((π β§ π₯ β π) β (πΉβπ₯) β€ (πΊβπ₯)) β β’ (π β (Ξ£^βπΉ) β€ (Ξ£^βπΊ)) | ||
Theorem | sge0ltfirpmpt 44371* | 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 44372 | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) +π (Ξ£^β(πΉ βΎ π΅)))) | ||
Theorem | sge0lempt 44373* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ πΆ))) | ||
Theorem | sge0splitmpt 44374* | Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄ β© π΅) = β ) & β’ ((π β§ π₯ β π΄) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β (π΄ βͺ π΅) β¦ πΆ)) = ((Ξ£^β(π₯ β π΄ β¦ πΆ)) +π (Ξ£^β(π₯ β π΅ β¦ πΆ)))) | ||
Theorem | sge0ss 44375* | 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 44376* | 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 44377* | 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 44378* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) & β’ ((π β§ π₯ β π΄) β (Ξ£^β(π β π΅ β¦ πΆ)) β β) & β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) β β*) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ)))) β β*) & β’ (π β (π β βͺ π₯ β π΄ π΅ β¦ πΆ):βͺ π₯ β π΄ π΅βΆ(0[,]+β)) & β’ (π β βͺ π₯ β π΄ π΅ β V) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0fodjrnlem 44379* | 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 44380* | 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 44381* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β βͺ π₯ β π΄ π΅ β¦ πΆ)) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(π β π΅ β¦ πΆ))))) | ||
Theorem | sge0iun 44382* | Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ π = βͺ π₯ β π΄ π΅ & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (Ξ£^βπΉ) = (Ξ£^β(π₯ β π΄ β¦ (Ξ£^β(πΉ βΎ π΅))))) | ||
Theorem | sge0nemnf 44383 | The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β -β) | ||
Theorem | sge0rpcpnf 44384* | The sum of an infinite number of a positive constant, is +β (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ (π β Β¬ π΄ β Fin) & β’ (π β π΅ β β+) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) = +β) | ||
Theorem | sge0rernmpt 44385* | If the sum of nonnegative extended reals is not +β then no term is +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) β β’ ((π β§ π₯ β π΄) β π΅ β (0[,)+β)) | ||
Theorem | sge0lefimpt 44386* | 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 44387 | Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β0 β (0[,)+β) | ||
Theorem | sge0clmpt 44388* | The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β (0[,]+β)) | ||
Theorem | sge0ltfirpmpt2 44389* | 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 44390 | 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 44391* | The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β*) | ||
Theorem | sge0xp 44392* | 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 44393* | 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 44394* | 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 44395* | 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 44396* | 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 44397* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,)+β)) & β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) β β) & β’ (π β (Ξ£^β(π β π΄ β¦ πΆ)) β β) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0xadd 44398* | The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) & β’ ((π β§ π β π΄) β πΆ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ (π΅ +π πΆ))) = ((Ξ£^β(π β π΄ β¦ π΅)) +π (Ξ£^β(π β π΄ β¦ πΆ)))) | ||
Theorem | sge0fsummptf 44399* | 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 44400* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |