Home | Metamath
Proof Explorer Theorem List (p. 395 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | caragenuni 39401 | The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → ∪ 𝑆 = ∪ dom 𝑂) | ||
Theorem | caragenuncllem 39402 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ (𝐸 ∪ 𝐹))) +𝑒 (𝑂‘(𝐴 ∖ (𝐸 ∪ 𝐹)))) = (𝑂‘𝐴)) | ||
Theorem | caragenuncl 39403 | The Caratheodory's construction is closed under the union. Step (c) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ 𝑆) | ||
Theorem | caragendifcl 39404 | The Caratheodory's construction is closed under the complement operation. Second part of Step (b) in the proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) ⇒ ⊢ (𝜑 → (∪ 𝑆 ∖ 𝐸) ∈ 𝑆) | ||
Theorem | caragenfiiuncl 39405* | The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆) | ||
Theorem | omeunle 39406 | The outer measure of the union of two sets is less or equal to the sum of the measures, Remark 113B (c) of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝐵 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘(𝐴 ∪ 𝐵)) ≤ ((𝑂‘𝐴) +𝑒 (𝑂‘𝐵))) | ||
Theorem | omeiunle 39407* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | omelesplit 39408 | The outer measure of a set 𝐴 is less than or equal to the extended addition of the outer measures of the decomposition induced on 𝐴 by any 𝐸. Step (a) in the proof of Caratheodory's Method, Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘(𝐴 ∩ 𝐸)) +𝑒 (𝑂‘(𝐴 ∖ 𝐸)))) | ||
Theorem | omeiunltfirp 39409* | If the outer measure of a countable union is not +∞, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) & ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐸‘𝑛)) + 𝑌)) | ||
Theorem | omeiunlempt 39410* | The outer measure of the indexed union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ Ⅎ𝑛𝜑 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ≥‘𝑁) & ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐸 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 𝐸) ≤ (Σ^‘(𝑛 ∈ 𝑍 ↦ (𝑂‘𝐸)))) | ||
Theorem | carageniuncllem1 39411* | The outer measure of 𝐴 ∩ (𝐺‘𝑛) is the sum of the outer measures of 𝐴 ∩ (𝐹‘𝑚). These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) & ⊢ (𝜑 → 𝐾 ∈ 𝑍) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝐾)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝐾)))) | ||
Theorem | carageniuncllem2 39412* | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → 𝑌 ∈ ℝ+) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) ⇒ ⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) | ||
Theorem | carageniuncl 39413* | The Caratheodory's construction is closed under indexed countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∈ 𝑆) | ||
Theorem | caragenunicl 39414 | The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of [Fremlin1] p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝑋 ⊆ 𝑆) & ⊢ (𝜑 → 𝑋 ≼ ω) ⇒ ⊢ (𝜑 → ∪ 𝑋 ∈ 𝑆) | ||
Theorem | caragensal 39415 | Caratheodory's method generates a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
Theorem | caratheodorylem1 39416* | Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐸:𝑍⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodorylem2 39417* | Caratheodory's construction is sigma-additive. Main part of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸:ℕ⟶𝑆) & ⊢ (𝜑 → Disj 𝑛 ∈ ℕ (𝐸‘𝑛)) & ⊢ 𝐺 = (𝑘 ∈ ℕ ↦ ∪ 𝑛 ∈ (1...𝑘)(𝐸‘𝑛)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ ℕ (𝐸‘𝑛)) = (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝐸‘𝑛))))) | ||
Theorem | caratheodory 39418 | Caratheodory's construction of a measure given an outer measure. Proof of Theorem 113C of [Fremlin1] p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → (𝑂 ↾ 𝑆) ∈ Meas) | ||
Theorem | 0ome 39419* | The map that assigns 0 to every subset, is an outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝑂 = (𝑥 ∈ 𝒫 𝑋 ↦ 0) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | isomenndlem 39420* | 𝑂 is sub-additive w.r.t. countable indexed union, implies that 𝑂 is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ (𝜑 → 𝑌 ⊆ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) & ⊢ (𝜑 → 𝐵 ⊆ ℕ) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑌) & ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝐵, (𝐹‘𝑛), ∅)) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑌) ≤ (Σ^‘(𝑂 ↾ 𝑌))) | ||
Theorem | isomennd 39421* | Sufficient condition to prove that 𝑂 is an outer measure. Definition 113A of [Fremlin1] p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑂:𝒫 𝑋⟶(0[,]+∞)) & ⊢ (𝜑 → (𝑂‘∅) = 0) & ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥) → (𝑂‘𝑦) ≤ (𝑂‘𝑥)) & ⊢ ((𝜑 ∧ 𝑎:ℕ⟶𝒫 𝑋) → (𝑂‘∪ 𝑛 ∈ ℕ (𝑎‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ (𝑂‘(𝑎‘𝑛))))) ⇒ ⊢ (𝜑 → 𝑂 ∈ OutMeas) | ||
Theorem | caragenel2d 39422* | Membership in the Caratheodory's construction. Similar to carageneld 39392, but here "less then or equal" is used, instead of equality. This is Remark 113D of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑆 = (CaraGen‘𝑂) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝑋) → ((𝑂‘(𝑎 ∩ 𝐸)) +𝑒 (𝑂‘(𝑎 ∖ 𝐸))) ≤ (𝑂‘𝑎)) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Theorem | omege0 39423 | If the outer measure of a set is greater than or equal to 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 0 ≤ (𝑂‘𝐴)) | ||
Theorem | omess0 39424 | If the outer measure of a set is 0, then the outer measure of its subsets is 0. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) = 0) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝑂‘𝐵) = 0) | ||
Theorem | caragencmpl 39425 | A measure built with the Caratheodory's construction is complete. See Definition 112Df of [Fremlin1] p. 19. This is Exercise 113Xa of [Fremlin1] p. 21 (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ (𝜑 → 𝐸 ⊆ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐸) = 0) & ⊢ 𝑆 = (CaraGen‘𝑂) ⇒ ⊢ (𝜑 → 𝐸 ∈ 𝑆) | ||
Proofs for most of the theorems in section 115 of [Fremlin1] | ||
Syntax | covoln 39426 | Extend class notation with the class of Lebesgue outer measure for the space of multidimensional real numbers. |
class voln* | ||
Definition | df-ovoln 39427* | Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑥) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Syntax | cvoln 39428 | Extend class notation with the class of Lebesgue measure for the space of multidimensional real numbers. |
class voln | ||
Definition | df-voln 39429 | Define the Lebesgue measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ voln = (𝑥 ∈ Fin ↦ ((voln*‘𝑥) ↾ (CaraGen‘(voln*‘𝑥)))) | ||
Theorem | vonval 39430 | Value of the Lebesgue measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln‘𝑋) = ((voln*‘𝑋) ↾ (CaraGen‘(voln*‘𝑋)))) | ||
Theorem | ovnval 39431* | Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))) | ||
Theorem | elhoi 39432* | Membership in a multidimensional half-open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑌 ∈ ((𝐴[,)𝐵) ↑𝑚 𝑋) ↔ (𝑌:𝑋⟶ℝ* ∧ ∀𝑥 ∈ 𝑋 (𝑌‘𝑥) ∈ (𝐴[,)𝐵)))) | ||
Theorem | icoresmbl 39433 | A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ran ([,) ↾ (ℝ × ℝ)) ⊆ dom vol | ||
Theorem | hoissre 39434* | The projection of a half-open interval onto a single dimension is a subset of ℝ. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (([,) ∘ 𝐼)‘𝑘) ⊆ ℝ) | ||
Theorem | ovnval2 39435* | Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < ))) | ||
Theorem | volicorecl 39436 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ) | ||
Theorem | hoiprodcl 39437* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝐼)‘𝑘)) ∈ (0[,)+∞)) | ||
Theorem | hoicvr 39438* | 𝐼 is a countable set of half-open intervals that covers the whole multidimensional reals. See Definition 1135 (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑥 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) & ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (ℝ ↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑖 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑖)) | ||
Theorem | hoissrrn 39439* | A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) ⊆ (ℝ ↑𝑚 𝑋)) | ||
Theorem | ovn0val 39440 | The Lebesgue outer measure (for the zero dimensional space of reals) of every subset is zero. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 ∅)) ⇒ ⊢ (𝜑 → ((voln*‘∅)‘𝐴) = 0) | ||
Theorem | ovnn0val 39441* | The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | ovnval2b 39442* | Value of the Lebesgue outer measure of a subset 𝐴 of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝐿 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf((𝐿‘𝐴), ℝ*, < ))) | ||
Theorem | volicorescl 39443 | The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝐴 ∈ ran ([,) ↾ (ℝ × ℝ)) → (vol‘𝐴) ∈ ℝ) | ||
Theorem | ovnprodcl 39444* | The product used in the definition of the outer Lebesgue measure in R^n is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐹:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐼 ∈ ℕ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝐹‘𝐼))‘𝑘)) ∈ (0[,)+∞)) | ||
Theorem | hoiprodcl2 39445* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) & ⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) ⇒ ⊢ (𝜑 → (𝐿‘𝐼) ∈ (0[,)+∞)) | ||
Theorem | hoicvrrex 39446* | Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | ||
Theorem | ovnsupge0 39447* | The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → 𝑀 ⊆ (0[,]+∞)) | ||
Theorem | ovnlecvr 39448* | Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with 𝑋 the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) & ⊢ (𝜑 → 𝐼:ℕ⟶((ℝ × ℝ) ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝐼‘𝑗))‘𝑘)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝐼‘𝑗))))) | ||
Theorem | ovnpnfelsup 39449* | +∞ is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → +∞ ∈ 𝑀) | ||
Theorem | ovnsslelem 39450* | The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝑁 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐵 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵)) | ||
Theorem | ovnssle 39451 | The (multidimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ ((voln*‘𝑋)‘𝐵)) | ||
Theorem | ovnlerp 39452* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑀 𝑧 ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸)) | ||
Theorem | ovnf 39453 | The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ ↑𝑚 𝑋)⟶(0[,]+∞)) | ||
Theorem | ovncvrrp 39454* | The Lebesgue outer measure of a subset of multidimensional real numbers can always be approximated by the total outer measure of a cover of half-open (multidimensional) intervals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) ⇒ ⊢ (𝜑 → ∃𝑖 𝑖 ∈ ((𝐷‘𝐴)‘𝐸)) | ||
Theorem | ovn0lem 39455* | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} & ⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈ (0[,]+∞)) & ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) ⇒ ⊢ (𝜑 → inf(𝑀, ℝ*, < ) = 0) | ||
Theorem | ovn0 39456 | For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘∅) = 0) | ||
Theorem | ovncl 39457 | The Lebesgue outer measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ (0[,]+∞)) | ||
Theorem | ovn02 39458 | For the zero-dimensional space, voln* assigns zero to every subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (voln*‘∅) = (𝑥 ∈ 𝒫 {∅} ↦ 0) | ||
Theorem | ovnxrcl 39459 | The Lebesgue outer measure of a set is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ*) | ||
Theorem | ovnsubaddlem1 39460* | The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {ℎ ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛)))) & ⊢ (𝜑 → 𝐹:ℕ–1-1-onto→(ℕ × ℕ)) & ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸)) | ||
Theorem | ovnsubaddlem2 39461* | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸)) | ||
Theorem | ovnsubadd 39462* | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛))))) | ||
Theorem | ovnome 39463 | (voln*‘𝑋) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set 𝑋. Proposition 115D (a) of [Fremlin1] p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln*‘𝑋) ∈ OutMeas) | ||
Theorem | vonmea 39464 | (voln‘𝑋) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set 𝑋. Comments in Definition 115E of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (voln‘𝑋) ∈ Meas) | ||
Theorem | volicon0 39465 | The measure of a nonempty left-closed, right-open interval. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (vol‘(𝐴[,)𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | hsphoif 39466* | 𝐻 is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑎‘𝑗), if((𝑎‘𝑗) ≤ 𝑥, (𝑎‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐻‘𝐴)‘𝐵):𝑋⟶ℝ) | ||
Theorem | hoidmvval 39467* | The dimensional volume of a multidimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = if(𝑋 = ∅, 0, ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))) | ||
Theorem | hoissrrn2 39468* | A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (𝐴[,)𝐵) ⊆ (ℝ ↑𝑚 𝑋)) | ||
Theorem | hsphoival 39469* | 𝐻 is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑎‘𝑗), if((𝑎‘𝑗) ≤ 𝑥, (𝑎‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝐻‘𝐴)‘𝐵)‘𝐾) = if(𝐾 ∈ 𝑌, (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝐴, (𝐵‘𝐾), 𝐴))) | ||
Theorem | hoiprodcl3 39470* | The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘(𝐴[,)𝐵)) ∈ (0[,)+∞)) | ||
Theorem | volicore 39471 | The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ) | ||
Theorem | hoidmvcl 39472* | The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈ (0[,)+∞)) | ||
Theorem | hoidmv0val 39473* | The dimensional volume of a 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝐴:∅⟶ℝ) & ⊢ (𝜑 → 𝐵:∅⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘∅)𝐵) = 0) | ||
Theorem | hoidmvn0val 39474* | The dimensional volume of a non 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
Theorem | hsphoidmvle2 39475* | The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑋 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)((𝐻‘𝐷)‘𝐵))) | ||
Theorem | hsphoidmvle 39476* | The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑋 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | hoidmvval0 39477* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ Ⅎ𝑗𝜑 & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = 0) | ||
Theorem | hoiprodp1 39478* | The dimensional volume of a half-open interval with dimension 𝑛 + 1. Used in the first equality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) & ⊢ 𝑋 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐺 = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) | ||
Theorem | sge0hsphoire 39479* | If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝑆 ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) | ||
Theorem | hoidmvval0b 39480* | The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐴) = 0) | ||
Theorem | hoidmv1lelem1 39481* | The supremum of 𝑈 belongs to 𝑈. This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐶:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷:ℕ⟶ℝ) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) & ⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) | ||
Theorem | hoidmv1lelem2 39482* | This is the contradiction proven in step (c) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷:ℕ⟶ℝ) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) & ⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ≤ 𝑆) & ⊢ (𝜑 → 𝑆 < 𝐵) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ ((𝐶‘𝐾)[,)(𝐷‘𝐾))) & ⊢ 𝑀 = if((𝐷‘𝐾) ≤ 𝐵, (𝐷‘𝐾), 𝐵) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) | ||
Theorem | hoidmv1lelem3 39483* | The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the non-empty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐶:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷:ℕ⟶ℝ) & ⊢ (𝜑 → (𝐴[,)𝐵) ⊆ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) & ⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) | ||
Theorem | hoidmv1le 39484* | The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ 𝑋 = {𝑍} & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) | ||
Theorem | hoidmvlelem1 39485* | The supremum of 𝑈 belongs to 𝑈. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) & ⊢ (𝜑 → (𝐴‘𝑍) < (𝐵‘𝑍)) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝑈) | ||
Theorem | hoidmvlelem2 39486* | This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) & ⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) & ⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗))) & ⊢ 𝑂 = ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) & ⊢ 𝑉 = ({(𝐵‘𝑍)} ∪ 𝑂) & ⊢ 𝑄 = inf(𝑉, ℝ, < ) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) | ||
Theorem | hoidmvlelem3 39487* | This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) & ⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ℎ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ 𝑂 = (𝑥 ∈ X𝑘 ∈ 𝑌 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ↦ (𝑘 ∈ 𝑊 ↦ if(𝑘 ∈ 𝑌, (𝑥‘𝑘), 𝑆))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) | ||
Theorem | hoidmvlelem4 39488* | The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29, case nonempty interval and dimension of the space greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ℎ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))) | ||
Theorem | hoidmvlelem5 39489* | The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑊)) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)∀ℎ ∈ ((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) | ||
Theorem | hoidmvle 39490* | The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) | ||
Theorem | ovnhoilem1 39491* | The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
Theorem | ovnhoilem2 39492* | The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝐹 = (𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) & ⊢ 𝑆 = (𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) | ||
Theorem | ovnhoi 39493* | The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
Theorem | dmovn 39494 | The domain of the Lebesgue outer measure is the power set of the n-dimensional Real numbers. Step (a)(i) of the proof of Proposition 115D (a) of [Fremlin1] p. 30 (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → dom (voln*‘𝑋) = 𝒫 (ℝ ↑𝑚 𝑋)) | ||
Theorem | hoicoto2 39495* | The half-open interval expressed using a composition of a function into (ℝ × ℝ) and using two distinct real valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐼:𝑋⟶(ℝ × ℝ)) & ⊢ 𝐴 = (𝑘 ∈ 𝑋 ↦ (1st ‘(𝐼‘𝑘))) & ⊢ 𝐵 = (𝑘 ∈ 𝑋 ↦ (2nd ‘(𝐼‘𝑘))) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | ||
Theorem | dmvon 39496 | Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → dom (voln‘𝑋) = (CaraGen‘(voln*‘𝑋))) | ||
Theorem | hoi2toco 39497* | The half-open interval expressed using a composition of a function into (ℝ × ℝ) and using two distinct real valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ 𝐼 = (𝑘 ∈ 𝑋 ↦ 〈(𝐴‘𝑘), (𝐵‘𝑘)〉) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (([,) ∘ 𝐼)‘𝑘) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | ||
Theorem | hoidifhspval 39498* | 𝐷 is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑥 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑥), (𝑎‘𝑘))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐷‘𝑌) = (𝑎 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑌 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑌), (𝑎‘𝑘))))) | ||
Theorem | hspval 39499* | The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑖 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑖, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐼(𝐻‘𝑋)𝑌) = X𝑘 ∈ 𝑋 if(𝑘 = 𝐼, (-∞(,)𝑌), ℝ)) | ||
Theorem | ovnlecvr2 39500* | Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑𝑚 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚 𝑥), 𝑏 ∈ (ℝ ↑𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |