Home | Metamath
Proof Explorer Theorem List (p. 231 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 | ehlval 23001 | Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁))) | ||
Theorem | ehlbase 23002 | The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℝ ↑𝑚 (1...𝑁)) = (Base‘𝐸)) | ||
Theorem | minveclem1 23003* | Lemma for minvec 23015. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | ||
Theorem | minveclem4c 23004* | Lemma for minvec 23015. The infimum of the distances to 𝐴 is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.) |
⊢ 𝑋 = (Base‘𝑈) & ⊢ − = (-g‘𝑈) & ⊢ 𝑁 = (norm‘𝑈) & ⊢ (𝜑 → 𝑈 ∈ ℂPreHil) & ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) & ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐽 = (TopOpen‘𝑈) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) ⇒ ⊢ (𝜑 → 𝑆 ∈ ℝ) | ||
Theorem | minveclem2 23005* | Lemma for minvec 23015. Any two points 𝐾 and 𝐿 in 𝑌 are close to each other if they are close to the infimum of distance to 𝐴. (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‘𝑈) ↾ (𝑋 × 𝑋)) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝑌) & ⊢ (𝜑 → 𝐿 ∈ 𝑌) & ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵)) & ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵)) ⇒ ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵)) | ||
Theorem | minveclem3a 23006* | Lemma for minvec 23015. 𝐷 is a complete metric when restricted to 𝑌. (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‘𝑈) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) | ||
Theorem | minveclem3b 23007* | Lemma for minvec 23015. The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed 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) + 𝑟)}) ⇒ ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) | ||
Theorem | minveclem3 23008* | Lemma for minvec 23015. 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 23009* | Lemma for minvec 23015. 𝐹 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 23010* | Lemma for minvec 23015. 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 23011* | Lemma for minvec 23015. 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 23012* | Lemma for minvec 23015. Discharge the assumptions in minveclem4 23011. (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 23013* | Lemma for minvec 23015. 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 23014* | Lemma for minvec 23015. 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 23015* | 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 23016* | Lemma for pjth 23018. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐿 = (LSubSp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂHil) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥))) & ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)) ⇒ ⊢ (𝜑 → (𝐴 , 𝐵) = 0) | ||
Theorem | pjthlem2 23017 | Lemma for pjth 23018. (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 23018 | 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 23019 | 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 23020 | 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‘𝑊) & ⊢ 𝐶 = (CSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂHil → (𝑈 ∈ 𝐶 ↔ (𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)))) | ||
Theorem | cldcss2 23021 | 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‘𝑊) & ⊢ 𝐶 = (CSubSp‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂHil → 𝐶 = (𝐿 ∩ (Clsd‘𝐽))) | ||
Theorem | hlhil 23022 | Corollary of the Projection Theorem: A complex 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 | mulcncf 23023* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | pmltpclem1 23024* | Lemma for pmltpc 23026. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶)))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpclem2 23025* | Lemma for pmltpc 23026. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≤ 𝑉) & ⊢ (𝜑 → 𝑊 ≤ 𝑋) & ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉)) & ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpc 23026* | 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 23027* | Lemma for ivth 23030. 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 23028* | Lemma for ivth 23030. 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 23029* | Lemma for ivth 23030, 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 23030* | 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 23031* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle 23032* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle2 23033* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthicc 23034* | 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 23035* | Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤))) | ||
Theorem | evthicc2 23036* | Combine ivthicc 23034 with evthicc 23035 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦)) | ||
Theorem | cniccbdd 23037* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥) | ||
Syntax | covol 23038 | Extend class notation with the outer Lebesgue measure. |
class vol* | ||
Syntax | cvol 23039 | Extend class notation with the Lebesgue measure. |
class vol | ||
Definition | df-ovol 23040* | 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({𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝑥 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}, ℝ*, < )) | ||
Definition | df-vol 23041* | 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 23042 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfioo 23043* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficc 23044* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficcss 23045 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) | ||
Theorem | ovolfsval 23046 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfsf 23047 | Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolsf 23048 | Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) & ⊢ 𝑆 = seq1( + , 𝐺) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolval 23049* | The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) = inf(𝑀, ℝ*, < )) | ||
Theorem | elovolm 23050* | Elementhood in the set 𝑀 of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))) | ||
Theorem | elovolmr 23051* | Sufficient condition for elementhood in the set 𝑀. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolmge0 23052* | The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵) | ||
Theorem | ovolcl 23053 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*) | ||
Theorem | ovollb 23054 | 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 23055* | 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*‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + 𝐵))) | ||
Theorem | ovolge0 23056 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴)) | ||
Theorem | ovolf 23057 | The domain and range of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
⊢ vol*:𝒫 ℝ⟶(0[,]+∞) | ||
Theorem | ovollecl 23058 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ) | ||
Theorem | ovolsslem 23059* | Lemma for ovolss 23060. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑁 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolss 23060 | The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolsscl 23061 | 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 23062 | A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0) | ||
Theorem | ovollb2lem 23063* | Lemma for ovollb2 23064. (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 23064 | 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 23054). (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolctb 23065 | 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 23066 | The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘ℚ) = 0 | ||
Theorem | ovolctb2 23067 | The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0) | ||
Theorem | ovol0 23068 | The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘∅) = 0 | ||
Theorem | ovolfi 23069 | A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0) | ||
Theorem | ovolsn 23070 | A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0) | ||
Theorem | ovolunlem1a 23071* | Lemma for ovolun 23074. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2))) & ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) ⇒ ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑈‘𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolunlem1 23072* | Lemma for ovolun 23074. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺)) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ (𝜑 → 𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2))) & ⊢ (𝜑 → 𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ (𝜑 → 𝐵 ⊆ ∪ ran ((,) ∘ 𝐺)) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2))) & ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2)))) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolunlem2 23073 | Lemma for ovolun 23074. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolun 23074 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 23080, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | ||
Theorem | ovolunnul 23075 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) | ||
Theorem | ovolfiniun 23076* | 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 23077* | Lemma for ovoliun 23080. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛))) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) & ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) & ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿) ⇒ ⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliunlem2 23078* | Lemma for ovoliun 23080. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹‘𝑛))) & ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻)) & ⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) & ⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) & ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliunlem3 23079* | Lemma for ovoliun 23080. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) | ||
Theorem | ovoliun 23080* | 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 23060, 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 23081* | 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 23080.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ 𝑇 = seq1( + , 𝐺) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ) & ⊢ (𝜑 → 𝑇 ∈ dom ⇝ ) ⇒ ⊢ (𝜑 → (vol*‘∪ 𝑛 ∈ ℕ 𝐴) ≤ Σ𝑛 ∈ ℕ (vol*‘𝐴)) | ||
Theorem | ovoliunnul 23082* | A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ ((𝐴 ≼ ℕ ∧ ∀𝑛 ∈ 𝐴 (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0)) → (vol*‘∪ 𝑛 ∈ 𝐴 𝐵) = 0) | ||
Theorem | shft2rab 23083* | 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 23084* | Lemma for ovolshft 23086. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) ⇒ ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) | ||
Theorem | ovolshftlem2 23085* | Lemma for ovolshft 23086. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ ∃𝑔 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑔) ∧ 𝑧 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑔)), ℝ*, < ))} ⊆ 𝑀) | ||
Theorem | ovolshft 23086* | 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 23087* | If 𝐵 is a scale of 𝐴 by 𝐶, then 𝐴 is a scale of 𝐵 by 1 / 𝐶. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) ⇒ ⊢ (𝜑 → 𝐴 = {𝑦 ∈ ℝ ∣ ((1 / 𝐶) · 𝑦) ∈ 𝐵}) | ||
Theorem | ovolscalem1 23088* | Lemma for ovolsca 23090. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ 〈((1st ‘(𝐹‘𝑛)) / 𝐶), ((2nd ‘(𝐹‘𝑛)) / 𝐶)〉) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝐴 ⊆ ∪ ran ((,) ∘ 𝐹)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)) | ||
Theorem | ovolscalem2 23089* | Lemma for ovolshft 23086. (Contributed by Mario Carneiro, 22-Mar-2014.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) ≤ ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolsca 23090* | The Lebesgue outer measure function respects scaling of sets by positive reals. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}) & ⊢ (𝜑 → (vol*‘𝐴) ∈ ℝ) ⇒ ⊢ (𝜑 → (vol*‘𝐵) = ((vol*‘𝐴) / 𝐶)) | ||
Theorem | ovolicc1 23091* | 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 23092* | Lemma for ovolicc2 23097. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝑃 ∈ 𝑋 ↔ (𝑃 ∈ ℝ ∧ (1st ‘(𝐹‘(𝐺‘𝑋))) < 𝑃 ∧ 𝑃 < (2nd ‘(𝐹‘(𝐺‘𝑋)))))) | ||
Theorem | ovolicc2lem2 23093* | Lemma for ovolicc2 23097. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) ≤ 𝐵) | ||
Theorem | ovolicc2lem3 23094* | Lemma for ovolicc2 23097. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} & ⊢ (𝜑 → 𝐻:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐶 ∈ 𝑇) & ⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ × {𝐶})) & ⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⇒ ⊢ ((𝜑 ∧ (𝑁 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑃 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑁 = 𝑃 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑁)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑃)))))) | ||
Theorem | ovolicc2lem4 23095* | Lemma for ovolicc2 23097. (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 23096* | Lemma for ovolicc2 23097. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) & ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) & ⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝐺:𝑈⟶ℕ) & ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) & ⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolicc2 23097* | The measure of a closed interval is upper bounded by its length. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)((𝐴[,]𝐵) ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝜑 → (𝐵 − 𝐴) ≤ (vol*‘(𝐴[,]𝐵))) | ||
Theorem | ovolicc 23098 | The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | ovolicopnf 23099 | The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘(𝐴[,)+∞)) = +∞) | ||
Theorem | ovolre 23100 | The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014.) |
⊢ (vol*‘ℝ) = +∞ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |