Home | Metamath
Proof Explorer Theorem List (p. 242 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zdis 24101 | The integers are a discrete set in the topology on β. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ (π½ βΎt β€) = π« β€ | ||
Theorem | sszcld 24102 | Every subset of the integers are closed in the topology on β. (Contributed by Mario Carneiro, 6-Jul-2017.) |
β’ π½ = (TopOpenββfld) β β’ (π΄ β β€ β π΄ β (Clsdβπ½)) | ||
Theorem | reperflem 24103* | 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 24104 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π½ = (TopOpenββfld) β β’ (π½ βΎt β) β Perf | ||
Theorem | cnperf 24105 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Perf | ||
Theorem | iccntr 24106 | 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 24107* | Lemma for icccmp 24110. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) β β’ (π β (π΄ β π β§ βπ¦ β π π¦ β€ π΅)) | ||
Theorem | icccmplem2 24108* | Lemma for icccmp 24110. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) & β’ (π β π β π) & β’ (π β πΆ β β+) & β’ (π β (πΊ(ballβπ·)πΆ) β π) & β’ πΊ = sup(π, β, < ) & β’ π = if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β β’ (π β π΅ β π) | ||
Theorem | icccmplem3 24109* | Lemma for icccmp 24110. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) & β’ π· = ((abs β β ) βΎ (β Γ β)) & β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β π β π½) & β’ (π β (π΄[,]π΅) β βͺ π) β β’ (π β π΅ β π) | ||
Theorem | icccmp 24110 | A closed interval in β is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
β’ π½ = (topGenβran (,)) & β’ π = (π½ βΎt (π΄[,]π΅)) β β’ ((π΄ β β β§ π΅ β β) β π β Comp) | ||
Theorem | reconnlem1 24111 | Lemma for reconn 24113. 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 24112* | Lemma for reconn 24113. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
β’ (π β π΄ β β) & β’ (π β π β (topGenβran (,))) & β’ (π β π β (topGenβran (,))) & β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯[,]π¦) β π΄) & β’ (π β π΅ β (π β© π΄)) & β’ (π β πΆ β (π β© π΄)) & β’ (π β (π β© π) β (β β π΄)) & β’ (π β π΅ β€ πΆ) & β’ π = sup((π β© (π΅[,]πΆ)), β, < ) β β’ (π β Β¬ π΄ β (π βͺ π)) | ||
Theorem | reconn 24113* | 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 24114 | Corollary of reconn 24113. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
β’ (topGenβran (,)) β Conn | ||
Theorem | iccconn 24115 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β Conn) | ||
Theorem | opnreen 24116 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
β’ ((π΄ β (topGenβran (,)) β§ π΄ β β ) β π΄ β π« β) | ||
Theorem | rectbntr0 24117 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π΄ β β β§ π΄ βΌ β) β ((intβ(topGenβran (,)))βπ΄) = β ) | ||
Theorem | xrge0gsumle 24118 | 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 24119* | 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 24120 | 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 24121 | 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 24122 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 24123 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 24123 | 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 24124 | 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 24125 | 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 24126 | 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 24127* | Continuity of the metric function; analogue of cnmpt12f 22939 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 24128* | Continuity of the metric function; analogue of cnmpt22f 22948 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 24129 | 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 24130 | 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 24131 | 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 24132* | 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 24133* | 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 24134* | 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 24135* | 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 24136* | 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 24137* | 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 24138* | 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 24139* | 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 24140* | Lemma for metdscn 24141. (Contributed by Mario Carneiro, 4-Sep-2015.) |
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, < )) & β’ π½ = (MetOpenβπ·) & β’ πΆ = (distββ*π ) & β’ πΎ = (MetOpenβπΆ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) & β’ (π β (π΄π·π΅) < π ) β β’ (π β ((πΉβπ΄) +π -π(πΉβπ΅)) < π ) | ||
Theorem | metdscn 24141* | 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 24142* | 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 24143* | Lemma for metnrm 24147. (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 24144* | Lemma for metnrm 24147. (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 24145* | Lemma for metnrm 24147. (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 24146* | Lemma for metnrm 24147. (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 24147 | 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 24148 | A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ β Reg) | ||
Theorem | addcnlem 24149* | Lemma for addcn 24150, subcn 24151, and mulcn 24152. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ + :(β Γ β)βΆβ & β’ ((π β β+ β§ π β β β§ π β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) β β’ + β ((π½ Γt π½) Cn π½) | ||
Theorem | addcn 24150 | 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 24151 | 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 24152 | 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 24153 | 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 24154 | 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 24155* | 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 24156* | Version of fsumcn 24155 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ (π β πΏ β (TopOnβπ)) & β’ ((π β§ π β π΄) β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΏ) Cn πΎ)) β β’ (π β (π₯ β π, π¦ β π β¦ Ξ£π β π΄ π΅) β ((π½ Γt πΏ) Cn πΎ)) | ||
Theorem | expcn 24157* | 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 24158* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) |
β’ π½ = (TopOpenββfld) β β’ ((π΄ β β β§ π΄ β 0) β (π₯ β β β¦ (π₯ / π΄)) β (π½ Cn π½)) | ||
Theorem | sqcn 24159* | 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 24160 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 24161 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class βcnβ | ||
Definition | df-ii 24162 | 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 24163* | 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 24164 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ II β (TopOnβ(0[,]1)) | ||
Theorem | iitop 24165 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II β Top | ||
Theorem | iiuni 24166 | 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 24167 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ II = ((topGenβran (,)) βΎt (0[,]1)) | ||
Theorem | dfii3 24168 | 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 24169 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ πΌ = (βfld βΎs (0[,]1)) β β’ II = (TopOpenβπΌ) | ||
Theorem | dfii5 24170 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ II = (ordTopβ( β€ β© ((0[,]1) Γ (0[,]1)))) | ||
Theorem | iicmp 24171 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
β’ II β Comp | ||
Theorem | iiconn 24172 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ II β Conn | ||
Theorem | cncfval 24173* | The value of the continuous complex function operation is the set of continuous functions from π΄ to π΅. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = {π β (π΅ βm π΄) β£ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦)}) | ||
Theorem | elcncf 24174* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)))) | ||
Theorem | elcncf2 24175* | Version of elcncf 24174 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ βπ€ β π΄ ((absβ(π€ β π₯)) < π§ β (absβ((πΉβπ€) β (πΉβπ₯))) < π¦)))) | ||
Theorem | cncfrss 24176 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β π΄ β β) | ||
Theorem | cncfrss2 24177 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β π΅ β β) | ||
Theorem | cncff 24178 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ (πΉ β (π΄βcnβπ΅) β πΉ:π΄βΆπ΅) | ||
Theorem | cncfi 24179* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ ((πΉ β (π΄βcnβπ΅) β§ πΆ β π΄ β§ π β β+) β βπ§ β β+ βπ€ β π΄ ((absβ(π€ β πΆ)) < π§ β (absβ((πΉβπ€) β (πΉβπΆ))) < π )) | ||
Theorem | elcncf1di 24180* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β ((π₯ β π΄ β§ π¦ β β+) β π β β+)) & β’ (π β (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β ((absβ(π₯ β π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦))) β β’ (π β ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅))) | ||
Theorem | elcncf1ii 24181* | Membership in the set of continuous complex functions from π΄ to π΅. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ πΉ:π΄βΆπ΅ & β’ ((π₯ β π΄ β§ π¦ β β+) β π β β+) & β’ (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β ((absβ(π₯ β π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅)) | ||
Theorem | rescncf 24182 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ (πΆ β π΄ β (πΉ β (π΄βcnβπ΅) β (πΉ βΎ πΆ) β (πΆβcnβπ΅))) | ||
Theorem | cncfcdm 24183 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((πΆ β β β§ πΉ β (π΄βcnβπ΅)) β (πΉ β (π΄βcnβπΆ) β πΉ:π΄βΆπΆ)) | ||
Theorem | cncfss 24184 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
β’ ((π΅ β πΆ β§ πΆ β β) β (π΄βcnβπ΅) β (π΄βcnβπΆ)) | ||
Theorem | climcncf 24185 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ:πβΆπ΄) & β’ (π β πΊ β π·) & β’ (π β π· β π΄) β β’ (π β (πΉ β πΊ) β (πΉβπ·)) | ||
Theorem | abscncf 24186 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ abs β (ββcnββ) | ||
Theorem | recncf 24187 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | imcncf 24188 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | cjcncf 24189 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
β’ β β (ββcnββ) | ||
Theorem | mulc1cncf 24190* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
β’ πΉ = (π₯ β β β¦ (π΄ Β· π₯)) β β’ (π΄ β β β πΉ β (ββcnββ)) | ||
Theorem | divccncf 24191* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
β’ πΉ = (π₯ β β β¦ (π₯ / π΄)) β β’ ((π΄ β β β§ π΄ β 0) β πΉ β (ββcnββ)) | ||
Theorem | cncfco 24192 | The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.) |
β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ β (π΅βcnβπΆ)) β β’ (π β (πΊ β πΉ) β (π΄βcnβπΆ)) | ||
Theorem | cncfcompt2 24193* | Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²π₯π & β’ (π β (π₯ β π΄ β¦ π ) β (π΄βcnβπ΅)) & β’ (π β (π¦ β πΆ β¦ π) β (πΆβcnβπΈ)) & β’ (π β π΅ β πΆ) & β’ (π¦ = π β π = π) β β’ (π β (π₯ β π΄ β¦ π) β (π΄βcnβπΈ)) | ||
Theorem | cncfmet 24194 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ πΆ = ((abs β β ) βΎ (π΄ Γ π΄)) & β’ π· = ((abs β β ) βΎ (π΅ Γ π΅)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (π½ Cn πΎ)) | ||
Theorem | cncfcn 24195 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π΄) & β’ πΏ = (π½ βΎt π΅) β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (πΎ Cn πΏ)) | ||
Theorem | cncfcn1 24196 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ (ββcnββ) = (π½ Cn π½) | ||
Theorem | cncfmptc 24197* | A constant function is a continuous function on β. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ ((π΄ β π β§ π β β β§ π β β) β (π₯ β π β¦ π΄) β (πβcnβπ)) | ||
Theorem | cncfmptid 24198* | The identity function is a continuous function on β. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.) |
β’ ((π β π β§ π β β) β (π₯ β π β¦ π₯) β (πβcnβπ)) | ||
Theorem | cncfmpt1f 24199* | Composition of continuous functions. βcnβ analogue of cnmpt11f 22937. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ (π β πΉ β (ββcnββ)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (πΉβπ΄)) β (πβcnββ)) | ||
Theorem | cncfmpt2f 24200* | Composition of continuous functions. βcnβ analogue of cnmpt12f 22939. (Contributed by Mario Carneiro, 3-Sep-2014.) |
β’ π½ = (TopOpenββfld) & β’ (π β πΉ β ((π½ Γt π½) Cn π½)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄πΉπ΅)) β (πβcnββ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |