Home | Metamath
Proof Explorer Theorem List (p. 325 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 | nfesum2 32401* | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.) |
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ต โ โข โฒ๐ฅฮฃ*๐ โ ๐ด๐ต | ||
Theorem | cbvesum 32402* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) & โข โฒ๐๐ด & โข โฒ๐๐ด & โข โฒ๐๐ต & โข โฒ๐๐ถ โ โข ฮฃ*๐ โ ๐ด๐ต = ฮฃ*๐ โ ๐ด๐ถ | ||
Theorem | cbvesumv 32403* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) โ โข ฮฃ*๐ โ ๐ด๐ต = ฮฃ*๐ โ ๐ด๐ถ | ||
Theorem | esumid 32404 | Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ถ โ ((โ*๐ โพs (0[,]+โ)) tsums (๐ โ ๐ด โฆ ๐ต))) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ๐ถ) | ||
Theorem | esumgsum 32405 | A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ((โ*๐ โพs (0[,]+โ)) ฮฃg (๐ โ ๐ด โฆ ๐ต))) | ||
Theorem | esumval 32406* | Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ฅ โ (๐ซ ๐ด โฉ Fin)) โ ((โ*๐ โพs (0[,]+โ)) ฮฃg (๐ โ ๐ฅ โฆ ๐ต)) = ๐ถ) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = sup(ran (๐ฅ โ (๐ซ ๐ด โฉ Fin) โฆ ๐ถ), โ*, < )) | ||
Theorem | esumel 32407* | The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โ ((โ*๐ โพs (0[,]+โ)) tsums (๐ โ ๐ด โฆ ๐ต))) | ||
Theorem | esumnul 32408 | Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.) |
โข ฮฃ*๐ฅ โ โ ๐ด = 0 | ||
Theorem | esum0 32409* | Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
โข โฒ๐๐ด โ โข (๐ด โ ๐ โ ฮฃ*๐ โ ๐ด0 = 0) | ||
Theorem | esumf1o 32410* | Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ต & โข โฒ๐๐ท & โข โฒ๐๐ด & โข โฒ๐๐ถ & โข โฒ๐๐น & โข (๐ = ๐บ โ ๐ต = ๐ท) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐น:๐ถโ1-1-ontoโ๐ด) & โข ((๐ โง ๐ โ ๐ถ) โ (๐นโ๐) = ๐บ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ฮฃ*๐ โ ๐ถ๐ท) | ||
Theorem | esumc 32411* | Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.) |
โข โฒ๐๐ท & โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ฆ = ๐ถ โ ๐ท = ๐ต) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ Fun โก(๐ โ ๐ด โฆ ๐ถ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ ๐) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ฮฃ*๐ฆ โ {๐ง โฃ โ๐ โ ๐ด ๐ง = ๐ถ}๐ท) | ||
Theorem | esumrnmpt 32412* | Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020.) |
โข โฒ๐๐ด & โข (๐ฆ = ๐ต โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ท โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (๐ โ {โ })) & โข (๐ โ Disj ๐ โ ๐ด ๐ต) โ โข (๐ โ ฮฃ*๐ฆ โ ran (๐ โ ๐ด โฆ ๐ต)๐ถ = ฮฃ*๐ โ ๐ด๐ท) | ||
Theorem | esumsplit 32413 | Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข โฒ๐๐ต & โข (๐ โ ๐ด โ V) & โข (๐ โ ๐ต โ V) & โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ต) โ ๐ถ โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ (๐ด โช ๐ต)๐ถ = (ฮฃ*๐ โ ๐ด๐ถ +๐ ฮฃ*๐ โ ๐ต๐ถ)) | ||
Theorem | esummono 32414* | Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
โข โฒ๐๐ & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ โ ๐ถ) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ด โ ๐ถ) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โค ฮฃ*๐ โ ๐ถ๐ต) | ||
Theorem | esumpad 32415* | Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ต) โ ๐ถ = 0) โ โข (๐ โ ฮฃ*๐ โ (๐ด โช ๐ต)๐ถ = ฮฃ*๐ โ ๐ด๐ถ) | ||
Theorem | esumpad2 32416* | Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ต) โ ๐ถ = 0) โ โข (๐ โ ฮฃ*๐ โ (๐ด โ ๐ต)๐ถ = ฮฃ*๐ โ ๐ด๐ถ) | ||
Theorem | esumadd 32417* | Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด(๐ต +๐ ๐ถ) = (ฮฃ*๐ โ ๐ด๐ต +๐ ฮฃ*๐ โ ๐ด๐ถ)) | ||
Theorem | esumle 32418* | If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โค ฮฃ*๐ โ ๐ด๐ถ) | ||
Theorem | gsumesum 32419* | Relate a group sum on (โ*๐ โพs (0[,]+โ)) to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ((โ*๐ โพs (0[,]+โ)) ฮฃg (๐ โ ๐ด โฆ ๐ต)) = ฮฃ*๐ โ ๐ด๐ต) | ||
Theorem | esumlub 32420* | The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ โ โ*) & โข (๐ โ ๐ < ฮฃ*๐ โ ๐ด๐ต) โ โข (๐ โ โ๐ โ (๐ซ ๐ด โฉ Fin)๐ < ฮฃ*๐ โ ๐๐ต) | ||
Theorem | esumaddf 32421* | Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด(๐ต +๐ ๐ถ) = (ฮฃ*๐ โ ๐ด๐ต +๐ ฮฃ*๐ โ ๐ด๐ถ)) | ||
Theorem | esumlef 32422* | If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โค ฮฃ*๐ โ ๐ด๐ถ) | ||
Theorem | esumcst 32423* | The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.) |
โข โฒ๐๐ด & โข โฒ๐๐ต โ โข ((๐ด โ ๐ โง ๐ต โ (0[,]+โ)) โ ฮฃ*๐ โ ๐ด๐ต = ((โฏโ๐ด) ยทe ๐ต)) | ||
Theorem | esumsnf 32424* | The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 2-May-2020.) |
โข โฒ๐๐ต & โข ((๐ โง ๐ = ๐) โ ๐ด = ๐ต) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ {๐}๐ด = ๐ต) | ||
Theorem | esumsn 32425* | The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017.) (Shortened by Thierry Arnoux, 2-May-2020.) |
โข ((๐ โง ๐ = ๐) โ ๐ด = ๐ต) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ต โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ {๐}๐ด = ๐ต) | ||
Theorem | esumpr 32426* | Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
โข ((๐ โง ๐ = ๐ด) โ ๐ถ = ๐ท) & โข ((๐ โง ๐ = ๐ต) โ ๐ถ = ๐ธ) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ท โ (0[,]+โ)) & โข (๐ โ ๐ธ โ (0[,]+โ)) & โข (๐ โ ๐ด โ ๐ต) โ โข (๐ โ ฮฃ*๐ โ {๐ด, ๐ต}๐ถ = (๐ท +๐ ๐ธ)) | ||
Theorem | esumpr2 32427* | Extended sum over a pair, with a relaxed condition compared to esumpr 32426. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
โข ((๐ โง ๐ = ๐ด) โ ๐ถ = ๐ท) & โข ((๐ โง ๐ = ๐ต) โ ๐ถ = ๐ธ) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ท โ (0[,]+โ)) & โข (๐ โ ๐ธ โ (0[,]+โ)) & โข (๐ โ (๐ด = ๐ต โ (๐ท = 0 โจ ๐ท = +โ))) โ โข (๐ โ ฮฃ*๐ โ {๐ด, ๐ต}๐ถ = (๐ท +๐ ๐ธ)) | ||
Theorem | esumrnmpt2 32428* | Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 30-May-2020.) |
โข (๐ฆ = ๐ต โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ท โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข (((๐ โง ๐ โ ๐ด) โง ๐ต = โ ) โ ๐ท = 0) & โข (๐ โ Disj ๐ โ ๐ด ๐ต) โ โข (๐ โ ฮฃ*๐ฆ โ ran (๐ โ ๐ด โฆ ๐ต)๐ถ = ฮฃ*๐ โ ๐ด๐ท) | ||
Theorem | esumfzf 32429* | Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
โข โฒ๐๐น โ โข ((๐น:โโถ(0[,]+โ) โง ๐ โ โ) โ ฮฃ*๐ โ (1...๐)(๐นโ๐) = (seq1( +๐ , ๐น)โ๐)) | ||
Theorem | esumfsup 32430 | Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
โข โฒ๐๐น โ โข (๐น:โโถ(0[,]+โ) โ ฮฃ*๐ โ โ(๐นโ๐) = sup(ran seq1( +๐ , ๐น), โ*, < )) | ||
Theorem | esumfsupre 32431 | Formulating an extended sum over integers using the recursive sequence builder. This version is limited to real-valued functions. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
โข โฒ๐๐น โ โข (๐น:โโถ(0[,)+โ) โ ฮฃ*๐ โ โ(๐นโ๐) = sup(ran seq1( + , ๐น), โ*, < )) | ||
Theorem | esumss 32432 | Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข โฒ๐๐ต & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ต โ ๐) & โข ((๐ โง ๐ โ ๐ต) โ ๐ถ โ (0[,]+โ)) & โข ((๐ โง ๐ โ (๐ต โ ๐ด)) โ ๐ถ = 0) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ถ = ฮฃ*๐ โ ๐ต๐ถ) | ||
Theorem | esumpinfval 32433* | The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ โ๐ โ ๐ด ๐ต = +โ) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = +โ) | ||
Theorem | esumpfinvallem 32434 | Lemma for esumpfinval 32435. (Contributed by Thierry Arnoux, 28-Jun-2017.) |
โข ((๐ด โ ๐ โง ๐น:๐ดโถ(0[,)+โ)) โ (โfld ฮฃg ๐น) = ((โ*๐ โพs (0[,]+โ)) ฮฃg ๐น)) | ||
Theorem | esumpfinval 32435* | The value of the extended sum of a finite set of nonnegative finite terms. (Contributed by Thierry Arnoux, 28-Jun-2017.) (Proof shortened by AV, 25-Jul-2019.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,)+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | esumpfinvalf 32436 | Same as esumpfinval 32435, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.) |
โข โฒ๐๐ด & โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,)+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | esumpinfsum 32437* | The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
โข โฒ๐๐ & โข โฒ๐๐ด & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ยฌ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ โค ๐ต) & โข (๐ โ ๐ โ โ*) & โข (๐ โ 0 < ๐) โ โข (๐ โ ฮฃ*๐ โ ๐ด๐ต = +โ) | ||
Theorem | esumpcvgval 32438* | The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.) |
โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,)+โ)) & โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ โ (๐ โ โ โฆ ฮฃ๐ โ (1...๐)๐ด) โ dom โ ) โ โข (๐ โ ฮฃ*๐ โ โ๐ด = ฮฃ๐ โ โ ๐ด) | ||
Theorem | esumpmono 32439* | The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,)+โ)) โ โข (๐ โ ฮฃ*๐ โ (1...๐)๐ด โค ฮฃ*๐ โ (1...๐)๐ด) | ||
Theorem | esumcocn 32440* | Lemma for esummulc2 32442 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017.) |
โข ๐ฝ = ((ordTopโ โค ) โพt (0[,]+โ)) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ถ โ (๐ฝ Cn ๐ฝ)) & โข (๐ โ (๐ถโ0) = 0) & โข ((๐ โง ๐ฅ โ (0[,]+โ) โง ๐ฆ โ (0[,]+โ)) โ (๐ถโ(๐ฅ +๐ ๐ฆ)) = ((๐ถโ๐ฅ) +๐ (๐ถโ๐ฆ))) โ โข (๐ โ (๐ถโฮฃ*๐ โ ๐ด๐ต) = ฮฃ*๐ โ ๐ด(๐ถโ๐ต)) | ||
Theorem | esummulc1 32441* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ถ โ (0[,)+โ)) โ โข (๐ โ (ฮฃ*๐ โ ๐ด๐ต ยทe ๐ถ) = ฮฃ*๐ โ ๐ด(๐ต ยทe ๐ถ)) | ||
Theorem | esummulc2 32442* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ถ โ (0[,)+โ)) โ โข (๐ โ (๐ถ ยทe ฮฃ*๐ โ ๐ด๐ต) = ฮฃ*๐ โ ๐ด(๐ถ ยทe ๐ต)) | ||
Theorem | esumdivc 32443* | An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ๐ถ โ โ+) โ โข (๐ โ (ฮฃ*๐ โ ๐ด๐ต /๐ ๐ถ) = ฮฃ*๐ โ ๐ด(๐ต /๐ ๐ถ)) | ||
Theorem | hashf2 32444 | Lemma for hasheuni 32445. (Contributed by Thierry Arnoux, 19-Nov-2016.) |
โข โฏ:Vโถ(0[,]+โ) | ||
Theorem | hasheuni 32445* | The cardinality of a disjoint union, not necessarily finite. cf. hashuni 15646. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.) |
โข ((๐ด โ ๐ โง Disj ๐ฅ โ ๐ด ๐ฅ) โ (โฏโโช ๐ด) = ฮฃ*๐ฅ โ ๐ด(โฏโ๐ฅ)) | ||
Theorem | esumcvg 32446* | The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 15547. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
โข ๐ฝ = (TopOpenโ(โ*๐ โพs (0[,]+โ))) & โข ๐น = (๐ โ โ โฆ ฮฃ*๐ โ (1...๐)๐ด) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,]+โ)) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ ๐น(โ๐กโ๐ฝ)ฮฃ*๐ โ โ๐ด) | ||
Theorem | esumcvg2 32447* | Simpler version of esumcvg 32446. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
โข ๐ฝ = (TopOpenโ(โ*๐ โพs (0[,]+โ))) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,]+โ)) & โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ = ๐ โ ๐ด = ๐ถ) โ โข (๐ โ (๐ โ โ โฆ ฮฃ*๐ โ (1...๐)๐ด)(โ๐กโ๐ฝ)ฮฃ*๐ โ โ๐ด) | ||
Theorem | esumcvgsum 32448* | The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.) |
โข (๐ = ๐ โ ๐ด = ๐ต) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,)+โ)) & โข ((๐ โง ๐ โ โ) โ (๐นโ๐) = ๐ด) & โข (๐ โ seq1( + , ๐น) โ ๐ฟ) & โข (๐ โ ๐ฟ โ โ) โ โข (๐ โ ฮฃ*๐ โ โ๐ด = ฮฃ๐ โ โ ๐ด) | ||
Theorem | esumsup 32449* | Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.) |
โข (๐ โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ โ๐ด = sup(ran (๐ โ โ โฆ ฮฃ*๐ โ (1...๐)๐ด), โ*, < )) | ||
Theorem | esumgect 32450* | "Send ๐ to +โ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.) |
โข (๐ โ ๐ต โ (0[,]+โ)) & โข ((๐ โง ๐ โ โ) โ ๐ด โ (0[,]+โ)) & โข ((๐ โง ๐ โ โ) โ ฮฃ*๐ โ (1...๐)๐ด โค ๐ต) โ โข (๐ โ ฮฃ*๐ โ โ๐ด โค ๐ต) | ||
Theorem | esumcvgre 32451* | All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ (0[,]+โ)) & โข (๐ โ ฮฃ*๐ โ ๐ด๐ต โ โ) โ โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) | ||
Theorem | esum2dlem 32452* | Lemma for esum2d 32453 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.) |
โข โฒ๐๐น & โข (๐ง = โจ๐, ๐โฉ โ ๐น = ๐ถ) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ (0[,]+โ)) & โข (๐ โ ๐ด โ Fin) โ โข (๐ โ ฮฃ*๐ โ ๐ดฮฃ*๐ โ ๐ต๐ถ = ฮฃ*๐ง โ โช ๐ โ ๐ด ({๐} ร ๐ต)๐น) | ||
Theorem | esum2d 32453* | Write a double extended sum as a sum over a two-dimensional region. Note that ๐ต(๐) is a function of ๐. This can be seen as "slicing" the relation ๐ด. (Contributed by Thierry Arnoux, 17-May-2020.) |
โข โฒ๐๐น & โข (๐ง = โจ๐, ๐โฉ โ ๐น = ๐ถ) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ ๐ดฮฃ*๐ โ ๐ต๐ถ = ฮฃ*๐ง โ โช ๐ โ ๐ด ({๐} ร ๐ต)๐น) | ||
Theorem | esumiun 32454* | Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.) |
โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข (((๐ โง ๐ โ ๐ด) โง ๐ โ ๐ต) โ ๐ถ โ (0[,]+โ)) โ โข (๐ โ ฮฃ*๐ โ โช ๐ โ ๐ด ๐ต๐ถ โค ฮฃ*๐ โ ๐ดฮฃ*๐ โ ๐ต๐ถ) | ||
Syntax | cofc 32455 | Extend class notation to include mapping of an operation to an operation for a function and a constant. |
class โf/c ๐ | ||
Definition | df-ofc 32456* | Define the function/constant operation map. The definition is designed so that if ๐ is a binary operation, then โf/c ๐ is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
โข โf/c ๐ = (๐ โ V, ๐ โ V โฆ (๐ฅ โ dom ๐ โฆ ((๐โ๐ฅ)๐ ๐))) | ||
Theorem | ofceq 32457 | Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
โข (๐ = ๐ โ โf/c ๐ = โf/c ๐) | ||
Theorem | ofcfval 32458* | Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
โข (๐ โ ๐น Fn ๐ด) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ฅ โ ๐ด) โ (๐นโ๐ฅ) = ๐ต) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) = (๐ฅ โ ๐ด โฆ (๐ต๐ ๐ถ))) | ||
Theorem | ofcval 32459 | Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข (๐ โ ๐น Fn ๐ด) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ โ ๐ด) โ (๐นโ๐) = ๐ต) โ โข ((๐ โง ๐ โ ๐ด) โ ((๐น โf/c ๐ ๐ถ)โ๐) = (๐ต๐ ๐ถ)) | ||
Theorem | ofcfn 32460 | The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข (๐ โ ๐น Fn ๐ด) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) Fn ๐ด) | ||
Theorem | ofcfeqd2 32461* | Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐นโ๐ฅ) โ ๐ต) & โข ((๐ โง ๐ฆ โ ๐ต) โ (๐ฆ๐ ๐ถ) = (๐ฆ๐๐ถ)) & โข (๐ โ ๐น Fn ๐ด) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) = (๐น โf/c ๐๐ถ)) | ||
Theorem | ofcfval3 32462* | General value of (๐น โf/c ๐ ๐ถ) with no assumptions on functionality of ๐น. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข ((๐น โ ๐ โง ๐ถ โ ๐) โ (๐น โf/c ๐ ๐ถ) = (๐ฅ โ dom ๐น โฆ ((๐นโ๐ฅ)๐ ๐ถ))) | ||
Theorem | ofcf 32463* | The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ๐ ๐ฆ) โ ๐) & โข (๐ โ ๐น:๐ดโถ๐) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ (๐น โf/c ๐ ๐ถ):๐ดโถ๐) | ||
Theorem | ofcfval2 32464* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ ๐น = (๐ฅ โ ๐ด โฆ ๐ต)) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) = (๐ฅ โ ๐ด โฆ (๐ต๐ ๐ถ))) | ||
Theorem | ofcfval4 32465* | The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข (๐ โ ๐น:๐ดโถ๐ต) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) = ((๐ฅ โ ๐ต โฆ (๐ฅ๐ ๐ถ)) โ ๐น)) | ||
Theorem | ofcc 32466 | Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ ((๐ด ร {๐ต}) โf/c ๐ ๐ถ) = (๐ด ร {(๐ต๐ ๐ถ)})) | ||
Theorem | ofcof 32467 | Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.) |
โข (๐ โ ๐น:๐ดโถ๐ต) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ถ โ ๐) โ โข (๐ โ (๐น โf/c ๐ ๐ถ) = (๐น โf ๐ (๐ด ร {๐ถ}))) | ||
Syntax | csiga 32468 | Extend class notation to include the function giving the sigma-algebras on a given base set. |
class sigAlgebra | ||
Definition | df-siga 32469* | Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using ๐ and ๐ as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016.) |
โข sigAlgebra = (๐ โ V โฆ {๐ โฃ (๐ โ ๐ซ ๐ โง (๐ โ ๐ โง โ๐ฅ โ ๐ (๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐ (๐ฅ โผ ฯ โ โช ๐ฅ โ ๐ )))}) | ||
Theorem | sigaex 32470* | Lemma for issiga 32472 and isrnsiga 32473. The class of sigma-algebras with base set ๐ is a set. Note: a more generic version with (๐ โ V โ ...) could be useful for sigaval 32471. (Contributed by Thierry Arnoux, 24-Oct-2016.) |
โข {๐ โฃ (๐ โ ๐ซ ๐ โง (๐ โ ๐ โง โ๐ฅ โ ๐ (๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐ (๐ฅ โผ ฯ โ โช ๐ฅ โ ๐ )))} โ V | ||
Theorem | sigaval 32471* | The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.) |
โข (๐ โ V โ (sigAlgebraโ๐) = {๐ โฃ (๐ โ ๐ซ ๐ โง (๐ โ ๐ โง โ๐ฅ โ ๐ (๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐ (๐ฅ โผ ฯ โ โช ๐ฅ โ ๐ )))}) | ||
Theorem | issiga 32472* | An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
โข (๐ โ V โ (๐ โ (sigAlgebraโ๐) โ (๐ โ ๐ซ ๐ โง (๐ โ ๐ โง โ๐ฅ โ ๐ (๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐(๐ฅ โผ ฯ โ โช ๐ฅ โ ๐))))) | ||
Theorem | isrnsiga 32473* | The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (Proof shortened by Thierry Arnoux, 23-Oct-2016.) |
โข (๐ โ โช ran sigAlgebra โ (๐ โ V โง โ๐(๐ โ ๐ซ ๐ โง (๐ โ ๐ โง โ๐ฅ โ ๐ (๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐(๐ฅ โผ ฯ โ โช ๐ฅ โ ๐))))) | ||
Theorem | 0elsiga 32474 | A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
โข (๐ โ โช ran sigAlgebra โ โ โ ๐) | ||
Theorem | baselsiga 32475 | A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.) |
โข (๐ โ (sigAlgebraโ๐ด) โ ๐ด โ ๐) | ||
Theorem | sigasspw 32476 | A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.) |
โข (๐ โ (sigAlgebraโ๐ด) โ ๐ โ ๐ซ ๐ด) | ||
Theorem | sigaclcu 32477 | A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ซ ๐ โง ๐ด โผ ฯ) โ โช ๐ด โ ๐) | ||
Theorem | sigaclcuni 32478* | A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
โข โฒ๐๐ด โ โข ((๐ โ โช ran sigAlgebra โง โ๐ โ ๐ด ๐ต โ ๐ โง ๐ด โผ ฯ) โ โช ๐ โ ๐ด ๐ต โ ๐) | ||
Theorem | sigaclfu 32479 | A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ซ ๐ โง ๐ด โ Fin) โ โช ๐ด โ ๐) | ||
Theorem | sigaclcu2 32480* | A sigma-algebra is closed under countable union - indexing on โ (Contributed by Thierry Arnoux, 29-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง โ๐ โ โ ๐ด โ ๐) โ โช ๐ โ โ ๐ด โ ๐) | ||
Theorem | sigaclfu2 32481* | A sigma-algebra is closed under finite union - indexing on (1..^๐). (Contributed by Thierry Arnoux, 28-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง โ๐ โ (1..^๐)๐ด โ ๐) โ โช ๐ โ (1..^๐)๐ด โ ๐) | ||
Theorem | sigaclcu3 32482* | A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
โข (๐ โ ๐ โ โช ran sigAlgebra) & โข (๐ โ (๐ = โ โจ ๐ = (1..^๐))) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ ๐) โ โข (๐ โ โช ๐ โ ๐ ๐ด โ ๐) | ||
Theorem | issgon 32483 | Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016.) (Revised by Thierry Arnoux, 23-Oct-2016.) |
โข (๐ โ (sigAlgebraโ๐) โ (๐ โ โช ran sigAlgebra โง ๐ = โช ๐)) | ||
Theorem | sgon 32484 | A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
โข (๐ โ โช ran sigAlgebra โ ๐ โ (sigAlgebraโโช ๐)) | ||
Theorem | elsigass 32485 | An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐) โ ๐ด โ โช ๐) | ||
Theorem | elrnsiga 32486 | Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
โข (๐ โ (sigAlgebraโ๐) โ ๐ โ โช ran sigAlgebra) | ||
Theorem | isrnsigau 32487* | The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.) |
โข (๐ โ โช ran sigAlgebra โ (๐ โ ๐ซ โช ๐ โง (โช ๐ โ ๐ โง โ๐ฅ โ ๐ (โช ๐ โ ๐ฅ) โ ๐ โง โ๐ฅ โ ๐ซ ๐(๐ฅ โผ ฯ โ โช ๐ฅ โ ๐)))) | ||
Theorem | unielsiga 32488 | A sigma-algebra contains its universe set. (Contributed by Thierry Arnoux, 13-Feb-2017.) (Shortened by Thierry Arnoux, 6-Jun-2017.) |
โข (๐ โ โช ran sigAlgebra โ โช ๐ โ ๐) | ||
Theorem | dmvlsiga 32489 | Lebesgue-measurable subsets of โ form a sigma-algebra. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
โข dom vol โ (sigAlgebraโโ) | ||
Theorem | pwsiga 32490 | Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
โข (๐ โ ๐ โ ๐ซ ๐ โ (sigAlgebraโ๐)) | ||
Theorem | prsiga 32491 | The smallest possible sigma-algebra containing ๐. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
โข (๐ โ ๐ โ {โ , ๐} โ (sigAlgebraโ๐)) | ||
Theorem | sigaclci 32492 | A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
โข (((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ซ ๐) โง (๐ด โผ ฯ โง ๐ด โ โ )) โ โฉ ๐ด โ ๐) | ||
Theorem | difelsiga 32493 | A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด โ ๐ต) โ ๐) | ||
Theorem | unelsiga 32494 | A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด โช ๐ต) โ ๐) | ||
Theorem | inelsiga 32495 | A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด โฉ ๐ต) โ ๐) | ||
Theorem | sigainb 32496 | Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
โข ((๐ โ โช ran sigAlgebra โง ๐ด โ ๐) โ (๐ โฉ ๐ซ ๐ด) โ (sigAlgebraโ๐ด)) | ||
Theorem | insiga 32497 | The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
โข ((๐ด โ โ โง ๐ด โ ๐ซ (sigAlgebraโ๐)) โ โฉ ๐ด โ (sigAlgebraโ๐)) | ||
Syntax | csigagen 32498 | Extend class notation to include the sigma-algebra generator. |
class sigaGen | ||
Definition | df-sigagen 32499* | Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
โข sigaGen = (๐ฅ โ V โฆ โฉ {๐ โ (sigAlgebraโโช ๐ฅ) โฃ ๐ฅ โ ๐ }) | ||
Theorem | sigagenval 32500* | Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
โข (๐ด โ ๐ โ (sigaGenโ๐ด) = โฉ {๐ โ (sigAlgebraโโช ๐ด) โฃ ๐ด โ ๐ }) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |