P. 451 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45001-45100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rrxngp 45001	Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ NrmGrp)
Theorem	rrxtps 45002	Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝐼 ∈ 𝑉 → (ℝ^‘𝐼) ∈ TopSp)
Theorem	rrxtopnfi 45003*	The topology of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐼 ∈ Fin)    ⇒   ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝐼)) = (MetOpen‘(𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))))
Theorem	rrxtopon 45004	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ (TopOn‘(Base‘(ℝ^‘𝐼))))
Theorem	rrxtop 45005	The topology on generalized Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐽 ∈ Top)
Theorem	rrndistlt 45006*	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 45007	The topology on n-dimensional Euclidean real spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐽 = (TopOpen‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ Fin → 𝐽 ∈ (TopOn‘(ℝ ↑m 𝐼)))
Theorem	rrxunitopnfi 45008	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 45009	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = 𝒫 {∅}
Theorem	qndenserrnbllem 45010*	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 45011*	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 45012	The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (TopOpen‘(ℝ^‘∅)) = {∅, {∅}}
Theorem	qndenserrnopnlem 45013*	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 45014*	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 45015	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 45016*	A multidimensional singleton expressed as a multidimensional closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐴‘𝑘)) = {𝐴})
Theorem	rrnprjdstle 45017	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 45018*	𝐷 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 45019*	𝐷 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 45020*	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 45021*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
Theorem	ioorrnopnxrlem 45022*	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 45023*	The indexed product of open intervals is an open set in (ℝ^‘𝑋). Similar to ioorrnopn 45021 but here unbounded intervals are allowed. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*)    ⇒   ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ (TopOpen‘(ℝ^‘𝑋)))
21.40.19  Basic measure theory
21.40.19.1  σ-Algebras Proofs for most of the theorems in section 111 of [Fremlin1]
Syntax	csalg 45024	Extend class notation with the class of all sigma-algebras.
class SAlg
Definition	df-salg 45025*	Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SAlg = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (∪ 𝑥 ∖ 𝑦) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑥))}
Syntax	csalon 45026	Extend class notation with the class of sigma-algebras on a set.
class SalOn
Definition	df-salon 45027*	Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ SalOn = (𝑥 ∈ V ↦ {𝑠 ∈ SAlg ∣ ∪ 𝑠 = 𝑥})
Syntax	csalgen 45028	Extend class notation with the class of sigma-algebra generator.
class SalGen
Definition	df-salgen 45029*	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 45057. 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 45059. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Glauco Siliprandi, 1-Jan-2021.)
⊢ SalGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠)})
Theorem	issal 45030*	Express the predicate "𝑆 is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ SAlg ↔ (∅ ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 (∪ 𝑆 ∖ 𝑦) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝒫 𝑆(𝑦 ≼ ω → ∪ 𝑦 ∈ 𝑆))))
Theorem	pwsal 45031	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 45032	SAlg sigma-algebra is closed under countable union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑇 ∈ 𝒫 𝑆)    &   ⊢ (𝜑 → 𝑇 ≼ ω)    ⇒   ⊢ (𝜑 → ∪ 𝑇 ∈ 𝑆)
Theorem	saluncl 45033	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	prsal 45034	The pair of the empty set and the whole base is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑋 ∈ 𝑉 → {∅, 𝑋} ∈ SAlg)
Theorem	saldifcl 45035	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	0sal 45036	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∅ ∈ 𝑆)
Theorem	salgenval 45037*	The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) = ∩ {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)})
Theorem	saliunclf 45038	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝑆    &   ⊢ Ⅎ𝑘𝐾    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saliuncl 45039*	SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	salincl 45040	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	saluni 45041	A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑆 ∈ SAlg → ∪ 𝑆 ∈ 𝑆)
Theorem	saliinclf 45042	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑘𝑆    &   ⊢ Ⅎ𝑘𝐾    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ (𝜑 → 𝐾 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saliincl 45043*	SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐾 ≼ ω)    &   ⊢ (𝜑 → 𝐾 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐾) → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆)
Theorem	saldifcl2 45044	The difference of two elements of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆) → (𝐸 ∖ 𝐹) ∈ 𝑆)
Theorem	intsaluni 45045*	The union of an arbitrary intersection of sigma-algebras on the same set 𝑋, is 𝑋. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
Theorem	intsal 45046*	The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 45045). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐺 ⊆ SAlg)    &   ⊢ (𝜑 → 𝐺 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)    ⇒   ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)
Theorem	salgenn0 45047*	The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ SAlg ∣ (∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠)} ≠ ∅)
Theorem	salgencl 45048	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝑋 ∈ 𝑉 → (SalGen‘𝑋) ∈ SAlg)
Theorem	issald 45049*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	salexct 45050*	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 45051	A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆)
Theorem	salgenss 45052	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 45060, 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 45053	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 45054*	One side of dfsalgen2 45057. 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 45055*	An example of a subset that does not belong to a nontrivial sigma-algebra, see salexct 45050. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ 𝐴 = (0[,]2)    &   ⊢ 𝑆 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑥 ≼ ω ∨ (𝐴 ∖ 𝑥) ≼ ω)}    &   ⊢ 𝐵 = (0[,]1)    ⇒   ⊢ ¬ 𝐵 ∈ 𝑆
Theorem	unisalgen 45056	The union of a set belongs to the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    &   ⊢ 𝑈 = ∪ 𝑋    ⇒   ⊢ (𝜑 → 𝑈 ∈ 𝑆)
Theorem	dfsalgen2 45057*	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 45058*	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 45059*	This counterexample shows that df-salgen 45029 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 45060*	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 45061*	Sufficient condition to prove that 𝑆 is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → ∅ ∈ 𝑆)    &   ⊢ 𝑋 = ∪ 𝑆    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝑋 ∖ 𝑦) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	dmvolsal 45062	Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ dom vol ∈ SAlg
Theorem	saldifcld 45063	The complement of an element of a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	saluncld 45064	The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	salgencld 45065	SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑆 = (SalGen‘𝑋)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	0sald 45066	The empty set belongs to every sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑆)
Theorem	iooborel 45067	An open interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝐴(,)𝐶) ∈ 𝐵
Theorem	salincld 45068	The intersection of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∩ 𝐹) ∈ 𝑆)
Theorem	salunid 45069	A set is an element of any sigma-algebra on it. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    ⇒   ⊢ (𝜑 → ∪ 𝑆 ∈ 𝑆)
Theorem	unisalgen2 45070	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 45071	The Borel sigma-algebra on the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ 𝐵 ∈ SAlg
Theorem	iocborel 45072	A left-open, right-closed interval is a Borel set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐵 = (SalGen‘𝐽)    ⇒   ⊢ (𝜑 → (𝐴(,]𝐶) ∈ 𝐵)
Theorem	subsaliuncllem 45073*	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 45074*	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 45075	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 45076	A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑆)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑆 ↾t 𝐴))
Theorem	salrestss 45077	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 𝐸) ⊆ 𝑆)
21.40.19.2  Sum of nonnegative extended reals
Syntax	csumge0 45078	Extend class notation to include the sum of nonnegative extended reals.
class Σ^
Definition	df-sumge0 45079*	Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
Theorem	sge0rnre 45080*	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 45081	If 𝐹 maps to nonnegative reals, then 𝐹 maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
Theorem	sge0val 45082*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝑋⟶(0[,]+∞)) → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑦 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝐹‘𝑤)), ℝ*, < )))
Theorem	fge0npnf 45083	If 𝐹 maps to nonnegative reals, then +∞ is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
Theorem	sge0rnn0 45084*	The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅
Theorem	sge0vald 45085*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = if(+∞ ∈ ran 𝐹, +∞, sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < )))
Theorem	fge0iccico 45086	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))
Theorem	gsumge0cl 45087	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 45088*	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 45089	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 45090	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ)
Theorem	sge0z 45091*	Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 0)) = 0)
Theorem	sge00 45092	The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (Σ^‘∅) = 0
Theorem	fsumlesge0 45093*	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 45094*	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 45095	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{𝐴}⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) = (𝐹‘𝐴))
Theorem	sge0tsms 45096	Σ^ 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 45097	The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞))
Theorem	sge0f1o 45098*	Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = (Σ^‘(𝑛 ∈ 𝐶 ↦ 𝐷)))
Theorem	sge0snmpt 45099*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,]+∞))    &   ⊢ (𝑘 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Σ^‘(𝑘 ∈ {𝐴} ↦ 𝐵)) = 𝐶)
Theorem	sge0ge0 45100	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹))