| Metamath
Proof Explorer Theorem List (p. 464 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rrxtps 46301 | Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp) | ||
| Theorem | rrxtopnfi 46302* | The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐼 ∈ Fin) ⇒ ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))) | ||
| Theorem | rrxtopon 46303 | The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼)))) | ||
| Theorem | rrxtop 46304 | The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top) | ||
| Theorem | rrndistlt 46305* | Given two points in the space of n-dimensional real numbers, if every component is closer than 𝐸 then the distance between the two points is less then ((√‘𝑛) · 𝐸). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ 𝑁 = (♯‘𝐼) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝐼)) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑌‘𝑖))) < 𝐸) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝜑 → (𝑋𝐷𝑌) < ((√‘𝑁) · 𝐸)) | ||
| Theorem | rrxtoponfi 46306 | The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑m 𝐼))) | ||
| Theorem | rrxunitopnfi 46307 | The base set of the standard topology on the space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝑋 ∈ Fin → ∪ (TopOpen‘(ℝ^‘𝑋)) = (ℝ ↑m 𝑋)) | ||
| Theorem | rrxtopn0 46308 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅} | ||
| Theorem | qndenserrnbllem 46309* | 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) & ⊢ (𝜑 → 𝐼 ≠ ∅) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
| Theorem | qndenserrnbl 46310* | 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) & ⊢ (𝜑 → 𝑋 ∈ (ℝ ↑m 𝐼)) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑m 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) | ||
| Theorem | rrxtopn0b 46311 | The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}} | ||
| Theorem | qndenserrnopnlem 46312* | 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 46313* | 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 46314 | 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 46315* | A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴}) | ||
| Theorem | rrnprjdstle 46316 | 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 46317* | 𝐷 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 46318* | 𝐷 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 46319* | 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 46320* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋))) | ||
| Theorem | ioorrnopnxrlem 46321* | 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 46322* | The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 46320 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 46323 | Extend class notation with the class of all sigma-algebras. |
| class SAlg | ||
| Definition | df-salg 46324* | Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))} | ||
| Syntax | csalon 46325 | Extend class notation with the class of sigma-algebras on a set. |
| class SalOn | ||
| Definition | df-salon 46326* | Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥}) | ||
| Syntax | csalgen 46327 | Extend class notation with the class of sigma-algebra generator. |
| class SalGen | ||
| Definition | df-salgen 46328* | 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 46356. 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 46358. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.) |
| ⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)}) | ||
| Theorem | issal 46329* | Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆)))) | ||
| Theorem | pwsal 46330 | 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 46331 | SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆) & ⊢ (𝜑 → 𝑇 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆) | ||
| Theorem | saluncl 46332 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
| Theorem | prsal 46333 | The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg) | ||
| Theorem | saldifcl 46334 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
| Theorem | 0sal 46335 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆) | ||
| Theorem | salgenval 46336* | The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)}) | ||
| Theorem | saliunclf 46337 | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝑆 & ⊢ Ⅎ𝑘𝐾 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
| Theorem | saliuncl 46338* | SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
| Theorem | salincl 46339 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
| Theorem | saluni 46340 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆) | ||
| Theorem | saliinclf 46341 | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝑆 & ⊢ Ⅎ𝑘𝐾 & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ (𝜑 → 𝐾 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
| Theorem | saliincl 46342* | SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐾 ≼ ω) & ⊢ (𝜑 → 𝐾 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆) | ||
| Theorem | saldifcl2 46343 | The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆) | ||
| Theorem | intsaluni 46344* | The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) | ||
| Theorem | intsal 46345* | The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 46344). (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐺 ⊆ SAlg) & ⊢ (𝜑 → 𝐺 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ⇒ ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg) | ||
| Theorem | salgenn0 46346* | The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅) | ||
| Theorem | salgencl 46347 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg) | ||
| Theorem | issald 46348* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
| Theorem | salexct 46349* | 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 46350 | A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆) | ||
| Theorem | salgenss 46351 | 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 46359, 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 46352 | 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 46353* | One side of dfsalgen2 46356. 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 46354* | An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 46349. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ 𝐴 = (0[,]2) & ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)} & ⊢ 𝐵 = (0[,]1) ⇒ ⊢ ¬ 𝐵 ∈ 𝑆 | ||
| Theorem | unisalgen 46355 | The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) & ⊢ 𝑈 = ∪ 𝑋 ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝑆) | ||
| Theorem | dfsalgen2 46356* | 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 46357* | 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 46358* | This counterexample shows that df-salgen 46328 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 46359* | 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 46360* | Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → ∅ ∈ 𝑆) & ⊢ 𝑋 = ∪ 𝑆 & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
| Theorem | dmvolsal 46361 | Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ dom vol ∈ SAlg | ||
| Theorem | saldifcld 46362 | The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
| Theorem | saluncld 46363 | The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
| Theorem | salgencld 46364 | SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑆 = (SalGen‘𝑋) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
| Theorem | 0sald 46365 | The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∅ ∈ 𝑆) | ||
| Theorem | iooborel 46366 | An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝐴(,)𝐶) ∈ 𝐵 | ||
| Theorem | salincld 46367 | The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆) | ||
| Theorem | salunid 46368 | A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) ⇒ ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆) | ||
| Theorem | unisalgen2 46369 | 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 46370 | The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ 𝐵 ∈ SAlg | ||
| Theorem | iocborel 46371 | A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐵 = (SalGen‘𝐽) ⇒ ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵) | ||
| Theorem | subsaliuncllem 46372* | 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 46373* | 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 46374 | 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 46375 | A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴)) | ||
| Theorem | salrestss 46376 | A sigma-algebra restricted to one of its elements is a subset of the original sigma-algebra. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
| ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑆 ↾t 𝐸) ⊆ 𝑆) | ||
| Syntax | csumge0 46377 | Extend class notation to include the sum of nonnegative extended reals. |
| class Σ^ | ||
| Definition | df-sumge0 46378* | Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $. |
| ⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))) | ||
| Theorem | sge0rnre 46379* | 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 46380 | If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | ||
| Theorem | sge0val 46381* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < ))) | ||
| Theorem | fge0npnf 46382 | If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) ⇒ ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) | ||
| Theorem | sge0rnn0 46383* | The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅ | ||
| Theorem | sge0vald 46384* | The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ))) | ||
| Theorem | fge0iccico 46385 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞)) | ||
| Theorem | gsumge0cl 46386 | 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 46387* | 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 46388 | 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 46389 | A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) | ||
| Theorem | sge0z 46390* | Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0) | ||
| Theorem | sge00 46391 | The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (Σ^‘∅) = 0 | ||
| Theorem | fsumlesge0 46392* | 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 46393* | 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 46394 | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴)) | ||
| Theorem | sge0tsms 46395 | Σ^ 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 46396 | The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞)) | ||
| Theorem | sge0f1o 46397* | Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑛𝜑 & ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷))) | ||
| Theorem | sge0snmpt 46398* | A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞)) & ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶) | ||
| Theorem | sge0ge0 46399 | The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) | ||
| Theorem | sge0xrcl 46400 | The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |