Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | lmfpm 12401 |
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
TopOn |
|
Theorem | lmfss 12402 |
Inclusion of a function having a limit (used to ensure the limit
relation is a set, under our definition). (Contributed by NM,
7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|
TopOn
|
|
Theorem | lmcl 12403 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
TopOn |
|
Theorem | lmss 12404 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
↾t |
|
Theorem | sslm 12405 |
A finer topology has fewer convergent sequences (but the sequences that
do converge, converge to the same value). (Contributed by Mario
Carneiro, 15-Sep-2015.)
|
TopOn
TopOn
|
|
Theorem | lmres 12406 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
TopOn |
|
Theorem | lmff 12407* |
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
TopOn |
|
Theorem | lmtopcnp 12408 |
The image of a convergent sequence under a continuous map is
convergent to the image of the original point. (Contributed by Mario
Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|
|
|
Theorem | lmcn 12409 |
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. (Contributed by Mario Carneiro,
3-May-2014.)
|
|
|
7.1.8 Product topologies
|
|
Syntax | ctx 12410 |
Extend class notation with the binary topological product operation.
|
|
|
Definition | df-tx 12411* |
Define the binary topological product, which is homeomorphic to the
general topological product over a two element set, but is more
convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | txvalex 12412 |
Existence of the binary topological product. If and are
known to be topologies, see txtop 12418. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
|
|
Theorem | txval 12413* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | txuni2 12414* |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | txbasex 12415* |
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txbas 12416* |
The set of Cartesian products of elements from two topological bases is
a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 31-Aug-2015.)
|
|
|
Theorem | eltx 12417* |
A set in a product is open iff each point is surrounded by an open
rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|
|
|
Theorem | txtop 12418 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | txtopi 12419 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
|
|
Theorem | txtopon 12420 |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro,
2-Sep-2015.)
|
TopOn
TopOn
TopOn |
|
Theorem | txuni 12421 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | txunii 12422 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
|
|
Theorem | txopn 12423 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | txss12 12424 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txbasval 12425 |
It is sufficient to consider products of the bases for the topologies in
the topological product. (Contributed by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | neitx 12426 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
|
|
Theorem | tx1cn 12427 |
Continuity of the first projection map of a topological product.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 22-Aug-2015.)
|
TopOn
TopOn
|
|
Theorem | tx2cn 12428 |
Continuity of the second projection map of a topological product.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 22-Aug-2015.)
|
TopOn
TopOn
|
|
Theorem | txcnp 12429* |
If two functions are continuous at , then the ordered pair of them
is continuous at into the product topology. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn TopOn TopOn
|
|
Theorem | upxp 12430* |
Universal property of the Cartesian product considered as a categorical
product in the category of sets. (Contributed by Jeff Madsen,
2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
|
|
Theorem | txcnmpt 12431* |
A map into the product of two topological spaces is continuous if both
of its projections are continuous. (Contributed by Jeff Madsen,
2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | uptx 12432* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
|
|
Theorem | txcn 12433 |
A map into the product of two topological spaces is continuous iff both
of its projections are continuous. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | txrest 12434 |
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, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 2-Sep-2015.)
|
↾t ↾t
↾t |
|
Theorem | txdis 12435 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | txdis1cn 12436* |
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, 19-Sep-2015.)
|
TopOn
|
|
Theorem | txlm 12437* |
Two sequences converge iff the sequence of their ordered pairs
converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by
NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|
TopOn TopOn
|
|
Theorem | lmcn2 12438* |
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, 15-May-2014.)
|
TopOn TopOn
|
|
7.1.9 Continuous function-builders
|
|
Theorem | cnmptid 12439* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmptc 12440* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt11 12441* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
TopOn
|
|
Theorem | cnmpt11f 12442* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt1t 12443* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt12f 12444* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt12 12445* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
TopOn TopOn
|
|
Theorem | cnmpt1st 12446* |
The projection onto the first coordinate is continuous. (Contributed by
Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt2nd 12447* |
The projection onto the second coordinate is continuous. (Contributed
by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt2c 12448* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn TopOn TopOn
|
|
Theorem | cnmpt21 12449* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
TopOn
|
|
Theorem | cnmpt21f 12450* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt2t 12451* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt22 12452* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
TopOn TopOn
|
|
Theorem | cnmpt22f 12453* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt1res 12454* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
↾t TopOn
|
|
Theorem | cnmpt2res 12455* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
↾t TopOn
↾t TopOn
|
|
Theorem | cnmptcom 12456* |
The argument converse of a continuous function is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
TopOn TopOn
|
|
Theorem | imasnopn 12457 |
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, 14-Jan-2018.)
|
|
|
7.1.10 Homeomorphisms
|
|
Syntax | chmeo 12458 |
Extend class notation with the class of all homeomorphisms.
|
|
|
Definition | df-hmeo 12459* |
Function returning all the homeomorphisms from topology to
topology .
(Contributed by FL, 14-Feb-2007.)
|
|
|
Theorem | hmeofn 12460 |
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | hmeofvalg 12461* |
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | ishmeo 12462 |
The predicate F is a homeomorphism between topology and topology
. Proposition
of [BourbakiTop1] p. I.2. (Contributed
by FL,
14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | hmeocn 12463 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
|
|
Theorem | hmeocnvcn 12464 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
|
|
Theorem | hmeocnv 12465 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | hmeof1o2 12466 |
A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
TopOn
TopOn |
|
Theorem | hmeof1o 12467 |
A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
(Revised by Mario Carneiro, 30-May-2014.)
|
|
|
Theorem | hmeoima 12468 |
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.)
|
|
|
Theorem | hmeoopn 12469 |
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
|
|
Theorem | hmeocld 12470 |
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
|
|
Theorem | hmeontr 12471 |
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25-Aug-2015.)
|
|
|
Theorem | hmeoimaf1o 12472* |
The function mapping open sets to their images under a homeomorphism is
a bijection of topologies. (Contributed by Mario Carneiro,
10-Sep-2015.)
|
|
|
Theorem | hmeores 12473 |
The restriction of a homeomorphism is a homeomorphism. (Contributed by
Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
↾t ↾t |
|
Theorem | hmeoco 12474 |
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | idhmeo 12475 |
The identity function is a homeomorphism. (Contributed by FL,
14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
TopOn |
|
Theorem | hmeocnvb 12476 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | txhmeo 12477* |
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txswaphmeolem 12478* |
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21-Mar-2015.)
|
|
|
Theorem | txswaphmeo 12479* |
There is a homeomorphism from to . (Contributed
by Mario Carneiro, 21-Mar-2015.)
|
TopOn
TopOn
|
|
7.2 Metric spaces
|
|
7.2.1 Pseudometric spaces
|
|
Theorem | psmetrel 12480 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
PsMet |
|
Theorem | ispsmet 12481* |
Express the predicate " is a pseudometric." (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmetdmdm 12482 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmetf 12483 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet |
|
Theorem | psmetcl 12484 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmet0 12485 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmettri2 12486 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
PsMet
|
|
Theorem | psmetsym 12487 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmettri 12488 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
PsMet
|
|
Theorem | psmetge0 12489 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
PsMet
|
|
Theorem | psmetxrge0 12490 |
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24-Feb-2018.)
|
PsMet |
|
Theorem | psmetres2 12491 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
PsMet
PsMet |
|
Theorem | psmetlecl 12492 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
PsMet
|
|
Theorem | distspace 12493 |
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
|
|
7.2.2 Basic metric space
properties
|
|
Syntax | cxms 12494 |
Extend class notation with the class of extended metric spaces.
|
|
|
Syntax | cms 12495 |
Extend class notation with the class of metric spaces.
|
|
|
Syntax | ctms 12496 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 12497 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Definition | df-ms 12498 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
|
|
Definition | df-tms 12499 |
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2-Sep-2015.)
|
toMetSp sSet
TopSet
|
|
Theorem | metrel 12500 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
|