Home | Metamath
Proof Explorer Theorem List (p. 302 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | esumeq2sdv 30101* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | nfesum1 30102 | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵 | ||
Theorem | nfesum2 30103* | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵 | ||
Theorem | cbvesum 30104* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶 | ||
Theorem | cbvesumv 30105* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶 | ||
Theorem | esumid 30106 | 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 30107 | 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 30108* | Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < )) | ||
Theorem | esumel 30109* | 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 30110 | Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.) |
⊢ Σ*𝑥 ∈ ∅𝐴 = 0 | ||
Theorem | esum0 30111* | Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0) | ||
Theorem | esumf1o 30112* | Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐵 & ⊢ Ⅎ𝑘𝐷 & ⊢ Ⅎ𝑛𝐴 & ⊢ Ⅎ𝑛𝐶 & ⊢ Ⅎ𝑛𝐹 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷) | ||
Theorem | esumc 30113* | Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑘𝐷 & ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷) | ||
Theorem | esumrnmpt 30114* | 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 30115 | Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶)) | ||
Theorem | esummono 30116* | Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵) | ||
Theorem | esumpad 30117* | Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumpad2 30118* | Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumadd 30119* | Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶)) | ||
Theorem | esumle 30120* | 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 30121* | 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 30122* | 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 30123* | Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶)) | ||
Theorem | esumlef 30124* | 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 30125* | The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 = ((#‘𝐴) ·e 𝐵)) | ||
Theorem | esumsnf 30126* | 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 30127* | 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 30128* | Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸)) | ||
Theorem | esumpr2 30129* | Extended sum over a pair, with a relaxed condition compared to esumpr 30128. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝜑 → (𝐴 = 𝐵 → (𝐷 = 0 ∨ 𝐷 = +∞))) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸)) | ||
Theorem | esumrnmpt2 30130* | 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 30131* | Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
⊢ Ⅎ𝑘𝐹 ⇒ ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑁 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑁)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑁)) | ||
Theorem | esumfsup 30132 | Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
⊢ Ⅎ𝑘𝐹 ⇒ ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < )) | ||
Theorem | esumfsupre 30133 | 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 30134 | Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumpinfval 30135* | 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 30136 | Lemma for esumpfinval 30137. (Contributed by Thierry Arnoux, 28-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → (ℂfld Σg 𝐹) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg 𝐹)) | ||
Theorem | esumpfinval 30137* | 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 30138 | Same as esumpfinval 30137, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | esumpinfsum 30139* | 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 30140* | 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 30141* | The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (1...𝑀)𝐴 ≤ Σ*𝑘 ∈ (1...𝑁)𝐴) | ||
Theorem | esumcocn 30142* | Lemma for esummulc2 30144 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 30143* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) | ||
Theorem | esummulc2 30144* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐶 ·e Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶 ·e 𝐵)) | ||
Theorem | esumdivc 30145* | An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 /𝑒 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 /𝑒 𝐶)) | ||
Theorem | hashf2 30146 | Lemma for hasheuni 30147. (Contributed by Thierry Arnoux, 19-Nov-2016.) |
⊢ #:V⟶(0[,]+∞) | ||
Theorem | hasheuni 30147* | The cardinality of a disjoint union, not necessarily finite. cf. hashuni 14558. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (#‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(#‘𝑥)) | ||
Theorem | esumcvg 30148* | The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 14458. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) | ||
Theorem | esumcvg2 30149* | Simpler version of esumcvg 30148. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵) & ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) | ||
Theorem | esumcvgsum 30150* | The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.) |
⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ∈ ℝ) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) | ||
Theorem | esumsup 30151* | Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴), ℝ*, < )) | ||
Theorem | esumgect 30152* | "Send 𝑛 to +∞ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 ≤ 𝐵) | ||
Theorem | esumcvgre 30153* | All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | ||
Theorem | esum2dlem 30154* | Lemma for esum2d 30155 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐹 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) | ||
Theorem | esum2d 30155* | 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 30156* | Sum over a non necessarily disjoint indexed union. The inegality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶) | ||
Syntax | cofc 30157 | Extend class notation to include mapping of an operation to an operation for a function and a constant. |
class ∘𝑓/𝑐𝑅 | ||
Definition | df-ofc 30158* | Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘𝑓/𝑐𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ ∘𝑓/𝑐𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐))) | ||
Theorem | ofceq 30159 | Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝑅 = 𝑆 → ∘𝑓/𝑐𝑅 = ∘𝑓/𝑐𝑆) | ||
Theorem | ofcfval 30160* | Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcval 30161 | Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹∘𝑓/𝑐𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofcfn 30162 | The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) Fn 𝐴) | ||
Theorem | ofcfeqd2 30163* | Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶)) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝐹∘𝑓/𝑐𝑃𝐶)) | ||
Theorem | ofcfval3 30164* | General value of (𝐹∘𝑓/𝑐𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶))) | ||
Theorem | ofcf 30165* | The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶):𝐴⟶𝑈) | ||
Theorem | ofcfval2 30166* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcfval4 30167* | The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹)) | ||
Theorem | ofcc 30168 | Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵})∘𝑓/𝑐𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | ofcof 30169 | Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝐹 ∘𝑓 𝑅(𝐴 × {𝐶}))) | ||
Syntax | csiga 30170 | Extend class notation to include the function giving the sigma-algebras on a given base set. |
class sigAlgebra | ||
Definition | df-siga 30171* | 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 30172* | Lemma for issiga 30174 and isrnsiga 30176. The class of sigma-algebras with base set 𝑜 is a set. Note: a more generic version with (𝑂 ∈ V → ...) could be useful for sigaval 30173. (Contributed by Thierry Arnoux, 24-Oct-2016.) |
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))} ∈ V | ||
Theorem | sigaval 30173* | The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.) |
⊢ (𝑂 ∈ V → (sigAlgebra‘𝑂) = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}) | ||
Theorem | issiga 30174* | An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (𝑆 ∈ V → (𝑆 ∈ (sigAlgebra‘𝑂) ↔ (𝑆 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | isrnsigaOLD 30175* | The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra ↔ (𝑆 ∈ V ∧ ∃𝑜(𝑆 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑜 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆))))) | ||
Theorem | isrnsiga 30176* | 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 30177 | A sigma-algebra contains the empty set. (Contributed by Thierry Arnoux, 4-Sep-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆) | ||
Theorem | baselsiga 30178 | A sigma-algebra contains its base universe set. (Contributed by Thierry Arnoux, 26-Oct-2016.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝐴 ∈ 𝑆) | ||
Theorem | sigasspw 30179 | A sigma-algebra is a set of subset of the base set. (Contributed by Thierry Arnoux, 18-Jan-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝐴) → 𝑆 ⊆ 𝒫 𝐴) | ||
Theorem | sigaclcu 30180 | A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcuni 30181* | A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | sigaclfu 30182 | A sigma-algebra is closed under finite union. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ∈ Fin) → ∪ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu2 30183* | A sigma-algebra is closed under countable union - indexing on ℕ (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ ℕ 𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆) | ||
Theorem | sigaclfu2 30184* | A sigma-algebra is closed under finite union - indexing on (1..^𝑁). (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ ∀𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) → ∪ 𝑘 ∈ (1..^𝑁)𝐴 ∈ 𝑆) | ||
Theorem | sigaclcu3 30185* | A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀))) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁) → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆) | ||
Theorem | issgon 30186 | 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 30187 | A sigma-algebra is a sigma on its union set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ (sigAlgebra‘∪ 𝑆)) | ||
Theorem | elsigass 30188 | An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → 𝐴 ⊆ ∪ 𝑆) | ||
Theorem | elrnsiga 30189 | Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra) | ||
Theorem | isrnsigau 30190* | The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016.) |
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ (∪ 𝑆 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∪ 𝑆 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆)))) | ||
Theorem | unielsiga 30191 | 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 30192 | 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 30193 | Any power set forms a sigma-algebra. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Revised by Thierry Arnoux, 24-Oct-2016.) |
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂)) | ||
Theorem | prsiga 30194 | The smallest possible sigma-algebra containing 𝑂. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ (𝑂 ∈ 𝑉 → {∅, 𝑂} ∈ (sigAlgebra‘𝑂)) | ||
Theorem | sigaclci 30195 | A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016.) |
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆) | ||
Theorem | difelsiga 30196 | A sigma-algebra is closed under class differences. (Contributed by Thierry Arnoux, 13-Sep-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆) | ||
Theorem | unelsiga 30197 | A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆) | ||
Theorem | inelsiga 30198 | A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆) | ||
Theorem | sigainb 30199 | Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.) |
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴)) | ||
Theorem | insiga 30200 | The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |