![]() |
Metamath
Proof Explorer Theorem List (p. 346 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | kur14lem10 34501* | Lemma for kur14 34502. Discharge the set π. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ β Top & β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ π = β© {π₯ β π« π« π β£ (π΄ β π₯ β§ βπ¦ β π₯ {(π β π¦), (πΎβπ¦)} β π₯)} & β’ π΄ β π β β’ (π β Fin β§ (β―βπ) β€ ;14) | ||
Theorem | kur14 34502* | Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ π = β© {π₯ β π« π« π β£ (π΄ β π₯ β§ βπ¦ β π₯ {(π β π¦), (πΎβπ¦)} β π₯)} β β’ ((π½ β Top β§ π΄ β π) β (π β Fin β§ (β―βπ) β€ ;14)) | ||
Syntax | cretr 34503 | Extend class notation with the retract relation. |
class Retr | ||
Definition | df-retr 34504* | Define the set of retractions on two topological spaces. We say that π is a retraction from π½ to πΎ. or π β (π½ Retr πΎ) iff there is an π such that π :π½βΆπΎ, π:πΎβΆπ½ are continuous functions called the retraction and section respectively, and their composite π β π is homotopic to the identity map. If a retraction exists, we say π½ is a retract of πΎ. (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ Retr = (π β Top, π β Top β¦ {π β (π Cn π) β£ βπ β (π Cn π)((π β π )(π Htpy π)( I βΎ βͺ π)) β β }) | ||
Syntax | cpconn 34505 | Extend class notation with the class of path-connected topologies. |
class PConn | ||
Syntax | csconn 34506 | Extend class notation with the class of simply connected topologies. |
class SConn | ||
Definition | df-pconn 34507* | Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the closed unit interval) that goes from π₯ to π¦ for any points π₯, π¦ in the space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ PConn = {π β Top β£ βπ₯ β βͺ πβπ¦ β βͺ πβπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)} | ||
Definition | df-sconn 34508* | Define the class of simply connected topologies. A topology is simply connected if it is path-connected and every loop (continuous path with identical start and endpoint) is contractible to a point (path-homotopic to a constant function). (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ SConn = {π β PConn β£ βπ β (II Cn π)((πβ0) = (πβ1) β π( βphβπ)((0[,]1) Γ {(πβ0)}))} | ||
Theorem | ispconn 34509* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ (π½ β PConn β (π½ β Top β§ βπ₯ β π βπ¦ β π βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦))) | ||
Theorem | pconncn 34510* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β βπ β (II Cn π½)((πβ0) = π΄ β§ (πβ1) = π΅)) | ||
Theorem | pconntop 34511 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β PConn β π½ β Top) | ||
Theorem | issconn 34512* | The property of being a simply connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β SConn β (π½ β PConn β§ βπ β (II Cn π½)((πβ0) = (πβ1) β π( βphβπ½)((0[,]1) Γ {(πβ0)})))) | ||
Theorem | sconnpconn 34513 | A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β SConn β π½ β PConn) | ||
Theorem | sconntop 34514 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β SConn β π½ β Top) | ||
Theorem | sconnpht 34515 | A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ ((π½ β SConn β§ πΉ β (II Cn π½) β§ (πΉβ0) = (πΉβ1)) β πΉ( βphβπ½)((0[,]1) Γ {(πΉβ0)})) | ||
Theorem | cnpconn 34516 | An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ πΎ β β’ ((π½ β PConn β§ πΉ:πβontoβπ β§ πΉ β (π½ Cn πΎ)) β πΎ β PConn) | ||
Theorem | pconnconn 34517 | A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β PConn β π½ β Conn) | ||
Theorem | txpconn 34518 | The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ ((π β PConn β§ π β PConn) β (π Γt π) β PConn) | ||
Theorem | ptpconn 34519 | The topological product of a collection of path-connected spaces is path-connected. The proof uses the axiom of choice. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆPConn) β (βtβπΉ) β PConn) | ||
Theorem | indispconn 34520 | The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) |
β’ {β , π΄} β PConn | ||
Theorem | connpconn 34521 | A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ ((π½ β Conn β§ π½ β π-Locally PConn) β π½ β PConn) | ||
Theorem | qtoppconn 34522 | A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β PConn β§ πΉ Fn π) β (π½ qTop πΉ) β PConn) | ||
Theorem | pconnpi1 34523 | All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = βͺ π½ & β’ π = (π½ Ο1 π΄) & β’ π = (π½ Ο1 π΅) & β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β π βπ π) | ||
Theorem | sconnpht2 34524 | Any two paths in a simply connected space with the same start and end point are path-homotopic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ (π β π½ β SConn) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ0) = (πΊβ0)) & β’ (π β (πΉβ1) = (πΊβ1)) β β’ (π β πΉ( βphβπ½)πΊ) | ||
Theorem | sconnpi1 34525 | A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = βͺ π½ β β’ ((π½ β PConn β§ π β π) β (π½ β SConn β (Baseβ(π½ Ο1 π)) β 1o)) | ||
Theorem | txsconnlem 34526 | Lemma for txsconn 34527. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ (π β π β Top) & β’ (π β π β Top) & β’ (π β πΉ β (II Cn (π Γt π))) & β’ π΄ = ((1st βΎ (βͺ π Γ βͺ π)) β πΉ) & β’ π΅ = ((2nd βΎ (βͺ π Γ βͺ π)) β πΉ) & β’ (π β πΊ β (π΄(PHtpyβπ )((0[,]1) Γ {(π΄β0)}))) & β’ (π β π» β (π΅(PHtpyβπ)((0[,]1) Γ {(π΅β0)}))) β β’ (π β πΉ( βphβ(π Γt π))((0[,]1) Γ {(πΉβ0)})) | ||
Theorem | txsconn 34527 | The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ ((π β SConn β§ π β SConn) β (π Γt π) β SConn) | ||
Theorem | cvxpconn 34528* | A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π‘ β (0[,]1))) β ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β π) & β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π) β β’ (π β πΎ β PConn) | ||
Theorem | cvxsconn 34529* | A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π‘ β (0[,]1))) β ((π‘ Β· π₯) + ((1 β π‘) Β· π¦)) β π) & β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π) β β’ (π β πΎ β SConn) | ||
Theorem | blsconn 34530 | An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π½ = (TopOpenββfld) & β’ π = (π(ballβ(abs β β ))π ) & β’ πΎ = (π½ βΎt π) β β’ ((π β β β§ π β β*) β πΎ β SConn) | ||
Theorem | cnllysconn 34531 | The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Locally SConn | ||
Theorem | resconn 34532 | A subset of β is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π½ = ((topGenβran (,)) βΎt π΄) β β’ (π΄ β β β (π½ β SConn β π½ β Conn)) | ||
Theorem | ioosconn 34533 | An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ ((topGenβran (,)) βΎt (π΄(,)π΅)) β SConn | ||
Theorem | iccsconn 34534 | A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β SConn) | ||
Theorem | retopsconn 34535 | The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ (topGenβran (,)) β SConn | ||
Theorem | iccllysconn 34536 | A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β Locally SConn) | ||
Theorem | rellysconn 34537 | The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ (topGenβran (,)) β Locally SConn | ||
Theorem | iisconn 34538 | The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ II β SConn | ||
Theorem | iillysconn 34539 | The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ II β Locally SConn | ||
Theorem | iinllyconn 34540 | The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ II β π-Locally Conn | ||
Syntax | ccvm 34541 | Extend class notation with the class of covering maps. |
class CovMap | ||
Definition | df-cvm 34542* | Define the class of covering maps on two topological spaces. A function π:πβΆπ is a covering map if it is continuous and for every point π₯ in the target space there is a neighborhood π of π₯ and a decomposition π of the preimage of π as a disjoint union such that π is a homeomorphism of each set π’ β π onto π. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ CovMap = (π β Top, π β Top β¦ {π β (π Cn π) β£ βπ₯ β βͺ πβπ β π (π₯ β π β§ βπ β (π« π β {β })(βͺ π = (β‘π β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (π βΎ π’) β ((π βΎt π’)Homeo(π βΎt π)))))}) | ||
Theorem | fncvm 34543 | Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ CovMap Fn (Top Γ Top) | ||
Theorem | cvmscbv 34544* | Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) | ||
Theorem | iscvm 34545* | The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β ((πΆ β Top β§ π½ β Top β§ πΉ β (πΆ Cn π½)) β§ βπ₯ β π βπ β π½ (π₯ β π β§ (πβπ) β β ))) | ||
Theorem | cvmtop1 34546 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β πΆ β Top) | ||
Theorem | cvmtop2 34547 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β π½ β Top) | ||
Theorem | cvmcn 34548 | A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β πΉ β (πΆ Cn π½)) | ||
Theorem | cvmcov 34549* | Property of a covering map. In order to make the covering property more manageable, we define here the set π(π) of all even coverings of an open set π in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π = βͺ π½ β β’ ((πΉ β (πΆ CovMap π½) β§ π β π) β βπ₯ β π½ (π β π₯ β§ (πβπ₯) β β )) | ||
Theorem | cvmsrcl 34550* | Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β π β π½) | ||
Theorem | cvmsi 34551* | One direction of cvmsval 34552. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β (π β π½ β§ (π β πΆ β§ π β β ) β§ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π)))))) | ||
Theorem | cvmsval 34552* | Elementhood in the set π of all even coverings of an open set in π½. π is an even covering of π if it is a nonempty collection of disjoint open sets in πΆ whose union is the preimage of π, such that each set π’ β π is homeomorphic under πΉ to π. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (πΆ β π β (π β (πβπ) β (π β π½ β§ (π β πΆ β§ π β β ) β§ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))))) | ||
Theorem | cvmsss 34553* | An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β π β πΆ) | ||
Theorem | cvmsn0 34554* | An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β π β β ) | ||
Theorem | cvmsuni 34555* | An even covering of π has union equal to the preimage of π by πΉ. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β βͺ π = (β‘πΉ β π)) | ||
Theorem | cvmsdisj 34556* | An even covering of π is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((π β (πβπ) β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β¨ (π΄ β© π΅) = β )) | ||
Theorem | cvmshmeo 34557* | Every element of an even covering of π is homeomorphic to π via πΉ. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((π β (πβπ) β§ π΄ β π) β (πΉ βΎ π΄) β ((πΆ βΎt π΄)Homeo(π½ βΎt π))) | ||
Theorem | cvmsf1o 34558* | πΉ, localized to an element of an even covering of π, is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β (πβπ) β§ π΄ β π) β (πΉ βΎ π΄):π΄β1-1-ontoβπ) | ||
Theorem | cvmscld 34559* | The sets of an even covering are clopen in the subspace topology on π. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β (πβπ) β§ π΄ β π) β π΄ β (Clsdβ(πΆ βΎt (β‘πΉ β π)))) | ||
Theorem | cvmsss2 34560* | An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β ((πβπ) β β β (πβπ) β β )) | ||
Theorem | cvmcov2 34561* | The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β βπ₯ β π« π(π β π₯ β§ (πβπ₯) β β )) | ||
Theorem | cvmseu 34562* | Every element in βͺ π is a member of a unique element of π. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ β β’ ((πΉ β (πΆ CovMap π½) β§ (π β (πβπ) β§ π΄ β π΅ β§ (πΉβπ΄) β π)) β β!π₯ β π π΄ β π₯) | ||
Theorem | cvmsiota 34563* | Identify the unique element of π containing π΄. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = (β©π₯ β π π΄ β π₯) β β’ ((πΉ β (πΆ CovMap π½) β§ (π β (πβπ) β§ π΄ β π΅ β§ (πΉβπ΄) β π)) β (π β π β§ π΄ β π)) | ||
Theorem | cvmopnlem 34564* | Lemma for cvmopn 34566. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ β β’ ((πΉ β (πΆ CovMap π½) β§ π΄ β πΆ) β (πΉ β π΄) β π½) | ||
Theorem | cvmfolem 34565* | Lemma for cvmfo 34586. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β πΉ:π΅βontoβπ) | ||
Theorem | cvmopn 34566 | A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ ((πΉ β (πΆ CovMap π½) β§ π΄ β πΆ) β (πΉ β π΄) β π½) | ||
Theorem | cvmliftmolem1 34567* | Lemma for cvmliftmo 34570. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β (πΉ β π) = (πΉ β π)) & β’ (π β (πβπ) = (πβπ)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ ((π β§ π) β π β (πβπ)) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β πΌ β (β‘π β π)) & β’ ((π β§ π) β (πΎ βΎt πΌ) β Conn) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β (πΉβ(πβπ)) β π) β β’ ((π β§ π) β (π β dom (π β© π) β π β dom (π β© π))) | ||
Theorem | cvmliftmolem2 34568* | Lemma for cvmliftmo 34570. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β (πΉ β π) = (πΉ β π)) & β’ (π β (πβπ) = (πβπ)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β π = π) | ||
Theorem | cvmliftmoi 34569 | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β (πΉ β π) = (πΉ β π)) & β’ (π β (πβπ) = (πβπ)) β β’ (π β π = π) | ||
Theorem | cvmliftmo 34570* | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β πΊ β (πΎ Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβπ)) β β’ (π β β*π β (πΎ Cn πΆ)((πΉ β π) = πΊ β§ (πβπ) = π)) | ||
Theorem | cvmliftlem1 34571* | Lemma for cvmlift 34585. In cvmliftlem15 34584, we picked an π large enough so that the sections (πΊ β [(π β 1) / π, π / π]) are all contained in an even covering, and the function π enumerates these even coverings. So 1st β(πβπ) is a neighborhood of (πΊ β [(π β 1) / π, π / π]), and 2nd β(πβπ) is an even covering of 1st β(πβπ), which is to say a disjoint union of open sets in πΆ whose image is 1st β(πβπ). (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ ((π β§ π) β π β (1...π)) β β’ ((π β§ π) β (2nd β(πβπ)) β (πβ(1st β(πβπ)))) | ||
Theorem | cvmliftlem2 34572* | Lemma for cvmlift 34585. π = [(π β 1) / π, π / π] is a subset of [0, 1] for each π β (1...π). (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ ((π β§ π) β π β (1...π)) & β’ π = (((π β 1) / π)[,](π / π)) β β’ ((π β§ π) β π β (0[,]1)) | ||
Theorem | cvmliftlem3 34573* | Lemma for cvmlift 34585. Since 1st β(πβπ) is a neighborhood of (πΊ β π), every element π΄ β π satisfies (πΊβπ΄) β (1st β(πβπ)). (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ ((π β§ π) β π β (1...π)) & β’ π = (((π β 1) / π)[,](π / π)) & β’ ((π β§ π) β π΄ β π) β β’ ((π β§ π) β (πΊβπ΄) β (1st β(πβπ))) | ||
Theorem | cvmliftlem4 34574* | Lemma for cvmlift 34585. The function π will be our lifted path, defined piecewise on each section [(π β 1) / π, π / π] for π β (1...π). For π = 0, it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to π. (Contributed by Mario Carneiro, 15-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) β β’ (πβ0) = {β¨0, πβ©} | ||
Theorem | cvmliftlem5 34575* | Lemma for cvmlift 34585. Definition of π at a successor. This is a function defined on π as β‘(π βΎ πΌ) β πΊ where πΌ is the unique covering set of 2nd β(πβπ) that contains π(π β 1) evaluated at the last defined point, namely (π β 1) / π (note that for π = 1 this is using the seed value π(0)(0) = π). (Contributed by Mario Carneiro, 15-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ π = (((π β 1) / π)[,](π / π)) β β’ ((π β§ π β β) β (πβπ) = (π§ β π β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))((πβ(π β 1))β((π β 1) / π)) β π))β(πΊβπ§)))) | ||
Theorem | cvmliftlem6 34576* | Lemma for cvmlift 34585. Induction step for cvmliftlem7 34577. Assuming that π(π β 1) is defined at (π β 1) / π and is a preimage of πΊ((π β 1) / π), the next segment π(π) is also defined and is a function on π which is a lift πΊ for this segment. This follows explicitly from the definition π(π) = β‘(πΉ βΎ πΌ) β πΊ since πΊ is in 1st β(πΉβπ) for the entire interval so that β‘(πΉ βΎ πΌ) maps this into πΌ and πΉ β π maps back to πΊ. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ π = (((π β 1) / π)[,](π / π)) & β’ ((π β§ π) β π β (1...π)) & β’ ((π β§ π) β ((πβ(π β 1))β((π β 1) / π)) β (β‘πΉ β {(πΊβ((π β 1) / π))})) β β’ ((π β§ π) β ((πβπ):πβΆπ΅ β§ (πΉ β (πβπ)) = (πΊ βΎ π))) | ||
Theorem | cvmliftlem7 34577* | Lemma for cvmlift 34585. Prove by induction that every π function is well-defined (we can immediately follow this theorem with cvmliftlem6 34576 to show functionality and lifting of π). (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ π = (((π β 1) / π)[,](π / π)) β β’ ((π β§ π β (1...π)) β ((πβ(π β 1))β((π β 1) / π)) β (β‘πΉ β {(πΊβ((π β 1) / π))})) | ||
Theorem | cvmliftlem8 34578* | Lemma for cvmlift 34585. The functions π are continuous functions because they are defined as β‘(πΉ βΎ πΌ) β πΊ where πΊ is continuous and (πΉ βΎ πΌ) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ π = (((π β 1) / π)[,](π / π)) β β’ ((π β§ π β (1...π)) β (πβπ) β ((πΏ βΎt π) Cn πΆ)) | ||
Theorem | cvmliftlem9 34579* | Lemma for cvmlift 34585. The π(π) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the π functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) β β’ ((π β§ π β (1...π)) β ((πβπ)β((π β 1) / π)) = ((πβ(π β 1))β((π β 1) / π))) | ||
Theorem | cvmliftlem10 34580* | Lemma for cvmlift 34585. The function πΎ is going to be our complete lifted path, formed by unioning together all the π functions (each of which is defined on one segment [(π β 1) / π, π / π] of the interval). Here we prove by induction that πΎ is a continuous function and a lift of πΊ by applying cvmliftlem6 34576, cvmliftlem7 34577 (to show it is a function and a lift), cvmliftlem8 34578 (to show it is continuous), and cvmliftlem9 34579 (to show that different π functions agree on the intersection of their domains, so that the pasting lemma paste 23019 gives that πΎ is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ πΎ = βͺ π β (1...π)(πβπ) & β’ (π β ((π β β β§ (π + 1) β (1...π)) β§ (βͺ π β (1...π)(πβπ) β ((πΏ βΎt (0[,](π / π))) Cn πΆ) β§ (πΉ β βͺ π β (1...π)(πβπ)) = (πΊ βΎ (0[,](π / π)))))) β β’ (π β (πΎ β ((πΏ βΎt (0[,](π / π))) Cn πΆ) β§ (πΉ β πΎ) = (πΊ βΎ (0[,](π / π))))) | ||
Theorem | cvmliftlem11 34581* | Lemma for cvmlift 34585. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ πΎ = βͺ π β (1...π)(πβπ) β β’ (π β (πΎ β (II Cn πΆ) β§ (πΉ β πΎ) = πΊ)) | ||
Theorem | cvmliftlem13 34582* | Lemma for cvmlift 34585. The initial value of πΎ is π because π(1) is a subset of πΎ which takes value π at 0. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ πΎ = βͺ π β (1...π)(πβπ) β β’ (π β (πΎβ0) = π) | ||
Theorem | cvmliftlem14 34583* | Lemma for cvmlift 34585. Putting the results of cvmliftlem11 34581, cvmliftlem13 34582 and cvmliftmo 34570 together, we have that πΎ is a continuous function, satisfies πΉ β πΎ = πΊ and πΎ(0) = π, and is equal to any other function which also has these properties, so it follows that πΎ is the unique lift of πΊ. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) & β’ (π β π β β) & β’ (π β π:(1...π)βΆβͺ π β π½ ({π} Γ (πβπ))) & β’ (π β βπ β (1...π)(πΊ β (((π β 1) / π)[,](π / π))) β (1st β(πβπ))) & β’ πΏ = (topGenβran (,)) & β’ π = seq0((π₯ β V, π β β β¦ (π§ β (((π β 1) / π)[,](π / π)) β¦ (β‘(πΉ βΎ (β©π β (2nd β(πβπ))(π₯β((π β 1) / π)) β π))β(πΊβπ§)))), (( I βΎ β) βͺ {β¨0, {β¨0, πβ©}β©})) & β’ πΎ = βͺ π β (1...π)(πβπ) β β’ (π β β!π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) | ||
Theorem | cvmliftlem15 34584* | Lemma for cvmlift 34585. Discharge the assumptions of cvmliftlem14 34583. The set of all open subsets π’ of the unit interval such that πΊ β π’ is contained in an even covering of some open set in π½ is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 24713, there is a subdivision of the closed unit interval into π equal parts such that each part is entirely contained within one such open set of π½. Then using finite choice ac6sfi 9290 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 34583. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) β β’ (π β β!π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) | ||
Theorem | cvmlift 34585* | One of the important properties of covering maps is that any path πΊ in the base space "lifts" to a path π in the covering space such that πΉ β π = πΊ, and given a starting point π in the covering space this lift is unique. The proof is contained in cvmliftlem1 34571 thru cvmliftlem15 34584. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π΅ = βͺ πΆ β β’ (((πΉ β (πΆ CovMap π½) β§ πΊ β (II Cn π½)) β§ (π β π΅ β§ (πΉβπ) = (πΊβ0))) β β!π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) | ||
Theorem | cvmfo 34586 | A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β πΉ:π΅βontoβπ) | ||
Theorem | cvmliftiota 34587* | Write out a function π» that is the unique lift of πΉ. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π΅ = βͺ πΆ & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) β β’ (π β (π» β (II Cn πΆ) β§ (πΉ β π») = πΊ β§ (π»β0) = π)) | ||
Theorem | cvmlift2lem1 34588* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ (βπ¦ β (0[,]1)βπ’ β ((neiβII)β{π¦})((π’ Γ {π₯}) β π β (π’ Γ {π‘}) β π) β (((0[,]1) Γ {π₯}) β π β ((0[,]1) Γ {π‘}) β π)) | ||
Theorem | cvmlift2lem9a 34589* | Lemma for cvmlift2 34602 and cvmlift3 34614. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β π»:πβΆπ΅) & β’ (π β (πΉ β π») β (πΎ Cn π½)) & β’ (π β πΎ β Top) & β’ (π β π β π) & β’ (π β π β (πβπ΄)) & β’ (π β (π β π β§ (π»βπ) β π)) & β’ (π β π β π) & β’ (π β (π» β π) β π) β β’ (π β (π» βΎ π) β ((πΎ βΎt π) Cn πΆ)) | ||
Theorem | cvmlift2lem2 34590* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) β β’ (π β (π» β (II Cn πΆ) β§ (πΉ β π») = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (π»β0) = π)) | ||
Theorem | cvmlift2lem3 34591* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (ππΊπ§)) β§ (πβ0) = (π»βπ))) β β’ ((π β§ π β (0[,]1)) β (πΎ β (II Cn πΆ) β§ (πΉ β πΎ) = (π§ β (0[,]1) β¦ (ππΊπ§)) β§ (πΎβ0) = (π»βπ))) | ||
Theorem | cvmlift2lem4 34592* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ ((π β (0[,]1) β§ π β (0[,]1)) β (ππΎπ) = ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (ππΊπ§)) β§ (πβ0) = (π»βπ)))βπ)) | ||
Theorem | cvmlift2lem5 34593* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ (π β πΎ:((0[,]1) Γ (0[,]1))βΆπ΅) | ||
Theorem | cvmlift2lem6 34594* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ ((π β§ π β (0[,]1)) β (πΎ βΎ ({π} Γ (0[,]1))) β (((II Γt II) βΎt ({π} Γ (0[,]1))) Cn πΆ)) | ||
Theorem | cvmlift2lem7 34595* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ (π β (πΉ β πΎ) = πΊ) | ||
Theorem | cvmlift2lem8 34596* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) β β’ ((π β§ π β (0[,]1)) β (ππΎ0) = (π»βπ)) | ||
Theorem | cvmlift2lem9 34597* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β (ππΊπ) β π) & β’ (π β π β (πβπ)) & β’ (π β π β II) & β’ (π β π β II) & β’ (π β (II βΎt π) β Conn) & β’ (π β (II βΎt π) β Conn) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π Γ π) β (β‘πΊ β π)) & β’ (π β π β π) & β’ (π β (πΎ βΎ (π Γ {π})) β (((II Γt II) βΎt (π Γ {π})) Cn πΆ)) & β’ π = (β©π β π (ππΎπ) β π) β β’ (π β (πΎ βΎ (π Γ π)) β (((II Γt II) βΎt (π Γ π)) Cn πΆ)) | ||
Theorem | cvmlift2lem10 34598* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β π β (0[,]1)) & β’ (π β π β (0[,]1)) β β’ (π β βπ’ β II βπ£ β II (π β π’ β§ π β π£ β§ (βπ€ β π£ (πΎ βΎ (π’ Γ {π€})) β (((II Γt II) βΎt (π’ Γ {π€})) Cn πΆ) β (πΎ βΎ (π’ Γ π£)) β (((II Γt II) βΎt (π’ Γ π£)) Cn πΆ)))) | ||
Theorem | cvmlift2lem11 34599* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = {π§ β ((0[,]1) Γ (0[,]1)) β£ πΎ β (((II Γt II) CnP πΆ)βπ§)} & β’ (π β π β II) & β’ (π β π β II) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (βπ€ β π (πΎ βΎ (π Γ {π€})) β (((II Γt II) βΎt (π Γ {π€})) Cn πΆ) β (πΎ βΎ (π Γ π)) β (((II Γt II) βΎt (π Γ π)) Cn πΆ))) β β’ (π β ((π Γ {π}) β π β (π Γ {π}) β π)) | ||
Theorem | cvmlift2lem12 34600* | Lemma for cvmlift2 34602. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ π΅ = βͺ πΆ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β ((II Γt II) Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (0πΊ0)) & β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) & β’ π = {π§ β ((0[,]1) Γ (0[,]1)) β£ πΎ β (((II Γt II) CnP πΆ)βπ§)} & β’ π΄ = {π β (0[,]1) β£ ((0[,]1) Γ {π}) β π} & β’ π = {β¨π, π‘β© β£ (π‘ β (0[,]1) β§ βπ’ β ((neiβII)β{π})((π’ Γ {π}) β π β (π’ Γ {π‘}) β π))} β β’ (π β πΎ β ((II Γt II) Cn πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |