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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ioorrnopnxr 44301* | The indexed product of open intervals is an open set in (β^βπ). Similar to ioorrnopn 44299 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β Fin) & β’ (π β π΄:πβΆβ*) & β’ (π β π΅:πβΆβ*) β β’ (π β Xπ β π ((π΄βπ)(,)(π΅βπ)) β (TopOpenβ(β^βπ))) | ||
Proofs for most of the theorems in section 111 of [Fremlin1] | ||
Syntax | csalg 44302 | Extend class notation with the class of all sigma-algebras. |
class SAlg | ||
Definition | df-salg 44303* | Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ SAlg = {π₯ β£ (β β π₯ β§ βπ¦ β π₯ (βͺ π₯ β π¦) β π₯ β§ βπ¦ β π« π₯(π¦ βΌ Ο β βͺ π¦ β π₯))} | ||
Syntax | csalon 44304 | Extend class notation with the class of sigma-algebras on a set. |
class SalOn | ||
Definition | df-salon 44305* | Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ SalOn = (π₯ β V β¦ {π β SAlg β£ βͺ π = π₯}) | ||
Syntax | csalgen 44306 | Extend class notation with the class of sigma-algebra generator. |
class SalGen | ||
Definition | df-salgen 44307* | Define the sigma-algebra generated by a given set. Definition 111G (b) of [Fremlin1] p. 13. The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set, see dfsalgen2 44335. The base set of the sigma-algebras used for the intersection needs to be the same, otherwise the resulting set is not guaranteed to be a sigma-algebra, as shown in the counterexample salgencntex 44337. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.) |
β’ SalGen = (π₯ β V β¦ β© {π β SAlg β£ (βͺ π = βͺ π₯ β§ π₯ β π )}) | ||
Theorem | issal 44308* | Express the predicate "π is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β (π β SAlg β (β β π β§ βπ¦ β π (βͺ π β π¦) β π β§ βπ¦ β π« π(π¦ βΌ Ο β βͺ π¦ β π)))) | ||
Theorem | pwsal 44309 | The power set of a given set is a sigma-algebra (the so called discrete sigma-algebra). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π« π β SAlg) | ||
Theorem | salunicl 44310 | SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β SAlg) & β’ (π β π β π« π) & β’ (π β π βΌ Ο) β β’ (π β βͺ π β π) | ||
Theorem | saluncl 44311 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β SAlg β§ πΈ β π β§ πΉ β π) β (πΈ βͺ πΉ) β π) | ||
Theorem | prsal 44312 | The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β {β , π} β SAlg) | ||
Theorem | saldifcl 44313 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β SAlg β§ πΈ β π) β (βͺ π β πΈ) β π) | ||
Theorem | 0sal 44314 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β SAlg β β β π) | ||
Theorem | salgenval 44315* | The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β (SalGenβπ) = β© {π β SAlg β£ (βͺ π = βͺ π β§ π β π )}) | ||
Theorem | saliunclf 44316 | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²ππ & β’ β²ππΎ & β’ (π β π β SAlg) & β’ (π β πΎ βΌ Ο) & β’ ((π β§ π β πΎ) β πΈ β π) β β’ (π β βͺ π β πΎ πΈ β π) | ||
Theorem | saliuncl 44317* | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β SAlg) & β’ (π β πΎ βΌ Ο) & β’ ((π β§ π β πΎ) β πΈ β π) β β’ (π β βͺ π β πΎ πΈ β π) | ||
Theorem | salincl 44318 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β SAlg β§ πΈ β π β§ πΉ β π) β (πΈ β© πΉ) β π) | ||
Theorem | saluni 44319 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β SAlg β βͺ π β π) | ||
Theorem | saliinclf 44320 | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
β’ β²ππ & β’ β²ππ & β’ β²ππΎ & β’ (π β π β SAlg) & β’ (π β πΎ βΌ Ο) & β’ (π β πΎ β β ) & β’ ((π β§ π β πΎ) β πΈ β π) β β’ (π β β© π β πΎ πΈ β π) | ||
Theorem | saliincl 44321* | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β SAlg) & β’ (π β πΎ βΌ Ο) & β’ (π β πΎ β β ) & β’ ((π β§ π β πΎ) β πΈ β π) β β’ (π β β© π β πΎ πΈ β π) | ||
Theorem | saldifcl2 44322 | The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β SAlg β§ πΈ β π β§ πΉ β π) β (πΈ β πΉ) β π) | ||
Theorem | intsaluni 44323* | The union of an arbitrary intersection of sigma-algebras on the same set π, is π. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΊ β SAlg) & β’ (π β πΊ β β ) & β’ ((π β§ π β πΊ) β βͺ π = π) β β’ (π β βͺ β© πΊ = π) | ||
Theorem | intsal 44324* | The arbitrary intersection of sigma-algebra (on the same set π) is a sigma-algebra ( on the same set π, see intsaluni 44323). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΊ β SAlg) & β’ (π β πΊ β β ) & β’ ((π β§ π β πΊ) β βͺ π = π) β β’ (π β β© πΊ β SAlg) | ||
Theorem | salgenn0 44325* | The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β {π β SAlg β£ (βͺ π = βͺ π β§ π β π )} β β ) | ||
Theorem | salgencl 44326 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β (SalGenβπ) β SAlg) | ||
Theorem | issald 44327* | Sufficient condition to prove that π is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ (π β β β π) & β’ π = βͺ π & β’ ((π β§ π¦ β π) β (π β π¦) β π) & β’ ((π β§ π¦ β π« π β§ π¦ βΌ Ο) β βͺ π¦ β π) β β’ (π β π β SAlg) | ||
Theorem | salexct 44328* | An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β π) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} β β’ (π β π β SAlg) | ||
Theorem | sssalgen 44329 | A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π = (SalGenβπ) β β’ (π β π β π β π) | ||
Theorem | salgenss 44330 | The sigma-algebra generated by a set is the smallest sigma-algebra, on the same base set, that includes the set. Proposition 111G (b) of [Fremlin1] p. 13. Notice that the condition "on the same base set" is needed, see the counterexample salgensscntex 44338, where a sigma-algebra is shown that includes a set, but does not include the sigma-algebra generated (the key is that its base set is larger than the base set of the generating set). (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ πΊ = (SalGenβπ) & β’ (π β π β SAlg) & β’ (π β π β π) & β’ (π β βͺ π = βͺ π) β β’ (π β πΊ β π) | ||
Theorem | salgenuni 44331 | The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ π = (SalGenβπ) & β’ π = βͺ π β β’ (π β βͺ π = π) | ||
Theorem | issalgend 44332* | One side of dfsalgen2 44335. 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 44333* | An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 44328. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ π΄ = (0[,]2) & β’ π = {π₯ β π« π΄ β£ (π₯ βΌ Ο β¨ (π΄ β π₯) βΌ Ο)} & β’ π΅ = (0[,]1) β β’ Β¬ π΅ β π | ||
Theorem | unisalgen 44334 | The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π β π) & β’ π = (SalGenβπ) & β’ π = βͺ π β β’ (π β π β π) | ||
Theorem | dfsalgen2 44335* | 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 44336* | 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 44337* | This counterexample shows that df-salgen 44307 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 44338* | 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 44339* | Sufficient condition to prove that π is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β π) & β’ (π β β β π) & β’ π = βͺ π & β’ ((π β§ π¦ β π) β (π β π¦) β π) & β’ ((π β§ π:ββΆπ) β βͺ π β β (πβπ) β π) β β’ (π β π β SAlg) | ||
Theorem | dmvolsal 44340 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ dom vol β SAlg | ||
Theorem | saldifcld 44341 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) β β’ (π β (βͺ π β πΈ) β π) | ||
Theorem | saluncld 44342 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ βͺ πΉ) β π) | ||
Theorem | salgencld 44343 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β π) & β’ π = (SalGenβπ) β β’ (π β π β SAlg) | ||
Theorem | 0sald 44344 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) β β’ (π β β β π) | ||
Theorem | iooborel 44345 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π΄(,)πΆ) β π΅ | ||
Theorem | salincld 44346 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β πΈ β π) & β’ (π β πΉ β π) β β’ (π β (πΈ β© πΉ) β π) | ||
Theorem | salunid 44347 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) β β’ (π β βͺ π β π) | ||
Theorem | unisalgen2 44348 | 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 44349 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ π΅ β SAlg | ||
Theorem | iocborel 44350 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β) & β’ π½ = (topGenβran (,)) & β’ π΅ = (SalGenβπ½) β β’ (π β (π΄(,]πΆ) β π΅) | ||
Theorem | subsaliuncllem 44351* | 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 44352* | 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 44353 | 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 44354 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π β SAlg) & β’ (π β π΄ β βͺ π) β β’ (π β π΄ β (π βΎt π΄)) | ||
Theorem | salrestss 44355 | 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 44356 | Extend class notation to include the sum of nonnegative extended reals. |
class Ξ£^ | ||
Definition | df-sumge0 44357* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
β’ Ξ£^ = (π₯ β V β¦ if(+β β ran π₯, +β, sup(ran (π¦ β (π« dom π₯ β© Fin) β¦ Ξ£π€ β π¦ (π₯βπ€)), β*, < ))) | ||
Theorem | sge0rnre 44358* | 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 44359 | If πΉ maps to nonnegative reals, then πΉ maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β πΉ:πβΆ(0[,]+β)) | ||
Theorem | sge0val 44360* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β π β§ πΉ:πβΆ(0[,]+β)) β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π¦ β (π« π β© Fin) β¦ Ξ£π€ β π¦ (πΉβπ€)), β*, < ))) | ||
Theorem | fge0npnf 44361 | If πΉ maps to nonnegative reals, then +β is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,)+β)) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0rnn0 44362* | The range used in the definition of Ξ£^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)) β β | ||
Theorem | sge0vald 44363* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = if(+β β ran πΉ, +β, sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β*, < ))) | ||
Theorem | fge0iccico 44364 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆ(0[,)+β)) | ||
Theorem | gsumge0cl 44365 | 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 44366* | 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 44367 | 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 44368 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β Β¬ +β β ran πΉ) β β’ (π β πΉ:πβΆβ) | ||
Theorem | sge0z 44369* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ (π β π΄ β π) β β’ (π β (Ξ£^β(π β π΄ β¦ 0)) = 0) | ||
Theorem | sge00 44370 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (Ξ£^ββ ) = 0 | ||
Theorem | fsumlesge0 44371* | 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 44372* | 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 44373 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΉ:{π΄}βΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) = (πΉβπ΄)) | ||
Theorem | sge0tsms 44374 | Ξ£^ 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 44375 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β (0[,]+β)) | ||
Theorem | sge0f1o 44376* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β π) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) β β’ (π β (Ξ£^β(π β π΄ β¦ π΅)) = (Ξ£^β(π β πΆ β¦ π·))) | ||
Theorem | sge0snmpt 44377* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β πΆ β (0[,]+β)) & β’ (π = π΄ β π΅ = πΆ) β β’ (π β (Ξ£^β(π β {π΄} β¦ π΅)) = πΆ) | ||
Theorem | sge0ge0 44378 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β 0 β€ (Ξ£^βπΉ)) | ||
Theorem | sge0xrcl 44379 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^βπΉ) β β*) | ||
Theorem | sge0repnf 44380 | 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 44381* | 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 44382 | If the sum of nonnegative extended reals is not +β then no terms is +β. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β Β¬ +β β ran πΉ) | ||
Theorem | sge0supre 44383* | 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 44385, but here we can use sup with respect to β instead of β*. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = sup(ran (π₯ β (π« π β© Fin) β¦ Ξ£π¦ β π₯ (πΉβπ¦)), β, < )) | ||
Theorem | sge0fsummpt 44384* | 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 44385* | 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 44386 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) β β’ (π β (Ξ£^β(πΉ βΎ π)) β€ (Ξ£^βπΉ)) | ||
Theorem | sge0rnbnd 44387* | 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 44388* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β π΄ β π΅) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) = (π· +π πΈ)) | ||
Theorem | sge0gerp 44389* | 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 44390* | 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 44391 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^β(πΉ βΎ π)) β β) | ||
Theorem | sge0lefi 44392* | 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 44393* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β€ (Ξ£^β(π₯ β π΄ β¦ π΅))) | ||
Theorem | sge0ltfirp 44394* | 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 44395* | 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 44388. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π· β (0[,]+β)) & β’ (π β πΈ β (0[,]+β)) & β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) β β’ (π β (Ξ£^β(π β {π΄, π΅} β¦ πΆ)) β€ (π· +π πΈ)) | ||
Theorem | sge0gerpmpt 44396* | 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 44397 | 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 44398 | 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 44399* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β π) & β’ ((π β§ π₯ β π΄) β π΅ β (0[,]+β)) & β’ (π β (Ξ£^β(π₯ β π΄ β¦ π΅)) β β) & β’ (π β πΆ β π΄) β β’ (π β (Ξ£^β(π₯ β πΆ β¦ π΅)) β β) | ||
Theorem | sge0resplit 44400 | Ξ£^ splits into two parts, when it's a real number. This is a special case of sge0split 44403. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ π = (π΄ βͺ π΅) & β’ (π β (π΄ β© π΅) = β ) & β’ (π β πΉ:πβΆ(0[,]+β)) & β’ (π β (Ξ£^βπΉ) β β) β β’ (π β (Ξ£^βπΉ) = ((Ξ£^β(πΉ βΎ π΄)) + (Ξ£^β(πΉ βΎ π΅)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |