| Metamath
Proof Explorer Theorem List (p. 257 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iccmbl 25601 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol) | ||
| Theorem | iccvolcl 25602 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ) | ||
| Theorem | ovolioo 25603 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
| Theorem | volioo 25604 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
| Theorem | ioovolcl 25605 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) | ||
| Theorem | ovolfs2 25606 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹)) | ||
| Theorem | ioorcl2 25607 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) | ||
| Theorem | ioorf 25608 | 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 25609* | 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 25610* | 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 25611* | 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 25612* | 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 25613 | 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 25614* | 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 25589.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
| Theorem | uniiccvol 25615* | 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 25589.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
| Theorem | uniioombllem1 25616* | Lemma for uniioombl 25624. (Contributed by Mario Carneiro, 25-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) | ||
| Theorem | uniioombllem2a 25617* | Lemma for uniioombl 25624. (Contributed by Mario Carneiro, 7-May-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) | ||
| Theorem | uniioombllem2 25618* | Lemma for uniioombl 25624. (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 25619* | Lemma for uniioombl 25624. (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 25620* | Lemma for uniioombl 25624. (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 25621* | Lemma for uniioombl 25624. (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 25622* | Lemma for uniioombl 25624. (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 25623* | Lemma for uniioombl 25624. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) | ||
| Theorem | uniioombl 25624* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25588.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol) | ||
| Theorem | uniiccmbl 25625* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 25588.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ∈ dom vol) | ||
| Theorem | dyadf 25626* | 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 25627* | Value of the dyadic rational function 𝐹. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (𝐴𝐹𝐵) = 〈(𝐴 / (2↑𝐵)), ((𝐴 + 1) / (2↑𝐵))〉) | ||
| Theorem | dyadovol 25628* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (vol*‘([,]‘(𝐴𝐹𝐵))) = (1 / (2↑𝐵))) | ||
| Theorem | dyadss 25629* | 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 25630* | Lemma for dyaddisj 25631. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) | ||
| Theorem | dyaddisj 25631* | 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 25632* | Lemma for dyadmax 25633. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ¬ 𝐷 < 𝐶) & ⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
| Theorem | dyadmax 25633* | 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 25634* | Lemma for dyadmbl 25635. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} & ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) ⇒ ⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,] “ 𝐺)) | ||
| Theorem | dyadmbl 25635* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} & ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) ⇒ ⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol) | ||
| Theorem | opnmbllem 25636* | Lemma for opnmbl 25637. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) | ||
| Theorem | opnmbl 25637 | All open sets are measurable. This proof, via dyadmbl 25635 and uniioombl 25624, 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 25638 | All open sets are measurable. This alternative proof of opnmbl 25637 is significantly shorter, at the expense of invoking countable choice ax-cc 10475. (This was also the original proof before the current opnmbl 25637 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) | ||
| Theorem | subopnmbl 25639 | 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 25640* | 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 25641* | 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 25642* | 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 25643* | Lemma for vitali 25648. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
| ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} ⇒ ⊢ ∼ Er (0[,]1) | ||
| Theorem | vitalilem2 25644* | Lemma for vitali 25648. (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 25645* | Lemma for vitali 25648. (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 25646* | Lemma for vitali 25648. (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 25647* | Lemma for vitali 25648. (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 25648 | 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 ⊊ 𝒫 ℝ) | ||
| Syntax | cmbf 25649 | Extend class notation with the class of measurable functions. |
| class MblFn | ||
| Syntax | citg1 25650 | Extend class notation with the Lebesgue integral for simple functions. |
| class ∫1 | ||
| Syntax | citg2 25651 | Extend class notation with the Lebesgue integral for nonnegative functions. |
| class ∫2 | ||
| Syntax | cibl 25652 | Extend class notation with the class of integrable functions. |
| class 𝐿1 | ||
| Syntax | citg 25653 | Extend class notation with the general Lebesgue integral. |
| class ∫𝐴𝐵 d𝑥 | ||
| Definition | df-mbf 25654* | 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 25561) 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 25655* | 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 25656* | 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 25657* | 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 25658* | 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 25656 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 25656 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.) |
| ⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))) | ||
| Theorem | ismbf1 25659* | The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 25663 and ismbfcn 25664 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 25660 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) | ||
| Theorem | mbfdm 25661 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol) | ||
| Theorem | mbfconstlem 25662 | Lemma for mbfconst 25668 and related theorems. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ ((𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ) → (◡(𝐴 × {𝐶}) “ 𝐵) ∈ dom vol) | ||
| Theorem | ismbf 25663* | 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 25561. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) | ||
| Theorem | ismbfcn 25664 | 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 25665 | 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 25666 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (◡𝐹 “ (𝐵[,]𝐶)) ∈ dom vol) | ||
| Theorem | mbfimasn 25667 | The preimage of a point under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ ∧ 𝐵 ∈ ℝ) → (◡𝐹 “ {𝐵}) ∈ dom vol) | ||
| Theorem | mbfconst 25668 | A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ MblFn) | ||
| Theorem | mbf0 25669 | The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018.) |
| ⊢ ∅ ∈ MblFn | ||
| Theorem | mbfid 25670 | The identity function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ (𝐴 ∈ dom vol → ( I ↾ 𝐴) ∈ MblFn) | ||
| Theorem | mbfmptcl 25671* | Lemma for the MblFn predicate applied to a mapping operation. (Contributed by Mario Carneiro, 11-Aug-2014.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | ||
| Theorem | mbfdm2 25672* | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Aug-2014.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 ∈ dom vol) | ||
| Theorem | ismbfcn2 25673* | 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 25674* | 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 25689. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
| Theorem | ismbf2d 25675* | Deduction to prove measurability of a real function. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (-∞(,)𝑥)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
| Theorem | mbfeqalem1 25676* | Lemma for mbfeqalem2 25677. (Contributed by Mario Carneiro, 2-Sep-2014.) (Revised by AV, 19-Aug-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((◡(𝑥 ∈ 𝐵 ↦ 𝐶) “ 𝑦) ∖ (◡(𝑥 ∈ 𝐵 ↦ 𝐷) “ 𝑦)) ∈ dom vol) | ||
| Theorem | mbfeqalem2 25677* | Lemma for mbfeqa 25678. (Contributed by Mario Carneiro, 2-Sep-2014.) (Proof shortened by AV, 19-Aug-2022.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐴) = 0) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ MblFn)) | ||
| Theorem | mbfeqa 25678* | 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 25679 | The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ MblFn) | ||
| Theorem | mbfres2 25680 | 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 25681* | Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014.) |
| ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ dom vol) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn) | ||
| Theorem | mbfmulc2lem 25682 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn) | ||
| Theorem | mbfmulc2re 25683 | Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn) | ||
| Theorem | mbfmax 25684* | The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥))) ⇒ ⊢ (𝜑 → 𝐻 ∈ MblFn) | ||
| Theorem | mbfneg 25685* | The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) | ||
| Theorem | mbfpos 25686* | The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) | ||
| Theorem | mbfposr 25687* | Converse to mbfpos 25686. (Contributed by Mario Carneiro, 11-Aug-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | ||
| Theorem | mbfposb 25688* | 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 25689* | Simplified form of ismbfd 25674. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol) ⇒ ⊢ (𝜑 → 𝐹 ∈ MblFn) | ||
| Theorem | mbfimaopnlem 25690* | Lemma for mbfimaopn 25691. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐵 = ((,) “ (ℚ × ℚ)) & ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol) | ||
| Theorem | mbfimaopn 25691 | The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25693, 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 25692 | 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 25693 | 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 25694 | 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 25695 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) & ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) & ⊢ (𝜑 → 𝐺:𝐴⟶ℝ) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
| Theorem | mbfadd 25696 | The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.) |
| ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) | ||
| Theorem | mbfsub 25697 | The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.) |
| ⊢ (𝜑 → 𝐹 ∈ MblFn) & ⊢ (𝜑 → 𝐺 ∈ MblFn) ⇒ ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ MblFn) | ||
| Theorem | mbfmulc2 25698* | A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.) |
| ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) | ||
| Theorem | mbfsup 25699* | 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 25700* | 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) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |