P. 260 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25901-26000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ioorval 25901*	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 25902*	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 25903*	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 25904*	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 25905	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 25906*	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 25881.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Theorem	uniiccvol 25907*	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 25881.) (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < ))
Theorem	uniioombllem1 25908*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
Theorem	uniioombllem2a 25909*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,))
Theorem	uniioombllem2 25910*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 11-Dec-2016.) (Revised by AV, 13-Sep-2020.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ 𝐻 = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))))    &   ⊢ 𝐾 = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ ℕ) → seq1( + , (vol* ∘ 𝐻)) ⇝ (vol*‘(((,)‘(𝐺‘𝐽)) ∩ 𝐴)))
Theorem	uniioombllem3a 25911*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
Theorem	uniioombllem3 25912*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
Theorem	uniioombllem4 25913*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))    &   ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))    ⇒   ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
Theorem	uniioombllem5 25914*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)    &   ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))    &   ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
Theorem	uniioombllem6 25915*	Lemma for uniioombl 25916. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    &   ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)    &   ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))    &   ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))    &   ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))    ⇒   ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
Theorem	uniioombl 25916*	A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25880.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol)
Theorem	uniiccmbl 25917*	An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25880.) (Contributed by Mario Carneiro, 25-Mar-2015.)
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))    &   ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))    &   ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))    ⇒   ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ∈ dom vol)
Theorem	dyadf 25918*	The function 𝐹 returns the endpoints of a dyadic rational covering of the real line. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ 𝐹:(ℤ × ℕ0)⟶( ≤ ∩ (ℝ × ℝ))
Theorem	dyadval 25919*	Value of the dyadic rational function 𝐹. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (𝐴𝐹𝐵) = ⟨(𝐴 / (2↑𝐵)), ((𝐴 + 1) / (2↑𝐵))⟩)
Theorem	dyadovol 25920*	Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (vol*‘([,]‘(𝐴𝐹𝐵))) = (1 / (2↑𝐵)))
Theorem	dyadss 25921*	Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.) (Proof shortened by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) → 𝐷 ≤ 𝐶))
Theorem	dyaddisjlem 25922*	Lemma for dyaddisj 25923. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅))
Theorem	dyaddisj 25923*	Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹) → (([,]‘𝐴) ⊆ ([,]‘𝐵) ∨ ([,]‘𝐵) ⊆ ([,]‘𝐴) ∨ (((,)‘𝐴) ∩ ((,)‘𝐵)) = ∅))
Theorem	dyadmaxlem 25924*	Lemma for dyadmax 25925. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ¬ 𝐷 < 𝐶)    &   ⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))
Theorem	dyadmax 25925*	Any nonempty set of dyadic rational intervals has a maximal element. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ ((𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → ∃𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤))
Theorem	dyadmbllem 25926*	Lemma for dyadmbl 25927. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)}    &   ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)    ⇒   ⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,] “ 𝐺))
Theorem	dyadmbl 25927*	Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    &   ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)}    &   ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)    ⇒   ⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol)
Theorem	opnmbllem 25928*	Lemma for opnmbl 25929. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ ⟨(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))⟩)    ⇒   ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	opnmbl 25929	All open sets are measurable. This proof, via dyadmbl 25927 and uniioombl 25916, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	opnmblALT 25930	All open sets are measurable. This alternative proof of opnmbl 25929 is significantly shorter, at the expense of invoking countable choice ax-cc 10517. (This was also the original proof before the current opnmbl 25929 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Theorem	subopnmbl 25931	Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ 𝐽) → 𝐵 ∈ dom vol)
Theorem	volsup2 25932*	The volume of 𝐴 is the supremum of the sequence vol*‘(𝐴 ∩ ( -𝑛[,]𝑛)) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ∧ 𝐵 < (vol‘𝐴)) → ∃𝑛 ∈ ℕ 𝐵 < (vol‘(𝐴 ∩ ( -𝑛[,]𝑛))))
Theorem	volcn 25933*	The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥))))    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ))
Theorem	volivth 25934*	The Intermediate Value Theorem for the Lebesgue volume function. For any positive 𝐵 ≤ (vol‘𝐴), there is a measurable subset of 𝐴 whose volume is 𝐵. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ (0[,](vol‘𝐴))) → ∃𝑥 ∈ dom vol(𝑥 ⊆ 𝐴 ∧ (vol‘𝑥) = 𝐵))
Theorem	vitalilem1 25935*	Lemma for vitali 25940. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    ⇒   ⊢ ∼ Er (0[,]1)
Theorem	vitalilem2 25936*	Lemma for vitali 25940. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ( -1[,]2)))
Theorem	vitalilem3 25937*	Lemma for vitali 25940. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))
Theorem	vitalilem4 25938*	Lemma for vitali 25940. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0)
Theorem	vitalilem5 25939*	Lemma for vitali 25940. (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}    &   ⊢ 𝑆 = ((0[,]1) / ∼ )    &   ⊢ (𝜑 → 𝐹 Fn 𝑆)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))    &   ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ ( -1[,]1)))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})    &   ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))    ⇒   ⊢ ¬ 𝜑
Theorem	vitali 25940	If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014.)
⊢ ( < We ℝ → dom vol ⊊ 𝒫 ℝ)
13.2.2  Lebesgue integration
13.2.2.1  Lesbesgue integral
Syntax	cmbf 25941	Extend class notation with the class of measurable functions.
class MblFn
Syntax	citg1 25942	Extend class notation with the Lebesgue integral for simple functions.
class ∫1
Syntax	citg2 25943	Extend class notation with the Lebesgue integral for nonnegative functions.
class ∫2
Syntax	cibl 25944	Extend class notation with the class of integrable functions.
class 𝐿1
Syntax	citg 25945	Extend class notation with the general Lebesgue integral.
class ∫𝐴𝐵 d𝑥
Definition	df-mbf 25946*	Define the class of measurable functions on the reals. A real function is measurable if the preimage of every open interval is a measurable set (see ismbl 25853) and a complex function is measurable if the real and imaginary parts of the function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
Definition	df-itg1 25947*	Define the Lebesgue integral for simple functions. A simple function is a finite linear combination of indicator functions for finitely measurable sets, whose assigned value is the sum of the measures of the sets times their respective weights. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ∫1 = (𝑓 ∈ {𝑔 ∈ MblFn ∣ (𝑔:ℝ⟶ℝ ∧ ran 𝑔 ∈ Fin ∧ (vol‘(◡𝑔 “ (ℝ ∖ {0}))) ∈ ℝ)} ↦ Σ𝑥 ∈ (ran 𝑓 ∖ {0})(𝑥 · (vol‘(◡𝑓 “ {𝑥}))))
Definition	df-itg2 25948*	Define the Lebesgue integral for nonnegative functions. A nonnegative function's integral is the supremum of the integrals of all simple functions that are less than the input function. Note that this may be +∞ for functions that take the value +∞ on a set of positive measure or functions that are bounded below by a positive number on a set of infinite measure. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫2 = (𝑓 ∈ ((0[,]+∞) ↑m ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < ))
Definition	df-ibl 25949*	Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
Definition	df-itg 25950*	Define the full Lebesgue integral, for complex-valued functions to ℝ. The syntax is designed to be suggestive of the standard notation for integrals. For example, our notation for the integral of 𝑥↑2 from 0 to 1 is ∫(0[,]1)(𝑥↑2) d𝑥 = (1 / 3). The only real function of this definition is to break the integral up into nonnegative real parts and send it off to df-itg2 25948 for further processing. Note that this definition cannot handle integrals which evaluate to infinity, because addition and multiplication are not currently defined on extended reals. (You can use df-itg2 25948 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))))
Theorem	ismbf1 25951*	The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 25955 and ismbfcn 25956 for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
Theorem	mbff 25952	A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ)
Theorem	mbfdm 25953	The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
Theorem	mbfconstlem 25954	Lemma for mbfconst 25960 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ) → (◡(𝐴 × {𝐶}) “ 𝐵) ∈ dom vol)
Theorem	ismbf 25955*	The predicate "𝐹 is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl 25853. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
Theorem	ismbfcn 25956	A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
Theorem	mbfima 25957	Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (◡𝐹 “ (𝐵(,)𝐶)) ∈ dom vol)
Theorem	mbfimaicc 25958	The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (◡𝐹 “ (𝐵[,]𝐶)) ∈ dom vol)
Theorem	mbfimasn 25959	The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ ∧ 𝐵 ∈ ℝ) → (◡𝐹 “ {𝐵}) ∈ dom vol)
Theorem	mbfconst 25960	A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn)
Theorem	mbf0 25961	The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.)
⊢ ∅ ∈ MblFn
Theorem	mbfid 25962	The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.)
⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn)
Theorem	mbfmptcl 25963*	Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
Theorem	mbfdm2 25964*	The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ dom vol)
Theorem	ismbfcn2 25965*	A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)))
Theorem	ismbfd 25966*	Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d 25981. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	ismbf2d 25967*	Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfeqalem1 25968*	Lemma for mbfeqalem2 25969. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐵 ↦ 𝐶) “ 𝑦) ∖ (◡(𝑥 ∈ 𝐵 ↦ 𝐷) “ 𝑦)) ∈ dom vol)
Theorem	mbfeqalem2 25969*	Lemma for mbfeqa 25970. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn))
Theorem	mbfeqa 25970*	If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn))
Theorem	mbfres 25971	The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ MblFn)
Theorem	mbfres2 25972	Measurability of a piecewise function: if 𝐹 is measurable on subsets 𝐵 and 𝐶 of its domain, and these pieces make up all of 𝐴, then 𝐹 is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ MblFn)    &   ⊢ (𝜑 → (𝐵 ∪ 𝐶) = 𝐴)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfss 25973*	Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn)
Theorem	mbfmulc2lem 25974	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn)
Theorem	mbfmulc2re 25975	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn)
Theorem	mbfmax 25976*	The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ MblFn)
Theorem	mbfneg 25977*	The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn)
Theorem	mbfpos 25978*	The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
Theorem	mbfposr 25979*	Converse to mbfpos 25978. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
Theorem	mbfposb 25980*	A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn)))
Theorem	ismbf3d 25981*	Simplified form of ismbfd 25966. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfimaopnlem 25982*	Lemma for mbfimaopn 25983. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐵 = ((,) “ (ℚ × ℚ))    &   ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol)
Theorem	mbfimaopn 25983	The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25985, which explains why 𝐴 ∈ dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol)
Theorem	mbfimaopn2 25984	The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐵)    ⇒   ⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ ℂ) ∧ 𝐶 ∈ 𝐾) → (◡𝐹 “ 𝐶) ∈ dom vol)
Theorem	cncombf 25985	The composition of a continuous function with a measurable function is measurable. (More generally, 𝐺 can be a Borel-measurable function, but notably the condition that 𝐺 be only measurable is too weak, the usual counterexample taking 𝐺 to be the Cantor function and 𝐹 the indicator function of the 𝐺-image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ MblFn)
Theorem	cnmbf 25986	A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → 𝐹 ∈ MblFn)
Theorem	mbfaddlem 25987	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn)
Theorem	mbfadd 25988	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn)
Theorem	mbfsub 25989	The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ MblFn)
Theorem	mbfmulc2 25990*	A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
Theorem	mbfsup 25991*	The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, 𝐵(𝑛, 𝑥) is a function of both 𝑛 and 𝑥, since it is an 𝑛-indexed sequence of functions on 𝑥. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbfinf 25992*	The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbflimsup 25993*	The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)))    &   ⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*), ℝ*, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbflimlem 25994*	The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
Theorem	mbflim 25995*	The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
Syntax	c0p 25996	Extend class notation to include the zero polynomial.
class 0𝑝
Definition	df-0p 25997	Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ 0𝑝 = (ℂ × {0})
Theorem	0pval 25998	The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (0𝑝‘𝐴) = 0)
Theorem	0plef 25999	Two ways to say that the function 𝐹 on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹))
Theorem	0pledm 26000	Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → (0𝑝 ∘r ≤ 𝐹 ↔ (𝐴 × {0}) ∘r ≤ 𝐹))