Home Intuitionistic Logic ExplorerTheorem List (p. 125 of 135) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12401-12500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremopnneip 12401 An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)

Theoremtpnei 12402 The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 12400. (Contributed by FL, 2-Oct-2006.)

Theoremneiuni 12403 The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.)

Theoremtopssnei 12404 A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)

Theoreminnei 12405 The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.)

Theoremopnneiid 12406 Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)

Theoremneissex 12407* For any neighborhood of , there is a neighborhood of such that is a neighborhood of all subsets of . Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)

Theorem0nei 12408 The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)

7.1.6  Subspace topologies

Theoremrestrcl 12409 Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.)
t

Theoremrestbasg 12410 A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.)
t

Theoremtgrest 12411 A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
t t

Theoremresttop 12412 A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. is normally a subset of the base set of . (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.)
t

Theoremresttopon 12413 A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
TopOn t TopOn

Theoremrestuni 12414 The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
t

Theoremstoig 12415 The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
TopSet t

Theoremrestco 12416 Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
t t t

Theoremrestabs 12417 Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
t t t

Theoremrestin 12418 When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.)
t t

Theoremrestuni2 12419 The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
t

Theoremresttopon2 12420 The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
TopOn t TopOn

Theoremrest0 12421 The subspace topology induced by the topology on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.)
t

Theoremrestsn 12422 The only subspace topology induced by the topology . (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
t

Theoremrestopnb 12423 If is an open subset of the subspace base set , then any subset of is open iff it is open in . (Contributed by Mario Carneiro, 2-Mar-2015.)
t

Theoremssrest 12424 If is a finer topology than , then the subspace topologies induced by maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
t t

Theoremrestopn2 12425 If is open, then is open in iff it is an open subset of . (Contributed by Mario Carneiro, 2-Mar-2015.)
t

Theoremrestdis 12426 A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
t

7.1.7  Limits and continuity in topological spaces

Syntaxccn 12427 Extend class notation with the class of continuous functions between topologies.

Syntaxccnp 12428 Extend class notation with the class of functions between topologies continuous at a given point.

Syntaxclm 12429 Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space.

Definitiondf-cn 12430* Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 12439 for the predicate form. (Contributed by NM, 17-Oct-2006.)

Definitiondf-cnp 12431* Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.)

Definitiondf-lm 12432* Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)

Theoremlmrcl 12433 Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)

Theoremlmfval 12434* The relation "sequence converges to point " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn

Theoremlmreltop 12435 The topological space convergence relation is a relation. (Contributed by Jim Kingdon, 25-Mar-2023.)

Theoremcnfval 12436* The set of all continuous functions from topology to topology . (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremcnpfval 12437* The function mapping the points in a topology to the set of all functions from to topology continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremcnovex 12438 The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.)

Theoremiscn 12439* The predicate "the class is a continuous function from topology to topology ". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremcnpval 12440* The set of all functions from topology to topology that are continuous at a point . (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
TopOn TopOn

Theoremiscnp 12441* The predicate "the class is a continuous function from topology to topology at point ". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremiscn2 12442* The predicate "the class is a continuous function from topology to topology ". Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.)

Theoremcntop1 12443 Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)

Theoremcntop2 12444 Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)

Theoremiscnp3 12445* The predicate "the class is a continuous function from topology to topology at point ". (Contributed by NM, 15-May-2007.)
TopOn TopOn

Theoremcnf 12446 A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Theoremcnf2 12447 A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremcnprcl2k 12448 Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
TopOn

Theoremcnpf2 12449 A continuous function at point is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
TopOn TopOn

Theoremtgcn 12450* The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
TopOn              TopOn

Theoremtgcnp 12451* The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
TopOn              TopOn

Theoremssidcn 12452 The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremicnpimaex 12453* Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
TopOn TopOn

Theoremidcn 12454 A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
TopOn

Theoremlmbr 12455* Express the binary relation "sequence converges to point " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition allows us to use objects more general than sequences when convenient; see the comment in df-lm 12432. (Contributed by Mario Carneiro, 14-Nov-2013.)
TopOn

Theoremlmbr2 12456* Express the binary relation "sequence converges to point " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
TopOn

Theoremlmbrf 12457* Express the binary relation "sequence converges to point " in a metric space using an arbitrary upper set of integers. This version of lmbr2 12456 presupposes that is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
TopOn

Theoremlmconst 12458 A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
TopOn

Theoremlmcvg 12459* Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)

Theoremiscnp4 12460* The predicate "the class is a continuous function from topology to topology at point " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
TopOn TopOn

Theoremcnpnei 12461* A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)

Theoremcnima 12462 An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)

Theoremcnco 12463 The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Theoremcnptopco 12464 The composition of a function continuous at with a function continuous at is continuous at . Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)

Theoremcnclima 12465 A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)

Theoremcnntri 12466 Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)

Theoremcnntr 12467* Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
TopOn TopOn

Theoremcnss1 12468 If the topology is finer than , then there are more continuous functions from than from . (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn

Theoremcnss2 12469 If the topology is finer than , then there are fewer continuous functions into than into from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn

Theoremcncnpi 12470 A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)

Theoremcnsscnp 12471 The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)

Theoremcncnp 12472* A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
TopOn TopOn

Theoremcncnp2m 12473* A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.)

Theoremcnnei 12474* Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)

Theoremcnconst2 12475 A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
TopOn TopOn

Theoremcnconst 12476 A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
TopOn TopOn

Theoremcnrest 12477 Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
t

Theoremcnrest2 12478 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

Theoremcnrest2r 12479 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

Theoremcnptopresti 12480 One direction of cnptoprest 12481 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

Theoremcnptoprest 12481 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

Theoremcnptoprest2 12482 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

Theoremcndis 12483 Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
TopOn

Theoremcnpdis 12484 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

Theoremlmfpm 12485 If converges, then is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
TopOn

Theoremlmfss 12486 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

Theoremlmcl 12487 Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
TopOn

Theoremlmss 12488 Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
t

Theoremsslm 12489 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

Theoremlmres 12490 A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
TopOn

Theoremlmff 12491* If converges, there is some upper integer set on which is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
TopOn

Theoremlmtopcnp 12492 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.)

Theoremlmcn 12493 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

Syntaxctx 12494 Extend class notation with the binary topological product operation.

Definitiondf-tx 12495* 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.)

Theoremtxvalex 12496 Existence of the binary topological product. If and are known to be topologies, see txtop 12502. (Contributed by Jim Kingdon, 3-Aug-2023.)

Theoremtxval 12497* Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)

Theoremtxuni2 12498* The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)

Theoremtxbasex 12499* The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)

Theoremtxbas 12500* 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.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13494
 Copyright terms: Public domain < Previous  Next >