Home | Metamath
Proof Explorer Theorem List (p. 237 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nmoleub 23601* | The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of 𝐹(𝑥) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐿 = (norm‘𝑆) & ⊢ 𝑀 = (norm‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ (𝜑 → 𝑆 ∈ NrmGrp) & ⊢ (𝜑 → 𝑇 ∈ NrmGrp) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((𝑁‘𝐹) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑉 (𝑥 ≠ 0 → ((𝑀‘(𝐹‘𝑥)) / (𝐿‘𝑥)) ≤ 𝐴))) | ||
Theorem | nghmrcl1 23602 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑆 ∈ NrmGrp) | ||
Theorem | nghmrcl2 23603 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝑇 ∈ NrmGrp) | ||
Theorem | nghmghm 23604 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | nmo0 23605 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑁‘(𝑉 × { 0 })) = 0) | ||
Theorem | nmoeq0 23606 | The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) = 0 ↔ 𝐹 = (𝑉 × { 0 }))) | ||
Theorem | nmoco 23607 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑈) & ⊢ 𝐿 = (𝑇 normOp 𝑈) & ⊢ 𝑀 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘ 𝐺)) ≤ ((𝐿‘𝐹) · (𝑀‘𝐺))) | ||
Theorem | nghmco 23608 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NGHom 𝑈) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NGHom 𝑈)) | ||
Theorem | nmotri 23609 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝑁‘(𝐹 ∘f + 𝐺)) ≤ ((𝑁‘𝐹) + (𝑁‘𝐺))) | ||
Theorem | nghmplusg 23610 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝑇 ∈ Abel ∧ 𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐺 ∈ (𝑆 NGHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | 0nghm 23611 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) → (𝑉 × { 0 }) ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmoid 23612 | The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑆) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) ⇒ ⊢ ((𝑆 ∈ NrmGrp ∧ { 0 } ⊊ 𝑉) → (𝑁‘( I ↾ 𝑉)) = 1) | ||
Theorem | idnghm 23613 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmGrp → ( I ↾ 𝑉) ∈ (𝑆 NGHom 𝑆)) | ||
Theorem | nmods 23614 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) & ⊢ 𝑉 = (Base‘𝑆) & ⊢ 𝐶 = (dist‘𝑆) & ⊢ 𝐷 = (dist‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐹‘𝐴)𝐷(𝐹‘𝐵)) ≤ ((𝑁‘𝐹) · (𝐴𝐶𝐵))) | ||
Theorem | nghmcn 23615 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐾 = (TopOpen‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | isnmhm 23616 | A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod) ∧ (𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐹 ∈ (𝑆 NGHom 𝑇)))) | ||
Theorem | nmhmrcl1 23617 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑆 ∈ NrmMod) | ||
Theorem | nmhmrcl2 23618 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝑇 ∈ NrmMod) | ||
Theorem | nmhmlmhm 23619 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 LMHom 𝑇)) | ||
Theorem | nmhmnghm 23620 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 NGHom 𝑇)) | ||
Theorem | nmhmghm 23621 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | isnmhm2 23622 | A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ)) | ||
Theorem | nmhmcl 23623 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
Theorem | idnmhm 23624 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆)) | ||
Theorem | 0nmhm 23625 | The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐹 = (Scalar‘𝑆) & ⊢ 𝐺 = (Scalar‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇)) | ||
Theorem | nmhmco 23626 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈)) | ||
Theorem | nmhmplusg 23627 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇)) | ||
Theorem | qtopbaslem 23628 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ 𝑆 ⊆ ℝ* ⇒ ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases | ||
Theorem | qtopbas 23629 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases | ||
Theorem | retopbas 23630 | A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.) |
⊢ ran (,) ∈ TopBases | ||
Theorem | retop 23631 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ (topGen‘ran (,)) ∈ Top | ||
Theorem | uniretop 23632 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
⊢ ℝ = ∪ (topGen‘ran (,)) | ||
Theorem | retopon 23633 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ) | ||
Theorem | retps 23634 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉, 〈(TopSet‘ndx), (topGen‘ran (,))〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | iooretop 23635 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
Theorem | icccld 23636 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | icopnfcld 23637 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | iocmnfcld 23638 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
Theorem | qdensere 23639 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
Theorem | cnmetdval 23640 | Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
Theorem | cnmet 23641 | The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.) |
⊢ (abs ∘ − ) ∈ (Met‘ℂ) | ||
Theorem | cnxmet 23642 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | ||
Theorem | cnbl0 23643 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) | ||
Theorem | cnblcld 23644* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) | ||
Theorem | cnfldms 23645 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ MetSp | ||
Theorem | cnfldxms 23646 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ ∞MetSp | ||
Theorem | cnfldtps 23647 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ ℂfld ∈ TopSp | ||
Theorem | cnfldnm 23648 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ abs = (norm‘ℂfld) | ||
Theorem | cnngp 23649 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ ℂfld ∈ NrmGrp | ||
Theorem | cnnrg 23650 | The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ ℂfld ∈ NrmRing | ||
Theorem | cnfldtopn 23651 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 = (MetOpen‘(abs ∘ − )) | ||
Theorem | cnfldtopon 23652 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ (TopOn‘ℂ) | ||
Theorem | cnfldtop 23653 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Top | ||
Theorem | cnfldhaus 23654 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Haus | ||
Theorem | unicntop 23655 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℂ = ∪ (TopOpen‘ℂfld) | ||
Theorem | cnopn 23656 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ℂ ∈ (TopOpen‘ℂfld) | ||
Theorem | zringnrg 23657 | The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.) |
⊢ ℤring ∈ NrmRing | ||
Theorem | remetdval 23658 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
Theorem | remet 23659 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (Met‘ℝ) | ||
Theorem | rexmet 23660 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ) | ||
Theorem | bl2ioo 23661 | A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(ball‘𝐷)𝐵) = ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) | ||
Theorem | ioo2bl 23662 | An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) = (((𝐴 + 𝐵) / 2)(ball‘𝐷)((𝐵 − 𝐴) / 2))) | ||
Theorem | ioo2blex 23663 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) | ||
Theorem | blssioo 23664 | The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ran (ball‘𝐷) ⊆ ran (,) | ||
Theorem | tgioo 23665 | The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
Theorem | qdensere2 23666 | ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((cls‘𝐽)‘ℚ) = ℝ | ||
Theorem | blcvx 23667 | An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅) ⇒ ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆) | ||
Theorem | rehaus 23668 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
⊢ (topGen‘ran (,)) ∈ Haus | ||
Theorem | tgqioo 23669 | The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
⊢ 𝑄 = (topGen‘((,) “ (ℚ × ℚ))) ⇒ ⊢ (topGen‘ran (,)) = 𝑄 | ||
Theorem | re2ndc 23670 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ 2ndω | ||
Theorem | resubmet 23671 | The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.) |
⊢ 𝑅 = (topGen‘ran (,)) & ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐽 = (𝑅 ↾t 𝐴)) | ||
Theorem | tgioo2 23672 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (topGen‘ran (,)) = (𝐽 ↾t ℝ) | ||
Theorem | rerest 23673 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
Theorem | tgioo3 23674 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.) |
⊢ 𝐽 = (TopOpen‘ℝfld) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
Theorem | xrtgioo 23675 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to ℝ. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t ℝ) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
Theorem | xrrest 23676 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = (ordTop‘ ≤ ) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
Theorem | xrrest2 23677 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑋 = (ordTop‘ ≤ ) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴)) | ||
Theorem | xrsxmet 23678 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ*) | ||
Theorem | xrsdsre 23679 | The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ)) | ||
Theorem | xrsblre 23680 | Any ball of the metric of the extended reals centered on an element of ℝ is entirely contained in ℝ. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ ℝ) | ||
Theorem | xrsmopn 23681 | The metric on the extended reals generates a topology, but this does not match the order topology on ℝ*; for example {+∞} is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (ordTop‘ ≤ ) ⊆ 𝐽 | ||
Theorem | zcld 23682 | The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
Theorem | recld2 23683 | The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℝ ∈ (Clsd‘𝐽) | ||
Theorem | zcld2 23684 | The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
Theorem | zdis 23685 | The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ | ||
Theorem | sszcld 23686 | Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | reperflem 23687* | A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆) & ⊢ 𝑆 ⊆ ℂ ⇒ ⊢ (𝐽 ↾t 𝑆) ∈ Perf | ||
Theorem | reperf 23688 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℝ) ∈ Perf | ||
Theorem | cnperf 23689 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Perf | ||
Theorem | iccntr 23690 | The interior of a closed interval in the standard topology on ℝ is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | ||
Theorem | icccmplem1 23691* | Lemma for icccmp 23694. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) | ||
Theorem | icccmplem2 23692* | Lemma for icccmp 23694. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) & ⊢ 𝐺 = sup(𝑆, ℝ, < ) & ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
Theorem | icccmplem3 23693* | Lemma for icccmp 23694. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
Theorem | icccmp 23694 | A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) | ||
Theorem | reconnlem1 23695 | Lemma for reconn 23697. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴) | ||
Theorem | reconnlem2 23696* | Lemma for reconn 23697. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) | ||
Theorem | reconn 23697* | A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝐴 ⊆ ℝ → (((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) | ||
Theorem | retopconn 23698 | Corollary of reconn 23697. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
⊢ (topGen‘ran (,)) ∈ Conn | ||
Theorem | iccconn 23699 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn) | ||
Theorem | opnreen 23700 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |