![]() |
Metamath
Proof Explorer Theorem List (p. 242 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ovolunlem1 24101* | Lemma for ovolun 24103. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2))) & ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)) & ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolunlem2 24102 | Lemma for ovolun 24103. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolun 24103 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 24109, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | ||
Theorem | ovolunnul 24104 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) | ||
Theorem | ovolfiniun 24105* | The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘∪ 𝑘 ∈ 𝐴 𝐵) ≤ Σ𝑘 ∈ 𝐴 (vol*‘𝐵)) | ||
Theorem | ovoliunlem1 24106* | Lemma for ovoliun 24109. (Contributed by Mario Carneiro, 12-Jun-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛))) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) & ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) & ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿) ⇒ ⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliunlem2 24107* | Lemma for ovoliun 24109. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛))) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) & ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) & ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliunlem3 24108* | Lemma for ovoliun 24109. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliun 24109* | The Lebesgue outer measure function is countably sub-additive. (Many books allow +∞ as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss 24089, so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ sup(ran 𝑇, ℝ*, < )) | ||
Theorem | ovoliun2 24110* | The Lebesgue outer measure function is countably sub-additive. (This version is a little easier to read, but does not allow infinite values like ovoliun 24109.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) | ||
Theorem | ovoliunnul 24111* | A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) | ||
Theorem | shft2rab 24112* | If 𝐵 is a shift of 𝐴 by 𝐶, then 𝐴 is a shift of 𝐵 by -𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) (Revised by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) ⇒ ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ (𝑦 − -𝐶) ∈ 𝐵}) | ||
Theorem | ovolshftlem1 24113* | Lemma for ovolshft 24115. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) ⇒ ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolshftlem2 24114* | Lemma for ovolshft 24115. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀) | ||
Theorem | ovolshft 24115* | The Lebesgue outer measure function is shift-invariant. (Contributed by Mario Carneiro, 22-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) ⇒ ⊢ (𝜑 → (vol*‘𝐴) = (vol*‘𝐵)) | ||
Theorem | sca2rab 24116* | If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) ⇒ ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵}) | ||
Theorem | ovolscalem1 24117* | Lemma for ovolsca 24119. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | ||
Theorem | ovolscalem2 24118* | Lemma for ovolshft 24115. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolsca 24119* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolicc1 24120* | The measure of a closed interval is lower bounded by its length. (Contributed by Mario Carneiro, 13-Jun-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 〈𝐴, 𝐵〉, 〈0, 0〉)) ⇒ ⊢ (𝜑 → (vol*‘(𝐴[,]𝐵)) ≤ (𝐵 − 𝐴)) | ||
Theorem | ovolicc2lem1 24121* | Lemma for ovolicc2 24126. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) | ||
Theorem | ovolicc2lem2 24122* | Lemma for ovolicc2 24126. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵) | ||
Theorem | ovolicc2lem3 24123* | Lemma for ovolicc2 24126. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) | ||
Theorem | ovolicc2lem4 24124* | Lemma for ovolicc2 24126. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by AV, 17-Sep-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} & ⊢ 𝑀 = inf(𝑊, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolicc2lem5 24125* | Lemma for ovolicc2 24126. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolicc2 24126* | The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)((𝐴[,]𝐵) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (vol*‘(𝐴[,]𝐵))) | ||
Theorem | ovolicc 24127 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ovolicopnf 24128 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞) | ||
Theorem | ovolre 24129 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (vol*‘ℝ) = +∞ | ||
Theorem | ismbl 24130* | The predicate "𝐴 is Lebesgue-measurable". A set is measurable if it splits every other set 𝑥 in a "nice" way, that is, if the measure of the pieces 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴 sum up to the measure of 𝑥 (assuming that the measure of 𝑥 is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))))) | ||
Theorem | ismbl2 24131* | From ovolun 24103, it suffices to show that the measure of 𝑥 is at least the sum of the measures of 𝑥 ∩ 𝐴 and 𝑥 ∖ 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.) |
⊢ (𝐴 ∈ dom vol ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) ≤ (vol*‘𝑥)))) | ||
Theorem | volres 24132 | A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ vol = (vol* ↾ dom vol) | ||
Theorem | volf 24133 | The domain and range of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ vol:dom vol⟶(0[,]+∞) | ||
Theorem | mblvol 24134 | The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴)) | ||
Theorem | mblss 24135 | A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ) | ||
Theorem | mblsplit 24136 | The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐵) = ((vol*‘(𝐵 ∩ 𝐴)) + (vol*‘(𝐵 ∖ 𝐴)))) | ||
Theorem | volss 24137 | 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 24138 | The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol) | ||
Theorem | nulmbl 24139 | A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) = 0) → 𝐴 ∈ dom vol) | ||
Theorem | nulmbl2 24140* | 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 24141 | A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) | ||
Theorem | shftmbl 24142* | A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol) | ||
Theorem | 0mbl 24143 | The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ∅ ∈ dom vol | ||
Theorem | rembl 24144 | The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ℝ ∈ dom vol | ||
Theorem | unidmvol 24145 | The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ∪ dom vol = ℝ | ||
Theorem | inmbl 24146 | An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) | ||
Theorem | difmbl 24147 | A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) | ||
Theorem | finiunmbl 24148* | A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | volun 24149 | 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 24150 | Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) | ||
Theorem | volfiniun 24151* | 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 24152* | Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2 24153* | A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | voliunlem1 24154* | Lemma for voliun 24158. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛)))) & ⊢ (𝜑 → 𝐸 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸)) | ||
Theorem | voliunlem2 24155* | Lemma for voliun 24158. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) ⇒ ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) | ||
Theorem | voliunlem3 24156* | Lemma for voliun 24158. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) & ⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | iunmbl 24157 | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) | ||
Theorem | voliun 24158 | 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 24159* | Lemma for volsup 24160. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | volsup 24160* | 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 24161* | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | ioombl1lem1 24162* | Lemma for ioombl1 24166. (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 24163* | Lemma for ioombl1 24166. (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 24164* | Lemma for ioombl1 24166. (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 24165* | Lemma for ioombl1 24166. (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 24166 | 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 24167 | A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol) | ||
Theorem | icombl 24168 | A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol) | ||
Theorem | ioombl 24169 | An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴(,)𝐵) ∈ dom vol | ||
Theorem | iccmbl 24170 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol) | ||
Theorem | iccvolcl 24171 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ) | ||
Theorem | ovolioo 24172 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | volioo 24173 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ioovolcl 24174 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) | ||
Theorem | ovolfs2 24175 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹)) | ||
Theorem | ioorcl2 24176 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) | ||
Theorem | ioorf 24177 | 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 24178* | 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 24179* | 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 24180* | 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 24181* | 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 24182 | 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 24183* | 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 24158.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | uniiccvol 24184* | 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 24158.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → (vol*‘∪ ran ([,] ∘ 𝐹)) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | uniioombllem1 24185* | Lemma for uniioombl 24193. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) | ||
Theorem | uniioombllem2a 24186* | Lemma for uniioombl 24193. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (((𝜑 ∧ 𝐽 ∈ ℕ) ∧ 𝑧 ∈ ℕ) → (((,)‘(𝐹‘𝑧)) ∩ ((,)‘(𝐺‘𝐽))) ∈ ran (,)) | ||
Theorem | uniioombllem2 24187* | Lemma for uniioombl 24193. (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 24188* | Lemma for uniioombl 24193. (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 24189* | Lemma for uniioombl 24193. (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 24190* | Lemma for uniioombl 24193. (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 24191* | Lemma for uniioombl 24193. (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 24192* | Lemma for uniioombl 24193. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶)) ⇒ ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶))) | ||
Theorem | uniioombl 24193* | A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24157.) Lemma 565Ca of [Fremlin5] p. 214. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ∈ dom vol) | ||
Theorem | uniiccmbl 24194* | An almost-disjoint union of closed intervals is measurable. (This proof does not use countable choice, unlike iunmbl 24157.) (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥))) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ∈ dom vol) | ||
Theorem | dyadf 24195* | 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 24196* | Value of the dyadic rational function 𝐹. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (𝐴𝐹𝐵) = 〈(𝐴 / (2↑𝐵)), ((𝐴 + 1) / (2↑𝐵))〉) | ||
Theorem | dyadovol 24197* | Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → (vol*‘([,]‘(𝐴𝐹𝐵))) = (1 / (2↑𝐵))) | ||
Theorem | dyadss 24198* | 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 24199* | Lemma for dyaddisj 24200. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⇒ ⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) | ||
Theorem | dyaddisj 24200* | 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 𝐹) → (([,]‘𝐴) ⊆ ([,]‘𝐵) ∨ ([,]‘𝐵) ⊆ ([,]‘𝐴) ∨ (((,)‘𝐴) ∩ ((,)‘𝐵)) = ∅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |