Home | Metamath
Proof Explorer Theorem List (p. 234 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | volss 23301 | The Lebesgue measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 17-Oct-2017.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ 𝐴 ⊆ 𝐵) → (vol‘𝐴) ≤ (vol‘𝐵)) | ||
Theorem | cmmbl 23302 | The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol) | ||
Theorem | nulmbl 23303 | A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) = 0) → 𝐴 ∈ dom vol) | ||
Theorem | nulmbl2 23304* | A set of outer measure zero is measurable. The term "outer measure zero" here is slightly different from "nullset/negligible set"; a nullset has vol*(𝐴) = 0 while "outer measure zero" means that for any 𝑥 there is a 𝑦 containing 𝐴 with volume less than 𝑥. Assuming AC, these notions are equivalent (because the intersection of all such 𝑦 is a nullset) but in ZF this is a strictly weaker notion. Proposition 563Gb of [Fremlin5] p. 193. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ dom vol(𝐴 ⊆ 𝑦 ∧ (vol*‘𝑦) ≤ 𝑥) → 𝐴 ∈ dom vol) | ||
Theorem | unmbl 23305 | A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) | ||
Theorem | shftmbl 23306* | A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol) | ||
Theorem | 0mbl 23307 | The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ∅ ∈ dom vol | ||
Theorem | rembl 23308 | The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ℝ ∈ dom vol | ||
Theorem | unidmvol 23309 | The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ∪ dom vol = ℝ | ||
Theorem | inmbl 23310 | An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) | ||
Theorem | difmbl 23311 | A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) | ||
Theorem | finiunmbl 23312* | A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | volun 23313 | The Lebesgue measure function is finitely additive. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵))) | ||
Theorem | volinun 23314 | Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) | ||
Theorem | volfiniun 23315* | The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ∈ dom vol ∧ (vol‘𝐵) ∈ ℝ) ∧ Disj 𝑘 ∈ 𝐴 𝐵) → (vol‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (vol‘𝐵)) | ||
Theorem | iundisj 23316* | Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2 23317* | A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | voliunlem1 23318* | Lemma for voliun 23322. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛)))) & ⊢ (𝜑 → 𝐸 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸)) | ||
Theorem | voliunlem2 23319* | Lemma for voliun 23322. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) ⇒ ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) | ||
Theorem | voliunlem3 23320* | Lemma for voliun 23322. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) & ⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | iunmbl 23321 | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) | ||
Theorem | voliun 23322 | 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 23323* | Lemma for volsup 23324. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | volsup 23324* | 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 23325* | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | ioombl1lem1 23326* | Lemma for ioombl1 23330. (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 23327* | Lemma for ioombl1 23330. (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 23328* | Lemma for ioombl1 23330. (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 23329* | Lemma for ioombl1 23330. (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 23330 | 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 23331 | A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol) | ||
Theorem | icombl 23332 | A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol) | ||
Theorem | ioombl 23333 | An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴(,)𝐵) ∈ dom vol | ||
Theorem | iccmbl 23334 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol) | ||
Theorem | iccvolcl 23335 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ) | ||
Theorem | ovolioo 23336 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | volioo 23337 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ioovolcl 23338 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) | ||
Theorem | ovolfs2 23339 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹)) | ||
Theorem | ioorcl2 23340 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) | ||
Theorem | ioorf 23341 | 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 23342* | 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 23343* | 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 23344* | 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 23345* | 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 23346 | 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 23347* | 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 23322.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | uniiccvol 23348* | 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 23322.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | uniioombllem1 23349* | Lemma for uniioombl 23357. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) | ||
Theorem | uniioombllem2a 23350* | Lemma for uniioombl 23357. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) | ||
Theorem | uniioombllem2 23351* | Lemma for uniioombl 23357. (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 23352* | Lemma for uniioombl 23357. (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 23353* | Lemma for uniioombl 23357. (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 23354* | Lemma for uniioombl 23357. (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 23355* | Lemma for uniioombl 23357. (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 23356* | Lemma for uniioombl 23357. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) | ||
Theorem | uniioombl 23357* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 23321.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol) | ||
Theorem | uniiccmbl 23358* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 23321.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ∈ dom vol) | ||
Theorem | dyadf 23359* | 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 23360* | Value of the dyadic rational function 𝐹. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (𝐴𝐹𝐵) = 〈(𝐴 / (2↑𝐵)), ((𝐴 + 1) / (2↑𝐵))〉) | ||
Theorem | dyadovol 23361* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (vol*‘([,]‘(𝐴𝐹𝐵))) = (1 / (2↑𝐵))) | ||
Theorem | dyadss 23362* | 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 23363* | Lemma for dyaddisj 23364. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) | ||
Theorem | dyaddisj 23364* | 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 23365* | Lemma for dyadmax 23366. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ¬ 𝐷 < 𝐶) & ⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | ||
Theorem | dyadmax 23366* | 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 23367* | Lemma for dyadmbl 23368. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} & ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) ⇒ ⊢ (𝜑 → ∪ ([,] “ 𝐴) = ∪ ([,] “ 𝐺)) | ||
Theorem | dyadmbl 23368* | Any union of dyadic rational intervals is measurable. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) & ⊢ 𝐺 = {𝑧 ∈ 𝐴 ∣ ∀𝑤 ∈ 𝐴 (([,]‘𝑧) ⊆ ([,]‘𝑤) → 𝑧 = 𝑤)} & ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) ⇒ ⊢ (𝜑 → ∪ ([,] “ 𝐴) ∈ dom vol) | ||
Theorem | opnmbllem 23369* | Lemma for opnmbl 23370. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) | ||
Theorem | opnmbl 23370 | All open sets are measurable. This proof, via dyadmbl 23368 and uniioombl 23357, 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 23371 | All open sets are measurable. This alternative proof of opnmbl 23370 is significantly shorter, at the expense of invoking countable choice ax-cc 9257. (This was also the original proof before the current opnmbl 23370 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) | ||
Theorem | subopnmbl 23372 | 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 23373* | 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 23374* | 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 23375* | 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 23376* | Lemma for vitali 23382. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof shortened by AV, 1-May-2021.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} ⇒ ⊢ ∼ Er (0[,]1) | ||
Theorem | vitalilem1OLD 23377* | Obsolete proof of vitalilem1 23376 as of 1-May-2021. Lemma for vitali 23382. (Contributed by Mario Carneiro, 16-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)} ⇒ ⊢ ∼ Er (0[,]1) | ||
Theorem | vitalilem2 23378* | Lemma for vitali 23382. (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 23379* | Lemma for vitali 23382. (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 23380* | Lemma for vitali 23382. (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 23381* | Lemma for vitali 23382. (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 23382 | 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 23383 | Extend class notation with the class of measurable functions. |
class MblFn | ||
Syntax | citg1 23384 | Extend class notation with the Lebesgue integral for simple functions. |
class ∫1 | ||
Syntax | citg2 23385 | Extend class notation with the Lebesgue integral for nonnegative functions. |
class ∫2 | ||
Syntax | cibl 23386 | Extend class notation with the class of integrable functions. |
class 𝐿1 | ||
Syntax | citg 23387 | Extend class notation with the general Lebesgue integral. |
class ∫𝐴𝐵 d𝑥 | ||
Definition | df-mbf 23388* | 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 23294) 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 23389* | 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 23390* | 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[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < )) | ||
Definition | df-ibl 23391* | 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 23392* | 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 23390 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 23390 directly for this use-case.) (Contributed by Mario Carneiro, 28-Jun-2014.) |
⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))) | ||
Theorem | ismbf1 23393* | The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 23397 and ismbfcn 23398 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 23394 | A measurable function is a function into the complex numbers. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) | ||
Theorem | mbfdm 23395 | The domain of a measurable function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol) | ||
Theorem | mbfconstlem 23396 | Lemma for mbfconst 23402. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐶 ∈ ℝ) → (◡(𝐴 × {𝐶}) “ 𝐵) ∈ dom vol) | ||
Theorem | ismbf 23397* | 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 23294. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) | ||
Theorem | ismbfcn 23398 | 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 23399 | 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 23400 | The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (◡𝐹 “ (𝐵[,]𝐶)) ∈ dom vol) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |