![]() |
Metamath
Proof Explorer Theorem List (p. 238 of 443) | < 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-28468) |
![]() (28469-29993) |
![]() (29994-44247) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rrxf 23701* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐹:𝐼⟶ℝ) | ||
Theorem | rrxfsupp 23702* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ∈ Fin) | ||
Theorem | rrxsuppss 23703* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ⊆ 𝐼) | ||
Theorem | rrxmvallem 23704* | Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) supp 0) ⊆ ((𝐹 supp 0) ∪ (𝐺 supp 0))) | ||
Theorem | rrxmval 23705* | The value of the Euclidean metric. Compare with rrnmval 34526. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | rrxmfval 23706* | The value of the Euclidean metric. Compare with rrnval 34525. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑓 supp 0) ∪ (𝑔 supp 0))(((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetlem 23707* | Lemma for rrxmet 23708. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ 𝐴 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | ||
Theorem | rrxmet 23708* | Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | rrxdstprj1 23709* | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑𝑚 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹𝐷𝐺)) | ||
Theorem | rrxbasefi 23710 | The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of (ℝ ↑𝑚 𝑋) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐻 = (ℝ^‘𝑋) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝜑 → 𝐵 = (ℝ ↑𝑚 𝑋)) | ||
Theorem | rrxdsfi 23711* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (ℝ ↑𝑚 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetfi 23712 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑𝑚 𝐼))) | ||
Theorem | rrxdsfival 23713* | The value of the Euclidean distance function in a generalized real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝑋 = (ℝ ↑𝑚 𝐼) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | ehlval 23714 | Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁))) | ||
Theorem | ehlbase 23715 | 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 | ehl0base 23716 | The base of the Euclidean space of dimension 0 consists only of one element, the empty set. (Contributed by AV, 12-Feb-2023.) |
⊢ 𝐸 = (𝔼hil‘0) ⇒ ⊢ (Base‘𝐸) = {∅} | ||
Theorem | ehl0 23717 | The Euclidean space of dimension 0 consists of the neutral element only. (Contributed by AV, 12-Feb-2023.) |
⊢ 𝐸 = (𝔼hil‘0) & ⊢ 0 = (0g‘𝐸) ⇒ ⊢ (Base‘𝐸) = { 0 } | ||
Theorem | ehleudis 23718* | The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝐼 = (1...𝑁) & ⊢ 𝐸 = (𝔼hil‘𝑁) & ⊢ 𝑋 = (ℝ ↑𝑚 𝐼) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | ehleudisval 23719* | The value of the Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝐼 = (1...𝑁) & ⊢ 𝐸 = (𝔼hil‘𝑁) & ⊢ 𝑋 = (ℝ ↑𝑚 𝐼) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | ehl1eudis 23720* | The Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘1) & ⊢ 𝑋 = (ℝ ↑𝑚 {1}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (abs‘((𝑓‘1) − (𝑔‘1)))) | ||
Theorem | ehl1eudisval 23721 | The value of the Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘1) & ⊢ 𝑋 = (ℝ ↑𝑚 {1}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (abs‘((𝐹‘1) − (𝐺‘1)))) | ||
Theorem | ehl2eudis 23722* | The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑𝑚 {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2)))) | ||
Theorem | ehl2eudisval 23723 | The value of the Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑𝑚 {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘((((𝐹‘1) − (𝐺‘1))↑2) + (((𝐹‘2) − (𝐺‘2))↑2)))) | ||
Theorem | minveclem1 23724* | Lemma for minvec 23736. 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 23725* | Lemma for minvec 23736. 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 23726* | Lemma for minvec 23736. 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 23727* | Lemma for minvec 23736. 𝐷 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 23728* | Lemma for minvec 23736. 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 23729* | Lemma for minvec 23736. 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 23730* | Lemma for minvec 23736. 𝐹 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 23731* | Lemma for minvec 23736. 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 23732* | Lemma for minvec 23736. 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 23733* | Lemma for minvec 23736. Discharge the assumptions in minveclem4 23732. (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 23734* | Lemma for minvec 23736. 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 23735* | Lemma for minvec 23736. 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 23736* | 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 23737* | Lemma for pjth 23739. (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 23738 | Lemma for pjth 23739. (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 23739 | 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 23740 | 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 23741 | 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 23742 | 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 23743 | 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 | mulcncf 23744* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | divcncf 23745* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→(ℂ ∖ {0}))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | pmltpclem1 23746* | Lemma for pmltpc 23748. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶)))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpclem2 23747* | Lemma for pmltpc 23748. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≤ 𝑉) & ⊢ (𝜑 → 𝑊 ≤ 𝑋) & ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉)) & ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpc 23748* | 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 23749* | Lemma for ivth 23752. 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 23750* | Lemma for ivth 23752. 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 23751* | Lemma for ivth 23752, 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 23752* | 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 23753* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle 23754* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle2 23755* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthicc 23756* | 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 23757* | Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤))) | ||
Theorem | evthicc2 23758* | Combine ivthicc 23756 with evthicc 23757 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦)) | ||
Theorem | cniccbdd 23759* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥) | ||
Syntax | covol 23760 | Extend class notation with the outer Lebesgue measure. |
class vol* | ||
Syntax | cvol 23761 | Extend class notation with the Lebesgue measure. |
class vol | ||
Definition | df-ovol 23762* | 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 23763* | 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 23764 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfioo 23765* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficc 23766* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficcss 23767 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) | ||
Theorem | ovolfsval 23768 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfsf 23769 | Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝐺:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolsf 23770 | Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) & ⊢ 𝑆 = seq1( + , 𝐺) ⇒ ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | ||
Theorem | ovolval 23771* | 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 | elovolmlem 23772 | Lemma for elovolm 23773 and related theorems. (Contributed by BJ, 23-Jul-2022.) |
⊢ (𝐹 ∈ ((𝐴 ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶(𝐴 ∩ (ℝ × ℝ))) | ||
Theorem | elovolm 23773* | 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 23774* | 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 23775* | The set 𝑀 is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))} ⇒ ⊢ (𝐵 ∈ 𝑀 → 0 ≤ 𝐵) | ||
Theorem | ovolcl 23776 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*) | ||
Theorem | ovollb 23777 | 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 23778* | 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 23779 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ (𝐴 ⊆ ℝ → 0 ≤ (vol*‘𝐴)) | ||
Theorem | ovolf 23780 | 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 23781 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (vol*‘𝐴) ≤ 𝐵) → (vol*‘𝐴) ∈ ℝ) | ||
Theorem | ovolsslem 23782* | Lemma for ovolss 23783. (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 23783 | The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ) → (vol*‘𝐴) ≤ (vol*‘𝐵)) | ||
Theorem | ovolsscl 23784 | 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 23785 | A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘𝐴) = 0) | ||
Theorem | ovollb2lem 23786* | Lemma for ovollb2 23787. (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 23787 | 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 23777). (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < )) | ||
Theorem | ovolctb 23788 | 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 23789 | The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘ℚ) = 0 | ||
Theorem | ovolctb2 23790 | The volume of a countable set is 0. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → (vol*‘𝐴) = 0) | ||
Theorem | ovol0 23791 | The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014.) |
⊢ (vol*‘∅) = 0 | ||
Theorem | ovolfi 23792 | A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ) → (vol*‘𝐴) = 0) | ||
Theorem | ovolsn 23793 | A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (vol*‘{𝐴}) = 0) | ||
Theorem | ovolunlem1a 23794* | Lemma for ovolun 23797. (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 23795* | Lemma for ovolun 23797. (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 23796 | Lemma for ovolun 23797. (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ)) & ⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (vol*‘(𝐴 ∪ 𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) | ||
Theorem | ovolun 23797 | The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun 23803, this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014.) |
⊢ (((𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) ∧ (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | ||
Theorem | ovolunnul 23798 | Adding a nullset does not change the measure of a set. (Contributed by Mario Carneiro, 25-Mar-2015.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ (vol*‘𝐵) = 0) → (vol*‘(𝐴 ∪ 𝐵)) = (vol*‘𝐴)) | ||
Theorem | ovolfiniun 23799* | 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 23800* | Lemma for ovoliun 23803. (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→(ℕ × ℕ)) & ⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐿 ∈ ℤ) & ⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿) ⇒ ⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |