P. 257 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25601-25700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ovolge0 25601	The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴))
Theorem	ovolf 25602	The domain and codomain of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ vol*:𝒫 ℝ⟶(0[,]+∞)
Theorem	ovollecl 25603	If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ)
Theorem	ovolsslem 25604*	Lemma for ovolss 25605. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑁 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵))
Theorem	ovolss 25605	The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵))
Theorem	ovolsscl 25606	If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐴) ∈ ℝ)
Theorem	ovolssnul 25607	A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0)
Theorem	ovollb2lem 25608*	Lemma for ovollb2 25609. (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩)    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
Theorem	ovollb2 25609	It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb 25599). (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolctb 25610	The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ) → (vol*‘𝐴) = 0)
Theorem	ovolq 25611	The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘ℚ) = 0
Theorem	ovolctb2 25612	The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0)
Theorem	ovol0 25613	The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘∅) = 0
Theorem	ovolfi 25614	A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0)
Theorem	ovolsn 25615	A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
Theorem	ovolunlem1a 25616*	Lemma for ovolun 25619. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolunlem1 25617*	Lemma for ovolun 25619. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))    &   ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))    ⇒   ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolunlem2 25618	Lemma for ovolun 25619. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolun 25619	The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 25625, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵)))
Theorem	ovolunnul 25620	Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴))
Theorem	ovolfiniun 25621*	The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘∪ 𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (vol*‘𝐵))
Theorem	ovoliunlem1 25622*	Lemma for ovoliun 25625. (Contributed by Mario Carneiro, 12-Jun-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛)))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))))    &   ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)    ⇒   ⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliunlem2 25623*	Lemma for ovoliun 25625. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛)))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))))    &   ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛)))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliunlem3 25624*	Lemma for ovoliun 25625. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliun 25625*	The Lebesgue outer measure function is countably sub-additive. (Many books allow +∞ as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss 25605, so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
Theorem	ovoliun2 25626*	The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun 25625.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴))
Theorem	ovoliunnul 25627*	A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)
Theorem	shft2rab 25628*	If 𝐵 is a shift of 𝐴 by 𝐶, then 𝐴 is a shift of 𝐵 by -𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) (Revised by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    ⇒   ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ (𝑦 − -𝐶) ∈ 𝐵})
Theorem	ovolshftlem1 25629*	Lemma for ovolshft 25631. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    ⇒   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolshftlem2 25630*	Lemma for ovolshft 25631. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀)
Theorem	ovolshft 25631*	The Lebesgue outer measure function is shift-invariant. (Contributed by Mario Carneiro, 22-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    ⇒   ⊢ (𝜑 → (vol*‘𝐴) = (vol*‘𝐵))
Theorem	sca2rab 25632*	If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    ⇒   ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵})
Theorem	ovolscalem1 25633*	Lemma for ovolsca 25635. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Theorem	ovolscalem2 25634*	Lemma for ovolshft 25631. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶))
Theorem	ovolsca 25635*	The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶))
Theorem	ovolicc1 25636*	The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, ⟨𝐴, 𝐵⟩, ⟨0, 0⟩))    ⇒   ⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵 − 𝐴))
Theorem	ovolicc2lem1 25637*	Lemma for ovolicc2 25642. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋))))))
Theorem	ovolicc2lem2 25638*	Lemma for ovolicc2 25642. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵)
Theorem	ovolicc2lem3 25639*	Lemma for ovolicc2 25642. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃))))))
Theorem	ovolicc2lem4 25640*	Lemma for ovolicc2 25642. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by AV, 17-Sep-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    &   ⊢ 𝑀 = inf(𝑊, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolicc2lem5 25641*	Lemma for ovolicc2 25642. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolicc2 25642*	The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)((𝐴[,]𝐵) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (vol*‘(𝐴[,]𝐵)))
Theorem	ovolicc 25643	The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
Theorem	ovolicopnf 25644	The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞)
Theorem	ovolre 25645	The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (vol*‘ℝ) = +∞
Theorem	ismbl 25646*	The predicate "𝐴 is Lebesgue-measurable". A set is measurable if it splits every other set 𝑥 in a "nice" way, that is, if the measure of the pieces 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴 sum up to the measure of 𝑥 (assuming that the measure of 𝑥 is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))))
Theorem	ismbl2 25647*	From ovolun 25619, it suffices to show that the measure of 𝑥 is at least the sum of the measures of 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥))))
Theorem	volres 25648	A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ vol = (vol* ↾ dom vol)
Theorem	volf 25649	The domain and codomain of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ vol:dom vol⟶(0[,]+∞)
Theorem	mblvol 25650	The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))
Theorem	mblss 25651	A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
Theorem	mblsplit 25652	The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐵) = ((vol*‘(𝐵 ∩ 𝐴)) + (vol*‘(𝐵 ∖ 𝐴))))
Theorem	volss 25653	The Lebesgue measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 17-Oct-2017.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ 𝐴 ⊆ 𝐵) → (vol‘𝐴) ≤ (vol‘𝐵))
Theorem	cmmbl 25654	The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol)
Theorem	nulmbl 25655	A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) = 0) → 𝐴 ∈ dom vol)
Theorem	nulmbl2 25656*	A set of outer measure zero is measurable. The term "outer measure zero" here is slightly different from "nullset/negligible set"; a nullset has vol*(𝐴) = 0 while "outer measure zero" means that for any 𝑥 there is a 𝑦 containing 𝐴 with volume less than 𝑥. Assuming AC, these notions are equivalent (because the intersection of all such 𝑦 is a nullset) but in ZF this is a strictly weaker notion. Proposition 563Gb of [Fremlin5] p. 193. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ∈ dom vol)
Theorem	unmbl 25657	A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol)
Theorem	shftmbl 25658*	A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol)
Theorem	0mbl 25659	The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ∅ ∈ dom vol
Theorem	rembl 25660	The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ℝ ∈ dom vol
Theorem	unidmvol 25661	The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ∪ dom vol = ℝ
Theorem	inmbl 25662	An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol)
Theorem	difmbl 25663	A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol)
Theorem	finiunmbl 25664*	A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	volun 25665	The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)))
Theorem	volinun 25666	Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵))))
Theorem	volfiniun 25667*	The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧ Disj 𝑘 ∈ 𝐴 𝐵) → (vol‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (vol‘𝐵))
Theorem	iundisj 25668*	Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2 25669*	A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	voliunlem1 25670*	Lemma for voliun 25674. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛))))    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸))
Theorem	voliunlem2 25671*	Lemma for voliun 25674. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    ⇒   ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol)
Theorem	voliunlem3 25672*	Lemma for voliun 25674. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    &   ⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Theorem	iunmbl 25673	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol)
Theorem	voliun 25674	The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘𝐴))    ⇒   ⊢ ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘∪ 𝑛 ∈ ℕ 𝐴) = sup(ran 𝑆, ℝ*, < ))
Theorem	volsuplem 25675*	Lemma for volsup 25676. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	volsup 25676*	The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ ((𝐹:ℕ⟶dom vol ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) → (vol‘∪ ran 𝐹) = sup((vol “ ran 𝐹), ℝ*, < ))
Theorem	iunmbl2 25677*	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	ioombl1lem1 25678*	Lemma for ioombl1 25682. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
Theorem	ioombl1lem2 25679*	Lemma for ioombl1 25682. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
Theorem	ioombl1lem3 25680*	Lemma for ioombl1 25682. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
Theorem	ioombl1lem4 25681*	Lemma for ioombl1 25682. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ 𝐵 = (𝐴(,)+∞)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))    &   ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))
Theorem	ioombl1 25682	An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.)
⊢ (𝐴 ∈ ℝ* → (𝐴(,)+∞) ∈ dom vol)
Theorem	icombl1 25683	A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol)
Theorem	icombl 25684	A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol)
Theorem	ioombl 25685	An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴(,)𝐵) ∈ dom vol
Theorem	iccmbl 25686	A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
Theorem	iccvolcl 25687	A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)
Theorem	ovolioo 25688	The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	volioo 25689	The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	ioovolcl 25690	An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
Theorem	ovolfs2 25691	Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹))
Theorem	ioorcl2 25692	An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
Theorem	ioorf 25693	Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ 𝐹:ran (,)⟶( ≤ ∩ (ℝ* × ℝ*))
Theorem	ioorval 25694*	Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ (𝐴 ∈ ran (,) → (𝐹‘𝐴) = if(𝐴 = ∅, ⟨0, 0⟩, ⟨inf(𝐴, ℝ*, < ), sup(𝐴, ℝ*, < )⟩))
Theorem	ioorinv2 25695*	The function 𝐹 is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝐴(,)𝐵) ≠ ∅ → (𝐹‘(𝐴(,)𝐵)) = ⟨𝐴, 𝐵⟩)
Theorem	ioorinv 25696*	The function 𝐹 is an "inverse" of sorts to the open interval function. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ (𝐴 ∈ ran (,) → ((,)‘(𝐹‘𝐴)) = 𝐴)
Theorem	ioorcl 25697*	The function 𝐹 does not always return real numbers, but it does on intervals of finite volume. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by AV, 13-Sep-2020.)
⊢ 𝐹 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝐴 ∈ ran (,) ∧ (vol*‘𝐴) ∈ ℝ) → (𝐹‘𝐴) ∈ ( ≤ ∩ (ℝ × ℝ)))
Theorem	uniiccdif 25698	A union of closed intervals differs from the equivalent union of open intervals by a nullset. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    ⇒   ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
Theorem	uniioovol 25699*	A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 25674.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Theorem	uniiccvol 25700*	An almost-disjoint union of closed intervals (disjoint interiors) has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun 25674.) (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))