Theorem List for Intuitionistic Logic Explorer - 12601-12700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | elbl2 12601 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) |
|
Theorem | elbl3ps 12602 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) |
|
Theorem | elbl3 12603 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) |
|
Theorem | blcomps 12604 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) |
|
Theorem | blcom 12605 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) |
|
Theorem | xblpnfps 12606 |
The infinity ball in an extended metric is the set of all points that
are a finite distance from the center. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝐴 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) ∈ ℝ))) |
|
Theorem | xblpnf 12607 |
The infinity ball in an extended metric is the set of all points that
are a finite distance from the center. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝐴 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) ∈ ℝ))) |
|
Theorem | blpnf 12608 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋) |
|
Theorem | bldisj 12609 |
Two balls are disjoint if the center-to-center distance is more than the
sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*
∧ (𝑅
+𝑒 𝑆)
≤ (𝑃𝐷𝑄))) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆)) = ∅) |
|
Theorem | blgt0 12610 |
A nonempty ball implies that the radius is positive. (Contributed by
NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝐴 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 < 𝑅) |
|
Theorem | bl2in 12611 |
Two balls are disjoint if they don't overlap. (Contributed by NM,
11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑅 ≤ ((𝑃𝐷𝑄) / 2))) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑅)) = ∅) |
|
Theorem | xblss2ps 12612 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. In this version of blss2 12615 for
extended metrics, we have to assume the balls are a finite distance
apart, or else 𝑃 will not even be in the infinity
ball around
𝑄. (Contributed by Mario Carneiro,
23-Aug-2015.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋)
& ⊢ (𝜑 → 𝑄 ∈ 𝑋)
& ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ (𝜑 → 𝑆 ∈ ℝ*) & ⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ) & ⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +𝑒
-𝑒𝑅)) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) |
|
Theorem | xblss2 12613 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. In this version of blss2 12615 for
extended metrics, we have to assume the balls are a finite distance
apart, or else 𝑃 will not even be in the infinity
ball around
𝑄. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋)
& ⊢ (𝜑 → 𝑄 ∈ 𝑋)
& ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ (𝜑 → 𝑆 ∈ ℝ*) & ⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ) & ⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +𝑒
-𝑒𝑅)) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) |
|
Theorem | blss2ps 12614 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. (Contributed by Mario Carneiro,
15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ (𝑃𝐷𝑄) ≤ (𝑆 − 𝑅))) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) |
|
Theorem | blss2 12615 |
One ball is contained in another if the center-to-center distance is
less than the difference of the radii. (Contributed by Mario Carneiro,
15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ (𝑃𝐷𝑄) ≤ (𝑆 − 𝑅))) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) |
|
Theorem | blhalf 12616 |
A ball of radius 𝑅 / 2 is contained in a ball of radius
𝑅
centered
at any point inside the smaller ball. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.)
|
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑍 ∈ (𝑌(ball‘𝑀)(𝑅 / 2)))) → (𝑌(ball‘𝑀)(𝑅 / 2)) ⊆ (𝑍(ball‘𝑀)𝑅)) |
|
Theorem | blfps 12617 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
|
Theorem | blf 12618 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
|
Theorem | blrnps 12619* |
Membership in the range of the ball function. Note that
ran (ball‘𝐷) is the collection of all balls for
metric 𝐷.
(Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro,
12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ ran (ball‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ* 𝐴 = (𝑥(ball‘𝐷)𝑟))) |
|
Theorem | blrn 12620* |
Membership in the range of the ball function. Note that
ran (ball‘𝐷) is the collection of all balls for
metric 𝐷.
(Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∈ ran (ball‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ* 𝐴 = (𝑥(ball‘𝐷)𝑟))) |
|
Theorem | xblcntrps 12621 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 <
𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | xblcntr 12622 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 <
𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | blcntrps 12623 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | blcntr 12624 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | xblm 12625* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) →
(∃𝑥 𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 0 < 𝑅)) |
|
Theorem | bln0 12626 |
A ball is not empty. It is also inhabited, as seen at blcntr 12624.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅) |
|
Theorem | blelrnps 12627 |
A ball belongs to the set of balls of a metric space. (Contributed by
NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) |
|
Theorem | blelrn 12628 |
A ball belongs to the set of balls of a metric space. (Contributed by
NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) |
|
Theorem | blssm 12629 |
A ball is a subset of the base set of a metric space. (Contributed by
NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋) |
|
Theorem | unirnblps 12630 |
The union of the set of balls of a metric space is its base set.
(Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → ∪ ran
(ball‘𝐷) = 𝑋) |
|
Theorem | unirnbl 12631 |
The union of the set of balls of a metric space is its base set.
(Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∪ ran
(ball‘𝐷) = 𝑋) |
|
Theorem | blininf 12632 |
The intersection of two balls with the same center is the smaller of
them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*))
→ ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) = (𝑃(ball‘𝐷)inf({𝑅, 𝑆}, ℝ*, <
))) |
|
Theorem | ssblps 12633 |
The size of a ball increases monotonically with its radius.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*)
∧ 𝑅 ≤ 𝑆) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑃(ball‘𝐷)𝑆)) |
|
Theorem | ssbl 12634 |
The size of a ball increases monotonically with its radius.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
24-Aug-2015.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*)
∧ 𝑅 ≤ 𝑆) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑃(ball‘𝐷)𝑆)) |
|
Theorem | blssps 12635* |
Any point 𝑃 in a ball 𝐵 can be centered in
another ball that is
a subset of 𝐵. (Contributed by NM, 31-Aug-2006.)
(Revised by
Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷) ∧ 𝑃 ∈ 𝐵) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐵) |
|
Theorem | blss 12636* |
Any point 𝑃 in a ball 𝐵 can be centered in
another ball that is
a subset of 𝐵. (Contributed by NM, 31-Aug-2006.)
(Revised by
Mario Carneiro, 24-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷) ∧ 𝑃 ∈ 𝐵) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐵) |
|
Theorem | blssexps 12637* |
Two ways to express the existence of a ball subset. (Contributed by NM,
5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝐴)) |
|
Theorem | blssex 12638* |
Two ways to express the existence of a ball subset. (Contributed by NM,
5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝐴)) |
|
Theorem | ssblex 12639* |
A nested ball exists whose radius is less than any desired amount.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+))
→ ∃𝑥 ∈
ℝ+ (𝑥
< 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆))) |
|
Theorem | blin2 12640* |
Given any two balls and a point in their intersection, there is a ball
contained in the intersection with the given center point. (Contributed
by Mario Carneiro, 12-Nov-2013.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝐵 ∩ 𝐶)) ∧ (𝐵 ∈ ran (ball‘𝐷) ∧ 𝐶 ∈ ran (ball‘𝐷))) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ (𝐵 ∩ 𝐶)) |
|
Theorem | blbas 12641 |
The balls of a metric space form a basis for a topology. (Contributed
by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ∈ TopBases) |
|
Theorem | blres 12642 |
A ball in a restricted metric space. (Contributed by Mario Carneiro,
5-Jan-2014.)
|
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) |
|
Theorem | xmeterval 12643 |
Value of the "finitely separated" relation. (Contributed by Mario
Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) |
|
Theorem | xmeter 12644 |
The "finitely separated" relation is an equivalence relation.
(Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) |
|
Theorem | xmetec 12645 |
The equivalence classes under the finite separation equivalence relation
are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → [𝑃] ∼ = (𝑃(ball‘𝐷)+∞)) |
|
Theorem | blssec 12646 |
A ball centered at 𝑃 is contained in the set of points
finitely
separated from 𝑃. This is just an application of ssbl 12634
to the
infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ ) |
|
Theorem | blpnfctr 12647 |
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 12648 |
An extended metric restricted to any ball (in particular the infinity
ball) is a proper metric. Together with xmetec 12645, 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 12649 |
The class of open sets of a metric space is a relation. (Contributed by
Jim Kingdon, 5-May-2023.)
|
⊢ Rel MetOpen |
|
Theorem | mopnval 12650 |
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 12652, the open sets of a
metric space form a topology 𝐽, whose base set is ∪ 𝐽 by
mopnuni 12653. (Contributed by NM, 1-Sep-2006.) (Revised
by Mario
Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷))) |
|
Theorem | mopntopon 12651 |
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 12652 |
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 12653 |
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 12654* |
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 12655 |
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 12656 |
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 12657* |
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 12658 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
Theorem | isxms 12659 |
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 12660 |
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 12661 |
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 12662 |
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 12663 |
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 12664 |
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 12665 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) |
|
Theorem | msxms 12666 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) |
|
Theorem | mstps 12667 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) |
|
Theorem | xmsxmet 12668 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Sep-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | msmet 12669 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | msf 12670 |
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 12671 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) |
|
Theorem | msmet2 12672 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
|
Theorem | mscl 12673 |
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 12674 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | xmsge0 12675 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmseq0 12676 |
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 12677 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmstri2 12678 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mstri2 12679 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri 12680 |
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 12681 |
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 12682 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mstri3 12683 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | msrtri 12684 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmspropd 12685 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
|
Theorem | mspropd 12686 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
|
Theorem | setsmsbasg 12687 |
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 12688 |
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 12689 |
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 12690* |
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 12691* |
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 12692* |
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 12693 |
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 12694 |
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 12695 |
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 12696 |
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 12697 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) |
|
Theorem | blopn 12698 |
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 12699* |
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 12700 |
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‘𝐽)‘{𝑃})) |