![]() |
Metamath
Proof Explorer Theorem List (p. 255 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48424) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | minveclem3 25401* | Lemma for minvec 25408. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) & ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) ⇒ ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) | ||
Theorem | minveclem4a 25402* | Lemma for minvec 25408. 𝐹 converges to a point 𝑃 in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) & ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) & ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹)) ⇒ ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) | ||
Theorem | minveclem4b 25403* | Lemma for minvec 25408. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) & ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) & ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹)) ⇒ ⊢ (𝜑 → 𝑃 ∈ 𝑋) | ||
Theorem | minveclem4 25404* | Lemma for minvec 25408. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) & ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) & ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹)) & ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | ||
Theorem | minveclem5 25405* | Lemma for minvec 25408. Discharge the assumptions in minveclem4 25404. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | ||
Theorem | minveclem6 25406* | Lemma for minvec 25408. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) | ||
Theorem | minveclem7 25407* | Lemma for minvec 25408. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | ||
Theorem | minvec 25408* | Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace 𝑊 that minimizes the distance to an arbitrary vector 𝐴 in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 3-Oct-2020.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) | ||
Theorem | pjthlem1 25409* | Lemma for pjth 25411. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂHil) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥))) & ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)) ⇒ ⊢ (𝜑 → (𝐴 , 𝐵) = 0) | ||
Theorem | pjthlem2 25410 | Lemma for pjth 25411. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂHil) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑂 = (ocv‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈))) | ||
Theorem | pjth 25411 | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝑂 = (ocv‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑈 ⊕ (𝑂‘𝑈)) = 𝑉) | ||
Theorem | pjth2 25412 | Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ 𝐾 = (proj‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ∈ dom 𝐾) | ||
Theorem | cldcss 25413 | Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂHil → (𝑈 ∈ 𝐶 ↔ (𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)))) | ||
Theorem | cldcss2 25414 | Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ 𝐶 = (ClSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂHil → 𝐶 = (𝐿 ∩ (Clsd‘𝐽))) | ||
Theorem | hlhil 25415 | Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Hil) | ||
Theorem | addcncf 25416* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | subcncf 25417* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 − 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | mulcncf 25418* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Avoid ax-mulf 11220. (Revised by GG, 16-Mar-2025.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | mulcncfOLD 25419* | Obsolete version of mulcncf 25418 as of 9-Apr-2025. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | divcncf 25420* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→(ℂ ∖ {0}))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | pmltpclem1 25421* | Lemma for pmltpc 25423. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶)))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpclem2 25422* | Lemma for pmltpc 25423. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≤ 𝑉) & ⊢ (𝜑 → 𝑊 ≤ 𝑋) & ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉)) & ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpc 25423* | Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ ((𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ∨ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝐹‘𝑥)) ∨ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐)))))) | ||
Theorem | ivthlem1 25424* | Lemma for ivth 25427. The set 𝑆 of all 𝑥 values with (𝐹‘𝑥) less than 𝑈 is lower bounded by 𝐴 and upper bounded by 𝐵. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈} ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)) | ||
Theorem | ivthlem2 25425* | Lemma for ivth 25427. Show that the supremum of 𝑆 cannot be less than 𝑈. If it was, continuity of 𝐹 implies that there are points just above the supremum that are also less than 𝑈, a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈} & ⊢ 𝐶 = sup(𝑆, ℝ, < ) ⇒ ⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈) | ||
Theorem | ivthlem3 25426* | Lemma for ivth 25427, the intermediate value theorem. Show that (𝐹‘𝐶) cannot be greater than 𝑈, and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 17-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈} & ⊢ 𝐶 = sup(𝑆, ℝ, < ) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴(,)𝐵) ∧ (𝐹‘𝐶) = 𝑈)) | ||
Theorem | ivth 25427* | The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivth2 25428* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle 25429* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle2 25430* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthicc 25431* | The interval between any two points of a continuous real function is contained in the range of the function. Equivalently, the range of a continuous real function is convex. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → 𝑁 ∈ (𝐴[,]𝐵)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐹‘𝑀)[,](𝐹‘𝑁)) ⊆ ran 𝐹) | ||
Theorem | evthicc 25432* | Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤))) | ||
Theorem | evthicc2 25433* | Combine ivthicc 25431 with evthicc 25432 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦)) | ||
Theorem | cniccbdd 25434* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥) | ||
Syntax | covol 25435 | Extend class notation with the outer Lebesgue measure. |
class vol* | ||
Syntax | cvol 25436 | Extend class notation with the Lebesgue measure. |
class vol | ||
Definition | df-ovol 25437* | Define the outer Lebesgue measure for subsets of the reals. Here 𝑓 is a function from the positive integers to pairs 〈𝑎, 𝑏〉 with 𝑎 ≤ 𝑏, and the outer volume of the set 𝑥 is the infimum over all such functions such that the union of the open intervals (𝑎, 𝑏) covers 𝑥 of the sum of 𝑏 − 𝑎. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
⊢ vol* = (𝑥 ∈ 𝒫 ℝ ↦ inf({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < )) | ||
Definition | df-vol 25438* | Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as 𝐴 ∈ dom vol. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ vol = (vol* ↾ {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))}) | ||
Theorem | ovolfcl 25439 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfioo 25440* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficc 25441* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficcss 25442 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) | ||
Theorem | ovolfsval 25443 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfsf 25444 | Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolsf 25445 | Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) & ⊢ 𝑆 = seq1( + , 𝐺) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolval 25446* | The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | elovolmlem 25447 | Lemma for elovolm 25448 and related theorems. (Contributed by BJ, 23-Jul-2022.) |
⊢ (𝐹 ∈ ((𝐴 ∩ (ℝ × ℝ)) ↑m ℕ) ↔ 𝐹:ℕ⟶(𝐴 ∩ (ℝ × ℝ))) | ||
Theorem | elovolm 25448* | Elementhood in the set 𝑀 of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))) | ||
Theorem | elovolmr 25449* | Sufficient condition for elementhood in the set 𝑀. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolmge0 25450* | The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵) | ||
Theorem | ovolcl 25451 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*) | ||
Theorem | ovollb 25452 | 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 25453* | 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 25454 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴)) | ||
Theorem | ovolf 25455 | 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 25456 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ) | ||
Theorem | ovolsslem 25457* | Lemma for ovolss 25458. (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 25458 | The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolsscl 25459 | 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 25460 | A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0) | ||
Theorem | ovollb2lem 25461* | Lemma for ovollb2 25462. (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 25462 | 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 25452). (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolctb 25463 | 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 25464 | The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘ℚ) = 0 | ||
Theorem | ovolctb2 25465 | The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0) | ||
Theorem | ovol0 25466 | The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘∅) = 0 | ||
Theorem | ovolfi 25467 | A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0) | ||
Theorem | ovolsn 25468 | A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0) | ||
Theorem | ovolunlem1a 25469* | Lemma for ovolun 25472. (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 25470* | Lemma for ovolun 25472. (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 25471 | Lemma for ovolun 25472. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolun 25472 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 25478, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | ||
Theorem | ovolunnul 25473 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) | ||
Theorem | ovolfiniun 25474* | 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 25475* | Lemma for ovoliun 25478. (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 25476* | Lemma for ovoliun 25478. (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 25477* | Lemma for ovoliun 25478. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliun 25478* | 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 25458, 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 25479* | 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 25478.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) | ||
Theorem | ovoliunnul 25480* | A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) | ||
Theorem | shft2rab 25481* | 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 25482* | Lemma for ovolshft 25484. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) ⇒ ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolshftlem2 25483* | Lemma for ovolshft 25484. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀) | ||
Theorem | ovolshft 25484* | 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 25485* | If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) ⇒ ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵}) | ||
Theorem | ovolscalem1 25486* | Lemma for ovolsca 25488. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | ||
Theorem | ovolscalem2 25487* | Lemma for ovolshft 25484. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolsca 25488* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolicc1 25489* | 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 25490* | Lemma for ovolicc2 25495. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) | ||
Theorem | ovolicc2lem2 25491* | Lemma for ovolicc2 25495. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵) | ||
Theorem | ovolicc2lem3 25492* | Lemma for ovolicc2 25495. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) | ||
Theorem | ovolicc2lem4 25493* | Lemma for ovolicc2 25495. (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 25494* | Lemma for ovolicc2 25495. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolicc2 25495* | 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 25496 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ovolicopnf 25497 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞) | ||
Theorem | ovolre 25498 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (vol*‘ℝ) = +∞ | ||
Theorem | ismbl 25499* | 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 25500* | From ovolun 25472, 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*‘𝑥)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |