mmtheorems106 - Metamath Proof Explorer

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-10781

Statement List for Metamath Proof Explorer - 10501-10600 - Page 106 of 108

Type	Label	Description
Statement
Definition	df-EucTop 10501	Definition of the euclidean topology (Morris. Def. 2.1.1 p. 34).
|- EucTop = {x | (x (_ RR /\ A.y e. x E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) (_ x))}
Theorem	iseuctopg 10502	The predicate "J belongs to the euclidean topology."
|- (J e. A -> (J e. EucTop <-> (J (_ RR /\ A.y e. J E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) (_ J))))
Theorem	iseuctopgb 10503	The predicate "J belongs to the euclidean topology."
|- J e. A   =>   |- (J e. EucTop <-> (J (_ RR /\ A.y e. J E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) (_ J)))
Theorem	osbr 10504	An open set of an euclidean topology is a subset of RR.
|- (J e. EucTop -> J (_ RR)
Theorem	osbs 10505	Property of an open set of an euclidean topology.
|- (J e. EucTop -> A.y e. J E.a e. RR E.b e. RR (y e. (a(,)b) /\ (a(,)b) (_ J))
Topology
Theorem	empntop 10506	The empty set is not a topology.
|- -. (/) e. Top
Theorem	topnem 10507	A topology is not empty.
|- (J e. Top -> J =/= (/))
Neighborhoods
Theorem	esnnei 10508	The empty set is not a neighborhood of a non empty set.
|- ((J e. Top /\ S =/= (/)) -> -. (/) e. ((nei` J)` S))
Continuous functions
Theorem	cnrsfin 10509	A mapping remains continuous when the topology associated to its domain is replaced by a finer one.
|- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Cn L) /\ U.J = U.K /\ J (_ K) -> F e. (K Cn L)))
Theorem	cnrscoa 10510	A mapping remains continuous when the topology associated to its range is replaced by a coarser one.
|- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Cn L) /\ U.L = U.K /\ K (_ L) -> F e. (J Cn K)))
Theorem	mapdiscn 10511	Any mapping whose domain is associated to the discrete topology is continuous.
|- F e. C   &   |- B = U.J   &   |- A e. V   =>   |- ((J e. Top /\ F:A-->B) -> F e. (P~A Cn J))
Theorem	mapudiscn 10512	Any mapping whose range is associated to the undiscrete topology is continuous.
|- A = U.J   &   |- B e. V   =>   |- ((J e. Top /\ F:A-->B) -> F e. (J Cn {(/), B}))
Homeomorphisms
Syntax	chomeosm 10513	Extend class notation with the class of all homeomorphisms.
class Homeo
Syntax	chomeo 10514	Extend class notation with the relation "is homeomorph to.".
class ~=
Definition	df-homeo 10515	Function returning all the homeomorphisms from topology j to topology k.
|- Homeo = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f | (f:U.j-1-1-onto->U.k /\ A.x e. j (f"x) e. k /\ A.x e. k (`'f"x) e. j)})}
Theorem	homeofval 10516	The set of all the homeomorphisms between two topologies.
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (J Homeo K) = {f | (f:X-1-1-onto->Y /\ A.x e. J (f"x) e. K /\ A.x e. K (`'f"x) e. J)})
Theorem	ishomeo 10517	The predicate F is a homeomorphism between topology J and topology K. Based on Bourbaki TG I.2.
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ A.x e. J (F"x) e. K /\ A.x e. K (`'F"x) e. J)))
Theorem	hmeomap 10518	A homeomorphism is a 1-1-onto mapping.
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> F:X-1-1-onto->Y))
Theorem	hmeocna 10519	The image of an open set by the converse of a homeomorphism is an open set.
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.x e. K (`'F"x) e. J))
Theorem	hmeocnb 10520	The image of an open set by a homeomorphism is an open set.
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> A.x e. J (F"x) e. K))
Theorem	cmphmp 10521	The composition of two homeomorphisms is a homeomorphism.
|- ((J e. Top /\ K e. Top /\ L e. Top) -> ((F e. (J Homeo K) /\ G e. (K Homeo L)) -> (G o. F) e. (J Homeo L)))
Theorem	idhme 10522	The identity function is a homeomorphism.
|- X = U.J   =>   |- (J e. Top -> (I |` X) e. (J Homeo J))
Definition	df-hmph 10523	Definition of the relation x is homeomorph to y.
|- ~= = {<.x, y>. | (x e. Top /\ y e. Top /\ E.f f e. (x Homeo y))}
Theorem	hmph 10524	Express the predicate J is homeomorph to K.
|- ((J e. Top /\ K e. Top) -> (J ~= K <-> E.f f e. (J Homeo K)))
Theorem	cnvhmpha 10525	The converse of a homeomorphism is a homeomorphism.
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> `'F e. (K Homeo J)))
Theorem	cnvhmphb 10526	The converse of a homeomorphism is a homeomorphism.
|- ((J e. Top /\ K e. Top /\ Rel F) -> (`'F e. (J Homeo K) -> F e. (K Homeo J)))
Theorem	cnvhmph 10527	The converse of a homeomorphism is a homeomorphism.
|- (((J e. Top /\ K e. Top /\ F e. A) /\ Rel F) -> (F e. (J Homeo K) <-> `'F e. (K Homeo J)))
Theorem	hmphsyma 10528	"Is homeomorph to" is symmetric.
|- ((J e. Top /\ K e. Top) -> (J ~= K -> K ~= J))
Theorem	hmphsym 10529	"Is homeomorph to" is symmetric.
|- ((J e. Top /\ K e. Top) -> (J ~= K <-> K ~= J))
Theorem	hmphre 10530	"Is homeomorph to" is reflexive.
|- (J e. Top -> J ~= J)
Theorem	hmphtr 10531	"Is homeomorph to" is transitive.
|- ((J e. Top /\ K e. Top /\ L e. Top) -> ((J ~= K /\ K ~= L) -> J ~= L))
Theorem	dmhmph 10532	~= is a relation whose domain is included in Top.
|- dom ~= (_ Top
Theorem	rnhmph 10533	~= is a relation whose range is included in Top.
|- ran ~= (_ Top
Theorem	dmhmpha 10534	The relation "being homeomorph to" implies the operands are topologies.
|- A e. V   =>   |- (A ~= B -> A e. Top)
Theorem	rnhmpha 10535	The relation "being homeomorph to" implies the operands are topologies.
|- A e. V   &   |- B e. V   =>   |- (A ~= B -> B e. Top)
Theorem	hmpher 10536	"Is homeomorph to" is an equivalence relation.
|- Er ~=
Theorem	hmphsymv 10537	A more general version of hmphsym 10529. Certainly not a useful proof (since it's a simple consequence of hmpher 10536) but it shows that the conditions of hmphsym 10529 could (and should) be weakened.
|- A e. V   &   |- B e. V   =>   |- (A ~= B <-> B ~= A)
Theorem	hmeogrp 10538	Homeomorphisms on a topology J is a group for composition. This means from Felix Klein's point of view that a set equipped with a topology is a geometry, namely the so-called rubber sheet geometry.
|- (J e. Top -> {<.<.x, y>., z>. | (x e. (J Homeo J) /\ y e. (J Homeo J) /\ z = (x o. y))} e. Grp)
Theorem	homcard 10539	Homeomorphisms preserve the cardinality of the topologies.
|- ((J e. Top /\ K e. Top) -> (J ~= K -> J ~~ K))
Theorem	homcardus 10540	Homeomorphisms preserve the cardinality of the underlying sets.
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (J ~= K -> X ~~ Y))
Theorem	eqindhome 10541	Equinumerous sets equipped with their indiscrete topologies are homeomorph. ( Which means in particular that in that special case a segment is homeomorph to a circle contrary to what wikipedia claims.)
|- A e. C   &   |- B e. D   =>   |- (A ~~ B -> {(/), A} ~= {(/), B})
Theorem	hmeobc 10542	A homeomorphism is a bicontinuous bijection.
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top /\ F e. A) -> (F e. (J Homeo K) <-> (F:X-1-1-onto->Y /\ F e. (J Cn K) /\ `'F e. (K Cn J))))
Theorem	sfseqeq 10543	A finite set is equal to its subset if they are equinumerous.
|- ((E.x e. om B ~~ x /\ A (_ B /\ A ~~ B) -> A = B)
Theorem	unpde2eg2 10544	Conditions to have a set of two elements.
|- ((A e. C /\ B e. D /\ A =/= B) -> {A, B} ~~ 2o)
Theorem	set2elt 10545	Building a set with two elements.
|- ((C ~~ 2o /\ A e. C /\ B e. C) -> (A =/= B -> C = {A, B}))
Theorem	setwoe 10546	Building a set with only one element.
|- ((A e. B /\ B ~~ 1o) -> B = {A})
Theorem	top1 10547	{(/)} is the only topology with one element.
|- (J e. Top -> (J ~~ 1o <-> J = {(/)}))
Theorem	top2ind 10548	If a topology has two element it is the indiscrete topology.
|- ((J e. Top /\ J ~~ 2o) -> J = {(/), U.J})
Theorem	top2usne 10549	If a toplogy has two elements its underlying set can't be empty.
|- ((J e. Top /\ J ~~ 2o) -> U.J =/= (/))
Theorem	homindlem2 10550	An unnamed topological preservation.
|- ((K e. Top /\ K ~= {(/)}) -> K = {(/)})
Theorem	homindlem3 10551	Homeomorphisms preserve topological indiscretion.
|- ((K e. Top /\ A =/= (/) /\ A e. B) -> ({(/), A} ~= K -> K = {(/), U.K}))
Initial and final topologies
Syntax	csubsp 10552	Extend class notation with the function returning a subspace topology.
class subSp
Definition	df-subsp 10553	Function returning the subspace topology induced by the topology y and the set x.
|- subSp = {<.<.x, y>., z>. | (y e. Top /\ z = {u | E.v e. y u = (v i^i x)})}
Theorem	subsp 10554	The subspace topology induced by the topology J on the set A.
|- J e. Top   &   |- A e. V   =>   |- (subSp` <.A, J>.) = {u | E.v e. J u = (v i^i A)}
Theorem	qusp 10555	A quotient space is a topology.
|- X = U.J   &   |- Er R   =>   |- (J e. Top -> {x | (x (_ (X/.R) /\ U.x e. J)} e. Top)
Filters
Syntax	cfil 10556	Extend class notation with the class of all filters.
class Fil
Definition	df-fil 10557	The class of all filters. Bourbaki TG I.36 def. 1 axioms FI, FIIa, FIIb, FIII. Filters are used to define the concept of limit in the general case. It's a generalization of the idea of neighborhoods. The problem with the concept of neighborhoods is that ( in RR for instance ) you can't express the idea of a variable which tends to infinity. A work-around for this limitation is to use the idea of limit point. However limit p