| Metamath
Proof Explorer Theorem List (p. 467 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hsphoidmvle 46601* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑋 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑗 ∈ 𝑋 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝐻‘𝐶)‘𝐵)) ≤ (𝐴(𝐿‘𝑋)𝐵)) | ||
| Theorem | hoidmvval0 46602* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → ∃𝑗 ∈ 𝑋 (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = 0) | ||
| Theorem | hoiprodp1 46603* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) & ⊢ 𝑋 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐺 = ∏𝑘 ∈ 𝑌 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = (𝐺 · (vol‘((𝐴‘𝑍)[,)(𝐵‘𝑍))))) | ||
| Theorem | sge0hsphoire 46604* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ (𝜑 → 𝑆 ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) | ||
| Theorem | hoidmvval0b 46605* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐴) = 0) | ||
| Theorem | hoidmv1lelem1 46606* | 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 46607* | 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 46608* | 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 nonempty, 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 46609* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ 𝑋 = {𝑍} & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) | ||
| Theorem | hoidmvlelem1 46610* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) & ⊢ (𝜑 → (𝐴‘𝑍) < (𝐵‘𝑍)) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝑈) | ||
| Theorem | hoidmvlelem2 46611* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) & ⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) & ⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗))) & ⊢ 𝑂 = ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) & ⊢ 𝑉 = ({(𝐵‘𝑍)} ∪ 𝑂) & ⊢ 𝑄 = inf(𝑉, ℝ, < ) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) | ||
| Theorem | hoidmvlelem3 46612* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) & ⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑m 𝑌)∀𝑓 ∈ (ℝ ↑m 𝑌)∀𝑔 ∈ ((ℝ ↑m 𝑌) ↑m ℕ)∀ℎ ∈ ((ℝ ↑m 𝑌) ↑m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ 𝑂 = (𝑥 ∈ X𝑘 ∈ 𝑌 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ↦ (𝑘 ∈ 𝑊 ↦ if(𝑘 ∈ 𝑌, (𝑥‘𝑘), 𝑆))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) | ||
| Theorem | hoidmvlelem4 46613* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) & ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) & ⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} & ⊢ 𝑆 = sup(𝑈, ℝ, < ) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑m 𝑌)∀𝑓 ∈ (ℝ ↑m 𝑌)∀𝑔 ∈ ((ℝ ↑m 𝑌) ↑m ℕ)∀ℎ ∈ ((ℝ ↑m 𝑌) ↑m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝐸) · (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))) | ||
| Theorem | hoidmvlelem5 46614* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) & ⊢ 𝑊 = (𝑌 ∪ {𝑍}) & ⊢ (𝜑 → 𝐴:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑊⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑊)) & ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑m 𝑌)∀𝑓 ∈ (ℝ ↑m 𝑌)∀𝑔 ∈ ((ℝ ↑m 𝑌) ↑m ℕ)∀ℎ ∈ ((ℝ ↑m 𝑌) ↑m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) & ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) | ||
| Theorem | hoidmvle 46615* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) | ||
| Theorem | ovnhoilem1 46616* | 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𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝐻 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ if(𝑗 = 1, 〈(𝐴‘𝑘), (𝐵‘𝑘)〉, 〈0, 0〉))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) ≤ ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
| Theorem | ovnhoilem2 46617* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝐹 = (𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) & ⊢ 𝑆 = (𝑖 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) | ||
| Theorem | ovnhoi 46618* | 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 ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
| Theorem | dmovn 46619 | 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*‘𝑋) = 𝒫 (ℝ ↑m 𝑋)) | ||
| Theorem | hoicoto2 46620* | 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 46621 | Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → dom (voln‘𝑋) = (CaraGen‘(voln*‘𝑋))) | ||
| Theorem | hoi2toco 46622* | 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 46623* | 𝐷 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.) |
| ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑥 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑥), (𝑎‘𝑘))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐷‘𝑌) = (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑌 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑌), (𝑎‘𝑘))))) | ||
| Theorem | hspval 46624* | 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 46625* | 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) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑋)(𝐷‘𝑗))))) | ||
| Theorem | ovncvr2 46626* | 𝐵 and 𝑇 are the left and right side of a cover of 𝐴. This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of 𝐴. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) & ⊢ (𝜑 → 𝐼 ∈ ((𝐷‘𝐴)‘𝐸)) & ⊢ 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (1st ‘((𝐼‘𝑗)‘𝑘)))) & ⊢ 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (2nd ‘((𝐼‘𝑗)‘𝑘)))) ⇒ ⊢ (𝜑 → (((𝐵:ℕ⟶(ℝ ↑m 𝑋) ∧ 𝑇:ℕ⟶(ℝ ↑m 𝑋)) ∧ 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))) ∧ (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐵‘𝑗)‘𝑘)[,)((𝑇‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 𝐸))) | ||
| Theorem | dmovnsal 46627 | The domain of the Lebesgue measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) ⇒ ⊢ (𝜑 → 𝑆 ∈ SAlg) | ||
| Theorem | unidmovn 46628 | Base set of the n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → ∪ dom (voln*‘𝑋) = (ℝ ↑m 𝑋)) | ||
| Theorem | rrnmbl 46629 | The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (ℝ ↑m 𝑋) ∈ dom (voln‘𝑋)) | ||
| Theorem | hoidifhspval2 46630* | 𝐷 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.) |
| ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑥 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑥), (𝑎‘𝑘))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐷‘𝑌)‘𝐴) = (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))) | ||
| Theorem | hspdifhsp 46631* | A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) | ||
| Theorem | unidmvon 46632 | Base set of the n-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) ⇒ ⊢ (𝜑 → ∪ 𝑆 = (ℝ ↑m 𝑋)) | ||
| Theorem | hoidifhspf 46633* | 𝐷 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.) |
| ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑥 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑥), (𝑎‘𝑘))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → ((𝐷‘𝑌)‘𝐴):𝑋⟶ℝ) | ||
| Theorem | hoidifhspval3 46634* | 𝐷 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.) |
| ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑎 ∈ (ℝ ↑m 𝑋) ↦ (𝑘 ∈ 𝑋 ↦ if(𝑘 = 𝐾, if(𝑥 ≤ (𝑎‘𝑘), (𝑎‘𝑘), 𝑥), (𝑎‘𝑘))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐽 ∈ 𝑋) ⇒ ⊢ (𝜑 → (((𝐷‘𝑌)‘𝐴)‘𝐽) = if(𝐽 = 𝐾, if(𝑌 ≤ (𝐴‘𝐽), (𝐴‘𝐽), 𝑌), (𝐴‘𝐽))) | ||
| Theorem | hoidifhspdmvle 46635* | The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ 𝐷 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (((𝐷‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ≤ (𝐴(𝐿‘𝑋)𝐵)) | ||
| Theorem | voncmpl 46636 | The Lebesgue measure is complete. See Definition 112Df of [Fremlin1] p. 19. This is an observation written after Definition 115E of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐸 ∈ dom (voln‘𝑋)) & ⊢ (𝜑 → ((voln‘𝑋)‘𝐸) = 0) & ⊢ (𝜑 → 𝐹 ⊆ 𝐸) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝑆) | ||
| Theorem | hoiqssbllem1 46637* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐶:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ⇒ ⊢ (𝜑 → 𝑌 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) | ||
| Theorem | hoiqssbllem2 46638* | The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐶:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) | ||
| Theorem | hoiqssbllem3 46639* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) | ||
| Theorem | hoiqssbl 46640* | A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (ℚ ↑m 𝑋)∃𝑑 ∈ (ℚ ↑m 𝑋)(𝑌 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))) | ||
| Theorem | hspmbllem1 46641* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) & ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) ⇒ ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵))) | ||
| Theorem | hspmbllem2 46642* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) & ⊢ (𝜑 → (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) & ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌))) ∈ ℝ) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) & ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦))))) & ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ))))) ⇒ ⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) + ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ (((voln*‘𝑋)‘𝐴) + 𝐸)) | ||
| Theorem | hspmbllem3 46643* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) & ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑m 𝑋) ↑m ℕ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑙‘𝑗))‘𝑘)}) & ⊢ 𝐿 = (ℎ ∈ ((ℝ × ℝ) ↑m 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ℎ)‘𝑘))) & ⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑m 𝑋) ↦ (𝑟 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑟)})) & ⊢ 𝐵 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑘)))) & ⊢ 𝑇 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑘)))) ⇒ ⊢ (𝜑 → (((voln*‘𝑋)‘(𝐴 ∩ (𝐾(𝐻‘𝑋)𝑌))) +𝑒 ((voln*‘𝑋)‘(𝐴 ∖ (𝐾(𝐻‘𝑋)𝑌)))) ≤ ((voln*‘𝑋)‘𝐴)) | ||
| Theorem | hspmbl 46644* | Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐾(𝐻‘𝑋)𝑌) ∈ dom (voln‘𝑋)) | ||
| Theorem | hoimbllem 46645* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∈ 𝑆) | ||
| Theorem | hoimbl 46646* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∈ 𝑆) | ||
| Theorem | opnvonmbllem1 46647* | The half-open interval expressed using a composition of a function (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ Ⅎ𝑖𝜑 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐶:𝑋⟶ℚ) & ⊢ (𝜑 → 𝐷:𝑋⟶ℚ) & ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐺) & ⊢ (𝜑 → 𝑌 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) & ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} & ⊢ 𝐻 = (𝑖 ∈ 𝑋 ↦ 〈(𝐶‘𝑖), (𝐷‘𝑖)〉) ⇒ ⊢ (𝜑 → ∃ℎ ∈ 𝐾 𝑌 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) | ||
| Theorem | opnvonmbllem2 46648* | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) & ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑆) | ||
| Theorem | opnvonmbl 46649 | An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑆) | ||
| Theorem | opnssborel 46650 | Open sets of a generalized real Euclidean space are Borel sets (notice that this theorem is even more general, because 𝑋 is not required to be a set). (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ 𝐴 = (TopOpen‘(ℝ^‘𝑋)) & ⊢ 𝐵 = (SalGen‘𝐴) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
| Theorem | borelmbl 46651 | All Borel subsets of the n-dimensional Real numbers are Lebesgue measurable. This is Proposition 115G (b) of [Fremlin1] p. 32. See also Definition 111G (d) of [Fremlin1] p. 13. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ 𝐵 = (SalGen‘(TopOpen‘(ℝ^‘𝑋))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝑆) | ||
| Theorem | volicorege0 46652 | The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,)+∞)) | ||
| Theorem | isvonmbl 46653* | The predicate "𝐴 is measurable w.r.t. the n-dimensional Lebesgue measure". 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 𝑥. Definition 114E of [Fremlin1] p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (𝐸 ∈ dom (voln‘𝑋) ↔ (𝐸 ⊆ (ℝ ↑m 𝑋) ∧ ∀𝑎 ∈ 𝒫 (ℝ ↑m 𝑋)(((voln*‘𝑋)‘(𝑎 ∩ 𝐸)) +𝑒 ((voln*‘𝑋)‘(𝑎 ∖ 𝐸))) = ((voln*‘𝑋)‘𝑎)))) | ||
| Theorem | mblvon 46654 | The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ dom (voln‘𝑋)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) = ((voln*‘𝑋)‘𝐴)) | ||
| Theorem | vonmblss 46655 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → dom (voln‘𝑋) ⊆ 𝒫 (ℝ ↑m 𝑋)) | ||
| Theorem | volico2 46656 | The measure of left-closed right-open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) = if(𝐴 ≤ 𝐵, (𝐵 − 𝐴), 0)) | ||
| Theorem | vonmblss2 46657 | n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ dom (voln‘𝑋)) ⇒ ⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑m 𝑋)) | ||
| Theorem | ovolval2lem 46658* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) ⇒ ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐹)) = ran (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)(vol‘(([,) ∘ 𝐹)‘𝑘)))) | ||
| Theorem | ovolval2 46659* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^. See ovolval 25508 for an alternative expression. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((abs ∘ − ) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
| Theorem | ovnsubadd2lem 46660* | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅))) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∪ 𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))) | ||
| Theorem | ovnsubadd2 46661 | (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) & ⊢ (𝜑 → 𝐵 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘(𝐴 ∪ 𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))) | ||
| Theorem | ovolval3 46662* | The value of the Lebesgue outer measure for subsets of the reals, expressed using Σ^ and vol ∘ (,). See ovolval 25508 and ovolval2 46659 for alternative expressions. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
| Theorem | ovnsplit 46663 | The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑m 𝑋)) ⇒ ⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) ≤ (((voln*‘𝑋)‘(𝐴 ∩ 𝐵)) +𝑒 ((voln*‘𝑋)‘(𝐴 ∖ 𝐵)))) | ||
| Theorem | ovolval4lem1 46664* | |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) 𝑛) = (((,) ∘ 𝐹) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))〉) & ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⇒ ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))) | ||
| Theorem | ovolval4lem2 46665* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 46662, but here 𝑓 is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈(1st ‘(𝑓‘𝑛)), if((1st ‘(𝑓‘𝑛)) ≤ (2nd ‘(𝑓‘𝑛)), (2nd ‘(𝑓‘𝑛)), (1st ‘(𝑓‘𝑛)))〉) ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
| Theorem | ovolval4 46666* | The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 46662, but here 𝑓 may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
| Theorem | ovolval5lem1 46667* | ⊢ (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛) ))(,)𝐵)))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵) ))) +𝑒 𝑊)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ 𝐶 = {𝑛 ∈ ℕ ∣ 𝐴 < 𝐵} ⇒ ⊢ (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) | ||
| Theorem | ovolval5lem2 46668* | ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 〈((1st ‘(𝐹‘𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹‘𝑛))〉 ∈ (ℝ × ℝ)). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} & ⊢ (𝜑 → 𝑌 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))) & ⊢ 𝑍 = (Σ^‘((vol ∘ (,)) ∘ 𝐺)) & ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ × ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ([,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑊 ∈ ℝ+) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) − (𝑊 / (2↑𝑛))), (2nd ‘(𝐹‘𝑛))〉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑄 𝑧 ≤ (𝑌 +𝑒 𝑊)) | ||
| Theorem | ovolval5lem3 46669* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} & ⊢ 𝑄 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ (,)) ∘ 𝑓)))} ⇒ ⊢ inf(𝑄, ℝ*, < ) = inf(𝑀, ℝ*, < ) | ||
| Theorem | ovolval5 46670* | The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐴 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑦 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
| Theorem | ovnovollem1 46671* | if 𝐹 is a cover of 𝐵 in ℝ, then 𝐼 is the corresponding cover in the space of 1-dimensional reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ ((ℝ × ℝ) ↑m ℕ)) & ⊢ 𝐼 = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝐹‘𝑗)〉}) & ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ([,) ∘ 𝐹)) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝐹))) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | ||
| Theorem | ovnovollem2 46672* | if 𝐼 is a cover of (𝐵 ↑m {𝐴}) in ℝ^1, then 𝐹 is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)) & ⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝐼‘𝑗))‘𝑘)) & ⊢ (𝜑 → 𝑍 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝐼‘𝑗))‘𝑘))))) & ⊢ 𝐹 = (𝑗 ∈ ℕ ↦ ((𝐼‘𝑗)‘𝐴)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑍 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | ||
| Theorem | ovnovollem3 46673* | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ 𝑀 = {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} & ⊢ 𝑁 = {𝑧 ∈ ℝ* ∣ ∃𝑓 ∈ ((ℝ × ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran ([,) ∘ 𝑓) ∧ 𝑧 = (Σ^‘((vol ∘ [,)) ∘ 𝑓)))} ⇒ ⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol*‘𝐵)) | ||
| Theorem | ovnovol 46674 | The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol*‘𝐵)) | ||
| Theorem | vonvolmbllem 46675* | If a subset 𝐵 of real numbers is Lebesgue measurable, then its corresponding 1-dimensional set is measurable w.r.t. the n-dimensional Lebesgue measure, (with 𝑛 equal to 1). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ℝ(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝐵)) +𝑒 (vol*‘(𝑦 ∖ 𝐵)))) & ⊢ (𝜑 → 𝑋 ⊆ (ℝ ↑m {𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → (((voln*‘{𝐴})‘(𝑋 ∩ (𝐵 ↑m {𝐴}))) +𝑒 ((voln*‘{𝐴})‘(𝑋 ∖ (𝐵 ↑m {𝐴})))) = ((voln*‘{𝐴})‘𝑋)) | ||
| Theorem | vonvolmbl 46676 | A subset of Real numbers is Lebesgue measurable if and only if its corresponding 1-dimensional set is measurable w.r.t. the 1-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) ⇒ ⊢ (𝜑 → ((𝐵 ↑m {𝐴}) ∈ dom (voln‘{𝐴}) ↔ 𝐵 ∈ dom vol)) | ||
| Theorem | vonvol 46677 | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ dom vol) ⇒ ⊢ (𝜑 → ((voln‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol‘𝐵)) | ||
| Theorem | vonvolmbl2 46678* | A subset 𝑋 of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection 𝑌 on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑓𝑌 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ⊆ (ℝ ↑m {𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → (𝑋 ∈ dom (voln‘{𝐴}) ↔ 𝑌 ∈ dom vol)) | ||
| Theorem | vonvol2 46679* | The 1-dimensional Lebesgue measure agrees with the Lebesgue measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
| ⊢ Ⅎ𝑓𝑌 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ dom (voln‘{𝐴})) & ⊢ 𝑌 = ∪ 𝑓 ∈ 𝑋 ran 𝑓 ⇒ ⊢ (𝜑 → ((voln‘{𝐴})‘𝑋) = (vol‘𝑌)) | ||
| Theorem | hoimbl2 46680* | Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝑋 (𝐴[,)𝐵) ∈ 𝑆) | ||
| Theorem | voncl 46681 | The Lebesgue measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) ∈ (0[,]+∞)) | ||
| Theorem | vonhoi 46682* | 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). A direct consequence of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
| Theorem | vonxrcl 46683 | The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐴) ∈ ℝ*) | ||
| Theorem | ioosshoi 46684 | A n-dimensional open interval is a subset of the half-open interval with the same bounds. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ X𝑘 ∈ 𝑋 (𝐴(,)𝐵) ⊆ X𝑘 ∈ 𝑋 (𝐴[,)𝐵) | ||
| Theorem | vonn0hoi 46685* | The Lebesgue outer measure of a multidimensional half-open interval when the dimension of the space is nonzero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) | ||
| Theorem | von0val 46686 | The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ dom (voln‘∅)) ⇒ ⊢ (𝜑 → ((voln‘∅)‘𝐴) = 0) | ||
| Theorem | vonhoire 46687* | The Lebesgue measure of a n-dimensional half-open interval is a real number. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (𝐴[,)𝐵)) ∈ ℝ) | ||
| Theorem | iinhoiicclem 46688* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) | ||
| Theorem | iinhoiicc 46689* | A n-dimensional closed interval expressed as the indexed intersection of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (𝐴[,)(𝐵 + (1 / 𝑛))) = X𝑘 ∈ 𝑋 (𝐴[,]𝐵)) | ||
| Theorem | iunhoiioolem 46690* | A n-dimensional open interval expressed as the indexed union of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐹 ∈ X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) & ⊢ 𝐶 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐹‘𝑘) − 𝐴)), ℝ, < ) ⇒ ⊢ (𝜑 → 𝐹 ∈ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵)) | ||
| Theorem | iunhoiioo 46691* | A n-dimensional open interval expressed as the indexed union of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ Ⅎ𝑘𝜑 & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐵 ∈ ℝ*) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴 + (1 / 𝑛))[,)𝐵) = X𝑘 ∈ 𝑋 (𝐴(,)𝐵)) | ||
| Theorem | ioovonmbl 46692* | Any n-dimensional open interval is Lebesgue measurable. This is the first statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)(,)(𝐵‘𝑖)) ∈ 𝑆) | ||
| Theorem | iccvonmbllem 46693* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑖 ∈ 𝑋 ↦ ((𝐴‘𝑖) − (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑖 ∈ 𝑋 ↦ ((𝐵‘𝑖) + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,](𝐵‘𝑖)) ∈ 𝑆) | ||
| Theorem | iccvonmbl 46694* | Any n-dimensional closed interval is Lebesgue measurable. This is the second statement in Proposition 115G (c) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝑆 = dom (voln‘𝑋) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) ⇒ ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,](𝐵‘𝑖)) ∈ 𝑆) | ||
| Theorem | vonioolem1 46695* | The sequence of the measures of the half-open intervals converges to the measure of their union. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) & ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) & ⊢ 𝐸 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) & ⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) & ⊢ 𝑍 = (ℤ≥‘𝑁) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
| Theorem | vonioolem2 46696* | The n-dimensional Lebesgue measure of open intervals. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
| Theorem | vonioo 46697* | The n-dimensional Lebesgue measure of an open interval. This is the first statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
| Theorem | vonicclem1 46698* | The sequence of the measures of the half-open intervals converges to the measure of their intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) & ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
| Theorem | vonicclem2 46699* | The n-dimensional Lebesgue measure of closed intervals. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) & ⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) & ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) | ||
| Theorem | vonicc 46700* | The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
| ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐴:𝑋⟶ℝ) & ⊢ (𝜑 → 𝐵:𝑋⟶ℝ) & ⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) & ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) ⇒ ⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |