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	sxuni 34201	The base set of a product sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑇 ∈ ∪ ran sigAlgebra) → (∪ 𝑆 × ∪ 𝑇) = ∪ (𝑆 ×s 𝑇))
Theorem	elsx 34202	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 34203	Extend class notation to include the class of measures.
class measures
Definition	df-meas 34204*	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 34205	The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑆 ∈ ∪ ran sigAlgebra)
Theorem	measval 34206*	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 34207*	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 34208*	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 34209	The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018.)
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
Theorem	measbasedom 34210	The base set of a measure is its domain. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀))
Theorem	measfrge0 34211	A measure is a function over its base to the positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀:𝑆⟶(0[,]+∞))
Theorem	measfn 34212	A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)
⊢ (𝑀 ∈ (measures‘𝑆) → 𝑀 Fn 𝑆)
Theorem	measvxrge0 34213	The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	measvnul 34214	The measure of the empty set is always zero. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ (𝑀 ∈ (measures‘𝑆) → (𝑀‘∅) = 0)
Theorem	measge0 34215	A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → 0 ≤ (𝑀‘𝐴))
Theorem	measle0 34216	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 34217*	The measure of a countable disjoint union is the sum of the measures. (Contributed by Thierry Arnoux, 26-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝒫 𝑆 ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝑥)) → (𝑀‘∪ 𝐴) = Σ*𝑥 ∈ 𝐴(𝑀‘𝑥))
Theorem	measxun2 34218	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵))))
Theorem	measun 34219	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measvunilem 34220*	Lemma for measvuni 34222. (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 34221*	Lemma for measvuni 34222. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ {∅} ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvuni 34222*	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 34223	A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	measunl 34224	A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measiuns 34225*	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 34226 and meascnbl 34227. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝐼)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑁 𝐴) = Σ*𝑛 ∈ 𝑁(𝑀‘(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
Theorem	measiun 34226*	A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ Σ*𝑛 ∈ ℕ(𝑀‘𝐵))
Theorem	meascnbl 34227*	A measure is continuous from below. Cf. volsup 25482. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ (𝜑 → (𝑀 ∘ 𝐹)(⇝𝑡‘𝐽)(𝑀‘∪ ran 𝐹))
Theorem	measinblem 34228*	Lemma for measinb 34229. (Contributed by Thierry Arnoux, 2-Jun-2017.)
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) ∧ 𝐵 ∈ 𝒫 𝑆) ∧ (𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥)) → (𝑀‘(∪ 𝐵 ∩ 𝐴)) = Σ*𝑥 ∈ 𝐵(𝑀‘(𝑥 ∩ 𝐴)))
Theorem	measinb 34229*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘𝑆))
Theorem	measres 34230	Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))
Theorem	measinb2 34231*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ (𝑆 ∩ 𝒫 𝐴) ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘(𝑆 ∩ 𝒫 𝐴)))
Theorem	measdivcst 34232	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 34233*	Alternate version of measdivcst 34232. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
21.3.18.7  The counting measure
Theorem	cntmeas 34234	The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (♯ ↾ 𝑆) ∈ (measures‘𝑆))
Theorem	pwcntmeas 34235	The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (♯ ↾ 𝒫 𝑂) ∈ (measures‘𝒫 𝑂))
Theorem	cntnevol 34236	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 34237	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 25431 and voliun 25480. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
Theorem	volfiniune 34238*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 25473 what voliune 34237 is to voliun 25480. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵))
Theorem	volmeas 34239	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 34240	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 34241	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
Theorem	ddeval1 34242	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ 0 ∈ 𝐴) → (δ‘𝐴) = 1)
Theorem	ddeval0 34243	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴) → (δ‘𝐴) = 0)
Theorem	ddemeas 34244	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 34245	Extend class notation to include the 'almost everywhere' relation.
class a.e.
Syntax	cfae 34246	Extend class notation to include the 'almost everywhere' builder.
class ~ a.e.
Definition	df-ae 34247*	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 34248	'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ Rel a.e.
Theorem	brae 34249	'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 34250*	'almost everywhere' relation for a measure 𝑀 and a property 𝜑 (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    ⇒   ⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0))
Theorem	truae 34251*	A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀)
Theorem	aean 34252*	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 34253*	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 34254*	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 34255	The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ((𝑅 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → Rel (𝑅~ a.e.𝑀))
Theorem	brfae 34256*	'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 34257	Extend class notation with the measurable functions builder.
class MblFnM
Definition	df-mbfm 34258*	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 25545. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ MblFnM = (𝑠 ∈ ∪ ran sigAlgebra, 𝑡 ∈ ∪ ran sigAlgebra ↦ {𝑓 ∈ (∪ 𝑡 ↑m ∪ 𝑠) ∣ ∀𝑥 ∈ 𝑡 (◡𝑓 “ 𝑥) ∈ 𝑠})
Theorem	ismbfm 34259*	The predicate "𝐹 is a measurable function from the measurable space 𝑆 to the measurable space 𝑇". Cf. ismbf 25554. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑m ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)))
Theorem	elunirnmbfm 34260*	The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝐹 ∈ ∪ ran MblFnM ↔ ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑m ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠))
Theorem	mbfmfun 34261	A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	mbfmf 34262	A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → 𝐹:∪ 𝑆⟶∪ 𝑇)
Theorem	mbfmcnvima 34263	The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝑆)
Theorem	isanmbfm 34264	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 34265	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 34266	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 34267*	A constant function is measurable. Cf. mbfconst 25559. (Contributed by Thierry Arnoux, 26-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ∪ 𝑆 ↦ 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑇)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))
Theorem	1stmbfm 34268	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 34269	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 34270*	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 34271	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 34272	The composition of two measurable functions is measurable. See cnmpt11 23576. (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝑅MblFnM𝑇))
Theorem	mbfmco2 34273*	The pair building of two measurable functions is measurable. ( cf. cnmpt1t 23578). (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑅MblFnM𝑇))    &   ⊢ 𝐻 = (𝑥 ∈ ∪ 𝑅 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑅MblFnM(𝑆 ×s 𝑇)))
Theorem	mbfmvolf 34274	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𝔅ℝ) → 𝐹:ℝ⟶ℝ)
Theorem	elmbfmvol2 34275	Measurable functions with respect to the Lebesgue measure. We only have the inclusion, since MblFn includes complex-valued functions. (Contributed by Thierry Arnoux, 26-Jan-2017.)
⊢ (𝐹 ∈ (dom volMblFnM𝔅ℝ) → 𝐹 ∈ MblFn)
Theorem	mbfmcnt 34276	All functions are measurable with respect to the counting measure. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂MblFnM𝔅ℝ) = (ℝ ↑m 𝑂))
21.3.18.12  Borel Algebra on ` ( RR X. RR ) `
Theorem	br2base 34277*	The base set for the generator of the Borel sigma-algebra on (ℝ × ℝ) is indeed (ℝ × ℝ). (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ∪ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦ (𝑥 × 𝑦)) = (ℝ × ℝ)
Theorem	dya2ub 34278	An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ (𝑅 ∈ ℝ+ → (1 / (2↑(⌊‘(1 − (2 logb 𝑅))))) < 𝑅)
Theorem	sxbrsigalem0 34279*	The closed half-spaces of (ℝ × ℝ) cover (ℝ × ℝ). (Contributed by Thierry Arnoux, 11-Oct-2017.)
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) = (ℝ × ℝ)
Theorem	sxbrsigalem3 34280*	The sigma-algebra generated by the closed half-spaces of (ℝ × ℝ) is a subset of the sigma-algebra generated by the closed sets of (ℝ × ℝ). (Contributed by Thierry Arnoux, 11-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞))))) ⊆ (sigaGen‘(Clsd‘(𝐽 ×t 𝐽)))
Theorem	dya2iocival 34281*	The function 𝐼 returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl 25526. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) = ((𝑋 / (2↑𝑁))[,)((𝑋 + 1) / (2↑𝑁))))
Theorem	dya2iocress 34282*	Dyadic intervals are subsets of ℝ. (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ⊆ ℝ)
Theorem	dya2iocbrsiga 34283*	Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ∈ 𝔅ℝ)
Theorem	dya2icobrsiga 34284*	Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 13-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ran 𝐼 ⊆ 𝔅ℝ
Theorem	dya2icoseg 34285*	For any point and any closed-below, open-above interval of ℝ centered on that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑁 = (⌊‘(1 − (2 logb 𝐷)))    ⇒   ⊢ ((𝑋 ∈ ℝ ∧ 𝐷 ∈ ℝ+) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ((𝑋 − 𝐷)(,)(𝑋 + 𝐷))))
Theorem	dya2icoseg2 34286*	For any point and any open interval of ℝ containing that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 12-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸) → ∃𝑏 ∈ ran 𝐼(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸))
Theorem	dya2iocrfn 34287*	The function returning dyadic square covering for a given size has domain (ran 𝐼 × ran 𝐼). (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ 𝑅 Fn (ran 𝐼 × ran 𝐼)
Theorem	dya2iocct 34288*	The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ ran 𝑅 ≼ ω
Theorem	dya2iocnrect 34289*	For any point of an open rectangle in (ℝ × ℝ), there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (Contributed by Thierry Arnoux, 12-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    &   ⊢ 𝐵 = ran (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓))    ⇒   ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴))
Theorem	dya2iocnei 34290*	For any point of an open set of the usual topology on (ℝ × ℝ) there is a closed-below open-above dyadic rational square which contains that point and is entirely in the open set. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴))
Theorem	dya2iocuni 34291*	Every open set of (ℝ × ℝ) is a union of closed-below open-above dyadic rational rectangular subsets of (ℝ × ℝ). This union must be a countable union by dya2iocct 34288. (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (𝐴 ∈ (𝐽 ×t 𝐽) → ∃𝑐 ∈ 𝒫 ran 𝑅∪ 𝑐 = 𝐴)
Theorem	dya2iocucvr 34292*	The dyadic rectangular set collection covers (ℝ × ℝ). (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ ∪ ran 𝑅 = (ℝ × ℝ)
Theorem	sxbrsigalem1 34293*	The Borel algebra on (ℝ × ℝ) is a subset of the sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ). This is a step of the proof of Proposition 1.1.5 of [Cohn] p. 4. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (sigaGen‘ran 𝑅)
Theorem	sxbrsigalem2 34294*	The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ) is a subset of the sigma-algebra generated by the closed half-spaces of (ℝ × ℝ). The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (sigaGen‘ran 𝑅) ⊆ (sigaGen‘(ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))))
Theorem	sxbrsigalem4 34295*	The Borel algebra on (ℝ × ℝ) is generated by the dyadic closed-below, open-above rectangular subsets of (ℝ × ℝ). Proposition 1.1.5 of [Cohn] p. 4 . Note that the interval used in this formalization are closed-below, open-above instead of open-below, closed-above in the proof as they are ultimately generated by the floor function. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (sigaGen‘(𝐽 ×t 𝐽)) = (sigaGen‘ran 𝑅)
Theorem	sxbrsigalem5 34296*	First direction for sxbrsiga 34298. (Contributed by Thierry Arnoux, 22-Sep-2017.) (Revised by Thierry Arnoux, 11-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (𝔅ℝ ×s 𝔅ℝ)
Theorem	sxbrsigalem6 34297	First direction for sxbrsiga 34298, same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (𝔅ℝ ×s 𝔅ℝ)
Theorem	sxbrsiga 34298	The product sigma-algebra (𝔅ℝ ×s 𝔅ℝ) is the Borel algebra on (ℝ × ℝ) See example 5.1.1 of [Cohn] p. 143 . (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝔅ℝ ×s 𝔅ℝ) = (sigaGen‘(𝐽 ×t 𝐽))
21.3.18.13  Caratheodory's extension theorem In this section, we define a function toOMeas which constructs an outer measure, from a pre-measure 𝑅. An explicit generic definition of an outer measure is not given. It consists of the three following statements: - the outer measure of an empty set is zero (oms0 34305) - it is monotone (omsmon 34306) - it is countably sub-additive (omssubadd 34308) See Definition 1.11.1 of [Bogachev] p. 41.
Syntax	coms 34299	Class declaration for the outer measure construction function.
class toOMeas
Definition	df-oms 34300*	Define a function constructing an outer measure. See omsval 34301 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))