P. 305 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30401-30500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	measxun2 30401	The measure the union of two complementary sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ 𝐵 ⊆ 𝐴) → (𝑀‘𝐴) = ((𝑀‘𝐵) +𝑒 (𝑀‘(𝐴 ∖ 𝐵))))
Theorem	measun 30402	The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measvunilem 30403*	Lemma for measvuni 30405. (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 30404*	Lemma for measvuni 30405. (Contributed by Thierry Arnoux, 6-Mar-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ((𝑀 ∈ (measures‘𝑆) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ {∅} ∧ (𝐴 ≼ ω ∧ Disj 𝑥 ∈ 𝐴 𝐵)) → (𝑀‘∪ 𝑥 ∈ 𝐴 𝐵) = Σ*𝑥 ∈ 𝐴(𝑀‘𝐵))
Theorem	measvuni 30405*	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 30406	A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	measunl 30407	A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	measiuns 30408*	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 30409 and meascnbl 30410. (Contributed by Thierry Arnoux, 22-Jan-2017.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝐼)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑁) → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑁 𝐴) = Σ*𝑛 ∈ 𝑁(𝑀‘(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)))
Theorem	measiun 30409*	A measure is sub-additive. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Proof shortened by Thierry Arnoux, 7-Feb-2017.)
⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑛 ∈ ℕ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ Σ*𝑛 ∈ ℕ(𝑀‘𝐵))
Theorem	meascnbl 30410*	A measure is continuous from below. Cf. volsup 23370. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
⊢ 𝐽 = (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞)))    &   ⊢ (𝜑 → 𝑀 ∈ (measures‘𝑆))    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ (𝜑 → (𝑀 ∘ 𝐹)(⇝𝑡‘𝐽)(𝑀‘∪ ran 𝐹))
Theorem	measinblem 30411*	Lemma for measinb 30412. (Contributed by Thierry Arnoux, 2-Jun-2017.)
⊢ ((((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) ∧ 𝐵 ∈ 𝒫 𝑆) ∧ (𝐵 ≼ ω ∧ Disj 𝑥 ∈ 𝐵 𝑥)) → (𝑀‘(∪ 𝐵 ∩ 𝐴)) = Σ*𝑥 ∈ 𝐵(𝑀‘(𝑥 ∩ 𝐴)))
Theorem	measinb 30412*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ 𝑆 ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘𝑆))
Theorem	measres 30413	Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆) → (𝑀 ↾ 𝑇) ∈ (measures‘𝑇))
Theorem	measinb2 30414*	Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆) → (𝑥 ∈ (𝑆 ∩ 𝒫 𝐴) ↦ (𝑀‘(𝑥 ∩ 𝐴))) ∈ (measures‘(𝑆 ∩ 𝒫 𝐴)))
Theorem	measdivcstOLD 30415*	Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 𝐴)) ∈ (measures‘𝑆))
Theorem	measdivcst 30416	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‘𝑆) ∧ 𝐴 ∈ ℝ+) → (𝑀∘𝑓/𝑐 /𝑒 𝐴) ∈ (measures‘𝑆))
20.3.16.7  The counting measure
Theorem	cntmeas 30417	The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016.)
⊢ (𝑆 ∈ ∪ ran sigAlgebra → (# ↾ 𝑆) ∈ (measures‘𝑆))
Theorem	pwcntmeas 30418	The counting measure is a measure on any power set. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (# ↾ 𝒫 𝑂) ∈ (measures‘𝒫 𝑂))
Theorem	cntnevol 30419	Counting and Lebesgue measures are different. (Contributed by Thierry Arnoux, 27-Jan-2017.)
⊢ (# ↾ 𝒫 𝑂) ≠ vol
20.3.16.8  The Lebesgue measure - misc additions
Theorem	voliune 30420	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 23319 and voliun 23368. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
Theorem	volfiniune 30421*	The Lebesgue measure function is countably additive. This theorem is to volfiniun 23361 what voliune 30420 is to voliun 23368. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol ∧ Disj 𝑛 ∈ 𝐴 𝐵) → (vol‘∪ 𝑛 ∈ 𝐴 𝐵) = Σ*𝑛 ∈ 𝐴(vol‘𝐵))
Theorem	volmeas 30422	The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.)
⊢ vol ∈ (measures‘dom vol)
20.3.16.9  The Dirac delta measure
Syntax	cdde 30423	Extend class notation to include the Dirac delta measure.
class δ
Definition	df-dde 30424	Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
Theorem	ddeval1 30425	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ 0 ∈ 𝐴) → (δ‘𝐴) = 1)
Theorem	ddeval0 30426	Value of the delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ ((𝐴 ⊆ ℝ ∧ ¬ 0 ∈ 𝐴) → (δ‘𝐴) = 0)
Theorem	ddemeas 30427	The Dirac delta measure is a measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ δ ∈ (measures‘𝒫 ℝ)
20.3.16.10  The 'almost everywhere' relation
Syntax	cae 30428	Extend class notation to include the 'almost everywhere' relation.
class a.e.
Syntax	cfae 30429	Extend class notation to include the 'almost everywhere' builder.
class ~ a.e.
Definition	df-ae 30430*	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 30431	'almost everywhere' is a relation. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ Rel a.e.
Theorem	brae 30432	'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 30433*	'almost everywhere' relation for a measure 𝑀 and a property 𝜑 (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    ⇒   ⊢ (𝑀 ∈ ∪ ran measures → ({𝑥 ∈ 𝑂 ∣ 𝜑}a.e.𝑀 ↔ (𝑀‘{𝑥 ∈ 𝑂 ∣ ¬ 𝜑}) = 0))
Theorem	truae 30434*	A truth holds almost everywhere. (Contributed by Thierry Arnoux, 20-Oct-2017.)
⊢ ∪ dom 𝑀 = 𝑂    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑂 ∣ 𝜓}a.e.𝑀)
Theorem	aean 30435*	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 30436*	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 𝑟 ↑𝑚 ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑𝑚 ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})
Theorem	faeval 30437*	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 𝑅 ↑𝑚 ∪ dom 𝑀) ∧ 𝑔 ∈ (dom 𝑅 ↑𝑚 ∪ dom 𝑀)) ∧ {𝑥 ∈ ∪ dom 𝑀 ∣ (𝑓‘𝑥)𝑅(𝑔‘𝑥)}a.e.𝑀)})
Theorem	relfae 30438	The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ ((𝑅 ∈ V ∧ 𝑀 ∈ ∪ ran measures) → Rel (𝑅~ a.e.𝑀))
Theorem	brfae 30439*	'almost everywhere' relation for two functions 𝐹 and 𝐺 with regard to the measure 𝑀. (Contributed by Thierry Arnoux, 22-Oct-2017.)
⊢ dom 𝑅 = 𝐷    &   ⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐷 ↑𝑚 ∪ dom 𝑀))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐷 ↑𝑚 ∪ dom 𝑀))    ⇒   ⊢ (𝜑 → (𝐹(𝑅~ a.e.𝑀)𝐺 ↔ {𝑥 ∈ ∪ dom 𝑀 ∣ (𝐹‘𝑥)𝑅(𝐺‘𝑥)}a.e.𝑀))
20.3.16.11  Measurable functions
Syntax	cmbfm 30440	Extend class notation with the measurable functions builder.
class MblFnM
Definition	df-mbfm 30441*	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 23433. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ MblFnM = (𝑠 ∈ ∪ ran sigAlgebra, 𝑡 ∈ ∪ ran sigAlgebra ↦ {𝑓 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∣ ∀𝑥 ∈ 𝑡 (◡𝑓 “ 𝑥) ∈ 𝑠})
Theorem	ismbfm 30442*	The predicate "𝐹 is a measurable function from the measurable space 𝑆 to the measurable space 𝑇". Cf. ismbf 23442. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝑆MblFnM𝑇) ↔ (𝐹 ∈ (∪ 𝑇 ↑𝑚 ∪ 𝑆) ∧ ∀𝑥 ∈ 𝑇 (◡𝐹 “ 𝑥) ∈ 𝑆)))
Theorem	elunirnmbfm 30443*	The property of being a measurable function. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝐹 ∈ ∪ ran MblFnM ↔ ∃𝑠 ∈ ∪ ran sigAlgebra∃𝑡 ∈ ∪ ran sigAlgebra(𝐹 ∈ (∪ 𝑡 ↑𝑚 ∪ 𝑠) ∧ ∀𝑥 ∈ 𝑡 (◡𝐹 “ 𝑥) ∈ 𝑠))
Theorem	mbfmfun 30444	A measurable function is a function. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	mbfmf 30445	A measurable function as a function with domain and codomain. (Contributed by Thierry Arnoux, 25-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → 𝐹:∪ 𝑆⟶∪ 𝑇)
Theorem	isanmbfm 30446	The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)
Theorem	mbfmcnvima 30447	The preimage by a measurable function is a measurable set. (Contributed by Thierry Arnoux, 23-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    ⇒   ⊢ (𝜑 → (◡𝐹 “ 𝐴) ∈ 𝑆)
Theorem	mbfmbfm 30448	A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM(sigaGen‘𝐽)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ ∪ ran MblFnM)
Theorem	mbfmcst 30449*	A constant function is measurable. Cf. mbfconst 23447. (Contributed by Thierry Arnoux, 26-Jan-2017.)
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ∪ 𝑆 ↦ 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ ∪ 𝑇)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆MblFnM𝑇))
Theorem	1stmbfm 30450	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 30451	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 30452*	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 30453	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 30454	The composition of two measurable functions is measurable. ( cf. cnmpt11 21514) (Contributed by Thierry Arnoux, 4-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑆MblFnM𝑇))    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝑅MblFnM𝑇))
Theorem	mbfmco2 30455*	The pair building of two measurable functions is measurable. ( cf. cnmpt1t 21516). (Contributed by Thierry Arnoux, 6-Jun-2017.)
⊢ (𝜑 → 𝑅 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝑇 ∈ ∪ ran sigAlgebra)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅MblFnM𝑆))    &   ⊢ (𝜑 → 𝐺 ∈ (𝑅MblFnM𝑇))    &   ⊢ 𝐻 = (𝑥 ∈ ∪ 𝑅 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑥)⟩)    ⇒   ⊢ (𝜑 → 𝐻 ∈ (𝑅MblFnM(𝑆 ×s 𝑇)))
Theorem	mbfmvolf 30456	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 30457	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 30458	All functions are measurable with respect to the counting measure. (Contributed by Thierry Arnoux, 24-Jan-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝒫 𝑂MblFnM𝔅ℝ) = (ℝ ↑𝑚 𝑂))
20.3.16.12  Borel Algebra on ` ( RR X. RR ) `
Theorem	br2base 30459*	The base set for the generator of the Borel sigma-algebra on (ℝ × ℝ) is indeed (ℝ × ℝ). (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ∪ ran (𝑥 ∈ 𝔅ℝ, 𝑦 ∈ 𝔅ℝ ↦ (𝑥 × 𝑦)) = (ℝ × ℝ)
Theorem	dya2ub 30460	An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017.)
⊢ (𝑅 ∈ ℝ+ → (1 / (2↑(⌊‘(1 − (2 logb 𝑅))))) < 𝑅)
Theorem	sxbrsigalem0 30461*	The closed half-spaces of (ℝ × ℝ) cover (ℝ × ℝ). (Contributed by Thierry Arnoux, 11-Oct-2017.)
⊢ ∪ (ran (𝑒 ∈ ℝ ↦ ((𝑒[,)+∞) × ℝ)) ∪ ran (𝑓 ∈ ℝ ↦ (ℝ × (𝑓[,)+∞)))) = (ℝ × ℝ)
Theorem	sxbrsigalem3 30462*	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 30463*	The function 𝐼 returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl 23414. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) = ((𝑋 / (2↑𝑁))[,)((𝑋 + 1) / (2↑𝑁))))
Theorem	dya2iocress 30464*	Dyadic intervals are subsets of ℝ. (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ⊆ ℝ)
Theorem	dya2iocbrsiga 30465*	Dyadic intervals are Borel sets of ℝ. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ) → (𝑋𝐼𝑁) ∈ 𝔅ℝ)
Theorem	dya2icobrsiga 30466*	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 30467*	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 30468*	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 30469*	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 30470*	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 30471*	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 30472*	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 30473*	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 30470. (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ (𝐴 ∈ (𝐽 ×t 𝐽) → ∃𝑐 ∈ 𝒫 ran 𝑅∪ 𝑐 = 𝐴)
Theorem	dya2iocucvr 30474*	The dyadic rectangular set collection covers (ℝ × ℝ). (Contributed by Thierry Arnoux, 18-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))))    &   ⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣))    ⇒   ⊢ ∪ ran 𝑅 = (ℝ × ℝ)
Theorem	sxbrsigalem1 30475*	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 30476*	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 30477*	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 30478*	First direction for sxbrsiga 30480. (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 30479	First direction for sxbrsiga 30480, same as sxbrsigalem6, dealing with the antecedents. (Contributed by Thierry Arnoux, 10-Oct-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (sigaGen‘(𝐽 ×t 𝐽)) ⊆ (𝔅ℝ ×s 𝔅ℝ)
Theorem	sxbrsiga 30480	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 𝐽))
20.3.16.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 30487) - it is monotone (omsmon 30488) - it is countably sub-additive (omssubadd 30490) See Definition 1.11.1 of [Bogachev] p. 41.
Syntax	coms 30481	Class declaration for the outer measure construction function.
class toOMeas
Definition	df-oms 30482*	Define a function constructing an outer measure. See omsval 30483 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[,]+∞), < )))
Theorem	omsval 30483*	Value of the function mapping a content function to the corresponding outer measure. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ (𝑅 ∈ V → (toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )))
Theorem	omsfval 30484*	Value of the outer measure evaluated for a given set 𝐴. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ))
Theorem	omscl 30485*	A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019.)
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) ⊆ (0[,]+∞))
Theorem	omsf 30486	A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → (toOMeas‘𝑅):𝒫 ∪ dom 𝑅⟶(0[,]+∞))
Theorem	oms0 30487	A constructed outer measure evaluates to zero for the empty set. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ (𝜑 → ∅ ∈ dom 𝑅)    &   ⊢ (𝜑 → (𝑅‘∅) = 0)    ⇒   ⊢ (𝜑 → (𝑀‘∅) = 0)
Theorem	omsmon 30488	A constructed outer measure is monotone. Note in Example 1.5.2 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝑄)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	omssubaddlem 30489*	For any small margin 𝐸, we can find a covering approaching the outer measure of a set 𝐴 by that margin. (Contributed by Thierry Arnoux, 18-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑄)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + 𝐸))
Theorem	omssubadd 30490*	A constructed outer measure is countably sub-additive. Lemma 1.5.4 of [Bogachev] p. 17. (Contributed by Thierry Arnoux, 21-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ 𝑀 = (toOMeas‘𝑅)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄)    &   ⊢ (𝜑 → 𝑋 ≼ ω)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))
Syntax	ccarsg 30491	Class declaration for the Caratheodory sigma-Algebra construction.
class toCaraSiga
Definition	df-carsg 30492*	Define a function constructing Caratheodory measurable sets for a given outer measure. See carsgval 30493 for its value. Definition 1.11.2 of [Bogachev] p. 41. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})
Theorem	carsgval 30493*	Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)})
Theorem	carsgcl 30494	Closure of the Caratheodory measurable sets. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑂)
Theorem	elcarsg 30495*	Property of being a Catatheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))))
Theorem	baselcarsg 30496	The universe set, 𝑂, is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → 𝑂 ∈ (toCaraSiga‘𝑀))
Theorem	0elcarsg 30497	The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → ∅ ∈ (toCaraSiga‘𝑀))
Theorem	carsguni 30498	The union of all Caratheodory measurable sets is the universe. (Contributed by Thierry Arnoux, 22-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    ⇒   ⊢ (𝜑 → ∪ (toCaraSiga‘𝑀) = 𝑂)
Theorem	elcarsgss 30499	Caratheodory measurable sets are subsets of the universe. (Contributed by Thierry Arnoux, 21-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)
Theorem	difelcarsg 30500	The Caratheodory measurable sets are closed under complement. (Contributed by Thierry Arnoux, 17-May-2020.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ∈ (toCaraSiga‘𝑀))    ⇒   ⊢ (𝜑 → (𝑂 ∖ 𝐴) ∈ (toCaraSiga‘𝑀))