Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | hmeocn 12401 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
|
Theorem | hmeocnvcn 12402 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) |
|
Theorem | hmeocnv 12403 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾Homeo𝐽)) |
|
Theorem | hmeof1o2 12404 |
A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌) |
|
Theorem | hmeof1o 12405 |
A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
(Revised by Mario Carneiro, 30-May-2014.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) |
|
Theorem | hmeoima 12406 |
The image of an open set by a homeomorphism is an open set. (Contributed
by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ∈ 𝐽) → (𝐹 “ 𝐴) ∈ 𝐾) |
|
Theorem | hmeoopn 12407 |
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐹 “ 𝐴) ∈ 𝐾)) |
|
Theorem | hmeocld 12408 |
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (𝐹 “ 𝐴) ∈ (Clsd‘𝐾))) |
|
Theorem | hmeontr 12409 |
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴))) |
|
Theorem | hmeoimaf1o 12410* |
The function mapping open sets to their images under a homeomorphism is
a bijection of topologies. (Contributed by Mario Carneiro,
10-Sep-2015.)
|
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥)) ⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾) |
|
Theorem | hmeores 12411 |
The restriction of a homeomorphism is a homeomorphism. (Contributed by
Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) |
|
Theorem | hmeoco 12412 |
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐺 ∈ (𝐾Homeo𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽Homeo𝐿)) |
|
Theorem | idhmeo 12413 |
The identity function is a homeomorphism. (Contributed by FL,
14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽Homeo𝐽)) |
|
Theorem | hmeocnvb 12414 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
⊢ (Rel 𝐹 → (◡𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹 ∈ (𝐾Homeo𝐽))) |
|
Theorem | txhmeo 12415* |
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿)) & ⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀))) |
|
Theorem | txswaphmeolem 12416* |
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21-Mar-2015.)
|
⊢ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 〈𝑥, 𝑦〉) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) = ( I ↾ (𝑋 × 𝑌)) |
|
Theorem | txswaphmeo 12417* |
There is a homeomorphism from 𝑋 × 𝑌 to 𝑌 × 𝑋. (Contributed
by Mario Carneiro, 21-Mar-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐾 ×t 𝐽))) |
|
7.2 Metric spaces
|
|
7.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 12418 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
⊢ Rel PsMet |
|
Theorem | ispsmet 12419* |
Express the predicate "𝐷 is a pseudometric."
(Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ (𝑋 ∈ 𝑉 → (𝐷 ∈ (PsMet‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐷𝑥) = 0 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) |
|
Theorem | psmetdmdm 12420 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 = dom dom 𝐷) |
|
Theorem | psmetf 12421 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
|
Theorem | psmetcl 12422 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | psmet0 12423 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
|
Theorem | psmettri2 12424 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | psmetsym 12425 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | psmettri 12426 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | psmetge0 12427 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | psmetxrge0 12428 |
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) |
|
Theorem | psmetres2 12429 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅)) |
|
Theorem | psmetlecl 12430 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) |
|
Theorem | distspace 12431 |
A set 𝑋 together with a (distance) function
𝐷
which is a
pseudometric is a distance space (according to E. Deza, M.M. Deza:
"Dictionary of Distances", Elsevier, 2006), i.e. a (base) set
𝑋
equipped with a distance 𝐷, which is a mapping of two elements
of
the base set to the (extended) reals and which is nonnegative, symmetric
and equal to 0 if the two elements are equal. (Contributed by AV,
15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ (𝐴𝐷𝐴) = 0) ∧ (0 ≤ (𝐴𝐷𝐵) ∧ (𝐴𝐷𝐵) = (𝐵𝐷𝐴)))) |
|
7.2.2 Basic metric space
properties
|
|
Syntax | cxms 12432 |
Extend class notation with the class of extended metric spaces.
|
class ∞MetSp |
|
Syntax | cms 12433 |
Extend class notation with the class of metric spaces.
|
class MetSp |
|
Syntax | ctms 12434 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
class toMetSp |
|
Definition | df-xms 12435 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
⊢ ∞MetSp = {𝑓 ∈ TopSp ∣ (TopOpen‘𝑓) =
(MetOpen‘((dist‘𝑓) ↾ ((Base‘𝑓) × (Base‘𝑓))))} |
|
Definition | df-ms 12436 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
⊢ MetSp = {𝑓 ∈ ∞MetSp ∣
((dist‘𝑓) ↾
((Base‘𝑓) ×
(Base‘𝑓))) ∈
(Met‘(Base‘𝑓))} |
|
Definition | df-tms 12437 |
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2-Sep-2015.)
|
⊢ toMetSp = (𝑑 ∈ ∪ ran
∞Met ↦ ({〈(Base‘ndx), dom dom 𝑑〉, 〈(dist‘ndx), 𝑑〉} sSet
〈(TopSet‘ndx), (MetOpen‘𝑑)〉)) |
|
Theorem | metrel 12438 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
⊢ Rel Met |
|
Theorem | xmetrel 12439 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
⊢ Rel ∞Met |
|
Theorem | ismet 12440* |
Express the predicate "𝐷 is a metric." (Contributed by
NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))) |
|
Theorem | isxmet 12441* |
Express the predicate "𝐷 is an extended metric."
(Contributed by
Mario Carneiro, 20-Aug-2015.)
|
⊢ (𝑋 ∈ 𝐴 → (𝐷 ∈ (∞Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))))) |
|
Theorem | ismeti 12442* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ 𝑋 ∈ V & ⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ & ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
& ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) |
|
Theorem | isxmetd 12443* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | isxmet2d 12444* |
It is safe to only require the triangle inequality when the values are
real (so that we can use the standard addition over the reals), but in
this case the nonnegativity constraint cannot be deduced and must be
provided separately. (Counterexample:
𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all
hypotheses
except nonnegativity.) (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝜑 → 𝑋 ∈ V) & ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ (𝑥𝐷𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | metflem 12445* |
Lemma for metf 12447 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))) |
|
Theorem | xmetf 12446 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
|
Theorem | metf 12447 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
|
Theorem | xmetcl 12448 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | metcl 12449 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ) |
|
Theorem | ismet2 12450 |
An extended metric is a metric exactly when it takes real values for all
values of the arguments. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ)) |
|
Theorem | metxmet 12451 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | xmetdmdm 12452 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = dom dom 𝐷) |
|
Theorem | metdmdm 12453 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷) |
|
Theorem | xmetunirn 12454 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
⊢ (𝐷 ∈ ∪ ran
∞Met ↔ 𝐷 ∈
(∞Met‘dom dom 𝐷)) |
|
Theorem | xmeteq0 12455 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) |
|
Theorem | meteq0 12456 |
The value of a metric is zero iff its arguments are equal. Property M2
of [Kreyszig] p. 4. (Contributed by
NM, 30-Aug-2006.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) |
|
Theorem | xmettri2 12457 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mettri2 12458 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) |
|
Theorem | xmet0 12459 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
|
Theorem | met0 12460 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM,
30-Aug-2006.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0) |
|
Theorem | xmetge0 12461 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | metge0 12462 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmetlecl 12463 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ) |
|
Theorem | xmetsym 12464 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmetpsmet 12465 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋)) |
|
Theorem | xmettpos 12466 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷) |
|
Theorem | metsym 12467 |
The distance function of a metric space is symmetric. Definition
14-1.1(c) of [Gleason] p. 223.
(Contributed by NM, 27-Aug-2006.)
(Revised by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmettri 12468 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mettri 12469 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by NM,
27-Aug-2006.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵))) |
|
Theorem | xmettri3 12470 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mettri3 12471 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | xmetrtri 12472 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶) +𝑒
-𝑒(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵)) |
|
Theorem | metrtri 12473 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
21-Apr-2023.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | metn0 12474 |
A metric space is nonempty iff its base set is nonempty. (Contributed
by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ≠ ∅ ↔ 𝑋 ≠ ∅)) |
|
Theorem | xmetres2 12475 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅)) |
|
Theorem | metreslem 12476 |
Lemma for metres 12479. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅)))) |
|
Theorem | metres2 12477 |
Lemma for metres 12479. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅)) |
|
Theorem | xmetres 12478 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅))) |
|
Theorem | metres 12479 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘(𝑋 ∩ 𝑅))) |
|
Theorem | 0met 12480 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
⊢ ∅ ∈
(Met‘∅) |
|
7.2.3 Metric space balls
|
|
Theorem | blfvalps 12481* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Feb-2018.)
|
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |
|
Theorem | blfval 12482* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry
Arnoux, 11-Feb-2018.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) |
|
Theorem | blex 12483 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) ∈ V) |
|
Theorem | blvalps 12484* |
The ball around a point 𝑃 is the set of all points whose
distance
from 𝑃 is less than the ball's radius 𝑅.
(Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) |
|
Theorem | blval 12485* |
The ball around a point 𝑃 is the set of all points whose
distance
from 𝑃 is less than the ball's radius 𝑅.
(Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) |
|
Theorem | elblps 12486 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) |
|
Theorem | elbl 12487 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) |
|
Theorem | elbl2ps 12488 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) |
|
Theorem | elbl2 12489 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) |
|
Theorem | elbl3ps 12490 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) |
|
Theorem | elbl3 12491 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) |
|
Theorem | blcomps 12492 |
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 12493 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) |
|
Theorem | xblpnfps 12494 |
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 12495 |
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 12496 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋) |
|
Theorem | bldisj 12497 |
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 12498 |
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 12499 |
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 12500 |
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 12503 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‘𝐷)𝑆)) |