P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elovolm 25401*	Elementhood in the set 𝑀 of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < )))
Theorem	elovolmr 25402*	Sufficient condition for elementhood in the set 𝑀. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolmge0 25403*	The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵)
Theorem	ovolcl 25404	The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
Theorem	ovollb 25405	The outer volume is a lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolgelb 25406*	The outer volume is the greatest lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝑔))    ⇒   ⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵)))
Theorem	ovolge0 25407	The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴))
Theorem	ovolf 25408	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 25409	If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ)
Theorem	ovolsslem 25410*	Lemma for ovolss 25411. (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 25411	The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵))
Theorem	ovolsscl 25412	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 25413	A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0)
Theorem	ovollb2lem 25414*	Lemma for ovollb2 25415. (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 25415	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 25405). (Contributed by Mario Carneiro, 24-Mar-2015.)
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolctb 25416	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 25417	The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘ℚ) = 0
Theorem	ovolctb2 25418	The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0)
Theorem	ovol0 25419	The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (vol*‘∅) = 0
Theorem	ovolfi 25420	A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0)
Theorem	ovolsn 25421	A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0)
Theorem	ovolunlem1a 25422*	Lemma for ovolun 25425. (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 25423*	Lemma for ovolun 25425. (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 25424	Lemma for ovolun 25425. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))    &   ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Theorem	ovolun 25425	The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 25431, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵)))
Theorem	ovolunnul 25426	Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴))
Theorem	ovolfiniun 25427*	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 25428*	Lemma for ovoliun 25431. (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 25429*	Lemma for ovoliun 25431. (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 25430*	Lemma for ovoliun 25431. (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Theorem	ovoliun 25431*	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 25411, 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 25432*	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 25431.) (Contributed by Mario Carneiro, 12-Jun-2014.)
⊢ 𝑇 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴))
Theorem	ovoliunnul 25433*	A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0)
Theorem	shft2rab 25434*	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 25435*	Lemma for ovolshft 25437. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    ⇒   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Theorem	ovolshftlem2 25436*	Lemma for ovolshft 25437. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})    &   ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}    ⇒   ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀)
Theorem	ovolshft 25437*	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 25438*	If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    ⇒   ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵})
Theorem	ovolscalem1 25439*	Lemma for ovolsca 25441. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)⟩)    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Theorem	ovolscalem2 25440*	Lemma for ovolshft 25437. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶))
Theorem	ovolsca 25441*	The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})    &   ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶))
Theorem	ovolicc1 25442*	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 25443*	Lemma for ovolicc2 25448. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋))))))
Theorem	ovolicc2lem2 25444*	Lemma for ovolicc2 25448. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵)
Theorem	ovolicc2lem3 25445*	Lemma for ovolicc2 25448. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    &   ⊢ (𝜑 → 𝐻:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶}))    &   ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)}    ⇒   ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃))))))
Theorem	ovolicc2lem4 25446*	Lemma for ovolicc2 25448. (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 25447*	Lemma for ovolicc2 25448. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin))    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈)    &   ⊢ (𝜑 → 𝐺:𝑈⟶ℕ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡)    &   ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅}    ⇒   ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
Theorem	ovolicc2 25448*	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 25449	The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
Theorem	ovolicopnf 25450	The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞)
Theorem	ovolre 25451	The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.)
⊢ (vol*‘ℝ) = +∞
Theorem	ismbl 25452*	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 25453*	From ovolun 25425, 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 25454	A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ vol = (vol* ↾ dom vol)
Theorem	volf 25455	The domain and codomain of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ vol:dom vol⟶(0[,]+∞)
Theorem	mblvol 25456	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 25457	A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
Theorem	mblsplit 25458	The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐵) = ((vol*‘(𝐵 ∩ 𝐴)) + (vol*‘(𝐵 ∖ 𝐴))))
Theorem	volss 25459	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 25460	The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol)
Theorem	nulmbl 25461	A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) = 0) → 𝐴 ∈ dom vol)
Theorem	nulmbl2 25462*	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 25463	A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol)
Theorem	shftmbl 25464*	A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol)
Theorem	0mbl 25465	The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ∅ ∈ dom vol
Theorem	rembl 25466	The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ℝ ∈ dom vol
Theorem	unidmvol 25467	The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.)
⊢ ∪ dom vol = ℝ
Theorem	inmbl 25468	An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol)
Theorem	difmbl 25469	A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol)
Theorem	finiunmbl 25470*	A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	volun 25471	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 25472	Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵))))
Theorem	volfiniun 25473*	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 25474*	Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2 25475*	A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	voliunlem1 25476*	Lemma for voliun 25480. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛))))    &   ⊢ (𝜑 → 𝐸 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸))
Theorem	voliunlem2 25477*	Lemma for voliun 25480. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    ⇒   ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol)
Theorem	voliunlem3 25478*	Lemma for voliun 25480. (Contributed by Mario Carneiro, 20-Mar-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶dom vol)    &   ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛))))    &   ⊢ 𝑆 = seq1( + , 𝐺)    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛)))    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < ))
Theorem	iunmbl 25479	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol)
Theorem	voliun 25480	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 25481*	Lemma for volsup 25482. (Contributed by Mario Carneiro, 4-Jul-2014.)
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	volsup 25482*	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 25483*	The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.)
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol)
Theorem	ioombl1lem1 25484*	Lemma for ioombl1 25488. (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 25485*	Lemma for ioombl1 25488. (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 25486*	Lemma for ioombl1 25488. (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 25487*	Lemma for ioombl1 25488. (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 25488	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 25489	A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol)
Theorem	icombl 25490	A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol)
Theorem	ioombl 25491	An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ (𝐴(,)𝐵) ∈ dom vol
Theorem	iccmbl 25492	A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
Theorem	iccvolcl 25493	A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)
Theorem	ovolioo 25494	The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	volioo 25495	The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
Theorem	ioovolcl 25496	An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
Theorem	ovolfs2 25497	Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹)    ⇒   ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹))
Theorem	ioorcl2 25498	An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
Theorem	ioorf 25499	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 25500*	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(𝐴, ℝ*, < )⟩))