P. 467 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46601-46700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	meadif 46601	The measure of the difference of two sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑀)    &   ⊢ (𝜑 → (𝑀‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑀‘(𝐴 ∖ 𝐵)) = ((𝑀‘𝐴) − (𝑀‘𝐵)))
Theorem	meaiuninclem 46602*	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 46603*	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 46604*	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 46605*	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 46606*	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 46603 and meaiuninc2 46604 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiuninc3 46607*	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 46603 and meaiuninc2 46604 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑛𝐸    &   ⊢ (𝜑 → 𝑀 ∈ Meas)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑁)    &   ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))    &   ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑆~~>*(𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
Theorem	meaiininclem 46608*	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 46609*	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 46610*	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 46611	Extend class notation with the class of outer measures.
class OutMeas
Definition	df-ome 46612*	Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤ (Σ^‘(𝑥 ↾ 𝑦))))}
Syntax	ccaragen 46613	Extend class notation with a function that takes an outer measure and generates a sigma-algebra and a measure.
class CaraGen
Definition	df-caragen 46614*	Define the sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ CaraGen = (𝑜 ∈ OutMeas ↦ {𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑜((𝑜‘(𝑎 ∩ 𝑒)) +𝑒 (𝑜‘(𝑎 ∖ 𝑒))) = (𝑜‘𝑎)})
Theorem	caragenval 46615*	The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑂 ∈ OutMeas → (CaraGen‘𝑂) = {𝑒 ∈ 𝒫 ∪ dom 𝑂 ∣ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝑒)) +𝑒 (𝑂‘(𝑎 ∖ 𝑒))) = (𝑂‘𝑎)})
Theorem	isome 46616*	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 46617*	Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → (𝐸 ∈ 𝑆 ↔ (𝐸 ∈ 𝒫 ∪ dom 𝑂 ∧ ∀𝑎 ∈ 𝒫 ∪ dom 𝑂((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))))
Theorem	omef 46618	An outer measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    ⇒   ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞))
Theorem	ome0 46619	The outer measure of the empty set is 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    ⇒   ⊢ (𝜑 → (𝑂‘∅) = 0)
Theorem	omessle 46620	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 46621	The domain of an outer measure is a power set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑂 ∈ OutMeas → dom 𝑂 = 𝒫 ∪ dom 𝑂)
Theorem	caragensplit 46622	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 46623	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 46624*	Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) = (𝑂‘𝑎))    ⇒   ⊢ (𝜑 → 𝐸 ∈ 𝑆)
Theorem	omecl 46625	The outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ (0[,]+∞))
Theorem	caragenss 46626	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 46627	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 46628	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 46629	The outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑋 = ∪ dom 𝑂    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ*)
Theorem	caragenunidm 46630	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 46631	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 46632	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 46633	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 46634	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 46635	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 46636	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 46637*	The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆)
Theorem	omeunle 46638	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 46639*	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 46640	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 46641*	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 46642*	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 46643*	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 46644*	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 46645*	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 46646	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 46647	Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝑂 ∈ OutMeas)    &   ⊢ 𝑆 = (CaraGen‘𝑂)    ⇒   ⊢ (𝜑 → 𝑆 ∈ SAlg)
Theorem	caratheodorylem1 46648*	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 46649*	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 46650	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 46651*	The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0)    ⇒   ⊢ (𝜑 → 𝑂 ∈ OutMeas)
Theorem	isomenndlem 46652*	𝑂 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 46653*	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 46654*	Membership in the Caratheodory's construction. Similar to carageneld 46624, 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 46655	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 46656	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 46657	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 46658	Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers.
class voln*
Definition	df-ovoln 46659*	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 46660	Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers.
class voln
Definition	df-voln 46661	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 46662	Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln‘𝑋) = ((voln*‘𝑋) ↾ (CaraGen‘(voln*‘𝑋))))
Theorem	ovnval 46663*	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 46664*	Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑌 ∈ ((𝐴[,)𝐵) ↑m 𝑋) ↔ (𝑌:𝑋⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 (𝑌‘𝑥) ∈ (𝐴[,)𝐵))))
Theorem	icoresmbl 46665	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 46666*	The projection of a half-open interval onto a single dimension is a subset of ℝ. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ 𝐼)‘𝑘) ⊆ ℝ)
Theorem	ovnval2 46667*	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 46668	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 46669*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝐼)‘𝑘)) ∈ (0[,)+∞))
Theorem	hoicvr 46670*	𝐼 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.)
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑥 ∈ 𝑋 ↦ ⟨-𝑗, 𝑗⟩))    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (ℝ ↑m 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖))
Theorem	hoissrrn 46671*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) ⊆ (ℝ ↑m 𝑋))
Theorem	ovn0val 46672	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)
Theorem	ovnn0val 46673*	The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = inf(𝑀, ℝ*, < ))
Theorem	ovnval2b 46674*	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 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))})    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf((𝐿‘𝐴), ℝ*, < )))
Theorem	volicorescl 46675	The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) → (vol‘𝐴) ∈ ℝ)
Theorem	ovnprodcl 46676*	The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:ℕ⟶((ℝ × ℝ) ↑m 𝑋))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐹‘𝐼))‘𝑘)) ∈ (0[,)+∞))
Theorem	hoiprodcl2 46677*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))    &   ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ))    ⇒   ⊢ (𝜑 → (𝐿‘𝐼) ∈ (0[,)+∞))
Theorem	hoicvrrex 46678*	Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))
Theorem	ovnsupge0 46679*	The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → 𝑀 ⊆ (0[,]+∞))
Theorem	ovnlecvr 46680*	Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with 𝑋 the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))    &   ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑m 𝑋))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗)))))
Theorem	ovnpnfelsup 46681*	+∞ is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → +∞ ∈ 𝑀)
Theorem	ovnsslelem 46682*	The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋))    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    &   ⊢ 𝑁 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐵 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵))
Theorem	ovnssle 46683	The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵))
Theorem	ovnlerp 46684*	The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝑀 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))
Theorem	ovnf 46685	The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑m 𝑋)⟶(0[,]+∞))
Theorem	ovncvrrp 46686*	The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)})    &   ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)))    &   ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))    ⇒   ⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸))
Theorem	ovn0lem 46687*	For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}    &   ⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈ (0[,]+∞))    &   ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ ⟨1, 0⟩))    ⇒   ⊢ (𝜑 → inf(𝑀, ℝ*, < ) = 0)
Theorem	ovn0 46688	For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘∅) = 0)
Theorem	ovncl 46689	The Lebesgue outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ (0[,]+∞))
Theorem	ovn02 46690	For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (voln*‘∅) = (𝑥 ∈ 𝒫 {∅} ↦ 0)
Theorem	ovnxrcl 46691	The Lebesgue outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ*)
Theorem	ovnsubaddlem1 46692*	The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))})    &   ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {ℎ ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)})    &   ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))    &   ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛))))    &   ⊢ (𝜑 → 𝐹:ℕ–1-1-onto→(ℕ × ℕ))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸))
Theorem	ovnsubaddlem2 46693*	(voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    &   ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))})    &   ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)})    &   ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘)))    &   ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸))
Theorem	ovnsubadd 46694*	(voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑m 𝑋))    ⇒   ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))))
Theorem	ovnome 46695	(voln*‘𝑋) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set 𝑋. Proposition 115D (a) of [Fremlin1] p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln*‘𝑋) ∈ OutMeas)
Theorem	vonmea 46696	(voln‘𝑋) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set 𝑋. Comments in Definition 115E of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (voln‘𝑋) ∈ Meas)
Theorem	volicon0 46697	The measure of a nonempty left-closed, right-open interval. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴))
Theorem	hsphoif 46698*	𝐻 is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑎‘𝑗), if((𝑎‘𝑗) ≤ 𝑥, (𝑎‘𝑗), 𝑥)))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    ⇒   ⊢ (𝜑 → ((𝐻‘𝐴)‘𝐵):𝑋⟶ℝ)
Theorem	hoidmvval 46699*	The dimensional volume of a multidimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))    &   ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))))
Theorem	hoissrrn2 46700*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ Ⅎ𝑘𝜑    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*)    ⇒   ⊢ (𝜑 → X𝑘 ∈ 𝑋 (𝐴[,)𝐵) ⊆ (ℝ ↑m 𝑋))