P. 343 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dynkin 34201*	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 34202*	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 34203*	A ring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elros 34204*	A ring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ (𝑆 ∈ 𝑄 → ∅ ∈ 𝑆)
Theorem	unelros 34205*	A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∪ 𝐵) ∈ 𝑆)
Theorem	difelros 34206*	A ring of sets is closed under set complement. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)
Theorem	inelros 34207*	A ring of sets is closed under intersection. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    ⇒   ⊢ ((𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	fiunelros 34208*	A ring of sets is closed under finite union. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ 𝑄 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∪ 𝑦) ∈ 𝑠 ∧ (𝑥 ∖ 𝑦) ∈ 𝑠))}    &   ⊢ (𝜑 → 𝑆 ∈ 𝑄)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (1..^𝑁)) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (1..^𝑁)𝐵 ∈ 𝑆)
Theorem	issros 34209*	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 34210*	A semiring of sets is a collection of subsets of 𝑂. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → 𝑆 ⊆ 𝒫 𝑂)
Theorem	0elsros 34211*	A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ (𝑆 ∈ 𝑁 → ∅ ∈ 𝑆)
Theorem	inelsros 34212*	A semiring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020.)
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))}    ⇒   ⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∩ 𝐵) ∈ 𝑆)
Theorem	diffiunisros 34213*	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 34214*	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 34215	The Borel Algebra on real numbers, usually a gothic B
class 𝔅ℝ
Definition	df-brsiga 34216	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 34217	The Borel Algebra on real numbers is a Borel sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigaGen “ Top)
Theorem	brsigarn 34218	The Borel Algebra is a sigma-algebra on the real numbers. (Contributed by Thierry Arnoux, 27-Dec-2016.)
⊢ 𝔅ℝ ∈ (sigAlgebra‘ℝ)
Theorem	brsigasspwrn 34219	The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017.)
⊢ 𝔅ℝ ⊆ 𝒫 ℝ
Theorem	unibrsiga 34220	The union of the Borel Algebra is the set of real numbers. (Contributed by Thierry Arnoux, 21-Jan-2017.)
⊢ ∪ 𝔅ℝ = ℝ
Theorem	cldssbrsiga 34221	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 34222	Extend class notation with the product sigma-algebra operation.
class ×s
Definition	df-sx 34223*	Define the product sigma-algebra operation, analogous to df-tx 23478. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ×s = (𝑠 ∈ V, 𝑡 ∈ V ↦ (sigaGen‘ran (𝑥 ∈ 𝑠, 𝑦 ∈ 𝑡 ↦ (𝑥 × 𝑦))))
Theorem	sxval 34224*	Value of the product sigma-algebra operation. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ 𝐴 = ran (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑇 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ×s 𝑇) = (sigaGen‘𝐴))
Theorem	sxsiga 34225	A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (𝑆 ×s 𝑇) ∈ ∪ ran sigAlgebra)
Theorem	sxsigon 34226	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 34227	The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇))
Theorem	elsx 34228	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 34229	Extend class notation to include the class of measures.
class measures
Definition	df-meas 34230*	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 34231	The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	measval 34232*	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 34233*	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 34234*	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 34235	The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
Theorem	measbasedom 34236	The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀))
Theorem	measfrge0 34237	A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
Theorem	measfn 34238	A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 Fn 𝑆)
Theorem	measvxrge0 34239	The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	measvnul 34240	The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
Theorem	measge0 34241	A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝑀‘𝐴))
Theorem	measle0 34242	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 34243*	The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑀‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑀‘𝑥))
Theorem	measxun2 34244	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵))))
Theorem	measun 34245	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measvunilem 34246*	Lemma for measvuni 34248. (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 34247*	Lemma for measvuni 34248. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ {∅} ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvuni 34248*	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 34249	A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	measunl 34250	A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measiuns 34251*	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 34252 and meascnbl 34253. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝐼)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑁 𝐴) = Σ*𝑛 ∈ 𝑁(𝑀‘(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
Theorem	measiun 34252*	A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ Σ*𝑛 ∈ ℕ(𝑀‘𝐵))
Theorem	meascnbl 34253*	A measure is continuous from below. Cf. volsup 25485. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ (𝜑 → (𝑀 ∘ 𝐹)(⇝𝑡‘𝐽)(𝑀‘∪ ran 𝐹))
Theorem	measinblem 34254*	Lemma for measinb 34255. (Contributed by Thierry Arnoux, 2-Jun-2017.)
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) ∧ 𝐵 ∈ 𝒫 𝑆) ∧ (𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥)) → (𝑀‘(∪ 𝐵 ∩ 𝐴)) = Σ*𝑥 ∈ 𝐵(𝑀‘(𝑥 ∩ 𝐴)))
Theorem	measinb 34255*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘𝑆))
Theorem	measres 34256	Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))
Theorem	measinb2 34257*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ (𝑆 ∩ 𝒫 𝐴) ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘(𝑆 ∩ 𝒫 𝐴)))
Theorem	measdivcst 34258	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 34259*	Alternate version of measdivcst 34258. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
21.3.18.7  The counting measure
Theorem	cntmeas 34260	The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (♯ ↾ 𝑆) ∈ (measures‘𝑆))
Theorem	pwcntmeas 34261	The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (♯ ↾ 𝒫 𝑂) ∈ (measures‘𝒫 𝑂))
Theorem	cntnevol 34262	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 34263	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 25434 and voliun 25483. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
Theorem	volfiniune 34264*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 25476 what voliune 34263 is to voliun 25483. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵))
Theorem	volmeas 34265	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 34266	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 34267	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
Theorem	ddeval1 34268	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ 0 ∈ 𝐴) → (δ‘𝐴) = 1)
Theorem	ddeval0 34269	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴) → (δ‘𝐴) = 0)
Theorem	ddemeas 34270	The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ ∈ (measures‘𝒫 ℝ)
21.3.18.10  The 'almost everywhere' relation
Syntax	cae 34271	Extend class notation to include the 'almost everywhere' relation.
class a.e.
Syntax	cfae 34272	Extend class notation to include the 'almost everywhere' builder.
class ~ a.e.
Definition	df-ae 34273*	Define 'almost everywhere' with regard to a measure 𝑀. A property holds almost everywhere if the measure of the set where it does not hold has measure zero. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0}
Theorem	relae 34274	'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ Rel a.e.
Theorem	brae 34275	'almost everywhere' relation for a measure and a measurable set 𝐴. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ((𝑀 ∈ ∪ ran measures ∧ 𝐴 ∈ dom 𝑀) → (𝐴a.e.𝑀 ↔ (𝑀‘(∪ dom 𝑀 ∖ 𝐴)) = 0))
Theorem	braew 34276*	'almost everywhere' relation for a measure 𝑀 and a property 𝜑 (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    ⇒   ⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0))
Theorem	truae 34277*	A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀)
Theorem	aean 34278*	A conjunction holds almost everywhere if and only if both its terms do. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    ⇒   ⊢ ((𝑀 ∈ ∪ ran measures ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜑} ∈ dom 𝑀 ∧ {𝑥 ∈ 𝑂 ∣ ¬ 𝜓} ∈ dom 𝑀) → ({𝑥 ∈ 𝑂 ∣ (𝜑 ∧ 𝜓)}a.e.𝑀 ↔ ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ∧ {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀)))
Definition	df-fae 34279*	Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of 𝑓 and 𝑔 is enforced in order to ensure the resulting relation is a set. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ~ a.e. = (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})
Theorem	faeval 34280*	Value of the 'almost everywhere' relation for a given relation and measure. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ((𝑅 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → (𝑅~ a.e.𝑀) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑅 ↑m ∪ dom 𝑀) ∧ 𝑔 ∈ (dom 𝑅 ↑m ∪ dom 𝑀)) ∧ {𝑥 ∈ ∪ dom 𝑀 ∣ (𝑓‘𝑥)𝑅(𝑔‘𝑥)}a.e.𝑀)})
Theorem	relfae 34281	The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ((𝑅 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → Rel (𝑅~ a.e.𝑀))
Theorem	brfae 34282*	'almost everywhere' relation for two functions 𝐹 and 𝐺 with regard to the measure 𝑀. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ dom 𝑅 = 𝐷    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 ↑m ∪ dom 𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 ↑m ∪ dom 𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑅~ a.e.𝑀)𝐺 ↔ {𝑥 ∈ ∪ dom 𝑀 ∣ (𝐹‘𝑥)𝑅(𝐺‘𝑥)}a.e.𝑀))
21.3.18.11  Measurable functions
Syntax	cmbfm 34283	Extend class notation with the measurable functions builder.
class MblFnM
Definition	df-mbfm 34284*	Define the measurable function builder, which generates the set of measurable functions from a measurable space to another one. Here, the measurable spaces are given using their sigma-algebras 𝑠 and 𝑡, and the spaces themselves are recovered by ∪ 𝑠 and ∪ 𝑡. Note the similarities between the definition of measurable functions in measure theory, and of continuous functions in topology. This is the definition for the generic measure theory. For the specific case of functions from ℝ to ℂ, see df-mbf 25548. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ MblFnM = (𝑠 ∈ ∪ ran sigAlgebra, 𝑡 ∈ ∪ ran sigAlgebra ↦ {𝑓 ∈ (∪ 𝑡 ↑m ∪ 𝑠) ∣ ∀𝑥 ∈ 𝑡 (◡𝑓 “ 𝑥) ∈ 𝑠})
Theorem	ismbfm 34285*	The predicate "𝐹 is a measurable function from the measurable space 𝑆 to the measurable space 𝑇". Cf. ismbf 25557. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑m ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)))
Theorem	elunirnmbfm 34286*	The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝐹 ∈ ∪ ran MblFnM ↔ ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑m ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠))
Theorem	mbfmfun 34287	A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	mbfmf 34288	A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → 𝐹:∪ 𝑆⟶∪ 𝑇)
Theorem	mbfmcnvima 34289	The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝑆)
Theorem	isanmbfm 34290	The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017.) Remove hypotheses. (Revised by SN, 13-Jan-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)
Theorem	mbfmbfmOLD 34291	A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM(sigaGen‘𝐽)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)
Theorem	mbfmbfm 34292	A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017.) Remove hypotheses. (Revised by SN, 13-Jan-2025.)
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM(sigaGen‘𝐽)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)
Theorem	mbfmcst 34293*	A constant function is measurable. Cf. mbfconst 25562. (Contributed by Thierry Arnoux, 26-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ∪ 𝑆 ↦ 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑇)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))
Theorem	1stmbfm 34294	The first projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    ⇒   ⊢ (𝜑 → (1st ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑆))
Theorem	2ndmbfm 34295	The second projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    ⇒   ⊢ (𝜑 → (2nd ↾ (∪ 𝑆 × ∪ 𝑇)) ∈ ((𝑆 ×s 𝑇)MblFnM𝑇))
Theorem	imambfm 34296*	If the sigma-algebra in the range of a given function is generated by a collection of basic sets 𝐾, then to check the measurability of that function, we need only consider inverse images of basic sets 𝑎. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝐾 ∈ V)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 = (sigaGen‘𝐾))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹:∪ 𝑆⟶∪ 𝑇 ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝑆)))
Theorem	cnmbfm 34297	A continuous function is measurable with respect to the Borel Algebra of its domain and range. (Contributed by Thierry Arnoux, 3-Jun-2017.)
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑆 = (sigaGen‘𝐽))    &   ⊢ (𝜑 → 𝑇 = (sigaGen‘𝐾))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))
Theorem	mbfmco 34298	The composition of two measurable functions is measurable. See cnmpt11 23579. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝑅MblFnM𝑇))
Theorem	mbfmco2 34299*	The pair building of two measurable functions is measurable. ( cf. cnmpt1t 23581). (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑅MblFnM𝑇))    &   ⊢ 𝐻 = (𝑥 ∈ ∪ 𝑅 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑅MblFnM(𝑆 ×s 𝑇)))
Theorem	mbfmvolf 34300	Measurable functions with respect to the Lebesgue measure are real-valued functions on the real numbers. (Contributed by Thierry Arnoux, 27-Mar-2017.)
⊢ (𝐹 ∈ (dom volMblFnM𝔅ℝ) → 𝐹:ℝ⟶ℝ)