Theorem List for Intuitionistic Logic Explorer - 13001-13100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | blres 13001 |
A ball in a restricted metric space. (Contributed by Mario Carneiro,
5-Jan-2014.)
|
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) |
|
Theorem | xmeterval 13002 |
Value of the "finitely separated" relation. (Contributed by Mario
Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) |
|
Theorem | xmeter 13003 |
The "finitely separated" relation is an equivalence relation.
(Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) |
|
Theorem | xmetec 13004 |
The equivalence classes under the finite separation equivalence relation
are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → [𝑃] ∼ = (𝑃(ball‘𝐷)+∞)) |
|
Theorem | blssec 13005 |
A ball centered at 𝑃 is contained in the set of points
finitely
separated from 𝑃. This is just an application of ssbl 12993
to the
infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ ) |
|
Theorem | blpnfctr 13006 |
The infinity ball in an extended metric acts like an ultrametric ball in
that every point in the ball is also its center. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ (𝑃(ball‘𝐷)+∞)) → (𝑃(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)+∞)) |
|
Theorem | xmetresbl 13007 |
An extended metric restricted to any ball (in particular the infinity
ball) is a proper metric. Together with xmetec 13004, this shows that any
extended metric space can be "factored" into the disjoint
union of
proper metric spaces, with points in the same region measured by that
region's metric, and points in different regions being distance +∞
from each other. (Contributed by Mario Carneiro, 23-Aug-2015.)
|
⊢ 𝐵 = (𝑃(ball‘𝐷)𝑅) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)) ∈ (Met‘𝐵)) |
|
7.2.4 Open sets of a metric space
|
|
Theorem | mopnrel 13008 |
The class of open sets of a metric space is a relation. (Contributed by
Jim Kingdon, 5-May-2023.)
|
⊢ Rel MetOpen |
|
Theorem | mopnval 13009 |
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 13011, the open sets of a
metric space form a topology 𝐽, whose base set is ∪ 𝐽 by
mopnuni 13012. (Contributed by NM, 1-Sep-2006.) (Revised
by Mario
Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷))) |
|
Theorem | mopntopon 13010 |
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 13011 |
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 13012 |
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 13013* |
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 13014 |
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 13015 |
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 13016* |
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 13017 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
Theorem | isxms 13018 |
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 13019 |
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 13020 |
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 13021 |
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 13022 |
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 13023 |
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 13024 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) |
|
Theorem | msxms 13025 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) |
|
Theorem | mstps 13026 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) |
|
Theorem | xmsxmet 13027 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Sep-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | msmet 13028 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | msf 13029 |
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 13030 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) |
|
Theorem | msmet2 13031 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
|
Theorem | mscl 13032 |
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 13033 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | xmsge0 13034 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmseq0 13035 |
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 13036 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmstri2 13037 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mstri2 13038 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri 13039 |
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 13040 |
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 13041 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mstri3 13042 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | msrtri 13043 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmspropd 13044 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
|
Theorem | mspropd 13045 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
|
Theorem | setsmsbasg 13046 |
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 13047 |
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 13048 |
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 13049* |
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 13050* |
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 13051* |
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 13052 |
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 13053 |
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 13054 |
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 13055 |
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 13056 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) |
|
Theorem | blopn 13057 |
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 13058* |
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 13059 |
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 13060* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
⊢ 𝐽 = (MetOpen‘𝐷)
& ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ*
∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) |
|
Theorem | metss 13061* |
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 13062* |
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 13063* |
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 13064* |
Lemma for metss2 13065. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |
|
Theorem | metss2 13065* |
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 13066* |
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 13067* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶:(𝑋 × 𝑋)⟶ℝ* ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = inf({(𝐴𝐶𝐵), 𝑅}, ℝ*, <
)) |
|
Theorem | bdxmet 13068* |
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 13069* |
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 13070* |
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 13071* |
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 13072* |
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 13073 |
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 13074* |
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 13075* |
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 13076* |
Lemma for xmettx 13077. (Contributed by Jim Kingdon, 15-Oct-2023.)
|
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st
‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, <
))
& ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ 𝐿 = (MetOpen‘𝑃)
⇒ ⊢ (𝜑 → 𝐿 ⊆ (𝐽 ×t 𝐾)) |
|
Theorem | xmettx 13077* |
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 𝐾)) |
|
7.2.5 Continuity in metric spaces
|
|
Theorem | metcnp3 13078* |
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 13079* |
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 13080* |
Two ways to say a mapping from metric 𝐶 to metric 𝐷 is
continuous at point 𝑃. The distance arguments are swapped
compared
to metcnp 13079 (and Munkres' metcn 13081) for compatibility with df-lm 12757.
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 13081* |
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 13082* |
Epsilon-delta property of a continuous metric space function, with
function arguments as in metcnp 13079. (Contributed by NM, 17-Dec-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) |
|
Theorem | metcnpi2 13083* |
Epsilon-delta property of a continuous metric space function, with
swapped distance function arguments as in metcnp2 13080. (Contributed by
NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) |
|
Theorem | metcnpi3 13084* |
Epsilon-delta property of a metric space function continuous at 𝑃.
A variation of metcnpi2 13083 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) |
|
Theorem | txmetcnp 13085* |
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 13086* |
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 13087* |
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 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
7.2.6 Topology on the reals
|
|
Theorem | qtopbasss 13088* |
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 13089 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
⊢ ((,) “ (ℚ × ℚ))
∈ TopBases |
|
Theorem | retopbas 13090 |
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 13091 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
⊢ (topGen‘ran (,)) ∈
Top |
|
Theorem | uniretop 13092 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
⊢ ℝ = ∪
(topGen‘ran (,)) |
|
Theorem | retopon 13093 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
⊢ (topGen‘ran (,)) ∈
(TopOn‘ℝ) |
|
Theorem | retps 13094 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉,
〈(TopSet‘ndx), (topGen‘ran
(,))〉} ⇒ ⊢ 𝐾 ∈ TopSp |
|
Theorem | iooretopg 13095 |
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 13096 |
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 13097 |
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 13098 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (abs ∘ − ) ∈
(∞Met‘ℂ) |
|
Theorem | cntoptopon 13099 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈
(TopOn‘ℂ) |
|
Theorem | cntoptop 13100 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈ Top |