P. 470 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46901-47000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ismea 46901*	Express the predicate "𝑀 is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑀 ∈ Meas ↔ (((𝑀:dom 𝑀⟶(0[,]+∞) ∧ dom 𝑀 ∈ SAlg) ∧ (𝑀‘∅) = 0) ∧ ∀𝑥 ∈ 𝒫 dom 𝑀((𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦) → (𝑀‘∪ 𝑥) = (Σ^‘(𝑀 ↾ 𝑥)))))
Theorem	dmmeasal 46902	The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	meaf 46903	A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    ⇒   ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞))
Theorem	mea0 46904	The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    ⇒   ⊢ (𝜑 → (𝑀‘∅) = 0)
Theorem	nnfoctbdjlem 46905*	There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐺:𝐴–1-1-onto→𝑋)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if((𝑛 = 1 ∨ ¬ (𝑛 − 1) ∈ 𝐴), ∅, (𝐺‘(𝑛 − 1))))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))
Theorem	nnfoctbdj 46906*	There exists a mapping from ℕ onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ≼ ω)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝑋 𝑦)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:ℕ–onto→(𝑋 ∪ {∅}) ∧ Disj 𝑛 ∈ ℕ (𝑓‘𝑛)))
Theorem	meadjuni 46907*	The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑋 ≼ ω)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝑥)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑋) = (Σ^‘(𝑀 ↾ 𝑋)))
Theorem	meacl 46908	The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ (0[,]+∞))
Theorem	iundjiunlem 46909*	The sets in the sequence 𝐹 are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    &   ⊢ (𝜑 → 𝐽 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐽 < 𝐾)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅)
Theorem	iundjiun 46910*	Given a sequence 𝐸 of sets, a sequence 𝐹 of disjoint sets is built, such that the indexed union stays the same. As in the proof of Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑛𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑉)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    ⇒   ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
Theorem	meaxrcl 46911	The measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ*)
Theorem	meadjun 46912	The measure of the union of two disjoint sets is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	meassle 46913	The measure of a set is greater than or equal to the measure of a subset, Property 112C (b) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) ≤ (𝑀‘𝐵))
Theorem	meaunle 46914	The measure of the union of two sets is less than or equal to the sum of the measures, Property 112C (c) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) ≤ ((𝑀‘𝐴) +𝑒 (𝑀‘𝐵)))
Theorem	meadjiunlem 46915*	The sum of nonnegative extended reals, restricted to the range of another function. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐺:𝑋⟶𝑆)    &   ⊢ 𝑌 = {𝑖 ∈ 𝑋 ∣ (𝐺‘𝑖) ≠ ∅}    &   ⊢ (𝜑 → Disj 𝑖 ∈ 𝑋 (𝐺‘𝑖))    ⇒   ⊢ (𝜑 → (Σ^‘(𝑀 ↾ ran 𝐺)) = (Σ^‘(𝑀 ∘ 𝐺)))
Theorem	meadjiun 46916*	The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → Disj 𝑘 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑘 ∈ 𝐴 𝐵) = (Σ^‘(𝑘 ∈ 𝐴 ↦ (𝑀‘𝐵))))
Theorem	ismeannd 46917*	Sufficient condition to prove that 𝑀 is a measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝑀:𝑆⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑀‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑒:ℕ⟶𝑆 ∧ Disj 𝑛 ∈ ℕ (𝑒‘𝑛)) → (𝑀‘∪ 𝑛 ∈ ℕ (𝑒‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑀‘(𝑒‘𝑛)))))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Meas)
Theorem	meaiunlelem 46918*	The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))))
Theorem	meaiunle 46919*	The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))))
Theorem	psmeasurelem 46920*	𝑀 applied to a disjoint union of subsets of its domain is the sum of 𝑀 applied to such subset. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞))    &   ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥)))    &   ⊢ (𝜑 → 𝑀:𝒫 𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → Disj 𝑦 ∈ 𝑌 𝑦)    ⇒   ⊢ (𝜑 → (𝑀‘∪ 𝑌) = (Σ^‘(𝑀 ↾ 𝑌)))
Theorem	psmeasure 46921*	Point supported measure, Remark 112B (d) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻:𝑋⟶(0[,]+∞))    &   ⊢ 𝑀 = (𝑥 ∈ 𝒫 𝑋 ↦ (Σ^‘(𝐻 ↾ 𝑥)))    ⇒   ⊢ (𝜑 → 𝑀 ∈ Meas)
Theorem	voliunsge0lem 46922*	The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))    &   ⊢ (𝜑 → 𝐸:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛))    ⇒   ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))))
Theorem	voliunsge0 46923*	The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐸:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛))    ⇒   ⊢ (𝜑 → (vol‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐸‘𝑛)))))
Theorem	volmea 46924	The Lebesgue measure on the Reals is actually a measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → vol ∈ Meas)
Theorem	meage0 46925	If the measure of a measurable set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    ⇒   ⊢ (𝜑 → 0 ≤ (𝑀‘𝐴))
Theorem	meadjunre 46926	The measure of the union of two disjoint sets, with finite measure, is the sum of the measures, Property 112C (a) of [Fremlin1] p. 15. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ 𝑆 = dom 𝑀    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∪ 𝐵)) = ((𝑀‘𝐴) + (𝑀‘𝐵)))
Theorem	meassre 46927	If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    ⇒   ⊢ (𝜑 → (𝑀‘𝐵) ∈ ℝ)
Theorem	meale0eq0 46928	A measure that is less than or equal to 0 is 0. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ≤ 0)    ⇒   ⊢ (𝜑 → (𝑀‘𝐴) = 0)
Theorem	meadif 46929	The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∖ 𝐵)) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
Theorem	meaiuninclem 46930*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc 46931*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc2 46932*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝐵)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiunincf 46933*	Measures are continuous from below (bounded case): if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc3v 46934*	Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46931 and meaiuninc2 46932 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc3 46935*	Measures are continuous from below: if 𝐸 is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of [Fremlin1] p. 16 . This theorem generalizes meaiuninc 46931 and meaiuninc2 46932 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiininclem 46936*	Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁))    &   ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))    &   ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiininc 46937*	Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁))    &   ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiininc2 46938*	Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))    &   ⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑀‘(𝐸‘𝑘)) ∈ ℝ)    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
21.43.19.4  Outer measures and Caratheodory's construction Proofs for most of the theorems in section 113 of [Fremlin1]
Syntax	come 46939	Extend class notation with the class of outer measures.
class OutMeas
Definition	df-ome 46940*	Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))}
Syntax	ccaragen 46941	Extend class notation with a function that takes an outer measure and generates a sigma-algebra and a measure.
class CaraGen
Definition	df-caragen 46942*	Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})
Theorem	caragenval 46943*	The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑂 ∈ OutMeas → (CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)})
Theorem	isome 46944*	Express the predicate "𝑂 is an outer measure." Definition 113A of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ OutMeas ↔ ((((𝑂:dom 𝑂⟶(0[,]+∞) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂) ∧ (𝑂‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑂∀𝑧 ∈ 𝒫 𝑦(𝑂‘𝑧) ≤ (𝑂‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑂(𝑦 ≼ ω → (𝑂‘∪ 𝑦) ≤ (Σ^‘(𝑂 ↾ 𝑦))))))
Theorem	caragenel 46945*	Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))))
Theorem	omef 46946	An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    ⇒   ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
Theorem	ome0 46947	The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    ⇒   ⊢ (𝜑 → (𝑂‘∅) = 0)
Theorem	omessle 46948	The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ≤ (𝑂‘𝐵))
Theorem	omedm 46949	The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑂 ∈ OutMeas → dom 𝑂 = 𝒫 ∪ dom 𝑂)
Theorem	caragensplit 46950	If 𝐸 is in the set generated by the Caratheodory's method, then it splits any set 𝐴 in two parts such that the sum of the outer measures of the two parts is equal to the outer measure of the whole set 𝐴. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸))) = (𝑂‘𝐴))
Theorem	caragenelss 46951	An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ 𝑋 = ∪ dom 𝑂    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)
Theorem	carageneld 46952*	Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑆)
Theorem	omecl 46953	The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ (0[,]+∞))
Theorem	caragenss 46954	The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the domain of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
Theorem	omeunile 46955	The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)    &   ⊢ (𝜑 → 𝑌 ≼ ω)    ⇒   ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌)))
Theorem	caragen0 46956	The empty set belongs to any Caratheodory's construction. First part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → ∅ ∈ 𝑆)
Theorem	omexrcl 46957	The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ*)
Theorem	caragenunidm 46958	The base set of an outer measure belongs to the sigma-algebra generated by the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑆)
Theorem	caragensspw 46959	The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the power set of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝒫 𝑋)
Theorem	omessre 46960	If the outer measure of a set is real, then the outer measure of any of its subset is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑂‘𝐵) ∈ ℝ)
Theorem	caragenuni 46961	The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → ∪ 𝑆 = ∪ dom 𝑂)
Theorem	caragenuncllem 46962	The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (𝑂‘𝐴))
Theorem	caragenuncl 46963	The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆)
Theorem	caragendifcl 46964	The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆)
Theorem	caragenfiiuncl 46965*	The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	omeunle 46966	The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘(𝐴 ∪ 𝐵)) ≤ ((𝑂‘𝐴) +𝑒 (𝑂‘𝐵)))
Theorem	omeiunle 46967*	The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))))
Theorem	omelesplit 46968	The outer measure of a set 𝐴 is less than or equal to the extended addition of the outer measures of the decomposition induced on 𝐴 by any 𝐸. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸))))
Theorem	omeiunltfirp 46969*	If the outer measure of a countable union is not +∞, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋)    &   ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐸‘𝑛)) + 𝑌))
Theorem	omeiunlempt 46970*	The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐸 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 𝐸) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘𝐸))))
Theorem	carageniuncllem1 46971*	The outer measure of 𝐴 ∩ (𝐺‘𝑛) is the sum of the outer measures of 𝐴 ∩ (𝐹‘𝑚). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    &   ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑍)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾))))
Theorem	carageniuncllem2 46972*	The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ+)    &   ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))    &   ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖)))    ⇒   ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌))
Theorem	carageniuncl 46973*	The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆)
Theorem	caragenunicl 46974	The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑆)    &   ⊢ (𝜑 → 𝑋 ≼ ω)    ⇒   ⊢ (𝜑 → ∪ 𝑋 ∈ 𝑆)
Theorem	caragensal 46975	Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	caratheodorylem1 46976*	Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)    &   ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
Theorem	caratheodorylem2 46977*	Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸:ℕ⟶𝑆)    &   ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛))    &   ⊢ 𝐺 = (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛))    ⇒   ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛)))))
Theorem	caratheodory 46978	Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → (𝑂 ↾ 𝑆) ∈ Meas)
Theorem	0ome 46979*	The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → 𝑂 ∈ OutMeas)
Theorem	isomenndlem 46980*	𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑂‘∅) = 0)    &   ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅))    ⇒   ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌)))
Theorem	isomennd 46981*	Sufficient condition to prove that 𝑂 is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))    &   ⊢ (𝜑 → (𝑂‘∅) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛)))))    ⇒   ⊢ (𝜑 → 𝑂 ∈ OutMeas)
Theorem	caragenel2d 46982*	Membership in the Caratheodory's construction. Similar to carageneld 46952, but here "less than or equal to" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) ≤ (𝑂‘𝑎))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑆)
Theorem	omege0 46983	If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → 0 ≤ (𝑂‘𝐴))
Theorem	omess0 46984	If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) = 0)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑂‘𝐵) = 0)
Theorem	caragencmpl 46985	A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐸 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐸) = 0)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑆)
21.43.19.5  Lebesgue measure on n-dimensional Real numbers Proofs for most of the theorems in section 115 of [Fremlin1]
Syntax	covoln 46986	Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers.
class voln*
Definition	df-ovoln 46987*	Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))))
Syntax	cvoln 46988	Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers.
class voln
Definition	df-voln 46989	Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥))))
Theorem	vonval 46990	Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln‘𝑋) = ((voln*‘𝑋) ↾ (CaraGen‘(voln*‘𝑋))))
Theorem	ovnval 46991*	Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))))
Theorem	elhoi 46992*	Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑌 ∈ ((𝐴[,)𝐵) ↑m 𝑋) ↔ (𝑌:𝑋⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 (𝑌‘𝑥) ∈ (𝐴[,)𝐵))))
Theorem	icoresmbl 46993	A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ran ([,) ↾ (ℝ × ℝ)) ⊆ dom vol
Theorem	hoissre 46994*	The projection of a half-open interval onto a single dimension is a subset of ℝ. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ 𝐼)‘𝑘) ⊆ ℝ)
Theorem	ovnval2 46995*	Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )))
Theorem	volicorecl 46996	The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ)
Theorem	hoiprodcl 46997*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝐼)‘𝑘)) ∈ (0[,)+∞))
Theorem	hoicvr 46998*	𝐼 is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) Avoid ax-rep 5206 and shorten proof. (Revised by GG, 2-Apr-2026.)
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑥 ∈ 𝑋 ↦ ⟨-𝑗, 𝑗⟩))    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (ℝ ↑m 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖))
Theorem	hoissrrn 46999*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) ⊆ (ℝ ↑m 𝑋))
Theorem	ovn0val 47000	The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m ∅))    ⇒   ⊢ (𝜑 → ((voln*‘∅)‘𝐴) = 0)