![]() |
Metamath
Proof Explorer Theorem List (p. 252 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmetcusp1 25101 | If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
β’ π = (BaseβπΉ) & β’ π· = ((distβπΉ) βΎ (π Γ π)) & β’ π = (UnifStβπΉ) β β’ ((π β β β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β πΉ β CUnifSp) | ||
Theorem | cmetcusp 25102 | The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
β’ ((π β β β§ π· β (CMetβπ)) β (toUnifSpβ(metUnifβπ·)) β CUnifSp) | ||
Theorem | cncms 25103 | The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ βfld β CMetSp | ||
Theorem | cnflduss 25104 | The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ π = (UnifStββfld) β β’ π = (metUnifβ(abs β β )) | ||
Theorem | cnfldcusp 25105 | The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld β CUnifSp | ||
Theorem | resscdrg 25106 | The real numbers are a subset of any complete subfield in the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (βfld βΎs πΎ) β β’ ((πΎ β (SubRingββfld) β§ πΉ β DivRing β§ πΉ β CMetSp) β β β πΎ) | ||
Theorem | cncdrg 25107 | The only complete subfields of the complex numbers are β and β. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (βfld βΎs πΎ) β β’ ((πΎ β (SubRingββfld) β§ πΉ β DivRing β§ πΉ β CMetSp) β πΎ β {β, β}) | ||
Theorem | srabn 25108 | The subring algebra over a complete normed ring is a Banach space iff the subring is a closed division ring. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π΄ = ((subringAlg βπ)βπ) & β’ π½ = (TopOpenβπ) β β’ ((π β NrmRing β§ π β CMetSp β§ π β (SubRingβπ)) β (π΄ β Ban β (π β (Clsdβπ½) β§ (π βΎs π) β DivRing))) | ||
Theorem | rlmbn 25109 | The ring module over a complete normed division ring is a Banach space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing β§ π β CMetSp) β (ringLModβπ ) β Ban) | ||
Theorem | ishl 25110 | The predicate "is a subcomplex Hilbert space". A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ (π β βHil β (π β Ban β§ π β βPreHil)) | ||
Theorem | hlbn 25111 | Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) |
β’ (π β βHil β π β Ban) | ||
Theorem | hlcph 25112 | Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β βHil β π β βPreHil) | ||
Theorem | hlphl 25113 | Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ (π β βHil β π β PreHil) | ||
Theorem | hlcms 25114 | Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
β’ (π β βHil β π β CMetSp) | ||
Theorem | hlprlem 25115 | Lemma for hlpr 25117. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β (πΎ β (SubRingββfld) β§ (βfld βΎs πΎ) β DivRing β§ (βfld βΎs πΎ) β CMetSp)) | ||
Theorem | hlress 25116 | The scalar field of a subcomplex Hilbert space contains β. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β β β πΎ) | ||
Theorem | hlpr 25117 | The scalar field of a subcomplex Hilbert space is either β or β. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β πΎ β {β, β}) | ||
Theorem | ishl2 25118 | 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 25119 | 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 25120 | 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 25084. (Contributed by AV, 8-Oct-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ (((π β NrmVec β§ (Scalarβπ) β CMetSp) β§ (π β CMetSp β§ π β π)) β π β Ban) | ||
Theorem | cmscsscms 25121 | 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 25122 | 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 25123 | 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 30741) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 25120. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (((π β NrmVec β§ (Scalarβπ) β CMetSp β§ π β π) β§ (Cauβπ·) β dom (βπ‘β(MetOpenβπ·))) β π β Ban) | ||
Theorem | csschl 25124 | 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 30741) 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 25125 | 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 25126 | 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 25127 | The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ (topGenβran (,)) = (TopOpenββfld) | ||
Theorem | recms 25128 | The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ βfld β CMetSp | ||
Theorem | reust 25129 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
β’ (UnifStββfld) = (metUnifβ((distββfld) βΎ (β Γ β))) | ||
Theorem | recusp 25130 | The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld β CUnifSp | ||
Syntax | crrx 25131 | Extend class notation with generalized real Euclidean spaces. |
class β^ | ||
Syntax | cehl 25132 | Extend class notation with real Euclidean spaces. |
class πΌhil | ||
Definition | df-rrx 25133 | 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 25134 | 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 25165). 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 25135 | Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β π» = (toβPreHilβ(βfld freeLMod πΌ))) | ||
Theorem | rrxbase 25136* | 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 25137 | 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 25138* | The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β (β βm πΌ), π β (β βm πΌ) β¦ (βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))))) = (Β·πβπ»)) | ||
Theorem | rrxnm 25139* | The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))))) = (normβπ»)) | ||
Theorem | rrxcph 25140 | 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 25141* | The distance over generalized Euclidean spaces. Compare with df-rrn 36997. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅, π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (distβπ»)) | ||
Theorem | rrxvsca 25142 | The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») & β’ β = ( Β·π βπ») & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β π΄ β β) & β’ (π β π β (Baseβπ»)) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | rrxplusgvscavalb 25143* | 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 25144 | 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 25145 | The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.) |
β’ π» = (β^βπΌ) & β’ 0 = (πΌ Γ {0}) β β’ (πΌ β π β (0gβπ») = 0 ) | ||
Theorem | rrx0el 25146 | 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 25147* | 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 25148* | 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 25149* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β πΉ:πΌβΆβ) | ||
Theorem | rrxfsupp 25150* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β Fin) | ||
Theorem | rrxsuppss 25151* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β πΌ) | ||
Theorem | rrxmvallem 25152* | 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 25153* | The value of the Euclidean metric. Compare with rrnmval 36999. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) | ||
Theorem | rrxmfval 25154* | The value of the Euclidean metric. Compare with rrnval 36998. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β π β π· = (π β π, π β π β¦ (ββΞ£π β ((π supp 0) βͺ (π supp 0))(((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetlem 25155* | Lemma for rrxmet 25156. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) & β’ (π β πΌ β π) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π΄ β πΌ) & β’ (π β π΄ β Fin) & β’ (π β ((πΉ supp 0) βͺ (πΊ supp 0)) β π΄) β β’ (π β Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) = Ξ£π β π΄ (((πΉβπ) β (πΊβπ))β2)) | ||
Theorem | rrxmet 25156* | 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 25157* | 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 25158 | 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 25159* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (β^βπΌ) & β’ π΅ = (β βm πΌ) β β’ (πΌ β Fin β (distβπ») = (π β π΅, π β π΅ β¦ (ββΞ£π β πΌ (((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetfi 25160 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β Fin β π· β (Metβ(β βm πΌ))) | ||
Theorem | rrxdsfival 25161* | 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 25162 | Value of the Euclidean space of dimension π. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ πΈ = (πΌhilβπ) β β’ (π β β0 β πΈ = (β^β(1...π))) | ||
Theorem | ehlbase 25163 | 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 25164 | 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 25165 | 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 25166* | 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 25167* | 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 25168* | 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 25169 | 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 25170* | 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 25171 | 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 25172* | Lemma for minvec 25184. 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 25173* | Lemma for minvec 25184. 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 25174* | Lemma for minvec 25184. 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 25175* | Lemma for minvec 25184. π· 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 25176* | Lemma for minvec 25184. 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 25177* | Lemma for minvec 25184. 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 25178* | Lemma for minvec 25184. πΉ 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 25179* | Lemma for minvec 25184. 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 25180* | Lemma for minvec 25184. 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 25181* | Lemma for minvec 25184. Discharge the assumptions in minveclem4 25180. (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 25182* | Lemma for minvec 25184. 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 25183* | Lemma for minvec 25184. 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 25184* | 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 25185* | Lemma for pjth 25187. (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 25186 | Lemma for pjth 25187. (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 25187 | 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 25188 | 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 25189 | 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 25190 | 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 25191 | 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 25192* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ + π΅)) β (πβcnββ)) | ||
Theorem | subcncf 25193* | The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ β π΅)) β (πβcnββ)) | ||
Theorem | mulcncf 25194* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Avoid ax-mulf 11192. (Revised by GG, 16-Mar-2025.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) | ||
Theorem | mulcncfOLD 25195* | Obsolete version of mulcncf 25194 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 25196* | The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnβ(β β {0}))) β β’ (π β (π₯ β π β¦ (π΄ / π΅)) β (πβcnββ)) | ||
Theorem | pmltpclem1 25197* | Lemma for pmltpc 25199. (Contributed by Mario Carneiro, 1-Jul-2014.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΄ < π΅) & β’ (π β π΅ < πΆ) & β’ (π β (((πΉβπ΄) < (πΉβπ΅) β§ (πΉβπΆ) < (πΉβπ΅)) β¨ ((πΉβπ΅) < (πΉβπ΄) β§ (πΉβπ΅) < (πΉβπΆ)))) β β’ (π β βπ β π βπ β π βπ β π (π < π β§ π < π β§ (((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ)) β¨ ((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ))))) | ||
Theorem | pmltpclem2 25198* | Lemma for pmltpc 25199. (Contributed by Mario Carneiro, 1-Jul-2014.) |
β’ (π β πΉ β (β βpm β)) & β’ (π β π΄ β dom πΉ) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β€ π) & β’ (π β π β€ π) & β’ (π β Β¬ (πΉβπ) β€ (πΉβπ)) & β’ (π β Β¬ (πΉβπ) β€ (πΉβπ)) β β’ (π β βπ β π΄ βπ β π΄ βπ β π΄ (π < π β§ π < π β§ (((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ)) β¨ ((πΉβπ) < (πΉβπ) β§ (πΉβπ) < (πΉβπ))))) | ||
Theorem | pmltpc 25199* | 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 25200* | Lemma for ivth 25203. The set π of all π₯ values with (πΉβπ₯) less than π is lower bounded by π΄ and upper bounded by π΅. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ (π β π΄ < π΅) & β’ (π β (π΄[,]π΅) β π·) & β’ (π β πΉ β (π·βcnββ)) & β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) & β’ (π β ((πΉβπ΄) < π β§ π < (πΉβπ΅))) & β’ π = {π₯ β (π΄[,]π΅) β£ (πΉβπ₯) β€ π} β β’ (π β (π΄ β π β§ βπ§ β π π§ β€ π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |