HomeHome Intuitionistic Logic Explorer
Theorem List (p. 133 of 141)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmopnval 13201 An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of [Kreyszig] p. 18. The object (MetOpen‘𝐷) is the family of all open sets in the metric space determined by the metric 𝐷. By mopntop 13203, the open sets of a metric space form a topology 𝐽, whose base set is 𝐽 by mopnuni 13204. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷)))
 
Theoremmopntopon 13202 The set of open sets of a metric space 𝑋 is a topology on 𝑋. Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
 
Theoremmopntop 13203 The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
 
Theoremmopnuni 13204 The union of all open sets in a metric space is its underlying set. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
 
Theoremelmopn 13205* The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → (𝐴𝐽 ↔ (𝐴𝑋 ∧ ∀𝑥𝐴𝑦 ∈ ran (ball‘𝐷)(𝑥𝑦𝑦𝐴))))
 
Theoremmopnfss 13206 The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ⊆ 𝒫 𝑋)
 
Theoremmopnm 13207 The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → 𝑋𝐽)
 
Theoremelmopn2 13208* A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → (𝐴𝐽 ↔ (𝐴𝑋 ∧ ∀𝑥𝐴𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝐴)))
 
Theoremmopnss 13209 An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽) → 𝐴𝑋)
 
Theoremisxms 13210 Express the predicate "𝑋, 𝐷 is an extended metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by Mario Carneiro, 2-Sep-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ ∞MetSp ↔ (𝐾 ∈ TopSp ∧ 𝐽 = (MetOpen‘𝐷)))
 
Theoremisxms2 13211 Express the predicate "𝑋, 𝐷 is an extended metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by Mario Carneiro, 2-Sep-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ ∞MetSp ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐽 = (MetOpen‘𝐷)))
 
Theoremisms 13212 Express the predicate "𝑋, 𝐷 is a metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ MetSp ↔ (𝐾 ∈ ∞MetSp ∧ 𝐷 ∈ (Met‘𝑋)))
 
Theoremisms2 13213 Express the predicate "𝑋, 𝐷 is a metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ MetSp ↔ (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 = (MetOpen‘𝐷)))
 
Theoremxmstopn 13214 The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
 
Theoremmstopn 13215 The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
𝐽 = (TopOpen‘𝐾)    &   𝑋 = (Base‘𝐾)    &   𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋))       (𝐾 ∈ MetSp → 𝐽 = (MetOpen‘𝐷))
 
Theoremxmstps 13216 An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
(𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp)
 
Theoremmsxms 13217 A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)
(𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)
 
Theoremmstps 13218 A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
(𝑀 ∈ MetSp → 𝑀 ∈ TopSp)
 
Theoremxmsxmet 13219 The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Sep-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))       (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
 
Theoremmsmet 13220 The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 12-Nov-2013.)
𝑋 = (Base‘𝑀)    &   𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))       (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
 
Theoremmsf 13221 The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝑋 = (Base‘𝑀)    &   𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))       (𝑀 ∈ MetSp → 𝐷:(𝑋 × 𝑋)⟶ℝ)
 
Theoremxmsxmet2 13222 The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋))
 
Theoremmsmet2 13223 The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋))
 
Theoremmscl 13224 Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ MetSp ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
 
Theoremxmscl 13225 Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
 
Theoremxmsge0 13226 The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ 𝐴𝑋𝐵𝑋) → 0 ≤ (𝐴𝐷𝐵))
 
Theoremxmseq0 13227 The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ 𝐴𝑋𝐵𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
 
Theoremxmssym 13228 The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
 
Theoremxmstri2 13229 Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ (𝐶𝑋𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
 
Theoremmstri2 13230 Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ MetSp ∧ (𝐶𝑋𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵)))
 
Theoremxmstri 13231 Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵)))
 
Theoremmstri 13232 Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ MetSp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵)))
 
Theoremxmstri3 13233 Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ ∞MetSp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
 
Theoremmstri3 13234 Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ MetSp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
 
Theoremmsrtri 13235 Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
𝑋 = (Base‘𝑀)    &   𝐷 = (dist‘𝑀)       ((𝑀 ∈ MetSp ∧ (𝐴𝑋𝐵𝑋𝐶𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
 
Theoremxmspropd 13236 Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
(𝜑𝐵 = (Base‘𝐾))    &   (𝜑𝐵 = (Base‘𝐿))    &   (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))       (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp))
 
Theoremmspropd 13237 Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
(𝜑𝐵 = (Base‘𝐾))    &   (𝜑𝐵 = (Base‘𝐿))    &   (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))       (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp))
 
Theoremsetsmsbasg 13238 The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
(𝜑𝑋 = (Base‘𝑀))    &   (𝜑𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   (𝜑𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   (𝜑𝑀𝑉)    &   (𝜑 → (MetOpen‘𝐷) ∈ 𝑊)       (𝜑𝑋 = (Base‘𝐾))
 
Theoremsetsmsdsg 13239 The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
(𝜑𝑋 = (Base‘𝑀))    &   (𝜑𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   (𝜑𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   (𝜑𝑀𝑉)    &   (𝜑 → (MetOpen‘𝐷) ∈ 𝑊)       (𝜑 → (dist‘𝑀) = (dist‘𝐾))
 
Theoremsetsmstsetg 13240 The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
(𝜑𝑋 = (Base‘𝑀))    &   (𝜑𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   (𝜑𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   (𝜑𝑀𝑉)    &   (𝜑 → (MetOpen‘𝐷) ∈ 𝑊)       (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾))
 
Theoremmopni 13241* An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽𝑃𝐴) → ∃𝑥 ∈ ran (ball‘𝐷)(𝑃𝑥𝑥𝐴))
 
Theoremmopni2 13242* An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽𝑃𝐴) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴)
 
Theoremmopni3 13243* An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽𝑃𝐴) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ (𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴))
 
Theoremblssopn 13244 The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ⊆ 𝐽)
 
Theoremunimopn 13245 The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽) → 𝐴𝐽)
 
Theoremmopnin 13246 The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽)
 
Theoremmopn0 13247 The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → ∅ ∈ 𝐽)
 
Theoremrnblopn 13248 A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵𝐽)
 
Theoremblopn 13249 A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝐽)
 
Theoremneibl 13250* The neighborhoods around a point 𝑃 of a metric space are those subsets containing a ball around 𝑃. Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁𝑋 ∧ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝑁)))
 
Theoremblnei 13251 A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
𝐽 = (MetOpen‘𝐷)       ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃}))
 
Theoremblsscls2 13252* A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)
𝐽 = (MetOpen‘𝐷)    &   𝑆 = {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}       (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋) ∧ (𝑅 ∈ ℝ*𝑇 ∈ ℝ*𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇))
 
Theoremmetss 13253* Two ways of saying that metric 𝐷 generates a finer topology than metric 𝐶. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽𝐾 ↔ ∀𝑥𝑋𝑟 ∈ ℝ+𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
 
Theoremmetequiv 13254* Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 = 𝐾 ↔ ∀𝑥𝑋 (∀𝑟 ∈ ℝ+𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑎 ∈ ℝ+𝑏 ∈ ℝ+ (𝑥(ball‘𝐶)𝑏) ⊆ (𝑥(ball‘𝐷)𝑎))))
 
Theoremmetequiv2 13255* If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥𝑋𝑟 ∈ ℝ+𝑠 ∈ ℝ+ (𝑠𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → 𝐽 = 𝐾))
 
Theoremmetss2lem 13256* Lemma for metss2 13257. (Contributed by Mario Carneiro, 14-Sep-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)    &   (𝜑𝐶 ∈ (Met‘𝑋))    &   (𝜑𝐷 ∈ (Met‘𝑋))    &   (𝜑𝑅 ∈ ℝ+)    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))       ((𝜑 ∧ (𝑥𝑋𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆))
 
Theoremmetss2 13257* If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), then 𝐷 generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)    &   (𝜑𝐶 ∈ (Met‘𝑋))    &   (𝜑𝐷 ∈ (Met‘𝑋))    &   (𝜑𝑅 ∈ ℝ+)    &   ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))       (𝜑𝐽𝐾)
 
Theoremcomet 13258* The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
(𝜑𝐷 ∈ (∞Met‘𝑋))    &   (𝜑𝐹:(0[,]+∞)⟶ℝ*)    &   ((𝜑𝑥 ∈ (0[,]+∞)) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0))    &   ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))    &   ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)))       (𝜑 → (𝐹𝐷) ∈ (∞Met‘𝑋))
 
Theorembdmetval 13259* Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < ))       (((𝐶:(𝑋 × 𝑋)⟶ℝ*𝑅 ∈ ℝ*) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) = inf({(𝐴𝐶𝐵), 𝑅}, ℝ*, < ))
 
Theorembdxmet 13260* The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < ))       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))
 
Theorembdmet 13261* The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < ))       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋))
 
Theorembdbl 13262* The standard bounded metric corresponding to 𝐶 generates the same balls as 𝐶 for radii less than 𝑅. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < ))       (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑃𝑋𝑆 ∈ ℝ*𝑆𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆))
 
Theorembdmopn 13263* The standard bounded metric corresponding to 𝐶 generates the same topology as 𝐶. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
𝐷 = (𝑥𝑋, 𝑦𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < ))    &   𝐽 = (MetOpen‘𝐶)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷))
 
Theoremmopnex 13264* The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)
𝐽 = (MetOpen‘𝐷)       (𝐷 ∈ (∞Met‘𝑋) → ∃𝑑 ∈ (Met‘𝑋)𝐽 = (MetOpen‘𝑑))
 
Theoremmetrest 13265 Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
𝐷 = (𝐶 ↾ (𝑌 × 𝑌))    &   𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = 𝐾)
 
Theoremxmetxp 13266* The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)
𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st𝑢)𝑀(1st𝑣)), ((2nd𝑢)𝑁(2nd𝑣))}, ℝ*, < ))    &   (𝜑𝑀 ∈ (∞Met‘𝑋))    &   (𝜑𝑁 ∈ (∞Met‘𝑌))       (𝜑𝑃 ∈ (∞Met‘(𝑋 × 𝑌)))
 
Theoremxmetxpbl 13267* The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point 𝐶 with radius 𝑅. (Contributed by Jim Kingdon, 22-Oct-2023.)
𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st𝑢)𝑀(1st𝑣)), ((2nd𝑢)𝑁(2nd𝑣))}, ℝ*, < ))    &   (𝜑𝑀 ∈ (∞Met‘𝑋))    &   (𝜑𝑁 ∈ (∞Met‘𝑌))    &   (𝜑𝑅 ∈ ℝ*)    &   (𝜑𝐶 ∈ (𝑋 × 𝑌))       (𝜑 → (𝐶(ball‘𝑃)𝑅) = (((1st𝐶)(ball‘𝑀)𝑅) × ((2nd𝐶)(ball‘𝑁)𝑅)))
 
Theoremxmettxlem 13268* Lemma for xmettx 13269. (Contributed by Jim Kingdon, 15-Oct-2023.)
𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st𝑢)𝑀(1st𝑣)), ((2nd𝑢)𝑁(2nd𝑣))}, ℝ*, < ))    &   (𝜑𝑀 ∈ (∞Met‘𝑋))    &   (𝜑𝑁 ∈ (∞Met‘𝑌))    &   𝐽 = (MetOpen‘𝑀)    &   𝐾 = (MetOpen‘𝑁)    &   𝐿 = (MetOpen‘𝑃)       (𝜑𝐿 ⊆ (𝐽 ×t 𝐾))
 
Theoremxmettx 13269* The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)
𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st𝑢)𝑀(1st𝑣)), ((2nd𝑢)𝑁(2nd𝑣))}, ℝ*, < ))    &   (𝜑𝑀 ∈ (∞Met‘𝑋))    &   (𝜑𝑁 ∈ (∞Met‘𝑌))    &   𝐽 = (MetOpen‘𝑀)    &   𝐾 = (MetOpen‘𝑁)    &   𝐿 = (MetOpen‘𝑃)       (𝜑𝐿 = (𝐽 ×t 𝐾))
 
8.2.5  Continuity in metric spaces
 
Theoremmetcnp3 13270* Two ways to express that 𝐹 is continuous at 𝑃 for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+ (𝐹 “ (𝑃(ball‘𝐶)𝑧)) ⊆ ((𝐹𝑃)(ball‘𝐷)𝑦))))
 
Theoremmetcnp 13271* Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹𝑃)𝐷(𝐹𝑤)) < 𝑦))))
 
Theoremmetcnp2 13272* Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 13271 (and Munkres' metcn 13273) for compatibility with df-lm 12949. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹𝑤)𝐷(𝐹𝑃)) < 𝑦))))
 
Theoremmetcn 13273* Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" 𝑦 there is a positive "delta" 𝑧 such that a distance less than delta in 𝐶 maps to a distance less than epsilon in 𝐷. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹𝑥)𝐷(𝐹𝑤)) < 𝑦))))
 
Theoremmetcnpi 13274* Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 13271. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+𝑦𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹𝑃)𝐷(𝐹𝑦)) < 𝐴))
 
Theoremmetcnpi2 13275* Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 13272. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+𝑦𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹𝑦)𝐷(𝐹𝑃)) < 𝐴))
 
Theoremmetcnpi3 13276* Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 13275 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)       (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+𝑦𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹𝑦)𝐷(𝐹𝑃)) ≤ 𝐴))
 
Theoremtxmetcnp 13277* Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)    &   𝐿 = (MetOpen‘𝐸)       (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) ∧ (𝐴𝑋𝐵𝑌)) → (𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘⟨𝐴, 𝐵⟩) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑧 ∈ ℝ+𝑤 ∈ ℝ+𝑢𝑋𝑣𝑌 (((𝐴𝐶𝑢) < 𝑤 ∧ (𝐵𝐷𝑣) < 𝑤) → ((𝐴𝐹𝐵)𝐸(𝑢𝐹𝑣)) < 𝑧))))
 
Theoremtxmetcn 13278* Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
𝐽 = (MetOpen‘𝐶)    &   𝐾 = (MetOpen‘𝐷)    &   𝐿 = (MetOpen‘𝐸)       ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) → (𝐹 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑥𝑋𝑦𝑌𝑧 ∈ ℝ+𝑤 ∈ ℝ+𝑢𝑋𝑣𝑌 (((𝑥𝐶𝑢) < 𝑤 ∧ (𝑦𝐷𝑣) < 𝑤) → ((𝑥𝐹𝑦)𝐸(𝑢𝐹𝑣)) < 𝑧))))
 
Theoremmetcnpd 13279* Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. (Contributed by Jim Kingdon, 14-Jun-2023.)
(𝜑𝐽 = (MetOpen‘𝐶))    &   (𝜑𝐾 = (MetOpen‘𝐷))    &   (𝜑𝐶 ∈ (∞Met‘𝑋))    &   (𝜑𝐷 ∈ (∞Met‘𝑌))    &   (𝜑𝑃𝑋)       (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹𝑃)𝐷(𝐹𝑤)) < 𝑦))))
 
8.2.6  Topology on the reals
 
Theoremqtopbasss 13280* The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.)
𝑆 ⊆ ℝ*    &   ((𝑥𝑆𝑦𝑆) → sup({𝑥, 𝑦}, ℝ*, < ) ∈ 𝑆)    &   ((𝑥𝑆𝑦𝑆) → inf({𝑥, 𝑦}, ℝ*, < ) ∈ 𝑆)       ((,) “ (𝑆 × 𝑆)) ∈ TopBases
 
Theoremqtopbas 13281 The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)
((,) “ (ℚ × ℚ)) ∈ TopBases
 
Theoremretopbas 13282 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
 
Theoremretop 13283 The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
(topGen‘ran (,)) ∈ Top
 
Theoremuniretop 13284 The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
ℝ = (topGen‘ran (,))
 
Theoremretopon 13285 The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
(topGen‘ran (,)) ∈ (TopOn‘ℝ)
 
Theoremretps 13286 The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩}       𝐾 ∈ TopSp
 
Theoremiooretopg 13287 Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴(,)𝐵) ∈ (topGen‘ran (,)))
 
Theoremcnmetdval 13288 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‘(𝐴𝐵)))
 
Theoremcnmet 13289 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‘ℂ)
 
Theoremcnxmet 13290 The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
(abs ∘ − ) ∈ (∞Met‘ℂ)
 
Theoremcntoptopon 13291 The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
𝐽 = (MetOpen‘(abs ∘ − ))       𝐽 ∈ (TopOn‘ℂ)
 
Theoremcntoptop 13292 The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
𝐽 = (MetOpen‘(abs ∘ − ))       𝐽 ∈ Top
 
Theoremcnbl0 13293 Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
𝐷 = (abs ∘ − )       (𝑅 ∈ ℝ* → (abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅))
 
Theoremcnblcld 13294* Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)
𝐷 = (abs ∘ − )       (𝑅 ∈ ℝ* → (abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅})
 
Theoremunicntopcntop 13295 The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
ℂ = (MetOpen‘(abs ∘ − ))
 
Theoremcnopncntop 13296 The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)
ℂ ∈ (MetOpen‘(abs ∘ − ))
 
Theoremreopnap 13297* The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
(𝐴 ∈ ℝ → {𝑤 ∈ ℝ ∣ 𝑤 # 𝐴} ∈ (topGen‘ran (,)))
 
Theoremremetdval 13298 Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)
𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))       ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴𝐵)))
 
Theoremremet 13299 The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)
𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))       𝐷 ∈ (Met‘ℝ)
 
Theoremrexmet 13300 The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))       𝐷 ∈ (∞Met‘ℝ)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14078
  Copyright terms: Public domain < Previous  Next >