mmtheorems170 - 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-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-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19465

Statement List for Metamath Proof Explorer - 16901-17000 - Page 170 of 195

Type	Label	Description
Statement
Theorem	incsequz2 16901	An increasing sequence of natural numbers takes on indefinitely large values.
|- ((F:NN-->NN /\ A.m e. NN (F` m) < (F` (m + 1)) /\ A e. NN) -> E.n e. NN A.k e. (ZZ>=` n)(F` k) e. (ZZ>=` A))
Theorem	seq1eq2 16902	Equality of series based on equality of finitely many terms.
|- S e. _V   &   |- F e. _V   &   |- G e. _V   =>   |- ((N e. NN /\ A.k e. (1...N)(F` k) = (G` k)) -> ((S seq1 F)` N) = ((S seq1 G)` N))
Theorem	nnubfi 16903	A bounded above set of natural numbers is finite.
|- ((A C_ NN /\ B e. NN) -> {x e. A | x < B} e. Fin)
Theorem	nninfnub 16904	An infinite set of natural numbers is unbounded above.
|- ((A C_ NN /\ -. A e. Fin /\ B e. NN) -> {x e. A | B < x} =/= (/))
Theorem	fsum00 16905	A sum of nonnegative numbers is zero iff all terms are zero.
|- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. RR /\ 0 <_ A)) -> (sum_k e. (M...N)A = 0 <-> A.k e. (M...N)A = 0))
Theorem	fsumlt 16906	If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second.
|- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(B e. RR /\ C e. RR /\ B < C)) -> sum_k e. (M...N)B < sum_k e. (M...N)C)
Theorem	fsumltisumii 16907	A partial sum of a series with positive terms is less than the infinite sum.
|- N e. (ZZ>=` M)   &   |- F:(ZZ>=` M)-->RR+   &   |- E.x(<.M, + >. seq F) ~~> x   =>   |- sum_k e. (M...N)(F` k) < sum_k e. (ZZ>=` M)(F` k)
Theorem	fsumltisumi 16908	A partial sum of a series with positive terms is less than the infinite sum.
|- N e. (ZZ>=` M)   =>   |- ((F:(ZZ>=` M)-->RR+ /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (M...N)(F` k) < sum_k e. (ZZ>=` M)(F` k))
Theorem	fsumltisum 16909	A partial sum of a series with positive terms is less than the infinite sum.
|- (((M e. ZZ /\ N e. (ZZ>=` M)) /\ (F:(ZZ>=` M)-->RR+ /\ E.x(<.M, + >. seq F) ~~> x)) -> sum_k e. (M...N)(F` k) < sum_k e. (ZZ>=` M)(F` k))
Theorem	fsumleisumii 16910	A partial sum of a series with nonnegative terms is less than or equal to the infinite sum.
|- N e. (ZZ>=` M)   &   |- F:(ZZ>=` M)-->RR   &   |- A.k e. (ZZ>=` M)0 <_ (F` k)   &   |- E.x(<.M, + >. seq F) ~~> x   =>   |- sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k)
Theorem	fsumleisumi 16911	A partial sum of a series with nonnegative terms is less than or equal to the infinite sum.
|- N e. (ZZ>=` M)   =>   |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k))
Theorem	fsumleisum 16912	A partial sum of a series with nonnegative terms is less than or equal to the infinite sum.
|- (((M e. ZZ /\ N e. (ZZ>=` M)) /\ (F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x)) -> sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k))
Theorem	isumclf 16913	Closure of an infinite sum.
|- (z e. F -> A.k z e. F)   &   |- F e. _V   =>   |- ((M e. ZZ /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (ZZ>=` M)(F` k) e. CC)
Theorem	iserzshft2 16914	Index shift of an infinite series.
|- (((F e. R /\ G e. S) /\ (M e. ZZ /\ K e. ZZ) /\ (A e. B /\ A.k e. (ZZ>=` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)))) -> ((<.M, + >. seq F) ~~> A <-> (<.(M + K), + >. seq G) ~~> A))
Theorem	isumshft2 16915	Index shift of an infinite sum.
|- ((F e. A /\ K e. ZZ /\ M e. ZZ) -> sum_k e. (ZZ>=` (M + K))(F` k) = sum_k e. (ZZ>=` M)(F` (K + k)))
Theorem	fsumlt1 16916	A sum of nonnegative numbers is greater than or equal to any one of its terms.
|- (k = K -> A = B)   =>   |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(A e. RR /\ 0 <_ A) /\ K e. (M...N)) -> B <_ sum_k e. (M...N)A)
Theorem	csbrni 16917	Cauchy-Schwarz-Bunjakovsky inequality for R^n.
|- N e. NN   &   |- X:(1...N)-->RR   &   |- Y:(1...N)-->RR   =>   |- (sum_k e. (1...N)((X` k) x. (Y` k))^2) <_ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))
Theorem	trirni 16918	Triangle inequality in R^n.
|- N e. NN   &   |- X:(1...N)-->RR   &   |- Y:(1...N)-->RR   =>   |- (sqr` sum_k e. (1...N)(((X` k) + (Y` k))^2)) <_ ((sqr` sum_k e. (1...N)((X` k)^2)) + (sqr` sum_k e. (1...N)((Y` k)^2)))
Theorem	trirn 16919	Triangle inequality in R^n.
|- ((N e. NN /\ X:(1...N)-->RR /\ Y:(1...N)-->RR) -> (sqr` sum_k e. (1...N)(((X` k) + (Y` k))^2)) <_ ((sqr` sum_k e. (1...N)((X` k)^2)) + (sqr` sum_k e. (1...N)((Y` k)^2))))
Topology
Theorem	unopnOLD 16920	The union of two open sets is open. (Moved to unopn 9855 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- ((J e. Top /\ A e. J /\ B e. J) -> (A u. B) e. J)
Theorem	incldOLD 16921	The intersection of two closed sets is closed. (Moved to incld 9972 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- ((J e. Top /\ A e. (Clsd` J) /\ B e. (Clsd` J)) -> (A i^i B) e. (Clsd` J))
Theorem	subspopn 16922	An open set is open in the subspace topology.
|- X = U.J   =>   |- (((J e. Top /\ A C_ X) /\ (B e. J /\ B C_ A)) -> B e. (subSp` <.A, J>.))
Theorem	subspcld 16923	A closed set is closed in the subspace topology.
|- X = U.J   =>   |- (((J e. Top /\ A C_ X) /\ (B e. (Clsd` J) /\ B C_ A)) -> B e. (Clsd` (subSp` <.A, J>.)))
Theorem	subspcld2 16924	A set which is closed in the subspace topology induced by a closed set is closed in the original topology.
|- ((J e. Top /\ A e. (Clsd` J) /\ B e. (Clsd` (subSp` <.A, J>.))) -> B e. (Clsd` J))
Theorem	subspabs 16925	Absorption law for subspace.
|- X = U.J   =>   |- ((J e. Top /\ A C_ X /\ B C_ A) -> (subSp` <.B, (subSp` <.A, J>.)>.) = (subSp` <.B, J>.))
Theorem	neificl 16926	Neighborhoods are closed under finite intersection.
|- X = U.J   =>   |- (((J e. Top /\ N C_ ((nei` J)` S)) /\ (N e. Fin /\ N =/= (/))) -> |^|N e. ((nei` J)` S))
Theorem	lpss2 16927	Limit points of a subset are limit points of the larger set.
|- X = U.J   =>   |- ((J e. Top /\ A C_ X /\ B C_ A) -> ((limPt` J)` B) C_ ((limPt` J)` A))
Metric spaces
Theorem	metf1o 16928	Use a bijection with a metric space to construct a metric on a set.
|- X = dom dom M   &   |- N = {<.<.x, y>., z>. | ((x e. Y /\ y e. Y) /\ z = ((F` x)M(F` y)))}   =>   |- ((Y e. A /\ M e. Met /\ F:Y-1-1-onto->X) -> N e. Met)
Theorem	blssp 16929	A ball in the subspace metric.
|- X = dom dom M   &   |- N = (M |` (S X. S))   =>   |- (((M e. Met /\ S C_ X) /\ (Y e. S /\ R e. RR+)) -> (Y( ball ` N)R) = ((Y( ball ` M)R) i^i S))
Theorem	stioo 16930	Two ways of expressing a subspace of RR.
|- (A C_ RR -> (subSp` <.A, (topGen` ran (,))>.) = (MetOpen` ((abs o. - ) |` (A X. A))))
Theorem	blhalf 16931	A ball of radius R / 2 is contained in a ball of radius R centered at any point inside the smaller ball.
|- X = dom dom M   =>   |- (((M e. Met /\ Y e. X) /\ (R e. RR+ /\ Z e. (Y( ball ` M)(R / 2)))) -> (Y( ball ` M)(R / 2)) C_ (Z( ball ` M)R))
Theorem	mettrifi 16932	Generalized triangle inequality for arbitrary finite sums.
|- X = dom dom M   =>   |- (((M e. Met /\ N e. NN) /\ (A.k e. (1...(N + 1))(F` k) e. X /\ A.k e. (1...N)(G` k) = ((F` k)M(F` (k + 1))))) -> ((F` 1)M(F` (N + 1))) <_ sum_k e. (1...N)(G` k))
Theorem	mettrifi2 16933	Generalized triangle inequality for arbitrary finite sums.
|- X = dom dom M   &   |- S e. _V   =>   |- (((M e. Met /\ F:S-->X) /\ (N e. ZZ /\ P e. (ZZ>=` (N + 1)) /\ (N...P) C_ S)) -> ((F` N)M(F` P)) <_ sum_k e. (N...(P - 1))((F` k)M(F` (k + 1))))
Theorem	geomcau 16934	If the distance between consecutive points in a sequence is bounded by a geometric sequence, then the sequence is Cauchy.
|- X = dom dom M   =>   |- (((M e. Met /\ F:NN-->X) /\ (A e. RR /\ B e. RR+ /\ B < 1) /\ A.k e. NN ((F` k)M(F` (k + 1))) <_ (A x. (B^k))) -> F e. (Cau` M))
Theorem	lmclim2 16935	A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0.
|- X = dom dom M   &   |- G = {<.x, y>. | (x e. NN /\ y = ((F` x)MY))}   =>   |- ((M e. Met /\ F:NN-->X /\ Y e. X) -> (F(~~>m` M)Y <-> G ~~> 0))
Theorem	caushft 16936	A shifted Cauchy sequence is Cauchy.
|- K e. NN   &   |- N e. NN   &   |- Z = (ZZ>=` K)   &   |- W = (ZZ>=` (K + N))   &   |- X = dom dom M   =>   |- ((M e. Met /\ (F:Z-->X /\ G:W-->X) /\ A.k e. Z (F` k) = (G` (k + N))) -> (F e. (Cau` M) <-> G e. (Cau` M)))
Theorem	caures 16937	The restriction of a Cauchy sequence to a set of upper integers is Cauchy.
|- X = dom dom M   &   |- N e. ZZ   &   |- Z = (ZZ>=` N)   =>   |- ((M e. Met /\ F C_ (CC X. X)) -> (F e. (Cau` M) <-> (F |` Z) e. (Cau` M)))
Theorem	metdcn 16938	The function which gives the distance to a fixed point in a metric space is a continuous function into nonnegative reals.
|- X = dom dom M   &   |- J = (MetOpen` M)   &   |- R = (MetOpen` ((abs o. - ) |` ((0[,) +oo) X. (0[,) +oo))))   &   |- D = {<.x, y>. | (x e. X /\ y = (YMx))}   =>   |- ((M e. Met /\ Y e. X) -> D e. (J Cn R))
Intervals
Theorem	iccsplit 16939	Split a closed interval into the union of two closed intervals.
|- ((A e. RR /\ B e. RR /\ C e. (A[,]B)) -> (A[,]B) = ((A[,]C) u. (C[,]B)))
Theorem	iccss 16940	Condition for a closed interval to be a subset of another closed interval.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR) /\ (A <_ C /\ D <_ B)) -> (C[,]D) C_ (A[,]B))
Theorem	iccss2 16941	Condition for a closed interval to be a subset of another closed interval.
|- ((A e. RR /\ B e. RR) -> ((C e. (A[,]B) /\ D e. (A[,]B)) -> (C[,]D) C_ (A[,]B)))
Theorem	iccshftr 16942	Membership in a shifted interval.
|- (A + R) = C   &   |- (B + R) = D   =>   |- (((A e. RR /\ B e. RR) /\ (X e. RR /\ R e. RR)) -> (X e. (A[,]B) <-> (X + R) e. (C[,]D)))
Theorem	iccshftri 16943	Membership in a shifted interval.
|- A e. RR   &   |- B e. RR   &   |- R e. RR   &   |- (A + R) = C   &   |- (B + R) = D   =>   |- (X e. (A[,]B) -> (X + R) e. (C[,]D))
Theorem	iccshftl 16944	Membership in a shifted interval.
|- (A - R) = C   &   |- (B - R) = D   =>   |- (((A e. RR /\ B e. RR) /\ (X e. RR /\ R e. RR)) -> (X e. (A[,]B) <-> (X - R) e. (C[,]D)))
Theorem	iccshftli 16945	Membership in a shifted interval.
|- A e. RR   &   |- B e. RR   &   |- R e. RR   &   |- (A - R) = C   &   |- (B - R) = D   =>   |- (X e. (A[,]B) -> (X - R) e. (C[,]D))
Theorem	iccdil 16946	Membership in a dilated interval.
|- (A x. R) = C   &   |- (B x. R) = D   =>   |- (((A e. RR /\ B e. RR) /\ (X e. RR /\ R e. RR+)) -> (X e. (A[,]B) <-> (X x. R) e. (C[,]D)))
Theorem	iccdili 16947	Membership in a dilated interval.
|- A e. RR   &   |- B e. RR   &   |- R e. RR+   &   |- (A x. R) = C   &   |- (B x. R) = D   =>   |- (X e. (A[,]B) -> (X x. R) e. (C[,]D))
Theorem	icccntr 16948	Membership in a contracted interval.
|- (A / R) = C   &   |- (B / R) = D   =>   |- (((A e. RR /\ B e. RR) /\ (X e. RR /\ R e. RR+)) -> (X e. (A[,]B) <-> (X / R) e. (C[,]D)))
Theorem	icccntri 16949	Membership in a contracted interval.
|- A e. RR   &   |- B e. RR   &   |- R e. RR+   &   |- (A / R) = C   &   |- (B / R) = D   =>   |- (X e. (A[,]B) -> (X / R) e. (C[,]D))
Syntax	cii 16950	Extend class notation with the unit interval.
class II
Definition	df-ii 16951	Define the unit interval with the Euclidean topology.
|- II = (MetOpen` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
Theorem	iitop 16952	The unit interval is a topological space.
|- II e. Top
Theorem	iiuni 16953	The base set of the unit interval.
|- (0[,]1) = U.II
Theorem	dfii2 16954	Alternate definition of the unit interval.
|- II = (subSp` <.(0[,]1), (topGen` ran (,))>.)
Theorem	dfii3 16955	Alternate definition of the unit interval.
|- II = (subSp` <.(0[,]1), (MetOpen` (abs o. - ))>.)
Theorem	iirev 16956	Reverse the unit interval.
|- (X e. (0[,]1) -> (1 - X) e. (0[,]1))
Theorem	iihalf1 16957	Map the first half of II into II.
|- (X e. (0[,](1 / 2)) -> (2 x. X) e. (0[,]1))
Theorem	iihalf2 16958	Map the second half of II into II.
|- (X e. ((1 / 2)[,]1) -> ((2 x. X) - 1) e. (0[,]1))
Theorem	iimulcl 16959	The unit interval is closed under multiplication.
|- ((A e. (0[,]1) /\ B e. (0[,]1)) -> (A x. B) e. (0[,]1))
Theorem	iccst 16960	The subspace topology induced by a closed interval.
|- R = (topGen` ran (,))   &   |- J = (MetOpen` ((abs o. - ) |` ((A[,]B) X. (A[,]B))))   =>   |- ((A e. RR /\ B e. RR) -> J = (subSp` <.(A[,]B), R>.))
Theorem	icoopnst 16961	A half-open interval starting at A is open in the closed interval from A to B.
|- J = (MetOpen` ((abs o. - ) |` ((A[,]B) X. (A[,]B))))   =>   |- ((A e. RR /\ B e. RR) -> (C e. (A(,]B) -> (A[,)C) e. J))
Theorem	iocopnst 16962	A half-open interval ending at B is open in the closed interval from A to B.
|- J = (MetOpen` ((abs o. - ) |` ((A[,]B) X. (A[,]B))))   =>   |- ((A e. RR /\ B e. RR) -> (C e. (A[,)B) -> (C(,]B) e. J))
Theorem	lincmb01cmp 16963	A linear combination of two reals which lies in the interval between them.
|- (((A e. RR /\ B e. RR /\ A < B) /\ T e. (0[,]1)) -> (((1 - T) x. A) + (T x. B)) e. (A[,]B))
Theorem	lincmb01icc 16964	A linear combination of two reals which lies in the interval between them.
|- ((A e. RR /\ B e. RR) -> ((C e. (A[,]B) /\ D e. (A[,]B) /\ T e. (0[,]1)) -> (((1 - T) x. C) + (T x. D)) e. (A[,]B)))
Theorem	oprpiece1res1 16965	Restriction to the first part of a piecewise defined function.
|- A e. RR   &   |- B e. RR   &   |- A <_ B   &   |- R e. _V   &   |- S e. _V   &   |- K e. (A[,]B)   &   |- F = {<.<.x, y>., z>. | ((x e. (A[,]B) /\ y e. C) /\ z = if(x <_ K, R, S))}   &   |- G = {<.<.x, y>., z>. | ((x e. (A[,]K) /\ y e. C) /\ z = R)}   =>   |- (F |` ((A[,]K) X. C)) = G
Theorem	oprpiece1res2 16966	Restriction to the second part of a piecewise defined function.
|- A e. RR   &   |- B e. RR   &   |- A <_ B   &   |- R e. _V   &   |- S e. _V   &   |- K e. (A[,]B)   &   |- F = {<.<.x, y>., z>. | ((x e. (A[,]B) /\ y e. C) /\ z = if(x <_ K, R, S))}   &   |- (x = K -> R = P)   &   |- (x = K -> S = Q)   &   |- (y e. C -> P = Q)   &   |- G = {<.<.x, y>., z>. | ((x e. (K[,]B) /\ y e. C) /\ z = S)}   =>   |- (F |` ((K[,]B) X. C)) = G
Continuous maps and homeomorphisms
Theorem	constcncf 16967	A constant function is a continuous function on CC.
|- F = {<.x, y>. | (x e. CC /\ y = A)}   =>   |- (A e. CC -> F e. (CC-cn->CC))
Theorem	addccncf 16968	Adding a constant is a continuous function.
|- F = {<.x, y>. | (x e. CC /\ y = (x + A))}   =>   |- (A e. CC -> F e. (CC-cn->CC))
Theorem	idcncf 16969	The identity function is a continuous function on CC.
|- F = {<.x, y>. | (x e. CC /\ y = x)}   =>   |- F e. (CC-cn->CC)
Theorem	sub1cncf 16970	Subtracting a constant is a continuous function.
|- F = {<.x, y>. | (x e. CC /\ y = (x - A))}   =>   |- (A e. CC -> F e. (CC-cn->CC))
Theorem	sub2cncf 16971	Subtraction from a constant is a continuous function.
|- F = {<.x, y>. | (x e. CC /\ y = (A - x))}   =>   |- (A e. CC -> F e. (CC-cn->CC))
Theorem	cncfco 16972	The composition of two continuous maps on complex numbers is also continuous.
|- (((A C_ CC /\ B C_ CC /\ C C_ CC) /\ (F e. (A-cn->B) /\ G e. (B-cn->C))) -> (G o. F) e. (A-cn->C))
Theorem	cnimass 16973	Restriction of the image of a continuous function.
|- X = U.J   &   |- Y = U.K   =>   |- (((J e. Top /\ K e. Top /\ F e. (J Cn K)) /\ (A C_ Y /\ A.x e. X (F` x) e. A)) -> F e. (J Cn (subSp` <.A, K>.)))
Theorem	cnres 16974	The restriction of a continuous function to a subset is continuous.
|- X = U.J   =>   |- (((J e. Top /\ K e. Top) /\ (F e. (J Cn K) /\ A C_ X)) -> (F |` A) e. ((subSp` <.A, J>.) Cn K))
Theorem	cnres2 16975	The restriction of a continuous function to a subset is continuous.
|- X = U.J   &   |- Y = U.K   =>   |- (((J e. Top /\ K e. Top) /\ (A C_ X /\ B C_ Y) /\ (F e. (J Cn K) /\ A.x e. A (F` x) e. B)) -> (F |` A) e. ((subSp` <.A, J>.) Cn (subSp` <.B, K>.)))
Theorem	cnresima 16976	A continuous function is continuous onto its image.
|- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> F e. (J Cn (subSp` <.ran F, K>.)))
Theorem	cnss 16977	A continuous function into a subspace is continuous into the larger space.
|- Y = U.K   =>   |- (((J e. Top /\ K e. Top) /\ (A C_ Y /\ F e. (J Cn (subSp` <.A, K>.)))) -> F e. (J Cn K))
Theorem	paste 16978	Pasting lemma. If A and B are closed sets in X with A u. B = X, then any function whose restrictions to A and B are continuous is continuous on all of X.
|- X = U.J   &   |- Y = U.K   =>   |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> F e. (J Cn K))
Theorem	piececn 16979	Piecewise definition of a continuous function on a real interval.
|- A e. RR   &   |- B e. RR   &   |- C e. (A[,]B)   &   |- R e. _V   &   |- S e. _V   &   |- F = {<.x, y>. | (x e. (A[,]B) /\ y = if(x <_ C, R, S))}   &   |- J = (subSp` <.(A[,]B), (topGen` ran (,))>.)   &   |- K = (subSp` <.(A[,]C), (topGen` ran (,))>.)   &   |- L = (subSp` <.(C[,]B), (topGen` ran (,))>.)   &   |- (x = C -> R = S)   &   |- G = {<.x, y>. | (x e. (A[,]C) /\ y = R)}   &   |- H = {<.x, y>. | (x e. (C[,]B) /\ y = S)}   &   |- M e. Top   &   |- G e. (K Cn M)   &   |- H e. (L Cn M)   =>   |- F e. (J Cn M)
Theorem	cncfres 16980	A continuous function on complex numbers restricted to a subset.
|- A C_ CC   &   |- B C_ CC   &   |- F = {<.x, y>. | (x e. CC /\ y = C)}   &   |- G = {<.x, y>. | (x e. A /\ y = C)}   &   |- (x e. A -> C e. B)   &   |- F e. (CC-cn->CC)   &   |- J = (MetOpen` ((abs o. - ) |` (A X. A)))   &   |- K = (MetOpen` ((abs o. - ) |` (B X. B)))   =>   |- G e. (J Cn K)
Theorem	ishomeo2 16981	The predicate "is a homeomorphism".
|- X = U.J   &   |- Y = U.K   =>   |- ((J e. Top /\ K e. Top) -> (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	hmeocn 16982	A homeomorphism is continuous.
|- ((J e. Top /\ K e. Top) -> (F e. (J Homeo K) -> F e. (J Cn K)))
Theorem	hmeocnv 16983	The inverse of a homeomorphism is a homeomorphism.
|- (((J e. Top /\ K e. Top) /\ F e. (J Homeo K)) -> `'F e. (K Homeo J))
Theorem	hmeoopn 16984	Homeomorphisms preserve openness.
|- X = U.J   =>   |- (((J e. Top /\ K e. Top) /\ (F e. (J Homeo K) /\ A C_ X)) -> (A e. J <-> (F"A) e. K))
Theorem	hmeocld 16985	Homeomorphisms preserve closedness.
|- X = U.J   =>   |- (((J e. Top /\ K e. Top) /\ (F e. (J Homeo K) /\ A C_ X)) -> (A e. (Clsd` J) <-> (F"A) e. (Clsd` K)))
Topological limits
Syntax	ctlm 16986	Extend class notation with the topological convergence relation.
class ~~>t
Definition	df-tlm 16987	Define the convergence relation on sequences in a topological space. A sequence f converges to a point x if for every open neighborhood U of x, for all large enough m we have f(m) e. U.
|- ~~>t = {<.j, r>. | (j e. Top /\ r = {<.f, x>. | (f:NN-->U.j /\ x e. U.j /\ A.u e. ((nei` j)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})}
Theorem	tlmval 16988	The convergence relation on sequences in a topological space.
|- X = U.J   =>   |- (J e. Top -> (~~>t` J) = {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})
Theorem	tlmbr 16989	The binary relation "F converges to Y topologically".
|- X = U.J   =>   |- ((J e. Top /\ Y e. A) -> (F(~~>t` J)Y <-> (F:NN-->X /\ Y e. X /\ A.u e. ((nei` J)` {Y})E.n e. NN A.m e. (ZZ>=` n)(F` m) e. u)))
Theorem	tlmbrf 16990	The binary relation "F converges to Y topologically".
|- X = U.J   =>   |- ((J e. Top /\ Y e. A /\ F:NN-->X) -> (F(~~>t` J)Y <-> (Y e. X /\ A.u e. ((nei` J)` {Y})E.n e. NN A.m e. (ZZ>=` n)(F` m) e. u)))
Theorem	haustlmu 16991	Limits are unique in a Hausdorff space.
|- X = U.J   =>   |- (J e. Haus -> E*x F(~~>t` J)x)
Theorem	tlmconst 16992	A constant sequence converges to the constant.
|- X = U.J   =>   |- ((J e. Top /\ Y e. X) -> (NN X. {Y})(~~>t` J)Y)
Theorem	lmtlm 16993	Metric space limits are topological limits under the standard topology.
|- J = (MetOpen` M)   &   |- X = dom dom M   =>   |- ((M e. Met /\ Y e. A /\ F:NN-->X) -> (F(~~>t` J)Y <-> F(~~>m` M)Y))
Product topologies
Theorem	txtopiOLD 16994	The product of two topologies is a topology. (Moved to txtopi 9943 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- R e. Top   &   |- S e. Top   =>   |- (R X.t S) e. Top
Theorem	txuniiOLD 16995	The underlying set of the product of two topologies. (Moved to txunii 9945 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- R e. Top   &   |- S e. Top   &   |- X = U.R   &   |- Y = U.S   =>   |- (X X. Y) = U.(R X.t S)
Theorem	txcnoprab 16996	A map into the product of two topological spaces is continuous if both of its projections are continuous.
|- T = (R X.t S)   &   |- X = U.U   &   |- Y = U.W   &   |- Z = (U X.t W)   &   |- H = {<.<.x, y>., z>. | ((x e. X /\ y e. Y) /\ z = <.(xFy), (xGy)>.)}   =>   |- (((R e. Top /\ S e. Top) /\ (U e. Top /\ W e. Top) /\ (F e. (Z Cn R) /\ G e. (Z Cn S))) -> H e. (Z Cn T))
Theorem	txsubsp 16997	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.
|- X = U.R   &   |- Y = U.S   =>   |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (subSp` <.(A X. B), (R X.t S)>.) = ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)))
Theorem	txopnOLD 16998	The product of two open sets is open in the product topology. (Moved to txopn 9946 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- T = (R X.t S)   =>   |- (((R e. Top /\ S e. Top) /\ (A e. R /\ B e. S)) -> (A X. B) e. T)
Theorem	txcldOLD 16999	The product of two closed sets is closed in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to txcld 10002 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- T = (R X.t S)   =>   |- (((R e. Top /\ S e. Top) /\ (A e. (Clsd` R) /\ B e. (Clsd` S))) -> (A X. B) e. (Clsd` T))
Theorem	cnresoprab 17000	Continuity of a restricted operation abstraction.
|- A = U.J   &   |- B = U.K   &   |- S = U.L   &   |- C C_ A   &   |- D C_ B   &   |- T C_ S   &   |- ((x e. C /\ y e. D) -> R e. T)   &   |- F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = R)}   &   |- G = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ z = R)}   &   |- J e. Top   &   |- K e. Top   &   |- L e. Top   &   |- F e. ((J X.t K) Cn L)   =>   |- G e. ((subSp` <.(C X. D), (J X.t K)>.) Cn (subSp` <.T, L>.))