Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cnnei 12401* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
|
|
Theorem | cnconst2 12402 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
TopOn
TopOn |
|
Theorem | cnconst 12403 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
TopOn TopOn
|
|
Theorem | cnrest 12404 |
Continuity of a restriction from a subspace. (Contributed by Jeff
Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|
↾t |
|
Theorem | cnrest2 12405 |
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened
by Mario Carneiro, 21-Aug-2015.)
|
TopOn
↾t |
|
Theorem | cnrest2r 12406 |
Equivalence of continuity in the parent topology and continuity in a
subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 7-Jun-2014.)
|
↾t
|
|
Theorem | cnptopresti 12407 |
One direction of cnptoprest 12408 under the weaker condition that the point
is in the subset rather than the interior of the subset. (Contributed
by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon,
31-Mar-2023.)
|
TopOn
↾t |
|
Theorem | cnptoprest 12408 |
Equivalence of continuity at a point and continuity of the restricted
function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.)
(Revised by Jim Kingdon, 5-Apr-2023.)
|
↾t |
|
Theorem | cnptoprest2 12409 |
Equivalence of point-continuity in the parent topology and
point-continuity in a subspace. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|
↾t |
|
Theorem | cndis 12410 |
Every function is continuous when the domain is discrete. (Contributed
by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro,
21-Aug-2015.)
|
TopOn
|
|
Theorem | cnpdis 12411 |
If is an isolated
point in (or
equivalently, the singleton
is open in ), then every function is continuous at
. (Contributed
by Mario Carneiro, 9-Sep-2015.)
|
TopOn TopOn
|
|
Theorem | lmfpm 12412 |
If converges, then
is a partial
function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
TopOn |
|
Theorem | lmfss 12413 |
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 12414 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
TopOn |
|
Theorem | lmss 12415 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
↾t |
|
Theorem | sslm 12416 |
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 12417 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
TopOn |
|
Theorem | lmff 12418* |
If converges, there
is some upper integer set on which is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
TopOn |
|
Theorem | lmtopcnp 12419 |
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 12420 |
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 12421 |
Extend class notation with the binary topological product operation.
|
|
|
Definition | df-tx 12422* |
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 12423 |
Existence of the binary topological product. If and are
known to be topologies, see txtop 12429. (Contributed by Jim Kingdon,
3-Aug-2023.)
|
|
|
Theorem | txval 12424* |
Value of the binary topological product operation. (Contributed by Jeff
Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | txuni2 12425* |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31-Aug-2015.)
|
|
|
Theorem | txbasex 12426* |
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txbas 12427* |
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 12428* |
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 12429 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | txtopi 12430 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
|
|
Theorem | txtopon 12431 |
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 12432 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | txunii 12433 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
|
|
Theorem | txopn 12434 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
|
|
Theorem | txss12 12435 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txbasval 12436 |
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 12437 |
The Cartesian product of two neighborhoods is a neighborhood in the
product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|
|
|
Theorem | tx1cn 12438 |
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 12439 |
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 12440* |
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 12441* |
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 12442* |
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 12443* |
Universal property of the binary topological product. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
22-Aug-2015.)
|
|
|
Theorem | txcn 12444 |
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 12445 |
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 12446 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | txdis1cn 12447* |
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 12448* |
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 12449* |
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 12450* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmptc 12451* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn TopOn
|
|
Theorem | cnmpt11 12452* |
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 12453* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt1t 12454* |
The composition of continuous functions is continuous. (Contributed by
Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt12f 12455* |
The composition of continuous functions is continuous. (Contributed
by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro,
22-Aug-2015.)
|
TopOn
|
|
Theorem | cnmpt12 12456* |
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 12457* |
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 12458* |
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 12459* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
TopOn TopOn TopOn
|
|
Theorem | cnmpt21 12460* |
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 12461* |
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 12462* |
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 12463* |
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 12464* |
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 12465* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
↾t TopOn
|
|
Theorem | cnmpt2res 12466* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
↾t TopOn
↾t TopOn
|
|
Theorem | cnmptcom 12467* |
The argument converse of a continuous function is continuous.
(Contributed by Mario Carneiro, 6-Jun-2014.)
|
TopOn TopOn
|
|
Theorem | imasnopn 12468 |
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 12469 |
Extend class notation with the class of all homeomorphisms.
|
|
|
Definition | df-hmeo 12470* |
Function returning all the homeomorphisms from topology to
topology .
(Contributed by FL, 14-Feb-2007.)
|
|
|
Theorem | hmeofn 12471 |
The set of homeomorphisms is a function on topologies. (Contributed by
Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | hmeofvalg 12472* |
The set of all the homeomorphisms between two topologies. (Contributed
by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | ishmeo 12473 |
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 12474 |
A homeomorphism is continuous. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
|
|
Theorem | hmeocnvcn 12475 |
The converse of a homeomorphism is continuous. (Contributed by Mario
Carneiro, 22-Aug-2015.)
|
|
|
Theorem | hmeocnv 12476 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
|
|
Theorem | hmeof1o2 12477 |
A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro,
22-Aug-2015.)
|
TopOn
TopOn |
|
Theorem | hmeof1o 12478 |
A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.)
(Revised by Mario Carneiro, 30-May-2014.)
|
|
|
Theorem | hmeoima 12479 |
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 12480 |
Homeomorphisms preserve openness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
|
|
Theorem | hmeocld 12481 |
Homeomorphisms preserve closedness. (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|
|
|
Theorem | hmeontr 12482 |
Homeomorphisms preserve interiors. (Contributed by Mario Carneiro,
25-Aug-2015.)
|
|
|
Theorem | hmeoimaf1o 12483* |
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 12484 |
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 12485 |
The composite of two homeomorphisms is a homeomorphism. (Contributed by
FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | idhmeo 12486 |
The identity function is a homeomorphism. (Contributed by FL,
14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|
TopOn |
|
Theorem | hmeocnvb 12487 |
The converse of a homeomorphism is a homeomorphism. (Contributed by FL,
5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | txhmeo 12488* |
Lift a pair of homeomorphisms on the factors to a homeomorphism of
product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | txswaphmeolem 12489* |
Show inverse for the "swap components" operation on a Cartesian
product.
(Contributed by Mario Carneiro, 21-Mar-2015.)
|
|
|
Theorem | txswaphmeo 12490* |
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 12491 |
The class of pseudometrics is a relation. (Contributed by Jim Kingdon,
24-Apr-2023.)
|
PsMet |
|
Theorem | ispsmet 12492* |
Express the predicate " is a pseudometric." (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmetdmdm 12493 |
Recover the base set from a pseudometric. (Contributed by Thierry
Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmetf 12494 |
The distance function of a pseudometric as a function. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet |
|
Theorem | psmetcl 12495 |
Closure of the distance function of a pseudometric space. (Contributed
by Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmet0 12496 |
The distance function of a pseudometric space is zero if its arguments
are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmettri2 12497 |
Triangle inequality for the distance function of a pseudometric.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
PsMet
|
|
Theorem | psmetsym 12498 |
The distance function of a pseudometric is symmetrical. (Contributed by
Thierry Arnoux, 7-Feb-2018.)
|
PsMet
|
|
Theorem | psmettri 12499 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
PsMet
|
|
Theorem | psmetge0 12500 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
PsMet
|