Home | Metamath
Proof Explorer Theorem List (p. 247 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | metsscmetcld 24601 | A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 24602. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 9-Oct-2022.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β (Clsdβπ½)) | ||
Theorem | cmetss 24602 | A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 9-Oct-2022.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (CMetβπ) β ((π· βΎ (π Γ π)) β (CMetβπ) β π β (Clsdβπ½))) | ||
Theorem | equivcmet 24603* | If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 24586, metss2 23790, this theorem does not have a one-directional form - it is possible for a metric πΆ that is strongly finer than the complete metric π· to be incomplete and vice versa. Consider π· = the metric on β induced by the usual homeomorphism from (0, 1) against the usual metric πΆ on β and against the discrete metric πΈ on β. Then both πΆ and πΈ are complete but π· is not, and πΆ is strongly finer than π·, which is strongly finer than πΈ. (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ (π Β· (π₯πΆπ¦))) β β’ (π β (πΆ β (CMetβπ) β π· β (CMetβπ))) | ||
Theorem | relcmpcmet 24604* | If π· is a metric space such that all the balls of some fixed size are relatively compact, then π· is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ π₯ β π) β (π½ βΎt ((clsβπ½)β(π₯(ballβπ·)π ))) β Comp) β β’ (π β π· β (CMetβπ)) | ||
Theorem | cmpcmet 24605 | A compact metric space is complete. One half of heibor 36166. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) β β’ (π β π· β (CMetβπ)) | ||
Theorem | cfilucfil3 24606 | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (βMetβπ)) β ((πΆ β (Filβπ) β§ πΆ β (CauFiluβ(metUnifβπ·))) β πΆ β (CauFilβπ·))) | ||
Theorem | cfilucfil4 24607 | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (βMetβπ) β§ πΆ β (Filβπ)) β (πΆ β (CauFiluβ(metUnifβπ·)) β πΆ β (CauFilβπ·))) | ||
Theorem | cncmet 24608 | The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ π· = (abs β β ) β β’ π· β (CMetββ) | ||
Theorem | recmet 24609 | The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((abs β β ) βΎ (β Γ β)) β (CMetββ) | ||
Theorem | bcthlem1 24610* | Lemma for bcth 24615. Substitutions for the function πΉ. (Contributed by Mario Carneiro, 9-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) β β’ ((π β§ (π΄ β β β§ π΅ β (π Γ β+))) β (πΆ β (π΄πΉπ΅) β (πΆ β (π Γ β+) β§ (2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) | ||
Theorem | bcthlem2 24611* | Lemma for bcth 24615. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ (π β βπ β β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) | ||
Theorem | bcthlem3 24612* | Lemma for bcth 24615. The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ ((π β§ (1st β π)(βπ‘βπ½)π₯ β§ π΄ β β) β π₯ β ((ballβπ·)β(πβπ΄))) | ||
Theorem | bcthlem4 24613* | Lemma for bcth 24615. Given any open ball (πΆ(ballβπ·)π ) as starting point (and in particular, a ball in int(βͺ ran π)), the limit point π₯ of the centers of the induced sequence of balls π is outside βͺ ran π. Note that a set π΄ has empty interior iff every nonempty open set π contains points outside π΄, i.e. (π β π΄) β β . (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ (π β ((πΆ(ballβπ·)π ) β βͺ ran π) β β ) | ||
Theorem | bcthlem5 24614* |
Lemma for bcth 24615. The proof makes essential use of the Axiom
of
Dependent Choice axdc4uz 13818, which in the form used here accepts a
"selection" function πΉ from each element of πΎ to a
nonempty
subset of πΎ, and the result function π maps
π(π + 1)
to an element of πΉ(π, π(π)). The trick here is thus in
the choice of πΉ and πΎ: we let πΎ be the
set of all tagged
nonempty open sets (tagged here meaning that we have a point and an
open set, in an ordered pair), and πΉ(π, β¨π₯, π§β©) gives the
set of all balls of size less than 1 / π, tagged by their
centers, whose closures fit within the given open set π§ and
miss
π(π).
Since π(π) is closed, π§ β π(π) is open and also nonempty, since π§ is nonempty and π(π) has empty interior. Then there is some ball contained in it, and hence our function πΉ is valid (it never maps to the empty set). Now starting at a point in the interior of βͺ ran π, DC gives us the function π all whose elements are constrained by πΉ acting on the previous value. (This is all proven in this lemma.) Now π is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 24611) and whose sizes tend to zero, since they are bounded above by 1 / π. Thus, the centers of these balls form a Cauchy sequence, and converge to a point π₯ (see bcthlem4 24613). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point π₯ must be in all these balls (see bcthlem3 24612) and hence misses each π(π), contradicting the fact that π₯ is in the interior of βͺ ran π (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β βπ β β ((intβπ½)β(πβπ)) = β ) β β’ (π β ((intβπ½)ββͺ ran π) = β ) | ||
Theorem | bcth 24615* | Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset πβπ must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 24614 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ π:ββΆ(Clsdβπ½) β§ ((intβπ½)ββͺ ran π) β β ) β βπ β β ((intβπ½)β(πβπ)) β β ) | ||
Theorem | bcth2 24616* | Baire's Category Theorem, version 2: If countably many closed sets cover π, then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ (((π· β (CMetβπ) β§ π β β ) β§ (π:ββΆ(Clsdβπ½) β§ βͺ ran π = π)) β βπ β β ((intβπ½)β(πβπ)) β β ) | ||
Theorem | bcth3 24617* | Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ π:ββΆπ½ β§ βπ β β ((clsβπ½)β(πβπ)) = π) β ((clsβπ½)ββ© ran π) = π) | ||
Syntax | ccms 24618 | Extend class notation with the class of complete metric spaces. |
class CMetSp | ||
Syntax | cbn 24619 | Extend class notation with the class of Banach spaces. |
class Ban | ||
Syntax | chl 24620 | Extend class notation with the class of subcomplex Hilbert spaces. |
class βHil | ||
Definition | df-cms 24621* | Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ CMetSp = {π€ β MetSp β£ [(Baseβπ€) / π]((distβπ€) βΎ (π Γ π)) β (CMetβπ)} | ||
Definition | df-bn 24622 | Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ Ban = {π€ β (NrmVec β© CMetSp) β£ (Scalarβπ€) β CMetSp} | ||
Definition | df-hl 24623 | Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a subfield of the field of complex numbers closed under square roots of nonnegative reals. (Contributed by Steve Rodriguez, 28-Apr-2007.) |
β’ βHil = (Ban β© βPreHil) | ||
Theorem | isbn 24624 | A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β Ban β (π β NrmVec β§ π β CMetSp β§ πΉ β CMetSp)) | ||
Theorem | bnsca 24625 | The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β Ban β πΉ β CMetSp) | ||
Theorem | bnnvc 24626 | A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmVec) | ||
Theorem | bnnlm 24627 | A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmMod) | ||
Theorem | bnngp 24628 | A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmGrp) | ||
Theorem | bnlmod 24629 | A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β LMod) | ||
Theorem | bncms 24630 | A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β CMetSp) | ||
Theorem | iscms 24631 | A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β CMetSp β (π β MetSp β§ π· β (CMetβπ))) | ||
Theorem | cmscmet 24632 | The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β CMetSp β π· β (CMetβπ)) | ||
Theorem | bncmet 24633 | The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β Ban β π· β (CMetβπ)) | ||
Theorem | cmsms 24634 | A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (πΊ β CMetSp β πΊ β MetSp) | ||
Theorem | cmspropd 24635 | Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β CMetSp β πΏ β CMetSp)) | ||
Theorem | cmssmscld 24636 | The restriction of a metric space is closed if it is complete. (Contributed by AV, 9-Oct-2022.) |
β’ πΎ = (π βΎs π΄) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π΄ β (Clsdβπ½)) | ||
Theorem | cmsss 24637 | The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΎ = (π βΎs π΄) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β CMetSp β§ π΄ β π) β (πΎ β CMetSp β π΄ β (Clsdβπ½))) | ||
Theorem | lssbn 24638 | A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β Ban β§ π β π) β (π β Ban β π β (Clsdβπ½))) | ||
Theorem | cmetcusp1 24639 | 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 24640 | 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 24641 | The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ βfld β CMetSp | ||
Theorem | cnflduss 24642 | 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 24643 | The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld β CUnifSp | ||
Theorem | resscdrg 24644 | 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 24645 | 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 24646 | 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 24647 | 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 24648 | 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 24649 | Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) |
β’ (π β βHil β π β Ban) | ||
Theorem | hlcph 24650 | Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β βHil β π β βPreHil) | ||
Theorem | hlphl 24651 | 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 24652 | Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
β’ (π β βHil β π β CMetSp) | ||
Theorem | hlprlem 24653 | Lemma for hlpr 24655. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β (πΎ β (SubRingββfld) β§ (βfld βΎs πΎ) β DivRing β§ (βfld βΎs πΎ) β CMetSp)) | ||
Theorem | hlress 24654 | The scalar field of a subcomplex Hilbert space contains β. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β β β πΎ) | ||
Theorem | hlpr 24655 | The scalar field of a subcomplex Hilbert space is either β or β. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (π β βHil β πΎ β {β, β}) | ||
Theorem | ishl2 24656 | 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 24657 | 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 24658 | 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 24622. (Contributed by AV, 8-Oct-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ (((π β NrmVec β§ (Scalarβπ) β CMetSp) β§ (π β CMetSp β§ π β π)) β π β Ban) | ||
Theorem | cmscsscms 24659 | 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 24660 | 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 24661 | 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 29949) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 24658. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (((π β NrmVec β§ (Scalarβπ) β CMetSp β§ π β π) β§ (Cauβπ·) β dom (βπ‘β(MetOpenβπ·))) β π β Ban) | ||
Theorem | csschl 24662 | 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 29949) 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 24663 | 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 24664 | 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 24665 | The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ (topGenβran (,)) = (TopOpenββfld) | ||
Theorem | recms 24666 | The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
β’ βfld β CMetSp | ||
Theorem | reust 24667 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
β’ (UnifStββfld) = (metUnifβ((distββfld) βΎ (β Γ β))) | ||
Theorem | recusp 24668 | The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld β CUnifSp | ||
Syntax | crrx 24669 | Extend class notation with generalized real Euclidean spaces. |
class β^ | ||
Syntax | cehl 24670 | Extend class notation with real Euclidean spaces. |
class πΌhil | ||
Definition | df-rrx 24671 | 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 24672 | 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 24703). 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 24673 | Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β π» = (toβPreHilβ(βfld freeLMod πΌ))) | ||
Theorem | rrxbase 24674* | 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 24675 | 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 24676* | The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β (β βm πΌ), π β (β βm πΌ) β¦ (βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯) Β· (πβπ₯))))) = (Β·πβπ»)) | ||
Theorem | rrxnm 24677* | The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ ((πβπ₯)β2))))) = (normβπ»)) | ||
Theorem | rrxcph 24678 | 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 24679* | The distance over generalized Euclidean spaces. Compare with df-rrn 36171. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») β β’ (πΌ β π β (π β π΅, π β π΅ β¦ (ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (distβπ»)) | ||
Theorem | rrxvsca 24680 | The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
β’ π» = (β^βπΌ) & β’ π΅ = (Baseβπ») & β’ β = ( Β·π βπ») & β’ (π β πΌ β π) & β’ (π β π½ β πΌ) & β’ (π β π΄ β β) & β’ (π β π β (Baseβπ»)) β β’ (π β ((π΄ β π)βπ½) = (π΄ Β· (πβπ½))) | ||
Theorem | rrxplusgvscavalb 24681* | 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 24682 | 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 24683 | The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.) |
β’ π» = (β^βπΌ) & β’ 0 = (πΌ Γ {0}) β β’ (πΌ β π β (0gβπ») = 0 ) | ||
Theorem | rrx0el 24684 | 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 24685* | 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 24686* | 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 24687* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β πΉ:πΌβΆβ) | ||
Theorem | rrxfsupp 24688* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β Fin) | ||
Theorem | rrxsuppss 24689* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ (π β πΉ β π) β β’ (π β (πΉ supp 0) β πΌ) | ||
Theorem | rrxmvallem 24690* | 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 24691* | The value of the Euclidean metric. Compare with rrnmval 36173. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) | ||
Theorem | rrxmfval 24692* | The value of the Euclidean metric. Compare with rrnval 36172. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β π β π· = (π β π, π β π β¦ (ββΞ£π β ((π supp 0) βͺ (π supp 0))(((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetlem 24693* | Lemma for rrxmet 24694. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
β’ π = {β β (β βm πΌ) β£ β finSupp 0} & β’ π· = (distβ(β^βπΌ)) & β’ (π β πΌ β π) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π΄ β πΌ) & β’ (π β π΄ β Fin) & β’ (π β ((πΉ supp 0) βͺ (πΊ supp 0)) β π΄) β β’ (π β Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) = Ξ£π β π΄ (((πΉβπ) β (πΊβπ))β2)) | ||
Theorem | rrxmet 24694* | 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 24695* | 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 24696 | 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 24697* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π» = (β^βπΌ) & β’ π΅ = (β βm πΌ) β β’ (πΌ β Fin β (distβπ») = (π β π΅, π β π΅ β¦ (ββΞ£π β πΌ (((πβπ) β (πβπ))β2)))) | ||
Theorem | rrxmetfi 24698 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ π· = (distβ(β^βπΌ)) β β’ (πΌ β Fin β π· β (Metβ(β βm πΌ))) | ||
Theorem | rrxdsfival 24699* | 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 24700 | Value of the Euclidean space of dimension π. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
β’ πΈ = (πΌhilβπ) β β’ (π β β0 β πΈ = (β^β(1...π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |