![]() |
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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | kur14lem7 34501 | Lemma for kur14 34505: main proof. The set π here contains all the distinct combinations of π and π that can arise, and we prove here that applying π or π to any element of π yields another elemnt of π. In operator shorthand, we have π = {π΄, ππ΄, ππ΄ , πππ΄, πππ΄, ππππ΄, ππππ΄, πππππ΄, πππππ΄, ππππππ΄, ππππππ΄, πππππππ΄, πππππππ΄, ππππππππ΄}. From the identities πππ΄ = π΄ and πππ΄ = ππ΄, we can reduce any operator combination containing two adjacent identical operators, which is why the list only contains alternating sequences. The reason the sequences don't keep going after a certain point is due to the identity ππππ΄ = ππππππππ΄, proved in kur14lem6 34500. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ β Top & β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ πΌ = (intβπ½) & β’ π΄ β π & β’ π΅ = (π β (πΎβπ΄)) & β’ πΆ = (πΎβ(π β π΄)) & β’ π· = (πΌβ(πΎβπ΄)) & β’ π = ((({π΄, (π β π΄), (πΎβπ΄)} βͺ {π΅, πΆ, (πΌβπ΄)}) βͺ {(πΎβπ΅), π·, (πΎβ(πΌβπ΄))}) βͺ ({(πΌβπΆ), (πΎβπ·), (πΌβ(πΎβπ΅))} βͺ {(πΎβ(πΌβπΆ)), (πΌβ(πΎβ(πΌβπ΄)))})) β β’ (π β π β (π β π β§ {(π β π), (πΎβπ)} β π)) | ||
Theorem | kur14lem8 34502 | Lemma for kur14 34505. Show that the set π contains at most 14 elements. (It could be less if some of the operators take the same value for a given set, but Kuratowski showed that this upper bound of 14 is tight in the sense that there exist topological spaces and subsets of these spaces for which all 14 generated sets are distinct, and indeed the real numbers form such a topological space.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ β Top & β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ πΌ = (intβπ½) & β’ π΄ β π & β’ π΅ = (π β (πΎβπ΄)) & β’ πΆ = (πΎβ(π β π΄)) & β’ π· = (πΌβ(πΎβπ΄)) & β’ π = ((({π΄, (π β π΄), (πΎβπ΄)} βͺ {π΅, πΆ, (πΌβπ΄)}) βͺ {(πΎβπ΅), π·, (πΎβ(πΌβπ΄))}) βͺ ({(πΌβπΆ), (πΎβπ·), (πΌβ(πΎβπ΅))} βͺ {(πΎβ(πΌβπΆ)), (πΌβ(πΎβ(πΌβπ΄)))})) β β’ (π β Fin β§ (β―βπ) β€ ;14) | ||
Theorem | kur14lem9 34503* | Lemma for kur14 34505. Since the set π is closed under closure and complement, it contains the minimal set π as a subset, so π also has at most 14 elements. (Indeed π = π, and it's not hard to prove this, but we don't need it for this proof.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ β Top & β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ πΌ = (intβπ½) & β’ π΄ β π & β’ π΅ = (π β (πΎβπ΄)) & β’ πΆ = (πΎβ(π β π΄)) & β’ π· = (πΌβ(πΎβπ΄)) & β’ π = ((({π΄, (π β π΄), (πΎβπ΄)} βͺ {π΅, πΆ, (πΌβπ΄)}) βͺ {(πΎβπ΅), π·, (πΎβ(πΌβπ΄))}) βͺ ({(πΌβπΆ), (πΎβπ·), (πΌβ(πΎβπ΅))} βͺ {(πΎβ(πΌβπΆ)), (πΌβ(πΎβ(πΌβπ΄)))})) & β’ π = β© {π₯ β π« π« π β£ (π΄ β π₯ β§ βπ¦ β π₯ {(π β π¦), (πΎβπ¦)} β π₯)} β β’ (π β Fin β§ (β―βπ) β€ ;14) | ||
Theorem | kur14lem10 34504* | Lemma for kur14 34505. Discharge the set π. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ β Top & β’ π = βͺ π½ & β’ πΎ = (clsβπ½) & β’ π = β© {π₯ β π« π« π β£ (π΄ β π₯ β§ βπ¦ β π₯ {(π β π¦), (πΎβπ¦)} β π₯)} & β’ π΄ β π β β’ (π β Fin β§ (β―βπ) β€ ;14) | ||
Theorem | kur14 34505* | 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 34506 | Extend class notation with the retract relation. |
class Retr | ||
Definition | df-retr 34507* | 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 34508 | Extend class notation with the class of path-connected topologies. |
class PConn | ||
Syntax | csconn 34509 | Extend class notation with the class of simply connected topologies. |
class SConn | ||
Definition | df-pconn 34510* | 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 34511* | 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 34512* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ (π½ β PConn β (π½ β Top β§ βπ₯ β π βπ¦ β π βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦))) | ||
Theorem | pconncn 34513* | The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = βͺ π½ β β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β βπ β (II Cn π½)((πβ0) = π΄ β§ (πβ1) = π΅)) | ||
Theorem | pconntop 34514 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β PConn β π½ β Top) | ||
Theorem | issconn 34515* | 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 34516 | A simply connected space is path-connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β SConn β π½ β PConn) | ||
Theorem | sconntop 34517 | A simply connected space is a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β SConn β π½ β Top) | ||
Theorem | sconnpht 34518 | 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 34519 | An image of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ πΎ β β’ ((π½ β PConn β§ πΉ:πβontoβπ β§ πΉ β (π½ Cn πΎ)) β πΎ β PConn) | ||
Theorem | pconnconn 34520 | A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (π½ β PConn β π½ β Conn) | ||
Theorem | txpconn 34521 | The topological product of two path-connected spaces is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ ((π β PConn β§ π β PConn) β (π Γt π) β PConn) | ||
Theorem | ptpconn 34522 | 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 34523 | 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 34524 | A connected and locally path-connected space is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ ((π½ β Conn β§ π½ β π-Locally PConn) β π½ β PConn) | ||
Theorem | qtoppconn 34525 | A quotient of a path-connected space is path-connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β PConn β§ πΉ Fn π) β (π½ qTop πΉ) β PConn) | ||
Theorem | pconnpi1 34526 | All fundamental groups in a path-connected space are isomorphic. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = βͺ π½ & β’ π = (π½ Ο1 π΄) & β’ π = (π½ Ο1 π΅) & β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ ((π½ β PConn β§ π΄ β π β§ π΅ β π) β π βπ π) | ||
Theorem | sconnpht2 34527 | 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 34528 | 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 34529 | Lemma for txsconn 34530. (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 34530 | The topological product of two simply connected spaces is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ ((π β SConn β§ π β SConn) β (π Γt π) β SConn) | ||
Theorem | cvxpconn 34531* | 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 34532* | 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 34533 | 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 34534 | The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Locally SConn | ||
Theorem | resconn 34535 | A subset of β is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ π½ = ((topGenβran (,)) βΎt π΄) β β’ (π΄ β β β (π½ β SConn β π½ β Conn)) | ||
Theorem | ioosconn 34536 | An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ ((topGenβran (,)) βΎt (π΄(,)π΅)) β SConn | ||
Theorem | iccsconn 34537 | A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β SConn) | ||
Theorem | retopsconn 34538 | The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ (topGenβran (,)) β SConn | ||
Theorem | iccllysconn 34539 | A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π΄ β β β§ π΅ β β) β ((topGenβran (,)) βΎt (π΄[,]π΅)) β Locally SConn) | ||
Theorem | rellysconn 34540 | The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ (topGenβran (,)) β Locally SConn | ||
Theorem | iisconn 34541 | The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.) |
β’ II β SConn | ||
Theorem | iillysconn 34542 | The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ II β Locally SConn | ||
Theorem | iinllyconn 34543 | The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ II β π-Locally Conn | ||
Syntax | ccvm 34544 | Extend class notation with the class of covering maps. |
class CovMap | ||
Definition | df-cvm 34545* | 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 34546 | Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ CovMap Fn (Top Γ Top) | ||
Theorem | cvmscbv 34547* | Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) | ||
Theorem | iscvm 34548* | The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β ((πΆ β Top β§ π½ β Top β§ πΉ β (πΆ Cn π½)) β§ βπ₯ β π βπ β π½ (π₯ β π β§ (πβπ) β β ))) | ||
Theorem | cvmtop1 34549 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β πΆ β Top) | ||
Theorem | cvmtop2 34550 | Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β π½ β Top) | ||
Theorem | cvmcn 34551 | A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ (πΉ β (πΆ CovMap π½) β πΉ β (πΆ Cn π½)) | ||
Theorem | cvmcov 34552* | 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 34553* | Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β π β π½) | ||
Theorem | cvmsi 34554* | One direction of cvmsval 34555. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β (π β π½ β§ (π β πΆ β§ π β β ) β§ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π)))))) | ||
Theorem | cvmsval 34555* | 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 34556* | 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 34557* | An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β π β β ) | ||
Theorem | cvmsuni 34558* | An even covering of π has union equal to the preimage of π by πΉ. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β (πβπ) β βͺ π = (β‘πΉ β π)) | ||
Theorem | cvmsdisj 34559* | An even covering of π is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((π β (πβπ) β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β¨ (π΄ β© π΅) = β )) | ||
Theorem | cvmshmeo 34560* | 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 34561* | πΉ, 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 34562* | 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 34563* | An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β ((πβπ) β β β (πβπ) β β )) | ||
Theorem | cvmcov2 34564* | The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β βπ₯ β π« π(π β π₯ β§ (πβπ₯) β β )) | ||
Theorem | cvmseu 34565* | Every element in βͺ π is a member of a unique element of π. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ β β’ ((πΉ β (πΆ CovMap π½) β§ (π β (πβπ) β§ π΄ β π΅ β§ (πΉβπ΄) β π)) β β!π₯ β π π΄ β π₯) | ||
Theorem | cvmsiota 34566* | Identify the unique element of π containing π΄. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = (β©π₯ β π π΄ β π₯) β β’ ((πΉ β (πΆ CovMap π½) β§ (π β (πβπ) β§ π΄ β π΅ β§ (πΉβπ΄) β π)) β (π β π β§ π΄ β π)) | ||
Theorem | cvmopnlem 34567* | Lemma for cvmopn 34569. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ β β’ ((πΉ β (πΆ CovMap π½) β§ π΄ β πΆ) β (πΉ β π΄) β π½) | ||
Theorem | cvmfolem 34568* | Lemma for cvmfo 34589. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β πΉ:π΅βontoβπ) | ||
Theorem | cvmopn 34569 | A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.) |
β’ ((πΉ β (πΆ CovMap π½) β§ π΄ β πΆ) β (πΉ β π΄) β π½) | ||
Theorem | cvmliftmolem1 34570* | Lemma for cvmliftmo 34573. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β (πΉ β π) = (πΉ β π)) & β’ (π β (πβπ) = (πβπ)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ ((π β§ π) β π β (πβπ)) & β’ ((π β§ π) β π β π) & β’ ((π β§ π) β πΌ β (β‘π β π)) & β’ ((π β§ π) β (πΎ βΎt πΌ) β Conn) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β π β πΌ) & β’ ((π β§ π) β (πΉβ(πβπ)) β π) β β’ ((π β§ π) β (π β dom (π β© π) β π β dom (π β© π))) | ||
Theorem | cvmliftmolem2 34571* | Lemma for cvmliftmo 34573. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΎ β Conn) & β’ (π β πΎ β π-Locally Conn) & β’ (π β π β π) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β π β (πΎ Cn πΆ)) & β’ (π β (πΉ β π) = (πΉ β π)) & β’ (π β (πβπ) = (πβπ)) & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) β β’ (π β π = π) | ||
Theorem | cvmliftmoi 34572 | 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 34573* | 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 34574* | Lemma for cvmlift 34588. In cvmliftlem15 34587, 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 34575* | Lemma for cvmlift 34588. π = [(π β 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 34576* | Lemma for cvmlift 34588. 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 34577* | Lemma for cvmlift 34588. 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 34578* | Lemma for cvmlift 34588. 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 34579* | Lemma for cvmlift 34588. Induction step for cvmliftlem7 34580. 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 34580* | Lemma for cvmlift 34588. Prove by induction that every π function is well-defined (we can immediately follow this theorem with cvmliftlem6 34579 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 34581* | Lemma for cvmlift 34588. 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 34582* | Lemma for cvmlift 34588. 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 34583* | Lemma for cvmlift 34588. 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 34579, cvmliftlem7 34580 (to show it is a function and a lift), cvmliftlem8 34581 (to show it is continuous), and cvmliftlem9 34582 (to show that different π functions agree on the intersection of their domains, so that the pasting lemma paste 23018 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 34584* | Lemma for cvmlift 34588. (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 34585* | Lemma for cvmlift 34588. 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 34586* | Lemma for cvmlift 34588. Putting the results of cvmliftlem11 34584, cvmliftlem13 34585 and cvmliftmo 34573 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 34587* | Lemma for cvmlift 34588. Discharge the assumptions of cvmliftlem14 34586. 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 24712, 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 9289 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 34586. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) & β’ π΅ = βͺ πΆ & β’ π = βͺ π½ & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β π΅) & β’ (π β (πΉβπ) = (πΊβ0)) β β’ (π β β!π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) | ||
Theorem | cvmlift 34588* | 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 34574 thru cvmliftlem15 34587. (Contributed by Mario Carneiro, 16-Feb-2015.) |
β’ π΅ = βͺ πΆ β β’ (((πΉ β (πΆ CovMap π½) β§ πΊ β (II Cn π½)) β§ (π β π΅ β§ (πΉβπ) = (πΊβ0))) β β!π β (II Cn πΆ)((πΉ β π) = πΊ β§ (πβ0) = π)) | ||
Theorem | cvmfo 34589 | A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ π½ β β’ (πΉ β (πΆ CovMap π½) β πΉ:π΅βontoβπ) | ||
Theorem | cvmliftiota 34590* | 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 34591* | Lemma for cvmlift2 34605. (Contributed by Mario Carneiro, 1-Jun-2015.) |
β’ (βπ¦ β (0[,]1)βπ’ β ((neiβII)β{π¦})((π’ Γ {π₯}) β π β (π’ Γ {π‘}) β π) β (((0[,]1) Γ {π₯}) β π β ((0[,]1) Γ {π‘}) β π)) | ||
Theorem | cvmlift2lem9a 34592* | Lemma for cvmlift2 34605 and cvmlift3 34617. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ π΅ = βͺ πΆ & β’ π = βͺ πΎ & β’ π = (π β π½ β¦ {π β (π« πΆ β {β }) β£ (βͺ π = (β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) & β’ (π β πΉ β (πΆ CovMap π½)) & β’ (π β π»:πβΆπ΅) & β’ (π β (πΉ β π») β (πΎ Cn π½)) & β’ (π β πΎ β Top) & β’ (π β π β π) & β’ (π β π β (πβπ΄)) & β’ (π β (π β π β§ (π»βπ) β π)) & β’ (π β π β π) & β’ (π β (π» β π) β π) β β’ (π β (π» βΎ π) β ((πΎ βΎt π) Cn πΆ)) | ||
Theorem | cvmlift2lem2 34593* | Lemma for cvmlift2 34605. (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 34594* | Lemma for cvmlift2 34605. (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 34595* | Lemma for cvmlift2 34605. (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 34596* | Lemma for cvmlift2 34605. (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 34597* | Lemma for cvmlift2 34605. (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 34598* | Lemma for cvmlift2 34605. (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 34599* | Lemma for cvmlift2 34605. (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 34600* | Lemma for cvmlift2 34605. (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 πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |