Home | Metamath
Proof Explorer Theorem List (p. 427 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rrxtopn0b 42601 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}} | ||
Theorem | qndenserrnopnlem 42602* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrnopn 42603* | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ 𝑉) | ||
Theorem | qndenserrn 42604 | n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘(ℚ ↑m 𝐼)) = (ℝ ↑m 𝐼)) | ||
Theorem | rrxsnicc 42605* | A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴}) | ||
Theorem | rrnprjdstle 42606 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐺:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ 𝐷 = (dist‘(ℝ^‘𝑋)) ⇒ ⊢ (𝜑 → (abs‘((𝐹‘𝐼) − (𝐺‘𝐼))) ≤ (𝐹𝐷𝐺)) | ||
Theorem | rrndsmet 42607* | 𝐷 is a metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ ↑m 𝑋))) | ||
Theorem | rrndsxmet 42608* | 𝐷 is an extended metric for the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ ↑m 𝑋))) | ||
Theorem | ioorrnopnlem 42609* | The a point in an indexed product of open intervals is contained in an open ball that is contained in the indexed product of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖))) & ⊢ 𝐻 = ran (𝑖 ∈ 𝑋 ↦ if(((𝐵‘𝑖) − (𝐹‘𝑖)) ≤ ((𝐹‘𝑖) − (𝐴‘𝑖)), ((𝐵‘𝑖) − (𝐹‘𝑖)), ((𝐹‘𝑖) − (𝐴‘𝑖)))) & ⊢ 𝐸 = inf(𝐻, ℝ, < ) & ⊢ 𝑉 = (𝐹(ball‘𝐷)𝐸) & ⊢ 𝐷 = (𝑓 ∈ (ℝ ↑m 𝑋), 𝑔 ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑘 ∈ 𝑋 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (TopOpen‘(ℝ^‘𝑋))(𝐹 ∈ 𝑣 ∧ 𝑣 ⊆ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)))) | ||
Theorem | ioorrnopn 42610* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋))) | ||
Theorem | ioorrnopnxrlem 42611* | 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 42612* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 42610 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 42613 | Extend class notation with the class of all sigma-algebras. |
class SAlg | ||
Definition | df-salg 42614* | Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))} | ||
Syntax | csalon 42615 | Extend class notation with the class of sigma-algebras on a set. |
class SalOn | ||
Definition | df-salon 42616* | Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥}) | ||
Syntax | csalgen 42617 | Extend class notation with the class of sigma-algebra generator. |
class SalGen | ||
Definition | df-salgen 42618* | 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 42644. 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 42646. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.) |
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}) | ||
Theorem | issal 42619* | Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆)))) | ||
Theorem | pwsal 42620 | 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 42621 | SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆) & ⊢ (𝜑 → 𝑇 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆) | ||
Theorem | saluncl 42622 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | prsal 42623 | The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg) | ||
Theorem | saldifcl 42624 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | 0sal 42625 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆) | ||
Theorem | salgenval 42626* | The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | ||
Theorem | saliuncl 42627* | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | salincl 42628 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | saluni 42629 | A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | saliincl 42630* | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ (𝜑 → 𝐾 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
Theorem | saldifcl2 42631 | The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆) | ||
Theorem | intsaluni 42632* | The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) | ||
Theorem | intsal 42633* | The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 42632). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg) | ||
Theorem | salgenn0 42634* | The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) | ||
Theorem | salgencl 42635 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg) | ||
Theorem | issald 42636* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | salexct 42637* | An example of nontrivial sigma-algebra: the collection of all subsets which either are countable or have countable complement. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | sssalgen 42638 | A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆) | ||
Theorem | salgenss 42639 | 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 42647, 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 42640 | 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 42641* | One side of dfsalgen2 42644. 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 42642* | An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 42637. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ 𝐴 = (0[,]2) & ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} & ⊢ 𝐵 = (0[,]1) ⇒ ⊢ ¬ 𝐵 ∈ 𝑆 | ||
Theorem | unisalgen 42643 | The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) & ⊢ 𝑈 = ∪ 𝑋 ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
Theorem | dfsalgen2 42644* | 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 42645* | 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 42646* | This counterexample shows that df-salgen 42618 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 42647* | 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 42648* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | dmvolsal 42649 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ dom vol ∈ SAlg | ||
Theorem | saldifcld 42650 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | saluncld 42651 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | salgencld 42652 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | 0sald 42653 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
Theorem | iooborel 42654 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝐴(,)𝐶) ∈ 𝐵 | ||
Theorem | salincld 42655 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
Theorem | salunid 42656 | A set is an element of any sigma-algebra on it . (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | unisalgen2 42657 | 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 42658 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ 𝐵 ∈ SAlg | ||
Theorem | iocborel 42659 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵) | ||
Theorem | subsaliuncllem 42660* | A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) & ⊢ 𝐸 = (𝐻 ∘ 𝐺) & ⊢ (𝜑 → 𝐻 Fn ran 𝐺) & ⊢ (𝜑 → ∀𝑦 ∈ ran 𝐺(𝐻‘𝑦) ∈ 𝑦) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) | ||
Theorem | subsaliuncl 42661* | 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 42662 | 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 42663 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴)) | ||
Syntax | csumge0 42664 | Extend class notation to include the sum of nonnegative extended reals. |
class Σ^ | ||
Definition | df-sumge0 42665* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))) | ||
Theorem | sge0rnre 42666* | 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 42667 | If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | ||
Theorem | sge0val 42668* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ))) | ||
Theorem | fge0npnf 42669 | If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0rnn0 42670* | The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ | ||
Theorem | sge0vald 42671* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ))) | ||
Theorem | fge0iccico 42672 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | ||
Theorem | gsumge0cl 42673 | 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 42674* | 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 42675 | 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 42676 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | ||
Theorem | sge0z 42677* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0) | ||
Theorem | sge00 42678 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (Σ^‘∅) = 0 | ||
Theorem | fsumlesge0 42679* | 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 42680* | 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 42681 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴)) | ||
Theorem | sge0tsms 42682 | Σ^ 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 42683 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞)) | ||
Theorem | sge0f1o 42684* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
Theorem | sge0snmpt 42685* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
Theorem | sge0ge0 42686 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0xrcl 42687 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) | ||
Theorem | sge0repnf 42688 | 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 42689* | 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 42690 | If the sum of nonnegative extended reals is not +∞ then no terms is +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
Theorem | sge0supre 42691* | 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 42693, but here we can use sup with respect to ℝ instead of ℝ* (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )) | ||
Theorem | sge0fsummpt 42692* | 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 42693* | 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 42694 | A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ≤ (Σ^‘𝐹)) | ||
Theorem | sge0rnbnd 42695* | 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 42696* | Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐸 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑘 = 𝐵 → 𝐶 = 𝐸) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴, 𝐵} ↦ 𝐶)) = (𝐷 +𝑒 𝐸)) | ||
Theorem | sge0gerp 42697* | The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑧 ∈ (𝒫 𝑋 ∩ Fin)𝐴 ≤ ((Σ^‘(𝐹 ↾ 𝑧)) +𝑒 𝑥)) ⇒ ⊢ (𝜑 → 𝐴 ≤ (Σ^‘𝐹)) | ||
Theorem | sge0pnffigt 42698* | 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 42699 | If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝐹 ↾ 𝑌)) ∈ ℝ) | ||
Theorem | sge0lefi 42700* | 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)(Σ^‘(𝐹 ↾ 𝑥)) ≤ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |