![]() |
Metamath
Proof Explorer Theorem List (p. 254 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ehl 25301 | 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 25332). 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 25302 | Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β π» = (toβPreHilβ(βfld freeLMod πΌ))) | ||
Theorem | rrxbase 25303* | 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 25304 | 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 25305* | The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β (β βm πΌ), π β (β βm πΌ) β¦ (βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))))) = (Β·πβπ»)) | ||
Theorem | rrxnm 25306* | The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))))) = (normβπ»)) | ||
Theorem | rrxcph 25307 | 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 25308* | The distance over generalized Euclidean spaces. Compare with df-rrn 37234. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅, π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (distβπ»)) | ||
Theorem | rrxvsca 25309 | The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») & β’ β = ( Β·π βπ») & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β π΄ β β) & β’ (π β π β (Baseβπ»)) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | rrxplusgvscavalb 25310* | 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 25311 | 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 25312 | The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.) |
β’ π» = (β^βπΌ) & β’ 0 = (πΌ Γ {0}) β β’ (πΌ β π β (0gβπ») = 0 ) | ||
Theorem | rrx0el 25313 | 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 25314* | 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 25315* | 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 25316* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β πΉ:πΌβΆβ) | ||
Theorem | rrxfsupp 25317* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β Fin) | ||
Theorem | rrxsuppss 25318* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β πΌ) | ||
Theorem | rrxmvallem 25319* | 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 25320* | The value of the Euclidean metric. Compare with rrnmval 37236. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) | ||
Theorem | rrxmfval 25321* | The value of the Euclidean metric. Compare with rrnval 37235. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β π β π· = (π β π, π β π β¦ (ββΞ£π β ((π supp 0) βͺ (π supp 0))(((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetlem 25322* | Lemma for rrxmet 25323. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) & β’ (π β πΌ β π) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π΄ β πΌ) & β’ (π β π΄ β Fin) & β’ (π β ((πΉ supp 0) βͺ (πΊ supp 0)) β π΄) β β’ (π β Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) = Ξ£π β π΄ (((πΉβπ) β (πΊβπ))β2)) | ||
Theorem | rrxmet 25323* | 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 25324* | 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 25325 | 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 25326* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (β^βπΌ) & β’ π΅ = (β βm πΌ) β β’ (πΌ β Fin β (distβπ») = (π β π΅, π β π΅ β¦ (ββΞ£π β πΌ (((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetfi 25327 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β Fin β π· β (Metβ(β βm πΌ))) | ||
Theorem | rrxdsfival 25328* | 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 25329 | Value of the Euclidean space of dimension π. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ πΈ = (πΌhilβπ) β β’ (π β β0 β πΈ = (β^β(1...π))) | ||
Theorem | ehlbase 25330 | 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 25331 | 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 25332 | 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 25333* | 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 25334* | 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 25335* | 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 25336 | 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 25337* | 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 25338 | 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 25339* | Lemma for minvec 25351. 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 25340* | Lemma for minvec 25351. 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 25341* | Lemma for minvec 25351. 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 25342* | Lemma for minvec 25351. π· 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 25343* | Lemma for minvec 25351. 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 25344* | Lemma for minvec 25351. 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 25345* | Lemma for minvec 25351. πΉ 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 25346* | Lemma for minvec 25351. 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 25347* | Lemma for minvec 25351. 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 25348* | Lemma for minvec 25351. Discharge the assumptions in minveclem4 25347. (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 25349* | Lemma for minvec 25351. 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 25350* | Lemma for minvec 25351. 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 25351* | 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 25352* | Lemma for pjth 25354. (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 25353 | Lemma for pjth 25354. (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 25354 | 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 25355 | 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 25356 | 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 25357 | 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 25358 | Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.) |
β’ (π β βHil β π β Hil) | ||
Theorem | addcncf 25359* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ + π΅)) β (πβcnββ)) | ||
Theorem | subcncf 25360* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ β π΅)) β (πβcnββ)) | ||
Theorem | mulcncf 25361* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Avoid ax-mulf 11210. (Revised by GG, 16-Mar-2025.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) | ||
Theorem | mulcncfOLD 25362* | Obsolete version of mulcncf 25361 as of 9-Apr-2025. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) | ||
Theorem | divcncf 25363* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnβ(β β {0}))) β β’ (π β (π₯ β π β¦ (π΄ / π΅)) β (πβcnββ)) | ||
Theorem | pmltpclem1 25364* | Lemma for pmltpc 25366. (Contributed by Mario Carneiro, 1-Jul-2014.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ < π΅) & β’ (π β π΅ < πΆ) & β’ (π β (((πΉβπ΄) < (πΉβπ΅) β§ (πΉβπΆ) < (πΉβπ΅)) β¨ ((πΉβπ΅) < (πΉβπ΄) β§ (πΉβπ΅) < (πΉβπΆ)))) β β’ (π β βπ β π βπ β π βπ β π (π < π β§ π < π β§ (((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ)) β¨ ((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ))))) | ||
Theorem | pmltpclem2 25365* | Lemma for pmltpc 25366. (Contributed by Mario Carneiro, 1-Jul-2014.) |
β’ (π β πΉ β (β βpm β)) & β’ (π β π΄ β dom πΉ) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β Β¬ (πΉβπ) β€ (πΉβπ)) & β’ (π β Β¬ (πΉβπ) β€ (πΉβπ)) β β’ (π β βπ β π΄ βπ β π΄ βπ β π΄ (π < π β§ π < π β§ (((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ)) β¨ ((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ))))) | ||
Theorem | pmltpc 25366* | 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 25367* | Lemma for ivth 25370. 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 25368* | Lemma for ivth 25370. 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 25369* | Lemma for ivth 25370, 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 25370* | 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 25371* | The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β π·) & β’ (π β πΉ β (π·βcnββ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) & β’ (π β ((πΉβπ΅) < π β§ π < (πΉβπ΄))) β β’ (π β βπ β (π΄(,)π΅)(πΉβπ) = π) | ||
Theorem | ivthle 25372* | The intermediate value theorem with weak inequality, increasing case. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β π·) & β’ (π β πΉ β (π·βcnββ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) & β’ (π β ((πΉβπ΄) β€ π β§ π β€ (πΉβπ΅))) β β’ (π β βπ β (π΄[,]π΅)(πΉβπ) = π) | ||
Theorem | ivthle2 25373* | The intermediate value theorem with weak inequality, decreasing case. (Contributed by Mario Carneiro, 12-May-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β π·) & β’ (π β πΉ β (π·βcnββ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) & β’ (π β ((πΉβπ΅) β€ π β§ π β€ (πΉβπ΄))) β β’ (π β βπ β (π΄[,]π΅)(πΉβπ) = π) | ||
Theorem | ivthicc 25374* | 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 25375* | Specialization of the Extreme Value Theorem to a closed interval of β. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β (βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(πΉβπ¦) β€ (πΉβπ₯) β§ βπ§ β (π΄[,]π΅)βπ€ β (π΄[,]π΅)(πΉβπ§) β€ (πΉβπ€))) | ||
Theorem | evthicc2 25376* | Combine ivthicc 25374 with evthicc 25375 to exactly describe the image of a closed interval. (Contributed by Mario Carneiro, 19-Feb-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β βπ₯ β β βπ¦ β β ran πΉ = (π₯[,]π¦)) | ||
Theorem | cniccbdd 25377* | A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) | ||
Syntax | covol 25378 | Extend class notation with the outer Lebesgue measure. |
class vol* | ||
Syntax | cvol 25379 | Extend class notation with the Lebesgue measure. |
class vol | ||
Definition | df-ovol 25380* | 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 25381* | 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 25382 | Closure for the interval endpoint function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ ((πΉ:ββΆ( β€ β© (β Γ β)) β§ π β β) β ((1st β(πΉβπ)) β β β§ (2nd β(πΉβπ)) β β β§ (1st β(πΉβπ)) β€ (2nd β(πΉβπ)))) | ||
Theorem | ovolfioo 25383* | Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β© (β Γ β))) β (π΄ β βͺ ran ((,) β πΉ) β βπ§ β π΄ βπ β β ((1st β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))))) | ||
Theorem | ovolficc 25384* | Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β© (β Γ β))) β (π΄ β βͺ ran ([,] β πΉ) β βπ§ β π΄ βπ β β ((1st β(πΉβπ)) β€ π§ β§ π§ β€ (2nd β(πΉβπ))))) | ||
Theorem | ovolficcss 25385 | Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (πΉ:ββΆ( β€ β© (β Γ β)) β βͺ ran ([,] β πΉ) β β) | ||
Theorem | ovolfsval 25386 | The value of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ πΊ = ((abs β β ) β πΉ) β β’ ((πΉ:ββΆ( β€ β© (β Γ β)) β§ π β β) β (πΊβπ) = ((2nd β(πΉβπ)) β (1st β(πΉβπ)))) | ||
Theorem | ovolfsf 25387 | Closure for the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ πΊ = ((abs β β ) β πΉ) β β’ (πΉ:ββΆ( β€ β© (β Γ β)) β πΊ:ββΆ(0[,)+β)) | ||
Theorem | ovolsf 25388 | Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ πΊ = ((abs β β ) β πΉ) & β’ π = seq1( + , πΊ) β β’ (πΉ:ββΆ( β€ β© (β Γ β)) β π:ββΆ(0[,)+β)) | ||
Theorem | ovolval 25389* | The value of the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 17-Sep-2020.) |
β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} β β’ (π΄ β β β (vol*βπ΄) = inf(π, β*, < )) | ||
Theorem | elovolmlem 25390 | Lemma for elovolm 25391 and related theorems. (Contributed by BJ, 23-Jul-2022.) |
β’ (πΉ β ((π΄ β© (β Γ β)) βm β) β πΉ:ββΆ(π΄ β© (β Γ β))) | ||
Theorem | elovolm 25391* | Elementhood in the set π of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} β β’ (π΅ β π β βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π΅ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))) | ||
Theorem | elovolmr 25392* | Sufficient condition for elementhood in the set π. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} & β’ π = seq1( + , ((abs β β ) β πΉ)) β β’ ((πΉ:ββΆ( β€ β© (β Γ β)) β§ π΄ β βͺ ran ((,) β πΉ)) β sup(ran π, β*, < ) β π) | ||
Theorem | ovolmge0 25393* | The set π is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} β β’ (π΅ β π β 0 β€ π΅) | ||
Theorem | ovolcl 25394 | The volume of a set is an extended real number. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ (π΄ β β β (vol*βπ΄) β β*) | ||
Theorem | ovollb 25395 | 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 25396* | The outer volume is the greatest lower bound on the sum of all interval coverings of π΄. (Contributed by Mario Carneiro, 15-Jun-2014.) |
β’ π = seq1( + , ((abs β β ) β π)) β β’ ((π΄ β β β§ (vol*βπ΄) β β β§ π΅ β β+) β βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ sup(ran π, β*, < ) β€ ((vol*βπ΄) + π΅))) | ||
Theorem | ovolge0 25397 | The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014.) |
β’ (π΄ β β β 0 β€ (vol*βπ΄)) | ||
Theorem | ovolf 25398 | The domain and codomain of the outer volume function. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
β’ vol*:π« ββΆ(0[,]+β) | ||
Theorem | ovollecl 25399 | If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ (vol*βπ΄) β€ π΅) β (vol*βπ΄) β β) | ||
Theorem | ovolsslem 25400* | Lemma for ovolss 25401. (Contributed by Mario Carneiro, 16-Mar-2014.) (Proof shortened by AV, 17-Sep-2020.) |
β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} & β’ π = {π¦ β β* β£ βπ β (( β€ β© (β Γ β)) βm β)(π΅ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β ) β π)), β*, < ))} β β’ ((π΄ β π΅ β§ π΅ β β) β (vol*βπ΄) β€ (vol*βπ΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |