Type  Label  Description 
Statement 

Theorem  eltx 12501* 
A set in a product is open iff each point is surrounded by an open
rectangle. (Contributed by Stefan O'Rear, 25Jan2015.)



Theorem  txtop 12502 
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2Sep2009.)



Theorem  txtopi 12503 
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15Jun2010.)



Theorem  txtopon 12504 
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 22Aug2015.) (Revised by Mario Carneiro,
2Sep2015.)

TopOn
TopOn
TopOn 

Theorem  txuni 12505 
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2Sep2009.)



Theorem  txunii 12506 
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15Jun2010.)



Theorem  txopn 12507 
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2Sep2009.)



Theorem  txss12 12508 
Subset property of the topological product. (Contributed by Mario
Carneiro, 2Sep2015.)



Theorem  txbasval 12509 
It is sufficient to consider products of the bases for the topologies in
the topological product. (Contributed by Mario Carneiro,
25Aug2014.)



Theorem  neitx 12510 
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13Jan2018.)



Theorem  tx1cn 12511 
Continuity of the first projection map of a topological product.
(Contributed by Jeff Madsen, 2Sep2009.) (Proof shortened by Mario
Carneiro, 22Aug2015.)

TopOn
TopOn


Theorem  tx2cn 12512 
Continuity of the second projection map of a topological product.
(Contributed by Jeff Madsen, 2Sep2009.) (Proof shortened by Mario
Carneiro, 22Aug2015.)

TopOn
TopOn


Theorem  txcnp 12513* 
If two functions are continuous at , then the ordered pair of them
is continuous at into the product topology. (Contributed by Mario
Carneiro, 9Aug2014.) (Revised by Mario Carneiro, 22Aug2015.)

TopOn TopOn TopOn


Theorem  upxp 12514* 
Universal property of the Cartesian product considered as a categorical
product in the category of sets. (Contributed by Jeff Madsen,
2Sep2009.) (Revised by Mario Carneiro, 27Dec2014.)



Theorem  txcnmpt 12515* 
A map into the product of two topological spaces is continuous if both
of its projections are continuous. (Contributed by Jeff Madsen,
2Sep2009.) (Revised by Mario Carneiro, 22Aug2015.)



Theorem  uptx 12516* 
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2Sep2009.) (Proof shortened by Mario Carneiro,
22Aug2015.)



Theorem  txcn 12517 
A map into the product of two topological spaces is continuous iff both
of its projections are continuous. (Contributed by Jeff Madsen,
2Sep2009.) (Proof shortened by Mario Carneiro, 22Aug2015.)



Theorem  txrest 12518 
The subspace of a topological product space induced by a subset with a
Cartesian product representation is a topological product of the
subspaces induced by the subspaces of the terms of the products.
(Contributed by Jeff Madsen, 2Sep2009.) (Proof shortened by Mario
Carneiro, 2Sep2015.)

↾_{t} ↾_{t}
↾_{t} 

Theorem  txdis 12519 
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14Aug2015.)



Theorem  txdis1cn 12520* 
A function is jointly continuous on a discrete left topology iff it is
continuous as a function of its right argument, for each fixed left
value. (Contributed by Mario Carneiro, 19Sep2015.)

TopOn


Theorem  txlm 12521* 
Two sequences converge iff the sequence of their ordered pairs
converges. Proposition 142.6 of [Gleason] p. 230. (Contributed by
NM, 16Jul2007.) (Revised by Mario Carneiro, 5May2014.)

TopOn TopOn


Theorem  lmcn2 12522* 
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. Binary operation version.
(Contributed by Mario Carneiro, 15May2014.)

TopOn TopOn


7.1.9 Continuous functionbuilders


Theorem  cnmptid 12523* 
The identity function is continuous. (Contributed by Mario Carneiro,
5May2014.) (Revised by Mario Carneiro, 22Aug2015.)

TopOn


Theorem  cnmptc 12524* 
A constant function is continuous. (Contributed by Mario Carneiro,
5May2014.) (Revised by Mario Carneiro, 22Aug2015.)

TopOn TopOn


Theorem  cnmpt11 12525* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn
TopOn


Theorem  cnmpt11f 12526* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn


Theorem  cnmpt1t 12527* 
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn


Theorem  cnmpt12f 12528* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn


Theorem  cnmpt12 12529* 
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 12Jun2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn
TopOn TopOn


Theorem  cnmpt1st 12530* 
The projection onto the first coordinate is continuous. (Contributed by
Mario Carneiro, 6May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn


Theorem  cnmpt2nd 12531* 
The projection onto the second coordinate is continuous. (Contributed
by Mario Carneiro, 6May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn


Theorem  cnmpt2c 12532* 
A constant function is continuous. (Contributed by Mario Carneiro,
5May2014.) (Revised by Mario Carneiro, 22Aug2015.)

TopOn TopOn TopOn


Theorem  cnmpt21 12533* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn
TopOn


Theorem  cnmpt21f 12534* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn


Theorem  cnmpt2t 12535* 
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn


Theorem  cnmpt22 12536* 
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn
TopOn TopOn


Theorem  cnmpt22f 12537* 
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5May2014.) (Revised by Mario Carneiro,
22Aug2015.)

TopOn TopOn


Theorem  cnmpt1res 12538* 
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5Jun2014.)

↾_{t} TopOn


Theorem  cnmpt2res 12539* 
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6Jun2014.)

↾_{t} TopOn
↾_{t} TopOn


Theorem  cnmptcom 12540* 
The argument converse of a continuous function is continuous.
(Contributed by Mario Carneiro, 6Jun2014.)

TopOn TopOn


Theorem  imasnopn 12541 
If a relation graph is open, then an image set of a singleton is also
open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26.
(Contributed by Thierry Arnoux, 14Jan2018.)



7.1.10 Homeomorphisms


Syntax  chmeo 12542 
Extend class notation with the class of all homeomorphisms.



Definition  dfhmeo 12543* 
Function returning all the homeomorphisms from topology to
topology .
(Contributed by FL, 14Feb2007.)



Theorem  hmeofn 12544 
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23Aug2015.)



Theorem  hmeofvalg 12545* 
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14Feb2007.) (Revised by Mario Carneiro, 22Aug2015.)



Theorem  ishmeo 12546 
The predicate F is a homeomorphism between topology and topology
. Proposition
of [BourbakiTop1] p. I.2. (Contributed
by FL,
14Feb2007.) (Revised by Mario Carneiro, 22Aug2015.)



Theorem  hmeocn 12547 
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22Aug2015.)



Theorem  hmeocnvcn 12548 
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22Aug2015.)



Theorem  hmeocnv 12549 
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5Mar2007.) (Revised by Mario Carneiro, 22Aug2015.)



Theorem  hmeof1o2 12550 
A homeomorphism is a 11onto mapping. (Contributed by Mario Carneiro,
22Aug2015.)

TopOn
TopOn 

Theorem  hmeof1o 12551 
A homeomorphism is a 11onto mapping. (Contributed by FL, 5Mar2007.)
(Revised by Mario Carneiro, 30May2014.)



Theorem  hmeoima 12552 
The image of an open set by a homeomorphism is an open set. (Contributed
by FL, 5Mar2007.) (Revised by Mario Carneiro, 22Aug2015.)



Theorem  hmeoopn 12553 
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2Sep2009.) (Proof shortened by Mario Carneiro, 25Aug2015.)



Theorem  hmeocld 12554 
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2Sep2009.) (Proof shortened by Mario Carneiro, 25Aug2015.)



Theorem  hmeontr 12555 
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25Aug2015.)



Theorem  hmeoimaf1o 12556* 
The function mapping open sets to their images under a homeomorphism is
a bijection of topologies. (Contributed by Mario Carneiro,
10Sep2015.)



Theorem  hmeores 12557 
The restriction of a homeomorphism is a homeomorphism. (Contributed by
Mario Carneiro, 14Sep2014.) (Proof shortened by Mario Carneiro,
22Aug2015.)

↾_{t} ↾_{t} 

Theorem  hmeoco 12558 
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9Mar2007.) (Proof shortened by Mario Carneiro, 23Aug2015.)



Theorem  idhmeo 12559 
The identity function is a homeomorphism. (Contributed by FL,
14Feb2007.) (Proof shortened by Mario Carneiro, 23Aug2015.)

TopOn 

Theorem  hmeocnvb 12560 
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5Mar2007.) (Revised by Mario Carneiro, 23Aug2015.)



Theorem  txhmeo 12561* 
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2Sep2015.)



Theorem  txswaphmeolem 12562* 
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21Mar2015.)



Theorem  txswaphmeo 12563* 
There is a homeomorphism from to . (Contributed
by Mario Carneiro, 21Mar2015.)

TopOn
TopOn


7.2 Metric spaces


7.2.1 Pseudometric spaces


Theorem  psmetrel 12564 
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24Apr2023.)

PsMet 

Theorem  ispsmet 12565* 
Express the predicate " is a pseudometric." (Contributed by
Thierry Arnoux, 7Feb2018.)

PsMet


Theorem  psmetdmdm 12566 
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7Feb2018.)

PsMet


Theorem  psmetf 12567 
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7Feb2018.)

PsMet 

Theorem  psmetcl 12568 
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7Feb2018.)

PsMet


Theorem  psmet0 12569 
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7Feb2018.)

PsMet


Theorem  psmettri2 12570 
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11Feb2018.)

PsMet


Theorem  psmetsym 12571 
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7Feb2018.)

PsMet


Theorem  psmettri 12572 
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11Feb2018.)

PsMet


Theorem  psmetge0 12573 
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7Feb2018.) (Revised by Jim Kingdon,
19Apr2023.)

PsMet


Theorem  psmetxrge0 12574 
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24Feb2018.)

PsMet 

Theorem  psmetres2 12575 
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11Feb2018.)

PsMet
PsMet 

Theorem  psmetlecl 12576 
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11Mar2018.)

PsMet


Theorem  distspace 12577 
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,
15Oct2021.) (Revised by AV, 5Jul2022.)

PsMet


7.2.2 Basic metric space
properties


Syntax  cxms 12578 
Extend class notation with the class of extended metric spaces.



Syntax  cms 12579 
Extend class notation with the class of metric spaces.



Syntax  ctms 12580 
Extend class notation with the function mapping a metric to the metric
space it defines.

toMetSp 

Definition  dfxms 12581 
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2Sep2015.)



Definition  dfms 12582 
Define the (proper) class of metric spaces. (Contributed by NM,
27Aug2006.)



Definition  dftms 12583 
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2Sep2015.)

toMetSp sSet
TopSet


Theorem  metrel 12584 
The class of metrics is a relation. (Contributed by Jim Kingdon,
20Apr2023.)



Theorem  xmetrel 12585 
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20Apr2023.)



Theorem  ismet 12586* 
Express the predicate " is a metric." (Contributed by NM,
25Aug2006.) (Revised by Mario Carneiro, 14Aug2015.)



Theorem  isxmet 12587* 
Express the predicate " is an extended metric." (Contributed by
Mario Carneiro, 20Aug2015.)



Theorem  ismeti 12588* 
Properties that determine a metric. (Contributed by NM, 17Nov2006.)
(Revised by Mario Carneiro, 14Aug2015.)



Theorem  isxmetd 12589* 
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  isxmet2d 12590* 
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:
satisfies all hypotheses
except nonnegativity.) (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  metflem 12591* 
Lemma for metf 12593 and others. (Contributed by NM,
30Aug2006.)
(Revised by Mario Carneiro, 14Aug2015.)



Theorem  xmetf 12592 
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20Aug2015.)



Theorem  metf 12593 
Mapping of the distance function of a metric space. (Contributed by NM,
30Aug2006.)



Theorem  xmetcl 12594 
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30Aug2006.)



Theorem  metcl 12595 
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30Aug2006.)



Theorem  ismet2 12596 
An extended metric is a metric exactly when it takes real values for all
values of the arguments. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  metxmet 12597 
A metric is an extended metric. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xmetdmdm 12598 
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  metdmdm 12599 
Recover the base set from a metric. (Contributed by Mario Carneiro,
23Aug2015.)



Theorem  xmetunirn 12600 
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13Oct2015.)

