Home | Metamath
Proof Explorer Theorem List (p. 239 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cphnmf 23801 | The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝑁:𝑉⟶𝐾) | ||
Theorem | cphnmcl 23802 | The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝑁‘𝐴) ∈ 𝐾) | ||
Theorem | reipcl 23803 | An inner product of an element with itself is real. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 𝐴) ∈ ℝ) | ||
Theorem | ipge0 23804 | The inner product in a subcomplex pre-Hilbert space is positive definite. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → 0 ≤ (𝐴 , 𝐴)) | ||
Theorem | cphipcj 23805 | Conjugate of an inner product in a subcomplex pre-Hilbert space. Complex version of ipcj 20780. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∗‘(𝐴 , 𝐵)) = (𝐵 , 𝐴)) | ||
Theorem | cphipipcj 23806 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (Revised by AV, 19-Oct-2021.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) · (𝐵 , 𝐴)) = ((abs‘(𝐴 , 𝐵))↑2)) | ||
Theorem | cphorthcom 23807 | Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 20781. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) = 0 ↔ (𝐵 , 𝐴) = 0)) | ||
Theorem | cphip0l 23808 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 20782. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ( 0 , 𝐴) = 0) | ||
Theorem | cphip0r 23809 | Inner product with a zero second argument. Complex version of ip0r 20783. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 0 ) = 0) | ||
Theorem | cphipeq0 23810 | The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. Complex version of ipeq0 20784. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ((𝐴 , 𝐴) = 0 ↔ 𝐴 = 0 )) | ||
Theorem | cphdir 23811 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 20785. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 + 𝐵) , 𝐶) = ((𝐴 , 𝐶) + (𝐵 , 𝐶))) | ||
Theorem | cphdi 23812 | Distributive law for inner product (left-distributivity). Complex version of ipdi 20786. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 + 𝐶)) = ((𝐴 , 𝐵) + (𝐴 , 𝐶))) | ||
Theorem | cph2di 23813 | Distributive law for inner product. Complex version of ip2di 20787. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) , (𝐶 + 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) + ((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | cphsubdir 23814 | Distributive law for inner product subtraction. Complex version of ipsubdir 20788. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶) − (𝐵 , 𝐶))) | ||
Theorem | cphsubdi 23815 | Distributive law for inner product subtraction. Complex version of ipsubdi 20789. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 − 𝐶)) = ((𝐴 , 𝐵) − (𝐴 , 𝐶))) | ||
Theorem | cph2subdi 23816 | Distributive law for inner product subtraction. Complex version of ip2subdi 20790. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) − ((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | cphass 23817 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 20791, his5 28865. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 · 𝐵) , 𝐶) = (𝐴 · (𝐵 , 𝐶))) | ||
Theorem | cphassr 23818 | "Associative" law for second argument of inner product (compare cphass 23817). See ipassr 20792, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 , (𝐴 · 𝐶)) = ((∗‘𝐴) · (𝐵 , 𝐶))) | ||
Theorem | cph2ass 23819 | Move scalar multiplication to outside of inner product. See his35 28867. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 · 𝐶) , (𝐵 · 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 , 𝐷))) | ||
Theorem | cphassi 23820 | Associative law for the first argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) = (i · (𝐵 , 𝐴))) | ||
Theorem | cphassir 23821 | "Associative" law for the second argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) = (-i · (𝐴 , 𝐵))) | ||
Theorem | tcphex 23822* | Lemma for tcphbas 23824 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))) ∈ V | ||
Theorem | tcphval 23823* | Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ 𝐺 = (𝑊 toNrmGrp (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) | ||
Theorem | tcphbas 23824 | The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ 𝑉 = (Base‘𝐺) | ||
Theorem | tchplusg 23825 | The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | tcphsub 23826 | The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ − = (-g‘𝐺) | ||
Theorem | tcphmulr 23827 | The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ · = (.r‘𝑊) ⇒ ⊢ · = (.r‘𝐺) | ||
Theorem | tcphsca 23828 | The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ 𝐹 = (Scalar‘𝐺) | ||
Theorem | tcphvsca 23829 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ · = ( ·𝑠 ‘𝐺) | ||
Theorem | tcphip 23830 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ · = (·𝑖‘𝑊) ⇒ ⊢ · = (·𝑖‘𝐺) | ||
Theorem | tcphtopn 23831 | The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝑊 ∈ 𝑉 → 𝐽 = (MetOpen‘𝐷)) | ||
Theorem | tcphphl 23832 | Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space (because all the original components are the same). (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil) | ||
Theorem | tchnmfval 23833* | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) | ||
Theorem | tcphnmval 23834 | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) | ||
Theorem | cphtcphnm 23835 | The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝑁 = (norm‘𝐺)) | ||
Theorem | tcphds 23836 | The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝑊) ⇒ ⊢ (𝑊 ∈ Grp → (𝑁 ∘ − ) = (dist‘𝐺)) | ||
Theorem | phclm 23837 | A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) ⇒ ⊢ (𝜑 → 𝑊 ∈ ℂMod) | ||
Theorem | tcphcphlem3 23838 | Lemma for tcphcph 23842: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ) | ||
Theorem | ipcau2 23839* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | tcphcphlem1 23840* | Lemma for tcphcph 23842: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))) | ||
Theorem | tcphcphlem2 23841* | Lemma for tcphcph 23842: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (√‘((𝑋 · 𝑌) , (𝑋 · 𝑌))) = ((abs‘𝑋) · (√‘(𝑌 , 𝑌)))) | ||
Theorem | tcphcph 23842* | The standard definition of a norm turns any pre-Hilbert space over a subfield of ℂfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂPreHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ℂPreHil) | ||
Theorem | ipcau 23843 | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | nmparlem 23844 | Lemma for nmpar 23845. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | nmpar 23845 | A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | cphipval2 23846 | Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4)) | ||
Theorem | 4cphipval2 23847 | Four times the inner product value cphipval2 23846. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴 , 𝐵)) = ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))))) | ||
Theorem | cphipval 23848* | Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴 + ((i↑𝑘) · 𝐵)))↑2)) / 4)) | ||
Theorem | ipcnlem2 23849 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝐴𝐷𝑋) < 𝑈) & ⊢ (𝜑 → (𝐵𝐷𝑌) < 𝑇) ⇒ ⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝑋 , 𝑌))) < 𝑅) | ||
Theorem | ipcnlem1 23850* | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) | ||
Theorem | ipcn 23851 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ , = (·if‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑊 ∈ ℂPreHil → , ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
Theorem | cnmpt1ip 23852* | Continuity of inner product; analogue of cnmpt12f 22276 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐶 = (TopOpen‘ℂfld) & ⊢ , = (·𝑖‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 , 𝐵)) ∈ (𝐾 Cn 𝐶)) | ||
Theorem | cnmpt2ip 23853* | Continuity of inner product; analogue of cnmpt22f 22285 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐶 = (TopOpen‘ℂfld) & ⊢ , = (·𝑖‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 , 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐶)) | ||
Theorem | csscld 23854 | A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (ClSubSp‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | clsocv 23855 | The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑂 = (ocv‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆)) | ||
Theorem | cphsscph 23856 | A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 25-Sep-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂPreHil) | ||
Syntax | ccfil 23857 | Extend class notation with the class of Cauchy filters. |
class CauFil | ||
Syntax | ccau 23858 | Extend class notation with the class of Cauchy sequences. |
class Cau | ||
Syntax | ccmet 23859 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 23860* | Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < 𝑥 there is an element of the filter whose metric diameter is less than 𝑥. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) | ||
Definition | df-cau 23861* | Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006.) |
⊢ Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}) | ||
Definition | df-cmet 23862* | Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.) |
⊢ CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) | ||
Theorem | lmmbr 23863* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21839. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) | ||
Theorem | lmmbr2 23864* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21839. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥)))) | ||
Theorem | lmmbr3 23865* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥)))) | ||
Theorem | lmmcvg 23866* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | lmmbrf 23867* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 23864 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥))) | ||
Theorem | lmnn 23868* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) | ||
Theorem | cfilfval 23869* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) | ||
Theorem | iscfil 23870* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | iscfil2 23871* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))) | ||
Theorem | cfilfil 23872 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | cfili 23873* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅) | ||
Theorem | cfil3i 23874* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹) | ||
Theorem | cfilss 23875 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷)) | ||
Theorem | fgcfil 23876* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) | ||
Theorem | fmcfil 23877* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥)) | ||
Theorem | iscfil3 23878* | A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑟) ∈ 𝐹))) | ||
Theorem | cfilfcls 23879 | Similar to ultrafilters (uffclsflim 22641), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑋 = dom dom 𝐷 ⇒ ⊢ (𝐹 ∈ (CauFil‘𝐷) → (𝐽 fClus 𝐹) = (𝐽 fLim 𝐹)) | ||
Theorem | caufval 23880* | The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑥)}) | ||
Theorem | iscau 23881* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷". Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21839. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥)))) | ||
Theorem | iscau2 23882* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) | ||
Theorem | iscau3 23883* | Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)))) | ||
Theorem | iscau4 23884* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥)))) | ||
Theorem | iscauf 23885* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " presupposing 𝐹 is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥)) | ||
Theorem | caun0 23886 | A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝑋 ≠ ∅) | ||
Theorem | caufpm 23887 | Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋 ↑pm ℂ)) | ||
Theorem | caucfil 23888 | A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ≥ “ 𝑍)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷))) | ||
Theorem | iscmet 23889* | The property "𝐷 is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅)) | ||
Theorem | cmetcvg 23890 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅) | ||
Theorem | cmetmet 23891 | A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | cmetmeti 23892 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
⊢ 𝐷 ∈ (CMet‘𝑋) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
Theorem | cmetcaulem 23893* | Lemma for cmetcau 23894. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃)) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | cmetcau 23894 | The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | iscmet3lem3 23895* | Lemma for iscmet3 23898. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅) | ||
Theorem | iscmet3lem1 23896* | Lemma for iscmet3 23898. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
Theorem | iscmet3lem2 23897* | Lemma for iscmet3 23898. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) & ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝑆:ℤ⟶𝐺) & ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅) | ||
Theorem | iscmet3 23898* | The property "𝐷 is a complete metric" expressed in terms of functions on ℕ (or any other upper integer set). Thus, we only have to look at functions on ℕ, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)))) | ||
Theorem | iscmet2 23899 | A metric 𝐷 is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of [Kreyszig] p. 28. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘𝐽))) | ||
Theorem | cfilresi 23900 | A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝐹) ∈ (CauFil‘𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |