![]() |
Metamath
Proof Explorer Theorem List (p. 244 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cnfldhaus 24301 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Haus | ||
Theorem | unicntop 24302 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β = βͺ (TopOpenββfld) | ||
Theorem | cnopn 24303 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β β (TopOpenββfld) | ||
Theorem | zringnrg 24304 | The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β NrmRing | ||
Theorem | remetdval 24305 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (absβ(π΄ β π΅))) | ||
Theorem | remet 24306 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ π· β (Metββ) | ||
Theorem | rexmet 24307 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ π· β (βMetββ) | ||
Theorem | bl2ioo 24308 | A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(ballβπ·)π΅) = ((π΄ β π΅)(,)(π΄ + π΅))) | ||
Theorem | ioo2bl 24309 | An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(,)π΅) = (((π΄ + π΅) / 2)(ballβπ·)((π΅ β π΄) / 2))) | ||
Theorem | ioo2blex 24310 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(,)π΅) β ran (ballβπ·)) | ||
Theorem | blssioo 24311 | The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) β β’ ran (ballβπ·) β ran (,) | ||
Theorem | tgioo 24312 | The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π½ = (MetOpenβπ·) β β’ (topGenβran (,)) = π½ | ||
Theorem | qdensere2 24313 | β is dense in β. (Contributed by NM, 24-Aug-2007.) |
β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π½ = (MetOpenβπ·) β β’ ((clsβπ½)ββ) = β | ||
Theorem | blcvx 24314 | An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ π = (π(ballβ(abs β β ))π ) β β’ (((π β β β§ π β β*) β§ (π΄ β π β§ π΅ β π β§ π β (0[,]1))) β ((π Β· π΄) + ((1 β π) Β· π΅)) β π) | ||
Theorem | rehaus 24315 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
β’ (topGenβran (,)) β Haus | ||
Theorem | tgqioo 24316 | The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π = (topGenβ((,) β (β Γ β))) β β’ (topGenβran (,)) = π | ||
Theorem | re2ndc 24317 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (topGenβran (,)) β 2ndΟ | ||
Theorem | resubmet 24318 | The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.) |
β’ π = (topGenβran (,)) & β’ π½ = (MetOpenβ((abs β β ) βΎ (π΄ Γ π΄))) β β’ (π΄ β β β π½ = (π βΎt π΄)) | ||
Theorem | tgioo2 24319 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) |
β’ π½ = (TopOpenββfld) β β’ (topGenβran (,)) = (π½ βΎt β) | ||
Theorem | rerest 24320 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ π = (topGenβran (,)) β β’ (π΄ β β β (π½ βΎt π΄) = (π βΎt π΄)) | ||
Theorem | tgioo3 24321 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.) |
β’ π½ = (TopOpenββfld) β β’ (topGenβran (,)) = π½ | ||
Theorem | xrtgioo 24322 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to β. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π½ = ((ordTopβ β€ ) βΎt β) β β’ (topGenβran (,)) = π½ | ||
Theorem | xrrest 24323 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = (ordTopβ β€ ) & β’ π = (topGenβran (,)) β β’ (π΄ β β β (π βΎt π΄) = (π βΎt π΄)) | ||
Theorem | xrrest2 24324 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ π = (ordTopβ β€ ) β β’ (π΄ β β β (π½ βΎt π΄) = (π βΎt π΄)) | ||
Theorem | xrsxmet 24325 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ π· = (distββ*π ) β β’ π· β (βMetββ*) | ||
Theorem | xrsdsre 24326 | The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ π· = (distββ*π ) β β’ (π· βΎ (β Γ β)) = ((abs β β ) βΎ (β Γ β)) | ||
Theorem | xrsblre 24327 | Any ball of the metric of the extended reals centered on an element of β is entirely contained in β. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ π· = (distββ*π ) β β’ ((π β β β§ π β β*) β (π(ballβπ·)π ) β β) | ||
Theorem | xrsmopn 24328 | The metric on the extended reals generates a topology, but this does not match the order topology on β*; for example {+β} is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ π· = (distββ*π ) & β’ π½ = (MetOpenβπ·) β β’ (ordTopβ β€ ) β π½ | ||
Theorem | zcld 24329 | The integers are a closed set in the topology on β. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π½ = (topGenβran (,)) β β’ β€ β (Clsdβπ½) | ||
Theorem | recld2 24330 | The real numbers are a closed set in the topology on β. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π½ = (TopOpenββfld) β β’ β β (Clsdβπ½) | ||
Theorem | zcld2 24331 | The integers are a closed set in the topology on β. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π½ = (TopOpenββfld) β β’ β€ β (Clsdβπ½) | ||
Theorem | zdis 24332 | The integers are a discrete set in the topology on β. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ (π½ βΎt β€) = π« β€ | ||
Theorem | sszcld 24333 | Every subset of the integers are closed in the topology on β. (Contributed by Mario Carneiro, 6-Jul-2017.) |
β’ π½ = (TopOpenββfld) β β’ (π΄ β β€ β π΄ β (Clsdβπ½)) | ||
Theorem | reperflem 24334* | A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π½ = (TopOpenββfld) & β’ ((π’ β π β§ π£ β β) β (π’ + π£) β π) & β’ π β β β β’ (π½ βΎt π) β Perf | ||
Theorem | reperf 24335 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π½ = (TopOpenββfld) β β’ (π½ βΎt β) β Perf | ||
Theorem | cnperf 24336 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Perf | ||
Theorem | iccntr 24337 | The interior of a closed interval in the standard topology on β is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β) β ((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) | ||
Theorem | icccmplem1 24338* | Lemma for icccmp 24341. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) β β’ (π β (π΄ β π β§ βπ¦ β π π¦ β€ π΅)) | ||
Theorem | icccmplem2 24339* | Lemma for icccmp 24341. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β π β π) & β’ (π β πΆ β β+) & β’ (π β (πΊ(ballβπ·)πΆ) β π) & β’ πΊ = sup(π, β, < ) & β’ π = if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β β’ (π β π΅ β π) | ||
Theorem | icccmplem3 24340* | Lemma for icccmp 24341. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) β β’ (π β π΅ β π) | ||
Theorem | icccmp 24341 | A closed interval in β is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) β β’ ((π΄ β β β§ π΅ β β) β π β Comp) | ||
Theorem | reconnlem1 24342 | Lemma for reconn 24344. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
β’ (((π΄ β β β§ ((topGenβran (,)) βΎt π΄) β Conn) β§ (π β π΄ β§ π β π΄)) β (π[,]π) β π΄) | ||
Theorem | reconnlem2 24343* | Lemma for reconn 24344. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
β’ (π β π΄ β β) & β’ (π β π β (topGenβran (,))) & β’ (π β π β (topGenβran (,))) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) & β’ (π β π΅ β (π β© π΄)) & β’ (π β πΆ β (π β© π΄)) & β’ (π β (π β© π) β (β β π΄)) & β’ (π β π΅ β€ πΆ) & β’ π = sup((π β© (π΅[,]πΆ)), β, < ) β β’ (π β Β¬ π΄ β (π βͺ π)) | ||
Theorem | reconn 24344* | A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
β’ (π΄ β β β (((topGenβran (,)) βΎt π΄) β Conn β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄)) | ||
Theorem | retopconn 24345 | Corollary of reconn 24344. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
β’ (topGenβran (,)) β Conn | ||
Theorem | iccconn 24346 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β Conn) | ||
Theorem | opnreen 24347 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
β’ ((π΄ β (topGenβran (,)) β§ π΄ β β ) β π΄ β π« β) | ||
Theorem | rectbntr0 24348 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π΄ β β β§ π΄ βΌ β) β ((intβ(topGenβran (,)))βπ΄) = β ) | ||
Theorem | xrge0gsumle 24349 | A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) & β’ (π β π΅ β (π« π΄ β© Fin)) & β’ (π β πΆ β π΅) β β’ (π β (πΊ Ξ£g (πΉ βΎ πΆ)) β€ (πΊ Ξ£g (πΉ βΎ π΅))) | ||
Theorem | xrge0tsms 24350* | Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Proof shortened by AV, 26-Jul-2019.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆ(0[,]+β)) & β’ π = sup(ran (π β (π« π΄ β© Fin) β¦ (πΊ Ξ£g (πΉ βΎ π ))), β*, < ) β β’ (π β (πΊ tsums πΉ) = {π}) | ||
Theorem | xrge0tsms2 24351 | Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set [0, +β]; a similar theorem is not true for β* or β or [0, +β). It is true for β0 βͺ {+β}, however, or more generally any additive submonoid of [0, +β) with +β adjoined. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ πΊ = (β*π βΎs (0[,]+β)) β β’ ((π΄ β π β§ πΉ:π΄βΆ(0[,]+β)) β (πΊ tsums πΉ) β 1o) | ||
Theorem | metdcnlem 24352 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ πΆ = (distββ*π ) & β’ πΎ = (MetOpenβπΆ) & β’ (π β π· β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄π·π) < (π / 2)) & β’ (π β (π΅π·π) < (π / 2)) β β’ (π β ((π΄π·π΅)πΆ(ππ·π)) < π ) | ||
Theorem | xmetdcn2 24353 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 24354 we use the metric topology instead of the order topology on β*, which makes the theorem a bit stronger. Since +β is an isolated point in the metric topology, this is saying that for any points π΄, π΅ which are an infinite distance apart, there is a product neighborhood around β¨π΄, π΅β© such that π(π, π) = +β for any π near π΄ and π near π΅, i.e., the distance function is locally constant +β. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ πΆ = (distββ*π ) & β’ πΎ = (MetOpenβπΆ) β β’ (π· β (βMetβπ) β π· β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | xmetdcn 24354 | The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ πΎ = (ordTopβ β€ ) β β’ (π· β (βMetβπ) β π· β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | metdcn2 24355 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ πΎ = (topGenβran (,)) β β’ (π· β (Metβπ) β π· β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | metdcn 24356 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ πΎ = (TopOpenββfld) β β’ (π· β (Metβπ) β π· β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | msdcn 24357 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = (distβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (topGenβran (,)) β β’ (π β MetSp β (π· βΎ (π Γ π)) β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | cnmpt1ds 24358* | Continuity of the metric function; analogue of cnmpt12f 23170 which cannot be used directly because π· is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π· = (distβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (topGenβran (,)) & β’ (π β πΊ β MetSp) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn π½)) & β’ (π β (π₯ β π β¦ π΅) β (πΎ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄π·π΅)) β (πΎ Cn π )) | ||
Theorem | cnmpt2ds 24359* | Continuity of the metric function; analogue of cnmpt22f 23179 which cannot be used directly because π· is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π· = (distβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = (topGenβran (,)) & β’ (π β πΊ β MetSp) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄π·π΅)) β ((πΎ Γt πΏ) Cn π )) | ||
Theorem | nmcn 24360 | The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (topGenβran (,)) β β’ (πΊ β NrmGrp β π β (π½ Cn πΎ)) | ||
Theorem | ngnmcncn 24361 | The norm of a normed group is a continuous function to β. (Contributed by NM, 12-Aug-2007.) (Revised by AV, 17-Oct-2021.) |
β’ π = (normβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenββfld) β β’ (πΊ β NrmGrp β π β (π½ Cn πΎ)) | ||
Theorem | abscn 24362 | The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (topGenβran (,)) β β’ abs β (π½ Cn πΎ) | ||
Theorem | metdsval 24363* | Value of the "distance to a set" function. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Revised by AV, 30-Sep-2020.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ (π΄ β π β (πΉβπ΄) = inf(ran (π¦ β π β¦ (π΄π·π¦)), β*, < )) | ||
Theorem | metdsf 24364* | The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) | ||
Theorem | metdsge 24365* | The distance from the point π΄ to the set π is greater than π iff the π -ball around π΄ misses π. (Contributed by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π β β*) β (π β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)π )) = β )) | ||
Theorem | metds0 24366* | If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) = 0) | ||
Theorem | metdstri 24367* | A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol π denotes the point-point and point-set distance functions, this theorem would be written π(π, π) β€ π(π, π) + π(π, π). (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΄) β€ ((π΄π·π΅) +π (πΉβπ΅))) | ||
Theorem | metdsle 24368* | The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ (((π· β (βMetβπ) β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (πΉβπ΅) β€ (π΄π·π΅)) | ||
Theorem | metdsre 24369* | The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) β β’ ((π· β (Metβπ) β§ π β π β§ π β β ) β πΉ:πβΆβ) | ||
Theorem | metdseq0 24370* | The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((πΉβπ΄) = 0 β π΄ β ((clsβπ½)βπ))) | ||
Theorem | metdscnlem 24371* | Lemma for metdscn 24372. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ πΆ = (distββ*π ) & β’ πΎ = (MetOpenβπΆ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) & β’ (π β (π΄π·π΅) < π ) β β’ (π β ((πΉβπ΄) +π -π(πΉβπ΅)) < π ) | ||
Theorem | metdscn 24372* | The function πΉ which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ πΆ = (distββ*π ) & β’ πΎ = (MetOpenβπΆ) β β’ ((π· β (βMetβπ) β§ π β π) β πΉ β (π½ Cn πΎ)) | ||
Theorem | metdscn2 24373* | The function πΉ which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ πΎ = (TopOpenββfld) β β’ ((π· β (Metβπ) β§ π β π β§ π β β ) β πΉ β (π½ Cn πΎ)) | ||
Theorem | metnrmlem1a 24374* | Lemma for metnrm 24378. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β (Clsdβπ½)) & β’ (π β π β (Clsdβπ½)) & β’ (π β (π β© π) = β ) β β’ ((π β§ π΄ β π) β (0 < (πΉβπ΄) β§ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β β+)) | ||
Theorem | metnrmlem1 24375* | Lemma for metnrm 24378. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β (Clsdβπ½)) & β’ (π β π β (Clsdβπ½)) & β’ (π β (π β© π) = β ) β β’ ((π β§ (π΄ β π β§ π΅ β π)) β if(1 β€ (πΉβπ΅), 1, (πΉβπ΅)) β€ (π΄π·π΅)) | ||
Theorem | metnrmlem2 24376* | Lemma for metnrm 24378. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β (Clsdβπ½)) & β’ (π β π β (Clsdβπ½)) & β’ (π β (π β© π) = β ) & β’ π = βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β β’ (π β (π β π½ β§ π β π)) | ||
Theorem | metnrmlem3 24377* | Lemma for metnrm 24378. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β (Clsdβπ½)) & β’ (π β π β (Clsdβπ½)) & β’ (π β (π β© π) = β ) & β’ π = βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) & β’ πΊ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π = βͺ π β π (π (ballβπ·)(if(1 β€ (πΊβπ ), 1, (πΊβπ )) / 2)) β β’ (π β βπ§ β π½ βπ€ β π½ (π β π§ β§ π β π€ β§ (π§ β© π€) = β )) | ||
Theorem | metnrm 24378 | A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013.) (Revised by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β Nrm) | ||
Theorem | metreg 24379 | A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β Reg) | ||
Theorem | addcnlem 24380* | Lemma for addcn 24381, subcn 24382, and mulcn 24383. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ + :(β Γ β)βΆβ & β’ ((π β β+ β§ π β β β§ π β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) β β’ + β ((π½ Γt π½) Cn π½) | ||
Theorem | addcn 24381 | Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ + β ((π½ Γt π½) Cn π½) | ||
Theorem | subcn 24382 | Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ β β ((π½ Γt π½) Cn π½) | ||
Theorem | mulcn 24383 | Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ Β· β ((π½ Γt π½) Cn π½) | ||
Theorem | divcn 24384 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt (β β {0})) β β’ / β ((π½ Γt πΎ) Cn π½) | ||
Theorem | cnfldtgp 24385 | The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ βfld β TopGrp | ||
Theorem | fsumcn 24386* | A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for π΅ normally contains free variables π and π₯ to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) | ||
Theorem | fsum2cn 24387* | Version of fsumcn 24386 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ (π β πΏ β (TopOnβπ)) & β’ ((π β§ π β π΄) β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΏ) Cn πΎ)) β β’ (π β (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) β ((π½ Γt πΏ) Cn πΎ)) | ||
Theorem | expcn 24388* | The power function on complex numbers, for fixed exponent π, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ π½ = (TopOpenββfld) β β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (π½ Cn π½)) | ||
Theorem | divccn 24389* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β β¦ (π₯ / π΄)) β (π½ Cn π½)) | ||
Theorem | sqcn 24390* | The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ (π₯ β β β¦ (π₯β2)) β (π½ Cn π½) | ||
Syntax | cii 24391 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 24392 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class βcnβ | ||
Definition | df-ii 24393 | Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ II = (MetOpenβ((abs β β ) βΎ ((0[,]1) Γ (0[,]1)))) | ||
Definition | df-cncf 24394* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
β’ βcnβ = (π β π« β, π β π« β β¦ {π β (π βm π) β£ βπ₯ β π βπ β β+ βπ β β+ βπ¦ β π ((absβ(π₯ β π¦)) < π β (absβ((πβπ₯) β (πβπ¦))) < π)}) | ||
Theorem | iitopon 24395 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ II β (TopOnβ(0[,]1)) | ||
Theorem | iitop 24396 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II β Top | ||
Theorem | iiuni 24397 | The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.) |
β’ (0[,]1) = βͺ II | ||
Theorem | dfii2 24398 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II = ((topGenβran (,)) βΎt (0[,]1)) | ||
Theorem | dfii3 24399 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ II = (π½ βΎt (0[,]1)) | ||
Theorem | dfii4 24400 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ πΌ = (βfld βΎs (0[,]1)) β β’ II = (TopOpenβπΌ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |