Home | Metamath
Proof Explorer Theorem List (p. 393 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 | ||
Theorem | ioorrnopn 39201* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋))) | ||
Theorem | ioorrnopnxrlem 39202* | Given a point 𝐹 that belongs to an indexed product of (possibly unbounded) open intervals, then 𝐹 belongs to an open product of bounded open intervals that's a subset of the original indexed product. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) & ⊢ 𝐿 = (𝑖 ∈ 𝑋 ↦ if((𝐴‘𝑖) = -∞, ((𝐹‘𝑖) − 1), (𝐴‘𝑖))) & ⊢ 𝑅 = (𝑖 ∈ 𝑋 ↦ if((𝐵‘𝑖) = +∞, ((𝐹‘𝑖) + 1), (𝐵‘𝑖))) & ⊢ 𝑉 = X𝑖 ∈ 𝑋 ((𝐿‘𝑖)(,)(𝑅‘𝑖)) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) | ||
Theorem | ioorrnopnxr 39203* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 39201 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 39204 | Extend class notation with the class of all sigma-algebras. |
class SAlg | ||
Definition | df-salg 39205* | Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))} | ||
Syntax | csalon 39206 | Extend class notation with the class of sigma-algebras on a set. |
class SalOn | ||
Definition | df-salon 39207* | Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥}) | ||
Syntax | csalgen 39208 | Extend class notation with the class of sigma-algebra generator. |
class SalGen | ||
Definition | df-salgen 39209* | 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 39235. 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 39237. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.) |
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}) | ||
Theorem | issal 39210* | Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆)))) | ||
Theorem | pwsal 39211 | 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 39212 | SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆) & ⊢ (𝜑 → 𝑇 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆) | ||
Theorem | saluncl 39213 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | prsal 39214 | The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg) | ||
Theorem | saldifcl 39215 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | 0sal 39216 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆) | ||
Theorem | salgenval 39217* | The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | ||
Theorem | saliuncl 39218* | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | salincl 39219 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | saluni 39220 | A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | saliincl 39221* | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ (𝜑 → 𝐾 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | saldifcl2 39222 | The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆) | ||
Theorem | intsaluni 39223* | The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) | ||
Theorem | intsal 39224* | The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 39223). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg) | ||
Theorem | salgenn0 39225* | The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) | ||
Theorem | salgencl 39226 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg) | ||
Theorem | issald 39227* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | salexct 39228* | An example of non trivial 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 39229 | A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆) | ||
Theorem | salgenss 39230 | 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 39238, 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 39231 | 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 39232* | One side of dfsalgen2 39235. 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 39233* | An example of a subset that does not belong to a non trivial sigma-algebra, see salexct 39228. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝐴 = (0[,]2) & ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} & ⊢ 𝐵 = (0[,]1) ⇒ ⊢ ¬ 𝐵 ∈ 𝑆 | ||
Theorem | unisalgen 39234 | The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) & ⊢ 𝑈 = ∪ 𝑋 ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | dfsalgen2 39235* | 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 39236* | 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 39237* | This counterexample shows that df-salgen 39209 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 39238* | 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 39239* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | dmvolsal 39240 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ dom vol ∈ SAlg | ||
Theorem | saldifcld 39241 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | saluncld 39242 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | salgencld 39243 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | 0sald 39244 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
Theorem | iooborel 39245 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝐴(,)𝐶) ∈ 𝐵 | ||
Theorem | salincld 39246 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | salunid 39247 | A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | unisalgen2 39248 | 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 39249 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ 𝐵 ∈ SAlg | ||
Theorem | iocborel 39250 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵) | ||
Theorem | subsaliuncllem 39251* | 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 𝐺(𝐻‘𝑦) ∈ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ (𝑆 ↑𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) | ||
Theorem | subsaliuncl 39252* | 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 39253 | 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 39254 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴)) | ||
Syntax | csumge0 39255 | Extend class notation to include the sum of nonnegative extended reals. |
class Σ^ | ||
Definition | df-sumge0 39256* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))) | ||
Theorem | sge0rnre 39257* | 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 39258 | If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | ||
Theorem | sge0val 39259* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ))) | ||
Theorem | fge0npnf 39260 | If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0rnn0 39261* | The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ | ||
Theorem | sge0vald 39262* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ))) | ||
Theorem | fge0iccico 39263 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | ||
Theorem | gsumge0cl 39264 | 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 39265* | 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 39266 | 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 39267 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | ||
Theorem | sge0z 39268* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0) | ||
Theorem | sge00 39269 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (Σ^‘∅) = 0 | ||
Theorem | fsumlesge0 39270* | 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 39271* | 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 39272 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | sge0tsms 39273 | Σ^ 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 39274 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞)) | ||
Theorem | sge0f1o 39275* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0snmpt 39276* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0 39277 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0xrcl 39278 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) | ||
Theorem | sge0repnf 39279 | 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 39280* | 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 39281 | If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0supre 39282* | 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 39284, but here we can use sup with respect to ℝ instead of ℝ* (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | ||
Theorem | sge0fsummpt 39283* | 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 39284* | 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 39285 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹)) | ||
Theorem | sge0rnbnd 39286* | 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 39287* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerp 39288* | The arbitrary sum of nonnegative extended reals is larger 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 39289* | 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 39290 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ) | ||
Theorem | sge0lefi 39291* | 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 39292* | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ≤ (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵))) | ||
Theorem | sge0ltfirp 39293* | 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 39294* | 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 39287. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) ≤ (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerpmpt 39295* | The arbitrary sum of nonnegative extended reals is larger 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 39296 | The sum of nonnegative extended reals restricted to the range of a function is less 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 39297 | The sum of nonnegative extended reals restricted to the range of a function is less 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 39298* | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (Σ^‘(𝑥 ∈ 𝐶 ↦ 𝐵)) ∈ ℝ) | ||
Theorem | sge0resplit 39299 | Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 39302. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑈 = (𝐴 ∪ 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = ((Σ^‘(𝐹 ↾ 𝐴)) + (Σ^‘(𝐹 ↾ 𝐵)))) | ||
Theorem | sge0le 39300* | If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐺:𝑋⟶(0[,]+∞)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ≤ (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ≤ (Σ^‘𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |