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