Home | Metamath
Proof Explorer Theorem List (p. 295 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ind 29401* | Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.) |
⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
Theorem | indv 29402* | Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0)))) | ||
Theorem | indval 29403* | Value of the indicator function generator for a set 𝐴 and a domain 𝑂. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0))) | ||
Theorem | indval2 29404 | Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0}))) | ||
Theorem | indf 29405 | An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1}) | ||
Theorem | indfval 29406 | Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0)) | ||
Theorem | pr01ssre 29407 | The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ {0, 1} ⊆ ℝ | ||
Theorem | ind1 29408 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1) | ||
Theorem | ind0 29409 | Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0) | ||
Theorem | ind1a 29410 | Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴)) | ||
Theorem | indpi1 29411 | Preimage of the singleton {1} by the indicator function. See i1f1lem 23262. (Contributed by Thierry Arnoux, 21-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴) | ||
Theorem | indsum 29412* | Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ (𝜑 → 𝑂 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝑂) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵) | ||
Theorem | indf1o 29413 | The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0, 1} ↑𝑚 𝑂)) | ||
Theorem | indpreima 29414 | A function with range {0, 1} as an indicator of the preimage of {1}. (Contributed by Thierry Arnoux, 23-Aug-2017.) |
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1}))) | ||
Theorem | indf1ofs 29415* | The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑𝑚 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin}) | ||
Syntax | cesum 29416 | Extend class notation to include infinite summations. |
class Σ*𝑘 ∈ 𝐴𝐵 | ||
Definition | df-esum 29417 | Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.) |
⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | esumex 29418 | An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ Σ*𝑘 ∈ 𝐴𝐵 ∈ V | ||
Theorem | esumcl 29419* | Closure for extended sum in the extended positive reals. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞)) | ||
Theorem | esumeq12dvaf 29420 | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 26-Mar-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq12dva 29421* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) (Revised by Thierry Arnoux, 29-Jun-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq12d 29422* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐷) | ||
Theorem | esumeq1 29423* | Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) |
⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumeq1d 29424 | Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumeq2 29425* | Equality theorem for extended sum. (Contributed by Thierry Arnoux, 24-Dec-2016.) |
⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2d 29426 | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 21-Sep-2016.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2dv 29427* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumeq2sdv 29428* | Equality deduction for extended sum. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | nfesum1 29429 | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ Ⅎ𝑘Σ*𝑘 ∈ 𝐴𝐵 | ||
Theorem | nfesum2 29430* | Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥Σ*𝑘 ∈ 𝐴𝐵 | ||
Theorem | cbvesum 29431* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ Ⅎ𝑗𝐶 ⇒ ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶 | ||
Theorem | cbvesumv 29432* | Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (𝑗 = 𝑘 → 𝐵 = 𝐶) ⇒ ⊢ Σ*𝑗 ∈ 𝐴𝐵 = Σ*𝑘 ∈ 𝐴𝐶 | ||
Theorem | esumid 29433 | 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 29434 | 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 29435* | Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠 ↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) = 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ 𝐶), ℝ*, < )) | ||
Theorem | esumel 29436* | 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 29437 | Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017.) |
⊢ Σ*𝑥 ∈ ∅𝐴 = 0 | ||
Theorem | esum0 29438* | Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
⊢ Ⅎ𝑘𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → Σ*𝑘 ∈ 𝐴0 = 0) | ||
Theorem | esumf1o 29439* | Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐵 & ⊢ Ⅎ𝑘𝐷 & ⊢ Ⅎ𝑛𝐴 & ⊢ Ⅎ𝑛𝐶 & ⊢ Ⅎ𝑛𝐹 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑛 ∈ 𝐶𝐷) | ||
Theorem | esumc 29440* | Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑘𝐷 & ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝑦 = 𝐶 → 𝐷 = 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡(𝑘 ∈ 𝐴 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ*𝑦 ∈ {𝑧 ∣ ∃𝑘 ∈ 𝐴 𝑧 = 𝐶}𝐷) | ||
Theorem | esumrnmpt 29441* | 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 29442 | Split an extended sum into two parts. (Contributed by Thierry Arnoux, 9-May-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ*𝑘 ∈ 𝐴𝐶 +𝑒 Σ*𝑘 ∈ 𝐵𝐶)) | ||
Theorem | esummono 29443* | Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ≤ Σ*𝑘 ∈ 𝐶𝐵) | ||
Theorem | esumpad 29444* | Extend an extended sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 31-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumpad2 29445* | Remove zeroes from an extended sum. (Contributed by Thierry Arnoux, 5-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (𝐴 ∖ 𝐵)𝐶 = Σ*𝑘 ∈ 𝐴𝐶) | ||
Theorem | esumadd 29446* | Addition of infinite sums. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶)) | ||
Theorem | esumle 29447* | 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 29448* | 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 29449* | 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 29450* | Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴(𝐵 +𝑒 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 +𝑒 Σ*𝑘 ∈ 𝐴𝐶)) | ||
Theorem | esumlef 29451* | 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 29452* | The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (0[,]+∞)) → Σ*𝑘 ∈ 𝐴𝐵 = ((#‘𝐴) ·e 𝐵)) | ||
Theorem | esumsnf 29453* | 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 29454* | 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 29455* | Extended sum over a pair. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸)) | ||
Theorem | esumpr2 29456* | Extended sum over a pair, with a relaxed condition compared to esumpr 29455. (Contributed by Thierry Arnoux, 2-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝜑 → (𝐴 = 𝐵 → (𝐷 = 0 ∨ 𝐷 = +∞))) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 +𝑒 𝐸)) | ||
Theorem | esumrnmpt2 29457* | 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 29458* | Formulating a partial extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
⊢ Ⅎ𝑘𝐹 ⇒ ⊢ ((𝐹:ℕ⟶(0[,]+∞) ∧ 𝑁 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑁)(𝐹‘𝑘) = (seq1( +𝑒 , 𝐹)‘𝑁)) | ||
Theorem | esumfsup 29459 | Formulating an extended sum over integers using the recursive sequence builder. (Contributed by Thierry Arnoux, 18-Oct-2017.) |
⊢ Ⅎ𝑘𝐹 ⇒ ⊢ (𝐹:ℕ⟶(0[,]+∞) → Σ*𝑘 ∈ ℕ(𝐹‘𝑘) = sup(ran seq1( +𝑒 , 𝐹), ℝ*, < )) | ||
Theorem | esumfsupre 29460 | 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 29461 | Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝐵 & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) | ||
Theorem | esumpinfval 29462* | 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 29463 | Lemma for esumpfinval 29464. (Contributed by Thierry Arnoux, 28-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,)+∞)) → (ℂfld Σg 𝐹) = ((ℝ*𝑠 ↾s (0[,]+∞)) Σg 𝐹)) | ||
Theorem | esumpfinval 29464* | 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 29465 | Same as esumpfinval 29464, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Proof shortened by AV, 25-Jul-2019.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | esumpinfsum 29466* | 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 29467* | 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 29468* | The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ (1...𝑀)𝐴 ≤ Σ*𝑘 ∈ (1...𝑁)𝐴) | ||
Theorem | esumcocn 29469* | Lemma for esummulc2 29471 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 29470* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) | ||
Theorem | esummulc2 29471* | An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → (𝐶 ·e Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴(𝐶 ·e 𝐵)) | ||
Theorem | esumdivc 29472* | An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 /𝑒 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 /𝑒 𝐶)) | ||
Theorem | hashf2 29473 | Lemma for hasheuni 29474. (Contributed by Thierry Arnoux, 19-Nov-2016.) |
⊢ #:V⟶(0[,]+∞) | ||
Theorem | hasheuni 29474* | The cardinality of a disjoint union, not necessarily finite. cf. hashuni 14397. (Contributed by Thierry Arnoux, 19-Nov-2016.) (Revised by Thierry Arnoux, 2-Jan-2017.) (Revised by Thierry Arnoux, 20-Jun-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Disj 𝑥 ∈ 𝐴 𝑥) → (#‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(#‘𝑥)) | ||
Theorem | esumcvg 29475* | The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 14305. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) | ||
Theorem | esumcvg2 29476* | Simpler version of esumcvg 29475. (Contributed by Thierry Arnoux, 5-Sep-2017.) |
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵) & ⊢ (𝑘 = 𝑚 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴)(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) | ||
Theorem | esumcvgsum 29477* | The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019.) |
⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝐿) & ⊢ (𝜑 → 𝐿 ∈ ℝ) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) | ||
Theorem | esumsup 29478* | Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑛 ∈ ℕ ↦ Σ*𝑘 ∈ (1...𝑛)𝐴), ℝ*, < )) | ||
Theorem | esumgect 29479* | "Send 𝑛 to +∞ " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 ≤ 𝐵) | ||
Theorem | esumcvgre 29480* | All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) | ||
Theorem | esum2dlem 29481* | Lemma for esum2d 29482 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.) |
⊢ Ⅎ𝑘𝐹 & ⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐹 = 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) | ||
Theorem | esum2d 29482* | 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 29483* | 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 29484 | Extend class notation to include mapping of an operation to an operation for a function and a constant. |
class ∘𝑓/𝑐𝑅 | ||
Definition | df-ofc 29485* | 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 29486 | Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝑅 = 𝑆 → ∘𝑓/𝑐𝑅 = ∘𝑓/𝑐𝑆) | ||
Theorem | ofcfval 29487* | Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcval 29488 | Evaluate a function/constant operation at a point. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹∘𝑓/𝑐𝑅𝐶)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofcfn 29489 | The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) Fn 𝐴) | ||
Theorem | ofcfeqd2 29490* | Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦𝑅𝐶) = (𝑦𝑃𝐶)) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝐹∘𝑓/𝑐𝑃𝐶)) | ||
Theorem | ofcfval3 29491* | General value of (𝐹∘𝑓/𝑐𝑅𝐶) with no assumptions on functionality of 𝐹. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ dom 𝐹 ↦ ((𝐹‘𝑥)𝑅𝐶))) | ||
Theorem | ofcf 29492* | The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶):𝐴⟶𝑈) | ||
Theorem | ofcfval2 29493* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofcfval4 29494* | The function/constant operation expressed as an operation composition. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = ((𝑥 ∈ 𝐵 ↦ (𝑥𝑅𝐶)) ∘ 𝐹)) | ||
Theorem | ofcc 29495 | Left operation by a constant on a mixed operation with a constant. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵})∘𝑓/𝑐𝑅𝐶) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | ofcof 29496 | Relate function operation with operation with a constant. (Contributed by Thierry Arnoux, 3-Oct-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹∘𝑓/𝑐𝑅𝐶) = (𝐹 ∘𝑓 𝑅(𝐴 × {𝐶}))) | ||
Syntax | csiga 29497 | Extend class notation to include the function giving the sigma-algebras on a given base set. |
class sigAlgebra | ||
Definition | df-siga 29498* | 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 29499* | Lemma for issiga 29501 and isrnsiga 29503. The class of sigma-algebras with base set 𝑜 is a set. Note: a more generic version with (𝑂 ∈ V → ...) could be useful for sigaval 29500. (Contributed by Thierry Arnoux, 24-Oct-2016.) |
⊢ {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑜 ∧ (𝑜 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑜 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))} ∈ V | ||
Theorem | sigaval 29500* | The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016.) |
⊢ (𝑂 ∈ V → (sigAlgebra‘𝑂) = {𝑠 ∣ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |