Theorem List for Intuitionistic Logic Explorer - 13201-13300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mopnval 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‘𝐷))) |
|
Theorem | mopntopon 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‘𝑋)) |
|
Theorem | mopntop 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) |
|
Theorem | mopnuni 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‘𝑋) → 𝑋 = ∪ 𝐽) |
|
Theorem | elmopn 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‘𝐷)(𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) |
|
Theorem | mopnfss 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‘𝑋) → 𝐽 ⊆ 𝒫 𝑋) |
|
Theorem | mopnm 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‘𝑋) → 𝑋 ∈ 𝐽) |
|
Theorem | elmopn2 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‘𝐷)𝑦) ⊆ 𝐴))) |
|
Theorem | mopnss 13209 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
Theorem | isxms 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‘𝐷))) |
|
Theorem | isxms2 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‘𝐷))) |
|
Theorem | isms 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‘𝑋))) |
|
Theorem | isms2 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‘𝐷))) |
|
Theorem | xmstopn 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‘𝐷)) |
|
Theorem | mstopn 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‘𝐷)) |
|
Theorem | xmstps 13216 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) |
|
Theorem | msxms 13217 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) |
|
Theorem | mstps 13218 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) |
|
Theorem | xmsxmet 13219 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Sep-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | msmet 13220 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | msf 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 → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
|
Theorem | xmsxmet2 13222 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) |
|
Theorem | msmet2 13223 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
|
Theorem | mscl 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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ) |
|
Theorem | xmscl 13225 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | xmsge0 13226 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmseq0 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 ↔ 𝐴 = 𝐵)) |
|
Theorem | xmssym 13228 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmstri2 13229 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mstri2 13230 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri 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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mstri 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 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri3 13233 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mstri3 13234 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | msrtri 13235 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmspropd 13236 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
|
Theorem | mspropd 13237 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
|
Theorem | setsmsbasg 13238 |
The base set of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋 = (Base‘𝐾)) |
|
Theorem | setsmsdsg 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‘𝐾)) |
|
Theorem | setsmstsetg 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‘𝐾)) |
|
Theorem | mopni 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‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
|
Theorem | mopni2 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‘𝐷)𝑥) ⊆ 𝐴) |
|
Theorem | mopni3 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‘𝐷)𝑥) ⊆ 𝐴)) |
|
Theorem | blssopn 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‘𝐷) ⊆ 𝐽) |
|
Theorem | unimopn 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‘𝑋) ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) |
|
Theorem | mopnin 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‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) |
|
Theorem | mopn0 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‘𝑋) → ∅ ∈ 𝐽) |
|
Theorem | rnblopn 13248 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) |
|
Theorem | blopn 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‘𝐷)𝑅) ∈ 𝐽) |
|
Theorem | neibl 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‘𝐷)𝑟) ⊆ 𝑁))) |
|
Theorem | blnei 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‘𝐽)‘{𝑃})) |
|
Theorem | blsscls2 13252* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
⊢ 𝐽 = (MetOpen‘𝐷)
& ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ*
∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) |
|
Theorem | metss 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‘𝐶)𝑟))) |
|
Theorem | metequiv 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‘𝐷)𝑎)))) |
|
Theorem | metequiv2 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‘𝐷)𝑠)) → 𝐽 = 𝐾)) |
|
Theorem | metss2lem 13256* |
Lemma for metss2 13257. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |
|
Theorem | metss2 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‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐽 ⊆ 𝐾) |
|
Theorem | comet 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‘𝑋)) |
|
Theorem | bdmetval 13259* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶:(𝑋 × 𝑋)⟶ℝ* ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = inf({(𝐴𝐶𝐵), 𝑅}, ℝ*, <
)) |
|
Theorem | bdxmet 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‘𝑋)) |
|
Theorem | bdmet 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‘𝑋)) |
|
Theorem | bdbl 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‘𝐶)𝑆)) |
|
Theorem | bdmopn 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‘𝐷)) |
|
Theorem | mopnex 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‘𝑑)) |
|
Theorem | metrest 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 𝑌) = 𝐾) |
|
Theorem | xmetxp 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‘(𝑋 × 𝑌))) |
|
Theorem | xmetxpbl 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‘𝑁)𝑅))) |
|
Theorem | xmettxlem 13268* |
Lemma for xmettx 13269. (Contributed by Jim Kingdon, 15-Oct-2023.)
|
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st
‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, <
))
& ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ 𝐿 = (MetOpen‘𝑃)
⇒ ⊢ (𝜑 → 𝐿 ⊆ (𝐽 ×t 𝐾)) |
|
Theorem | xmettx 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
|
|
Theorem | metcnp3 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‘𝐷)𝑦)))) |
|
Theorem | metcnp 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 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
Theorem | metcnp2 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 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹‘𝑤)𝐷(𝐹‘𝑃)) < 𝑦)))) |
|
Theorem | metcn 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 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹‘𝑥)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
Theorem | metcnpi 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 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) |
|
Theorem | metcnpi2 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 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) |
|
Theorem | metcnpi3 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 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) |
|
Theorem | txmetcnp 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 𝐿)‘〈𝐴, 𝐵〉) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝐴𝐶𝑢) < 𝑤 ∧ (𝐵𝐷𝑣) < 𝑤) → ((𝐴𝐹𝐵)𝐸(𝑢𝐹𝑣)) < 𝑧)))) |
|
Theorem | txmetcn 13278* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ 𝐿 = (MetOpen‘𝐸) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) → (𝐹 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑥𝐶𝑢) < 𝑤 ∧ (𝑦𝐷𝑣) < 𝑤) → ((𝑥𝐹𝑦)𝐸(𝑢𝐹𝑣)) < 𝑧)))) |
|
Theorem | metcnpd 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
|
|
Theorem | qtopbasss 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 |
|
Theorem | qtopbas 13281 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
⊢ ((,) “ (ℚ × ℚ))
∈ TopBases |
|
Theorem | retopbas 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 |
|
Theorem | retop 13283 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
⊢ (topGen‘ran (,)) ∈
Top |
|
Theorem | uniretop 13284 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
⊢ ℝ = ∪
(topGen‘ran (,)) |
|
Theorem | retopon 13285 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
⊢ (topGen‘ran (,)) ∈
(TopOn‘ℝ) |
|
Theorem | retps 13286 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉,
〈(TopSet‘ndx), (topGen‘ran
(,))〉} ⇒ ⊢ 𝐾 ∈ TopSp |
|
Theorem | iooretopg 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
(,))) |
|
Theorem | cnmetdval 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‘(𝐴 − 𝐵))) |
|
Theorem | cnmet 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‘ℂ) |
|
Theorem | cnxmet 13290 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (abs ∘ − ) ∈
(∞Met‘ℂ) |
|
Theorem | cntoptopon 13291 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈
(TopOn‘ℂ) |
|
Theorem | cntoptop 13292 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈ Top |
|
Theorem | cnbl0 13293 |
Two ways to write the open ball centered at zero. (Contributed by Mario
Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) |
|
Theorem | cnblcld 13294* |
Two ways to write the closed ball centered at zero. (Contributed by
Mario Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) |
|
Theorem | unicntopcntop 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 ∘ − )) |
|
Theorem | cnopncntop 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 ∘
− )) |
|
Theorem | reopnap 13297* |
The real numbers apart from a given real number form an open set.
(Contributed by Jim Kingdon, 13-Dec-2023.)
|
⊢ (𝐴 ∈ ℝ → {𝑤 ∈ ℝ ∣ 𝑤 # 𝐴} ∈ (topGen‘ran
(,))) |
|
Theorem | remetdval 13298 |
Value of the distance function of the metric space of real numbers.
(Contributed by NM, 16-May-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) |
|
Theorem | remet 13299 |
The absolute value metric determines a metric space on the reals.
(Contributed by NM, 10-Feb-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(Met‘ℝ) |
|
Theorem | rexmet 13300 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(∞Met‘ℝ) |