![]() |
Metamath
Proof Explorer Theorem List (p. 256 of 486) | < 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-30854) |
![]() (30855-32377) |
![]() (32378-48571) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ovolcl 25501 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*) | ||
Theorem | ovollb 25502 | The outer volume is a lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolgelb 25503* | The outer volume is the greatest lower bound on the sum of all interval coverings of 𝐴. (Contributed by Mario Carneiro, 15-Jun-2014.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝑔)) ⇒ ⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵))) | ||
Theorem | ovolge0 25504 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴)) | ||
Theorem | ovolf 25505 | The domain and codomain of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
⊢ vol*:𝒫 ℝ⟶(0[,]+∞) | ||
Theorem | ovollecl 25506 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ) | ||
Theorem | ovolsslem 25507* | Lemma for ovolss 25508. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑁 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolss 25508 | The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolsscl 25509 | If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐴) ∈ ℝ) | ||
Theorem | ovolssnul 25510 | A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0) | ||
Theorem | ovollb2lem 25511* | Lemma for ovollb2 25512. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)) | ||
Theorem | ovollb2 25512 | It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb 25502). (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolctb 25513 | The volume of a denumerable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) (Proof shortened by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≈ ℕ) → (vol*‘𝐴) = 0) | ||
Theorem | ovolq 25514 | The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘ℚ) = 0 | ||
Theorem | ovolctb2 25515 | The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0) | ||
Theorem | ovol0 25516 | The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘∅) = 0 | ||
Theorem | ovolfi 25517 | A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0) | ||
Theorem | ovolsn 25518 | A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0) | ||
Theorem | ovolunlem1a 25519* | Lemma for ovolun 25522. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (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*‘𝐵)) + 𝐶)) | ||
Theorem | ovolunlem1 25520* | Lemma for ovolun 25522. (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 25521 | Lemma for ovolun 25522. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolun 25522 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 25528, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | ||
Theorem | ovolunnul 25523 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) | ||
Theorem | ovolfiniun 25524* | 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 25525* | Lemma for ovoliun 25528. (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 25526* | Lemma for ovoliun 25528. (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 25527* | Lemma for ovoliun 25528. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliun 25528* | 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 25508, 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 25529* | 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 25528.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) | ||
Theorem | ovoliunnul 25530* | A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) | ||
Theorem | shft2rab 25531* | 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 25532* | Lemma for ovolshft 25534. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) ⇒ ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolshftlem2 25533* | Lemma for ovolshft 25534. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀) | ||
Theorem | ovolshft 25534* | 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 25535* | If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) ⇒ ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵}) | ||
Theorem | ovolscalem1 25536* | Lemma for ovolsca 25538. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | ||
Theorem | ovolscalem2 25537* | Lemma for ovolshft 25534. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolsca 25538* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolicc1 25539* | 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 25540* | Lemma for ovolicc2 25545. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) | ||
Theorem | ovolicc2lem2 25541* | Lemma for ovolicc2 25545. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵) | ||
Theorem | ovolicc2lem3 25542* | Lemma for ovolicc2 25545. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) | ||
Theorem | ovolicc2lem4 25543* | Lemma for ovolicc2 25545. (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 25544* | Lemma for ovolicc2 25545. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolicc2 25545* | 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 25546 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ovolicopnf 25547 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞) | ||
Theorem | ovolre 25548 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (vol*‘ℝ) = +∞ | ||
Theorem | ismbl 25549* | 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 25550* | From ovolun 25522, 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 25551 | A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ vol = (vol* ↾ dom vol) | ||
Theorem | volf 25552 | The domain and codomain of the Lebesgue measure function. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ vol:dom vol⟶(0[,]+∞) | ||
Theorem | mblvol 25553 | 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 25554 | A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ) | ||
Theorem | mblsplit 25555 | The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → (vol*‘𝐵) = ((vol*‘(𝐵 ∩ 𝐴)) + (vol*‘(𝐵 ∖ 𝐴)))) | ||
Theorem | volss 25556 | 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 25557 | The complement of a measurable set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (𝐴 ∈ dom vol → (ℝ ∖ 𝐴) ∈ dom vol) | ||
Theorem | nulmbl 25558 | A nullset is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) = 0) → 𝐴 ∈ dom vol) | ||
Theorem | nulmbl2 25559* | 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 25560 | A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) | ||
Theorem | shftmbl 25561* | A shift of a measurable set is measurable. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝑥 − 𝐵) ∈ 𝐴} ∈ dom vol) | ||
Theorem | 0mbl 25562 | The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ∅ ∈ dom vol | ||
Theorem | rembl 25563 | The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ℝ ∈ dom vol | ||
Theorem | unidmvol 25564 | The union of the Lebesgue measurable sets is ℝ. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
⊢ ∪ dom vol = ℝ | ||
Theorem | inmbl 25565 | An intersection of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) | ||
Theorem | difmbl 25566 | A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) | ||
Theorem | finiunmbl 25567* | A finite union of measurable sets is measurable. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | volun 25568 | 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 25569 | Addition of non-disjoint sets. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ ((vol‘𝐴) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) | ||
Theorem | volfiniun 25570* | 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 25571* | Rewrite a countable union as a disjoint union. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2 25572* | A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | voliunlem1 25573* | Lemma for voliun 25577. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝐸 ∩ (𝐹‘𝑛)))) & ⊢ (𝜑 → 𝐸 ⊆ ℝ) & ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( + , 𝐻)‘𝑘) + (vol*‘(𝐸 ∖ ∪ ran 𝐹))) ≤ (vol*‘𝐸)) | ||
Theorem | voliunlem2 25574* | Lemma for voliun 25577. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) ⇒ ⊢ (𝜑 → ∪ ran 𝐹 ∈ dom vol) | ||
Theorem | voliunlem3 25575* | Lemma for voliun 25577. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶dom vol) & ⊢ (𝜑 → Disj 𝑖 ∈ ℕ (𝐹‘𝑖)) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (vol*‘(𝑥 ∩ (𝐹‘𝑛)))) & ⊢ 𝑆 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol‘(𝐹‘𝑛))) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ (vol‘(𝐹‘𝑖)) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol‘∪ ran 𝐹) = sup(ran 𝑆, ℝ*, < )) | ||
Theorem | iunmbl 25576 | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ∪ 𝑛 ∈ ℕ 𝐴 ∈ dom vol) | ||
Theorem | voliun 25577 | 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 25578* | Lemma for volsup 25579. (Contributed by Mario Carneiro, 4-Jul-2014.) |
⊢ ((∀𝑛 ∈ ℕ (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘𝐴))) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | volsup 25579* | 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 25580* | The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 𝐵 ∈ dom vol) → ∪ 𝑛 ∈ 𝐴 𝐵 ∈ dom vol) | ||
Theorem | ioombl1lem1 25581* | Lemma for ioombl1 25585. (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 25582* | Lemma for ioombl1 25585. (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 25583* | Lemma for ioombl1 25585. (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 25584* | Lemma for ioombl1 25585. (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 25585 | 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 25586 | A closed unbounded-above interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ dom vol) | ||
Theorem | icombl 25587 | A closed-below, open-above real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → (𝐴[,)𝐵) ∈ dom vol) | ||
Theorem | ioombl 25588 | An open real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ (𝐴(,)𝐵) ∈ dom vol | ||
Theorem | iccmbl 25589 | A closed real interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol) | ||
Theorem | iccvolcl 25590 | A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ) | ||
Theorem | ovolioo 25591 | The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | volioo 25592 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ioovolcl 25593 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ) | ||
Theorem | ovolfs2 25594 | Alternative expression for the interval length function. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺 = ((vol* ∘ (,)) ∘ 𝐹)) | ||
Theorem | ioorcl2 25595 | An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.) |
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) | ||
Theorem | ioorf 25596 | 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 25597* | 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 25598* | 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 25599* | 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 25600* | 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*‘𝐴) ∈ ℝ) → (𝐹‘𝐴) ∈ ( ≤ ∩ (ℝ × ℝ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |