Home | Metamath
Proof Explorer Theorem List (p. 240 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlpr 23901 | The scalar field of a subcomplex Hilbert space is either ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂHil → 𝐾 ∈ {ℝ, ℂ}) | ||
Theorem | ishl2 23902 | A Hilbert space is a complete subcomplex pre-Hilbert space over ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂHil ↔ (𝑊 ∈ CMetSp ∧ 𝑊 ∈ ℂPreHil ∧ 𝐾 ∈ {ℝ, ℂ})) | ||
Theorem | cphssphl 23903 | A Banach subspace of a subcomplex pre-Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 11-Apr-2008.) (Revised by AV, 25-Sep-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban) → 𝑋 ∈ ℂHil) | ||
Theorem | cmslssbn 23904 | A complete linear subspace of a normed vector space is a Banach space. We furthermore have to assume that the field of scalars is complete since this is a requirement in the current definition of Banach spaces df-bn 23868. (Contributed by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp) ∧ (𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆)) → 𝑋 ∈ Ban) | ||
Theorem | cmscsscms 23905 | A closed subspace of a complete metric space which is also a subcomplex pre-Hilbert space is a complete metric space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized to arbitrary topological spaces (or at least topological modules), this assumption could be omitted. (Contributed by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (ClSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ CMetSp ∧ 𝑊 ∈ ℂPreHil) ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ CMetSp) | ||
Theorem | bncssbn 23906 | A closed subspace of a Banach space which is also a subcomplex pre-Hilbert space is a Banach space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized for arbitrary topological spaces, this assuption could be omitted. (Contributed by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (ClSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ Ban ∧ 𝑊 ∈ ℂPreHil) ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ Ban) | ||
Theorem | cssbn 23907 | A complete subspace of a normed vector space with a complete scalar field is a Banach space. Remark: In contrast to ClSubSp, a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition Cℋ (df-ch 28926) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 23904. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈)) ⇒ ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp ∧ 𝑈 ∈ 𝑆) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → 𝑋 ∈ Ban) | ||
Theorem | csschl 23908 | A complete subspace of a complex pre-Hilbert space is a complex Hilbert space. Remarks: (a) In contrast to ClSubSp, a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition Cℋ (df-ch 28926) of closed subspaces of a Hilbert space. (b) This theorem does not hold for arbitrary subcomplex (pre-)Hilbert spaces, because the scalar field as restriction of the field of the complex numbers need not be closed. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈)) & ⊢ (Scalar‘𝑊) = ℂfld ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → (𝑋 ∈ ℂHil ∧ (Scalar‘𝑋) = ℂfld)) | ||
Theorem | cmslsschl 23909 | A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂHil) | ||
Theorem | chlcsschl 23910 | A closed subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (ClSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂHil) | ||
Theorem | retopn 23911 | The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ (topGen‘ran (,)) = (TopOpen‘ℝfld) | ||
Theorem | recms 23912 | The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝfld ∈ CMetSp | ||
Theorem | reust 23913 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (UnifSt‘ℝfld) = (metUnif‘((dist‘ℝfld) ↾ (ℝ × ℝ))) | ||
Theorem | recusp 23914 | The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℝfld ∈ CUnifSp | ||
Syntax | crrx 23915 | Extend class notation with generalized real Euclidean spaces. |
class ℝ^ | ||
Syntax | cehl 23916 | Extend class notation with real Euclidean spaces. |
class 𝔼hil | ||
Definition | df-rrx 23917 | Define the function associating with a set the free real vector space on that set, equipped with the natural inner product and norm. This is the direct sum of copies of the field of real numbers indexed by that set. We call it here a "generalized real Euclidean space", but note that it need not be complete (for instance if the given set is infinite countable). (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ ℝ^ = (𝑖 ∈ V ↦ (toℂPreHil‘(ℝfld freeLMod 𝑖))) | ||
Definition | df-ehl 23918 | Define a function generating the real Euclidean spaces of finite dimension. The case 𝑛 = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 23949). Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛))) | ||
Theorem | rrxval 23919 | Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼))) | ||
Theorem | rrxbase 23920* | The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {𝑓 ∈ (ℝ ↑m 𝐼) ∣ 𝑓 finSupp 0}) | ||
Theorem | rrxprds 23921 | Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)})) ↾s 𝐵))) | ||
Theorem | rrxip 23922* | The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) = (·𝑖‘𝐻)) | ||
Theorem | rrxnm 23923* | The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻)) | ||
Theorem | rrxcph 23924 | Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil) | ||
Theorem | rrxds 23925* | The distance over generalized Euclidean spaces. Compare with df-rrn 34987. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻)) | ||
Theorem | rrxvsca 23926 | The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ ∙ = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) ⇒ ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽))) | ||
Theorem | rrxplusgvscavalb 23927* | The result of the addition combined with scalar multiplication in a generalized Euclidean space is defined by its coordinate-wise operations. (Contributed by AV, 21-Jan-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ ∙ = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ✚ = (+g‘𝐻) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑍 = ((𝐴 ∙ 𝑋) ✚ (𝐶 ∙ 𝑌)) ↔ ∀𝑖 ∈ 𝐼 (𝑍‘𝑖) = ((𝐴 · (𝑋‘𝑖)) + (𝐶 · (𝑌‘𝑖))))) | ||
Theorem | rrxsca 23928 | The field of real numbers is the scalar field of the generalized real Euclidean space. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (Scalar‘𝐻) = ℝfld) | ||
Theorem | rrx0 23929 | The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 0 = (𝐼 × {0}) ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝐻) = 0 ) | ||
Theorem | rrx0el 23930 | The zero ("origin") in a generalized real Euclidean space is an element of its base set. (Contributed by AV, 11-Feb-2023.) |
⊢ 0 = (𝐼 × {0}) & ⊢ 𝑃 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 0 ∈ 𝑃) | ||
Theorem | csbren 23931* | Cauchy-Schwarz-Bunjakovsky inequality for R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)↑2) ≤ (Σ𝑘 ∈ 𝐴 (𝐵↑2) · Σ𝑘 ∈ 𝐴 (𝐶↑2))) | ||
Theorem | trirn 23932* | Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (√‘Σ𝑘 ∈ 𝐴 ((𝐵 + 𝐶)↑2)) ≤ ((√‘Σ𝑘 ∈ 𝐴 (𝐵↑2)) + (√‘Σ𝑘 ∈ 𝐴 (𝐶↑2)))) | ||
Theorem | rrxf 23933* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐹:𝐼⟶ℝ) | ||
Theorem | rrxfsupp 23934* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ∈ Fin) | ||
Theorem | rrxsuppss 23935* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ⊆ 𝐼) | ||
Theorem | rrxmvallem 23936* | Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) supp 0) ⊆ ((𝐹 supp 0) ∪ (𝐺 supp 0))) | ||
Theorem | rrxmval 23937* | The value of the Euclidean metric. Compare with rrnmval 34989. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | rrxmfval 23938* | The value of the Euclidean metric. Compare with rrnval 34988. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑓 supp 0) ∪ (𝑔 supp 0))(((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetlem 23939* | Lemma for rrxmet 23940. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ 𝐴 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | ||
Theorem | rrxmet 23940* | 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.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | rrxdstprj1 23941* | 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.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹𝐷𝐺)) | ||
Theorem | rrxbasefi 23942 | The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of (ℝ ↑m 𝑋) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ 𝐻 = (ℝ^‘𝑋) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝜑 → 𝐵 = (ℝ ↑m 𝑋)) | ||
Theorem | rrxdsfi 23943* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetfi 23944 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑m 𝐼))) | ||
Theorem | rrxdsfival 23945* | The value of the Euclidean distance function in a generalized real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | ehlval 23946 | Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁))) | ||
Theorem | ehlbase 23947 | The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℝ ↑m (1...𝑁)) = (Base‘𝐸)) | ||
Theorem | ehl0base 23948 | 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 23949 | 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 23950* | The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝐼 = (1...𝑁) & ⊢ 𝐸 = (𝔼hil‘𝑁) & ⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | ehleudisval 23951* | The value of the Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.) |
⊢ 𝐼 = (1...𝑁) & ⊢ 𝐸 = (𝔼hil‘𝑁) & ⊢ 𝑋 = (ℝ ↑m 𝐼) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | ehl1eudis 23952* | The Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘1) & ⊢ 𝑋 = (ℝ ↑m {1}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (abs‘((𝑓‘1) − (𝑔‘1)))) | ||
Theorem | ehl1eudisval 23953 | The value of the Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘1) & ⊢ 𝑋 = (ℝ ↑m {1}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (abs‘((𝐹‘1) − (𝐺‘1)))) | ||
Theorem | ehl2eudis 23954* | The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑m {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2)))) | ||
Theorem | ehl2eudisval 23955 | The value of the Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.) |
⊢ 𝐸 = (𝔼hil‘2) & ⊢ 𝑋 = (ℝ ↑m {1, 2}) & ⊢ 𝐷 = (dist‘𝐸) ⇒ ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘((((𝐹‘1) − (𝐺‘1))↑2) + (((𝐹‘2) − (𝐺‘2))↑2)))) | ||
Theorem | minveclem1 23956* | Lemma for minvec 23968. 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 23957* | Lemma for minvec 23968. 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 23958* | Lemma for minvec 23968. 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 23959* | Lemma for minvec 23968. 𝐷 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 23960* | Lemma for minvec 23968. 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 23961* | Lemma for minvec 23968. 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 23962* | Lemma for minvec 23968. 𝐹 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 23963* | Lemma for minvec 23968. 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 23964* | Lemma for minvec 23968. 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 23965* | Lemma for minvec 23968. Discharge the assumptions in minveclem4 23964. (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 23966* | Lemma for minvec 23968. 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 23967* | Lemma for minvec 23968. 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 23968* | 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 23969* | Lemma for pjth 23971. (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 23970 | Lemma for pjth 23971. (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 23971 | 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 23972 | 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 23973 | 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 23974 | 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 23975 | 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 23976* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | divcncf 23977* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→(ℂ ∖ {0}))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | pmltpclem1 23978* | Lemma for pmltpc 23980. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) & ⊢ (𝜑 → (((𝐹‘𝐴) < (𝐹‘𝐵) ∧ (𝐹‘𝐶) < (𝐹‘𝐵)) ∨ ((𝐹‘𝐵) < (𝐹‘𝐴) ∧ (𝐹‘𝐵) < (𝐹‘𝐶)))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpclem2 23979* | Lemma for pmltpc 23980. (Contributed by Mario Carneiro, 1-Jul-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℝ ↑pm ℝ)) & ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐴) & ⊢ (𝜑 → 𝑊 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑈 ≤ 𝑉) & ⊢ (𝜑 → 𝑊 ≤ 𝑋) & ⊢ (𝜑 → ¬ (𝐹‘𝑈) ≤ (𝐹‘𝑉)) & ⊢ (𝜑 → ¬ (𝐹‘𝑋) ≤ (𝐹‘𝑊)) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐴 ∃𝑐 ∈ 𝐴 (𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ (((𝐹‘𝑎) < (𝐹‘𝑏) ∧ (𝐹‘𝑐) < (𝐹‘𝑏)) ∨ ((𝐹‘𝑏) < (𝐹‘𝑎) ∧ (𝐹‘𝑏) < (𝐹‘𝑐))))) | ||
Theorem | pmltpc 23980* | 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 23981* | Lemma for ivth 23984. 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 23982* | Lemma for ivth 23984. 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 23983* | Lemma for ivth 23984, 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 23984* | 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 23985* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle 23986* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthle2 23987* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑈 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) & ⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) & ⊢ (𝜑 → ((𝐹‘𝐵) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐴))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) | ||
Theorem | ivthicc 23988* | 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 23989* | Specialization of the Extreme Value Theorem to a closed interval of ℝ. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑥) ∧ ∃𝑧 ∈ (𝐴[,]𝐵)∀𝑤 ∈ (𝐴[,]𝐵)(𝐹‘𝑧) ≤ (𝐹‘𝑤))) | ||
Theorem | evthicc2 23990* | Combine ivthicc 23988 with evthicc 23989 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran 𝐹 = (𝑥[,]𝑦)) | ||
Theorem | cniccbdd 23991* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥) | ||
Syntax | covol 23992 | Extend class notation with the outer Lebesgue measure. |
class vol* | ||
Syntax | cvol 23993 | Extend class notation with the Lebesgue measure. |
class vol | ||
Definition | df-ovol 23994* | 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 23995* | 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 23996 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → ((1st ‘(𝐹‘𝑁)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑁)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑁)) ≤ (2nd ‘(𝐹‘𝑁)))) | ||
Theorem | ovolfioo 23997* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficc 23998* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ⊆ ∪ ran ([,] ∘ 𝐹) ↔ ∀𝑧 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑛))))) | ||
Theorem | ovolficcss 23999 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) | ||
Theorem | ovolfsval 24000 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
⊢ 𝐺 = ((abs ∘ − ) ∘ 𝐹) ⇒ ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑁 ∈ ℕ) → (𝐺‘𝑁) = ((2nd ‘(𝐹‘𝑁)) − (1st ‘(𝐹‘𝑁)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |