P. 348 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34701-34800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	difelsiga 34701	A sigma-algebra is closed under class differences. The proof goes through difunielsiga 34699 and unelsiga 34700 rather than countable intersection, and so does not use ax-ac 10509. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Proof shortened by Vincent Gonzalez, 17-Aug-2026.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelsiga 34702	A sigma-algebra is closed under pairwise intersections. (Contributed by Thierry Arnoux, 13-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigainb 34703	Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (𝑆 ∩ 𝒫 𝐴) ∈ (sigAlgebra‘𝐴))
Theorem	insiga 34704	The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
21.3.18.2  Generated sigma-Algebra
Syntax	csigagen 34705	Extend class notation to include the sigma-algebra generator.
class sigaGen
Definition	df-sigagen 34706*	Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})
Theorem	sigagenval 34707*	Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠})
Theorem	sigagensiga 34708	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) ∈ (sigAlgebra‘∪ 𝐴))
Theorem	sgsiga 34709	A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (sigaGen‘𝐴) ∈ ∪ ran sigAlgebra)
Theorem	unisg 34710	The sigma-algebra generated by a collection 𝐴 is a sigma-algebra on ∪ 𝐴. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ (𝐴 ∈ 𝑉 → ∪ (sigaGen‘𝐴) = ∪ 𝐴)
Theorem	dmsigagen 34711	A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ dom sigaGen = V
Theorem	sssigagen 34712	A set is a subset of the sigma-algebra it generates. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (sigaGen‘𝐴))
Theorem	sssigagen2 34713	A subset of the generating set is also a subset of the generated sigma-algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ (sigaGen‘𝐴))
Theorem	elsigagen 34714	Any element of a set is also an element of the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 27-Mar-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ (sigaGen‘𝐴))
Theorem	elsigagen2 34715	Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≼ ω) → ∪ 𝐵 ∈ (sigaGen‘𝐴))
Theorem	sigagenss 34716	The generated sigma-algebra is a subset of all sigma-algebras containing the generating set, i.e. the generated sigma-algebra is the smallest sigma-algebra containing the generating set, here 𝐴. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ ((𝑆 ∈ (sigAlgebra‘∪ 𝐴) ∧ 𝐴 ⊆ 𝑆) → (sigaGen‘𝐴) ⊆ 𝑆)
Theorem	sigagenss2 34717	Sufficient condition for inclusion of sigma-algebras. This is used to prove equality of sigma-algebras. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ ((∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ (sigaGen‘𝐵) ∧ 𝐵 ∈ 𝑉) → (sigaGen‘𝐴) ⊆ (sigaGen‘𝐵))
Theorem	sigagenid 34718	The sigma-algebra generated by a sigma-algebra is itself. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (sigaGen‘𝑆) = 𝑆)
21.3.18.3  lambda and pi-Systems, Rings of Sets Because they are not widely used outside of measure theory, we do not introduce specific definitions for lambda- and pi-systems. Instead, we define 𝑃 and 𝐿 respectively as the classes of pi- and lambda-systems in 𝑂 throughout this section.
Theorem	ispisys 34719*	The property of being a pi-system. (Contributed by Thierry Arnoux, 10-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑆) ⊆ 𝑆))
Theorem	ispisys2 34720*	The property of being a pi-system, expanded version. Pi-systems are closed under finite intersections. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (𝑆 ∈ 𝑃 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∀𝑥 ∈ ((𝒫 𝑆 ∩ Fin) ∖ {∅})∩ 𝑥 ∈ 𝑆))
Theorem	inelpisys 34721*	Pi-systems are closed under pairwise intersections. (Contributed by Thierry Arnoux, 6-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ ((𝑆 ∈ 𝑃 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	sigapisys 34722*	All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝑃
Theorem	isldsys 34723*	The property of being a lambda-system or Dynkin system. Lambda-systems contain the empty set, are closed under complement, and closed under countable disjoint union. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝐿 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (𝑂 ∖ 𝑥) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑆))))
Theorem	pwldsys 34724*	The power set of the universe set 𝑂 is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿)
Theorem	unelldsys 34725*	Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	sigaldsys 34726*	All sigma-algebras are lambda-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) ⊆ 𝐿
Theorem	ldsysgenld 34727*	The intersection of all lambda-systems containing a given collection of sets 𝐴, which is called the lambda-system generated by 𝐴, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑂)    ⇒   ⊢ (𝜑 → ∩ {𝑡 ∈ 𝐿 ∣ 𝐴 ⊆ 𝑡} ∈ 𝐿)
Theorem	sigapildsyslem 34728*	Lemma for sigapildsys 34729. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑡 ∈ (𝑃 ∩ 𝐿))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑡)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐵 ∈ 𝑡)    ⇒   ⊢ (𝜑 → (𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵) ∈ 𝑡)
Theorem	sigapildsys 34729*	Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    ⇒   ⊢ (sigAlgebra‘𝑂) = (𝑃 ∩ 𝐿)
Theorem	ldgenpisyslem1 34730*	Lemma for ldgenpisys 34733. (Contributed by Thierry Arnoux, 29-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    ⇒   ⊢ (𝜑 → {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸} ∈ 𝐿)
Theorem	ldgenpisyslem2 34731*	Lemma for ldgenpisys 34733. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐸)    &   ⊢ (𝜑 → 𝑇 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisyslem3 34732*	Lemma for ldgenpisys 34733. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → 𝐸 ⊆ {𝑏 ∈ 𝒫 𝑂 ∣ (𝐴 ∩ 𝑏) ∈ 𝐸})
Theorem	ldgenpisys 34733*	The lambda system 𝐸 generated by a pi-system 𝑇 is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ 𝐸 = ∩ {𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡}    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑃)
Theorem	dynkin 34734*	Dynkin's lambda-pi theorem: if a lambda-system contains a pi-system, it also contains the sigma-algebra generated by that pi-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
⊢ 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}    &   ⊢ 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → ∪ 𝑥 ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐿)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑃)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ∩ {𝑢 ∈ (sigAlgebra‘𝑂) ∣ 𝑇 ⊆ 𝑢} ⊆ 𝑆)
Theorem	isros 34735*	The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ((𝑢 ∪ 𝑣) ∈ 𝑆 ∧ (𝑢 ∖ 𝑣) ∈ 𝑆)))
Theorem	rossspw 34736*	A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elros 34737*	A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆)
Theorem	unelros 34738*	A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	difelros 34739*	A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelros 34740*	A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	fiunelros 34741*	A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)
Theorem	issros 34742*	The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧))))
Theorem	srossspw 34743*	A semiring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elsros 34744*	A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆)
Theorem	inelsros 34745*	A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	diffiunisros 34746*	In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))
Theorem	rossros 34747*	Rings of sets are semirings of sets. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ∈ 𝑁)
21.3.18.4  The Borel algebra on the real numbers
Syntax	cbrsiga 34748	The Borel Algebra on real numbers, usually a gothic B
class 𝔅ℝ
Definition	df-brsiga 34749	A Borel Algebra is defined as a sigma-algebra generated by a topology. 'The' Borel sigma-algebra here refers to the sigma-algebra generated by the topology of open intervals on real numbers. The Borel algebra of a given topology 𝐽 is the sigma-algebra generated by 𝐽, (sigaGen‘𝐽), so there is no need to introduce a special constant function for Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ = (sigaGen‘(topGen‘ran (,)))
Theorem	brsiga 34750	The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigaGen “ Top)
Theorem	brsigarn 34751	The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigAlgebra‘ℝ)
Theorem	brsigasspwrn 34752	The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ 𝔅ℝ ⊆ 𝒫 ℝ
Theorem	unibrsiga 34753	The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ∪ 𝔅ℝ = ℝ
Theorem	cldssbrsiga 34754	A Borel Algebra contains all closed sets of its base topology. (Contributed by Thierry Arnoux, 27-Mar-2017.)
⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
21.3.18.5  Product Sigma-Algebra
Syntax	csx 34755	Extend class notation with the product sigma-algebra operation.
class ×s
Definition	df-sx 34756*	Define the product sigma-algebra operation, analogous to df-tx 23843. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))))
Theorem	sxval 34757*	Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ 𝐴 = ran (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑇 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ×s 𝑇) = (sigaGen‘𝐴))
Theorem	sxsiga 34758	A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra)
Theorem	sxsigon 34759	A product sigma-algebra is a sigma-algebra on the product of the bases. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ (sigAlgebra‘(∪ 𝑆 × ∪ 𝑇)))
Theorem	sxuni 34760	The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇))
Theorem	elsx 34761	The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → (𝐴 × 𝐵) ∈ (𝑆 ×s 𝑇))
21.3.18.6  Measures
Syntax	cmeas 34762	Extend class notation to include the class of measures.
class measures
Definition	df-meas 34763*	Define a measure as a nonnegative countably additive function over a sigma-algebra onto (0[,]+∞). (Contributed by Thierry Arnoux, 10-Sep-2016.)
⊢ measures = (𝑠 ∈ ∪ ran sigAlgebra ↦ {𝑚 ∣ (𝑚:𝑠⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
Theorem	measbase 34764	The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	measval 34765*	The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (measures‘𝑆) = {𝑚 ∣ (𝑚:𝑆⟶(0[,]+∞) ∧ (𝑚‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑚‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑚‘𝑦)))})
Theorem	ismeas 34766*	The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Revised by Thierry Arnoux, 19-Oct-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (𝑀 ∈ (measures‘𝑆) ↔ (𝑀:𝑆⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 𝑆((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))))
Theorem	isrnmeas 34767*	The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures → (dom 𝑀 ∈ ∪ ran sigAlgebra ∧ (𝑀:dom 𝑀⟶(0[,]+∞) ∧ (𝑀‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)))))
Theorem	dmmeas 34768	The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
Theorem	measbasedom 34769	The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀))
Theorem	measfrge0 34770	A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
Theorem	measfn 34771	A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 Fn 𝑆)
Theorem	measvxrge0 34772	The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	measvnul 34773	The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
Theorem	measge0 34774	A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝑀‘𝐴))
Theorem	measle0 34775	If the measure of a given set is bounded by zero, it is zero. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ≤ 0) → (𝑀‘𝐴) = 0)
Theorem	measvun 34776*	The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑀‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑀‘𝑥))
Theorem	measxun2 34777	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵))))
Theorem	measun 34778	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measvunilem 34779*	Lemma for measvuni 34781. (Contributed by Thierry Arnoux, 7-Feb-2017.) (Revised by Thierry Arnoux, 19-Feb-2017.) (Revised by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑆 ∖ {∅}) ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvunilem0 34780*	Lemma for measvuni 34781. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ {∅} ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvuni 34781*	The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of 𝑆. (Contributed by Thierry Arnoux, 7-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measssd 34782	A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	measunl 34783	A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measiuns 34784*	The measure of the union of a collection of sets, expressed as the sum of a disjoint set. This is used as a lemma for both measiun 34785 and meascnbl 34786. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝐼)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑁 𝐴) = Σ*𝑛 ∈ 𝑁(𝑀‘(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
Theorem	measiun 34785*	A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ Σ*𝑛 ∈ ℕ(𝑀‘𝐵))
Theorem	meascnbl 34786*	A measure is continuous from below. Cf. volsup 25839. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ (𝜑 → (𝑀 ∘ 𝐹)(⇝𝑡‘𝐽)(𝑀‘∪ ran 𝐹))
Theorem	measinblem 34787*	Lemma for measinb 34788. (Contributed by Thierry Arnoux, 2-Jun-2017.)
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) ∧ 𝐵 ∈ 𝒫 𝑆) ∧ (𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥)) → (𝑀‘(∪ 𝐵 ∩ 𝐴)) = Σ*𝑥 ∈ 𝐵(𝑀‘(𝑥 ∩ 𝐴)))
Theorem	measinb 34788*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘𝑆))
Theorem	measres 34789	Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))
Theorem	measinb2 34790*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ (𝑆 ∩ 𝒫 𝐴) ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘(𝑆 ∩ 𝒫 𝐴)))
Theorem	measdivcst 34791	Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (Revised by Thierry Arnoux, 30-Jan-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑀 ∘f/c /𝑒 𝐴) ∈ (measures‘𝑆))
Theorem	measdivcstALTV 34792*	Alternate version of measdivcst 34791. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
21.3.18.7  The counting measure
Theorem	cntmeas 34793	The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (♯ ↾ 𝑆) ∈ (measures‘𝑆))
Theorem	pwcntmeas 34794	The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (♯ ↾ 𝒫 𝑂) ∈ (measures‘𝒫 𝑂))
Theorem	cntnevol 34795	Counting and Lebesgue measures are different. (Contributed by Thierry Arnoux, 27-Jan-2017.)
⊢ (♯ ↾ 𝒫 𝑂) ≠ vol
21.3.18.8  The Lebesgue measure - misc additions
Theorem	voliune 34796	The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +∞ for the measure of any set in the sum. Cf. ovoliun 25788 and voliun 25837. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
Theorem	volfiniune 34797*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 25830 what voliune 34796 is to voliun 25837. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵))
Theorem	volmeas 34798	The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ vol ∈ (measures‘dom vol)
21.3.18.9  The Dirac delta measure
Syntax	cdde 34799	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 34800	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))