![]() |
Metamath
Proof Explorer Theorem List (p. 248 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 | cnheiborlem 24701* | Lemma for cnheibor 24702. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π½ = (TopOpenββfld) & β’ π = (π½ βΎt π) & β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π = (πΉ β ((-π [,]π ) Γ (-π [,]π ))) β β’ ((π β (Clsdβπ½) β§ (π β β β§ βπ§ β π (absβπ§) β€ π )) β π β Comp) | ||
Theorem | cnheibor 24702* | Heine-Borel theorem for complex numbers. A subset of β is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π½ = (TopOpenββfld) & β’ π = (π½ βΎt π) β β’ (π β β β (π β Comp β (π β (Clsdβπ½) β§ βπ β β βπ₯ β π (absβπ₯) β€ π))) | ||
Theorem | cnllycmp 24703 | The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β π-Locally Comp | ||
Theorem | rellycmp 24704 | The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (topGenβran (,)) β π-Locally Comp | ||
Theorem | bndth 24705* | The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -πΉ.) (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β βπ₯ β β βπ¦ β π (πΉβπ¦) β€ π₯) | ||
Theorem | evth 24706* | The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β βπ₯ β π βπ¦ β π (πΉβπ¦) β€ (πΉβπ₯)) | ||
Theorem | evth2 24707* | The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
β’ π = βͺ π½ & β’ πΎ = (topGenβran (,)) & β’ (π β π½ β Comp) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β π β β ) β β’ (π β βπ₯ β π βπ¦ β π (πΉβπ₯) β€ (πΉβπ¦)) | ||
Theorem | lebnumlem1 24708* | Lemma for lebnum 24711. The function πΉ measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β Fin) & β’ (π β Β¬ π β π) & β’ πΉ = (π¦ β π β¦ Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) β β’ (π β πΉ:πβΆβ+) | ||
Theorem | lebnumlem2 24709* | Lemma for lebnum 24711. As a finite sum of point-to-set distance functions, which are continuous by metdscn 24593, the function πΉ is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β Fin) & β’ (π β Β¬ π β π) & β’ πΉ = (π¦ β π β¦ Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) & β’ πΎ = (topGenβran (,)) β β’ (π β πΉ β (π½ Cn πΎ)) | ||
Theorem | lebnumlem3 24710* | Lemma for lebnum 24711. By the previous lemmas, πΉ is continuous and positive on a compact set, so it has a positive minimum π. Then setting π = π / β―(π), since for each π’ β π we have ball(π₯, π) β π’ iff π β€ π(π₯, π β π’), if Β¬ ball(π₯, π) β π’ for all π’ then summing over π’ yields Ξ£π’ β ππ(π₯, π β π’) = πΉ(π₯) < Ξ£π’ β ππ = π, in contradiction to the assumption that π is the minimum of πΉ. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β Fin) & β’ (π β Β¬ π β π) & β’ πΉ = (π¦ β π β¦ Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) & β’ πΎ = (topGenβran (,)) β β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) | ||
Theorem | lebnum 24711* | The Lebesgue number lemma, or Lebesgue covering lemma. If π is a compact metric space and π is an open cover of π, then there exists a positive real number π such that every ball of size π (and every subset of a ball of size π, including every subset of diameter less than π) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) & β’ (π β π β π½) & β’ (π β π = βͺ π) β β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) | ||
Theorem | xlebnum 24712* | Generalize lebnum 24711 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π½ β Comp) & β’ (π β π β π½) & β’ (π β π = βͺ π) β β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) | ||
Theorem | lebnumii 24713* | Specialize the Lebesgue number lemma lebnum 24711 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.) |
β’ ((π β II β§ (0[,]1) = βͺ π) β βπ β β βπ β (1...π)βπ’ β π (((π β 1) / π)[,](π / π)) β π’) | ||
Syntax | chtpy 24714 | Extend class notation with the class of homotopies between two continuous functions. |
class Htpy | ||
Syntax | cphtpy 24715 | Extend class notation with the class of path homotopies between two continuous functions. |
class PHtpy | ||
Syntax | cphtpc 24716 | Extend class notation with the path homotopy relation. |
class βph | ||
Definition | df-htpy 24717* | Define the function which takes topological spaces π, π and two continuous functions πΉ, πΊ:πβΆπ and returns the class of homotopies from πΉ to πΊ. (Contributed by Mario Carneiro, 22-Feb-2015.) |
β’ Htpy = (π₯ β Top, π¦ β Top β¦ (π β (π₯ Cn π¦), π β (π₯ Cn π¦) β¦ {β β ((π₯ Γt II) Cn π¦) β£ βπ β βͺ π₯((π β0) = (πβπ ) β§ (π β1) = (πβπ ))})) | ||
Definition | df-phtpy 24718* | Define the class of path homotopies between two paths πΉ, πΊ:IIβΆπ; these are homotopies (in the sense of df-htpy 24717) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ PHtpy = (π₯ β Top β¦ (π β (II Cn π₯), π β (II Cn π₯) β¦ {β β (π(II Htpy π₯)π) β£ βπ β (0[,]1)((0βπ ) = (πβ0) β§ (1βπ ) = (πβ1))})) | ||
Theorem | ishtpy 24719* | Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (π» β (πΉ(π½ Htpy πΎ)πΊ) β (π» β ((π½ Γt II) Cn πΎ) β§ βπ β π ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ ))))) | ||
Theorem | htpycn 24720 | A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β (πΉ(π½ Htpy πΎ)πΊ) β ((π½ Γt II) Cn πΎ)) | ||
Theorem | htpyi 24721 | A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ (π β π» β (πΉ(π½ Htpy πΎ)πΊ)) β β’ ((π β§ π΄ β π) β ((π΄π»0) = (πΉβπ΄) β§ (π΄π»1) = (πΊβπ΄))) | ||
Theorem | ishtpyd 24722* | Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ (π β π» β ((π½ Γt II) Cn πΎ)) & β’ ((π β§ π β π) β (π π»0) = (πΉβπ )) & β’ ((π β§ π β π) β (π π»1) = (πΊβπ )) β β’ (π β π» β (πΉ(π½ Htpy πΎ)πΊ)) | ||
Theorem | htpycom 24723* | Given a homotopy from πΉ to πΊ, produce a homotopy from πΊ to πΉ. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ π = (π₯ β π, π¦ β (0[,]1) β¦ (π₯π»(1 β π¦))) & β’ (π β π» β (πΉ(π½ Htpy πΎ)πΊ)) β β’ (π β π β (πΊ(π½ Htpy πΎ)πΉ)) | ||
Theorem | htpyid 24724* | A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ πΊ = (π₯ β π, π¦ β (0[,]1) β¦ (πΉβπ₯)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) β β’ (π β πΊ β (πΉ(π½ Htpy πΎ)πΉ)) | ||
Theorem | htpyco1 24725* | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ π = (π₯ β π, π¦ β (0[,]1) β¦ ((πβπ₯)π»π¦)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β (π½ Cn πΎ)) & β’ (π β πΉ β (πΎ Cn πΏ)) & β’ (π β πΊ β (πΎ Cn πΏ)) & β’ (π β π» β (πΉ(πΎ Htpy πΏ)πΊ)) β β’ (π β π β ((πΉ β π)(π½ Htpy πΏ)(πΊ β π))) | ||
Theorem | htpyco2 24726 | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ (π β π β (πΎ Cn πΏ)) & β’ (π β π» β (πΉ(π½ Htpy πΎ)πΊ)) β β’ (π β (π β π») β ((π β πΉ)(π½ Htpy πΏ)(π β πΊ))) | ||
Theorem | htpycc 24727* | Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ π = (π₯ β π, π¦ β (0[,]1) β¦ if(π¦ β€ (1 / 2), (π₯πΏ(2 Β· π¦)), (π₯π((2 Β· π¦) β 1)))) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ (π β π» β (π½ Cn πΎ)) & β’ (π β πΏ β (πΉ(π½ Htpy πΎ)πΊ)) & β’ (π β π β (πΊ(π½ Htpy πΎ)π»)) β β’ (π β π β (πΉ(π½ Htpy πΎ)π»)) | ||
Theorem | isphtpy 24728* | Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β (π» β (πΉ(PHtpyβπ½)πΊ) β (π» β (πΉ(II Htpy π½)πΊ) β§ βπ β (0[,]1)((0π»π ) = (πΉβ0) β§ (1π»π ) = (πΉβ1))))) | ||
Theorem | phtpyhtpy 24729 | A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β (πΉ(PHtpyβπ½)πΊ) β (πΉ(II Htpy π½)πΊ)) | ||
Theorem | phtpycn 24730 | A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β (πΉ(PHtpyβπ½)πΊ) β ((II Γt II) Cn π½)) | ||
Theorem | phtpyi 24731 | Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ ((π β§ π΄ β (0[,]1)) β ((0π»π΄) = (πΉβ0) β§ (1π»π΄) = (πΉβ1))) | ||
Theorem | phtpy01 24732 | Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) | ||
Theorem | isphtpyd 24733* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (πΉ(II Htpy π½)πΊ)) & β’ ((π β§ π β (0[,]1)) β (0π»π ) = (πΉβ0)) & β’ ((π β§ π β (0[,]1)) β (1π»π ) = (πΉβ1)) β β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) | ||
Theorem | isphtpy2d 24734* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β ((II Γt II) Cn π½)) & β’ ((π β§ π β (0[,]1)) β (π π»0) = (πΉβπ )) & β’ ((π β§ π β (0[,]1)) β (π π»1) = (πΊβπ )) & β’ ((π β§ π β (0[,]1)) β (0π»π ) = (πΉβ0)) & β’ ((π β§ π β (0[,]1)) β (1π»π ) = (πΉβ1)) β β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) | ||
Theorem | phtpycom 24735* | Given a homotopy from πΉ to πΊ, produce a homotopy from πΊ to πΉ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (π₯π»(1 β π¦))) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β πΎ β (πΊ(PHtpyβπ½)πΉ)) | ||
Theorem | phtpyid 24736* | A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβπ₯)) & β’ (π β πΉ β (II Cn π½)) β β’ (π β πΊ β (πΉ(PHtpyβπ½)πΉ)) | ||
Theorem | phtpyco2 24737 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π β (π½ Cn πΎ)) & β’ (π β π» β (πΉ(PHtpyβπ½)πΊ)) β β’ (π β (π β π») β ((π β πΉ)(PHtpyβπΎ)(π β πΊ))) | ||
Theorem | phtpycc 24738* | Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π¦ β€ (1 / 2), (π₯πΎ(2 Β· π¦)), (π₯πΏ((2 Β· π¦) β 1)))) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (II Cn π½)) & β’ (π β πΎ β (πΉ(PHtpyβπ½)πΊ)) & β’ (π β πΏ β (πΊ(PHtpyβπ½)π»)) β β’ (π β π β (πΉ(PHtpyβπ½)π»)) | ||
Definition | df-phtpc 24739* | Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ βph = (π₯ β Top β¦ {β¨π, πβ© β£ ({π, π} β (II Cn π₯) β§ (π(PHtpyβπ₯)π) β β )}) | ||
Theorem | phtpcrel 24740 | The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.) |
β’ Rel ( βphβπ½) | ||
Theorem | isphtpc 24741 | The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (πΉ( βphβπ½)πΊ β (πΉ β (II Cn π½) β§ πΊ β (II Cn π½) β§ (πΉ(PHtpyβπ½)πΊ) β β )) | ||
Theorem | phtpcer 24742 | Path homotopy is an equivalence relation. Proposition 1.2 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 6-Jul-2015.) (Proof shortened by AV, 1-May-2021.) |
β’ ( βphβπ½) Er (II Cn π½) | ||
Theorem | phtpc01 24743 | Path homotopic paths have the same endpoints. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (πΉ( βphβπ½)πΊ β ((πΉβ0) = (πΊβ0) β§ (πΉβ1) = (πΊβ1))) | ||
Theorem | reparphti 24744* | Lemma for reparpht 24746. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) Avoid ax-mulf 11193. (Revised by GG, 16-Mar-2025.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) & β’ π» = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβ(((1 β π¦) Β· (πΊβπ₯)) + (π¦ Β· π₯)))) β β’ (π β π» β ((πΉ β πΊ)(PHtpyβπ½)πΉ)) | ||
Theorem | reparphtiOLD 24745* | Obsolete version of reparphti 24744 as of 9-Apr-2025. (Contributed by NM, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) & β’ π» = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ (πΉβ(((1 β π¦) Β· (πΊβπ₯)) + (π¦ Β· π₯)))) β β’ (π β π» β ((πΉ β πΊ)(PHtpyβπ½)πΉ)) | ||
Theorem | reparpht 24746 | Reparametrization lemma. The reparametrization of a path by any continuous map πΊ:IIβΆII with πΊ(0) = 0 and πΊ(1) = 1 is path-homotopic to the original path. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Feb-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn II)) & β’ (π β (πΊβ0) = 0) & β’ (π β (πΊβ1) = 1) β β’ (π β (πΉ β πΊ)( βphβπ½)πΉ) | ||
Theorem | phtpcco2 24747 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 6-Jul-2015.) |
β’ (π β πΉ( βphβπ½)πΊ) & β’ (π β π β (π½ Cn πΎ)) β β’ (π β (π β πΉ)( βphβπΎ)(π β πΊ)) | ||
Syntax | cpco 24748 | Extend class notation with the concatenation operation for paths in a topological space. |
class *π | ||
Syntax | comi 24749 | Extend class notation with the loop space. |
class Ξ©1 | ||
Syntax | comn 24750 | Extend class notation with the higher loop spaces. |
class Ξ©π | ||
Syntax | cpi1 24751 | Extend class notation with the fundamental group. |
class Ο1 | ||
Syntax | cpin 24752 | Extend class notation with the higher homotopy groups. |
class Οn | ||
Definition | df-pco 24753* | Define the concatenation of two paths in a topological space π½. For simplicity of definition, we define it on all paths, not just those whose endpoints line up. Definition of [Hatcher] p. 26. Hatcher denotes path concatenation with a square dot; other authors, such as Munkres, use a star. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ *π = (π β Top β¦ (π β (II Cn π), π β (II Cn π) β¦ (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πβ(2 Β· π₯)), (πβ((2 Β· π₯) β 1)))))) | ||
Definition | df-om1 24754* | Define the loop space of a topological space, with a magma structure on it given by concatenation of loops. This structure is not a group, but the operation is compatible with homotopy, which allows the homotopy groups to be defined based on this operation. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ Ξ©1 = (π β Top, π¦ β βͺ π β¦ {β¨(Baseβndx), {π β (II Cn π) β£ ((πβ0) = π¦ β§ (πβ1) = π¦)}β©, β¨(+gβndx), (*πβπ)β©, β¨(TopSetβndx), (π βko II)β©}) | ||
Definition | df-omn 24755* | Define the n-th iterated loop space of a topological space. Unlike Ξ©1 this is actually a pointed topological space, which is to say a tuple of a topological space (a member of TopSp, not Top) and a point in the space. Higher loop spaces select the constant loop at the point from the lower loop space for the distinguished point. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ Ξ©π = (π β Top, π¦ β βͺ π β¦ seq0(((π₯ β V, π β V β¦ β¨((TopOpenβ(1st βπ₯)) Ξ©1 (2nd βπ₯)), ((0[,]1) Γ {(2nd βπ₯)})β©) β 1st ), β¨{β¨(Baseβndx), βͺ πβ©, β¨(TopSetβndx), πβ©}, π¦β©)) | ||
Definition | df-pi1 24756* | Define the fundamental group, whose operation is given by concatenation of homotopy classes of loops. Definition of [Hatcher] p. 26. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ Ο1 = (π β Top, π¦ β βͺ π β¦ ((π Ξ©1 π¦) /s ( βphβπ))) | ||
Definition | df-pin 24757* | Define the n-th homotopy group, which is formed by taking the π-th loop space and forming the quotient under the relation of path homotopy equivalence in the base space of the π-th loop space, which is the π β 1-th loop space. For π = 0, since this is not well-defined we replace this relation with the path-connectedness relation, so that the 0-th homotopy group is the set of path components of π. (Since the 0-th loop space does not have a group operation, neither does the 0-th homotopy group, but the rest are genuine groups.) (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ Οn = (π β Top, π β βͺ π β¦ (π β β0 β¦ ((1st β((π Ξ©π π)βπ)) /s if(π = 0, {β¨π₯, π¦β© β£ βπ β (II Cn π)((πβ0) = π₯ β§ (πβ1) = π¦)}, ( βphβ(TopOpenβ(1st β((π Ξ©π π)β(π β 1))))))))) | ||
Theorem | pcofval 24758* | The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof shortened by AV, 2-Mar-2024.) |
β’ (*πβπ½) = (π β (II Cn π½), π β (II Cn π½) β¦ (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πβ(2 Β· π₯)), (πβ((2 Β· π₯) β 1))))) | ||
Theorem | pcoval 24759* | The concatenation of two paths. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β (πΉ(*πβπ½)πΊ) = (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), (πΉβ(2 Β· π₯)), (πΊβ((2 Β· π₯) β 1))))) | ||
Theorem | pcovalg 24760 | Evaluate the concatenation of two paths. (Contributed by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ ((π β§ π β (0[,]1)) β ((πΉ(*πβπ½)πΊ)βπ) = if(π β€ (1 / 2), (πΉβ(2 Β· π)), (πΊβ((2 Β· π) β 1)))) | ||
Theorem | pcoval1 24761 | Evaluate the concatenation of two paths on the first half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ ((π β§ π β (0[,](1 / 2))) β ((πΉ(*πβπ½)πΊ)βπ) = (πΉβ(2 Β· π))) | ||
Theorem | pco0 24762 | The starting point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β ((πΉ(*πβπ½)πΊ)β0) = (πΉβ0)) | ||
Theorem | pco1 24763 | The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) β β’ (π β ((πΉ(*πβπ½)πΊ)β1) = (πΊβ1)) | ||
Theorem | pcoval2 24764 | Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) β β’ ((π β§ π β ((1 / 2)[,]1)) β ((πΉ(*πβπ½)πΊ)βπ) = (πΊβ((2 Β· π) β 1))) | ||
Theorem | pcocn 24765 | The concatenation of two paths is a path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) β β’ (π β (πΉ(*πβπ½)πΊ) β (II Cn π½)) | ||
Theorem | copco 24766 | The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β π» β (π½ Cn πΎ)) β β’ (π β (π» β (πΉ(*πβπ½)πΊ)) = ((π» β πΉ)(*πβπΎ)(π» β πΊ))) | ||
Theorem | pcohtpylem 24767* | Lemma for pcohtpy 24768. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β πΉ( βphβπ½)π») & β’ (π β πΊ( βphβπ½)πΎ) & β’ π = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ if(π₯ β€ (1 / 2), ((2 Β· π₯)ππ¦), (((2 Β· π₯) β 1)ππ¦))) & β’ (π β π β (πΉ(PHtpyβπ½)π»)) & β’ (π β π β (πΊ(PHtpyβπ½)πΎ)) β β’ (π β π β ((πΉ(*πβπ½)πΊ)(PHtpyβπ½)(π»(*πβπ½)πΎ))) | ||
Theorem | pcohtpy 24768 | Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 24-Feb-2015.) |
β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β πΉ( βphβπ½)π») & β’ (π β πΊ( βphβπ½)πΎ) β β’ (π β (πΉ(*πβπ½)πΊ)( βphβπ½)(π»(*πβπ½)πΎ)) | ||
Theorem | pcoptcl 24769 | A constant function is a path from π to itself. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 19-Mar-2015.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((π½ β (TopOnβπ) β§ π β π) β (π β (II Cn π½) β§ (πβ0) = π β§ (πβ1) = π)) | ||
Theorem | pcopt 24770 | Concatenation with a point does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((πΉ β (II Cn π½) β§ (πΉβ0) = π) β (π(*πβπ½)πΉ)( βphβπ½)πΉ) | ||
Theorem | pcopt2 24771 | Concatenation with a point does not affect homotopy class. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π = ((0[,]1) Γ {π}) β β’ ((πΉ β (II Cn π½) β§ (πΉβ1) = π) β (πΉ(*πβπ½)π)( βphβπ½)πΉ) | ||
Theorem | pcoass 24772* | Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β π» β (II Cn π½)) & β’ (π β (πΉβ1) = (πΊβ0)) & β’ (π β (πΊβ1) = (π»β0)) & β’ π = (π₯ β (0[,]1) β¦ if(π₯ β€ (1 / 2), if(π₯ β€ (1 / 4), (2 Β· π₯), (π₯ + (1 / 4))), ((π₯ / 2) + (1 / 2)))) β β’ (π β ((πΉ(*πβπ½)πΊ)(*πβπ½)π»)( βphβπ½)(πΉ(*πβπ½)(πΊ(*πβπ½)π»))) | ||
Theorem | pcorevcl 24773* | Closure for a reversed path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (πΉ β (II Cn π½) β (πΊ β (II Cn π½) β§ (πΊβ0) = (πΉβ1) β§ (πΊβ1) = (πΉβ0))) | ||
Theorem | pcorevlem 24774* | Lemma for pcorev 24775. Prove continuity of the homotopy function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ1)}) & β’ π» = (π β (0[,]1), π‘ β (0[,]1) β¦ (πΉβif(π β€ (1 / 2), (1 β ((1 β π‘) Β· (2 Β· π ))), (1 β ((1 β π‘) Β· (1 β ((2 Β· π ) β 1))))))) β β’ (πΉ β (II Cn π½) β (π» β ((πΊ(*πβπ½)πΉ)(PHtpyβπ½)π) β§ (πΊ(*πβπ½)πΉ)( βphβπ½)π)) | ||
Theorem | pcorev 24775* | Concatenation with the reverse path. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ1)}) β β’ (πΉ β (II Cn π½) β (πΊ(*πβπ½)πΉ)( βphβπ½)π) | ||
Theorem | pcorev2 24776* | Concatenation with the reverse path. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ πΊ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ0)}) β β’ (πΉ β (II Cn π½) β (πΉ(*πβπ½)πΊ)( βphβπ½)π) | ||
Theorem | pcophtb 24777* | The path homotopy equivalence relation on two paths πΉ, πΊ with the same start and end point can be written in terms of the loop πΉ β πΊ formed by concatenating πΉ with the inverse of πΊ. Thus, all the homotopy information in βphβπ½ is available if we restrict our attention to closed loops, as in the definition of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) |
β’ π» = (π₯ β (0[,]1) β¦ (πΊβ(1 β π₯))) & β’ π = ((0[,]1) Γ {(πΉβ0)}) & β’ (π β πΉ β (II Cn π½)) & β’ (π β πΊ β (II Cn π½)) & β’ (π β (πΉβ0) = (πΊβ0)) & β’ (π β (πΉβ1) = (πΊβ1)) β β’ (π β ((πΉ(*πβπ½)π»)( βphβπ½)π β πΉ( βphβπ½)πΊ)) | ||
Theorem | om1val 24778* | The definition of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = {π β (II Cn π½) β£ ((πβ0) = π β§ (πβ1) = π)}) & β’ (π β + = (*πβπ½)) & β’ (π β πΎ = (π½ βko II)) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β π = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(TopSetβndx), πΎβ©}) | ||
Theorem | om1bas 24779* | The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) β β’ (π β π΅ = {π β (II Cn π½) β£ ((πβ0) = π β§ (πβ1) = π)}) | ||
Theorem | om1elbas 24780 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) β β’ (π β (πΉ β π΅ β (πΉ β (II Cn π½) β§ (πΉβ0) = π β§ (πΉβ1) = π))) | ||
Theorem | om1addcl 24781 | Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (Baseβπ)) & β’ (π β π» β π΅) & β’ (π β πΎ β π΅) β β’ (π β (π»(*πβπ½)πΎ) β π΅) | ||
Theorem | om1plusg 24782 | The group operation (which isn't much more than a magma) of the loop space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (*πβπ½) = (+gβπ)) | ||
Theorem | om1tset 24783 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π½ βko II) = (TopSetβπ)) | ||
Theorem | om1opn 24784 | The topology of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ π = (π½ Ξ©1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ πΎ = (TopOpenβπ) & β’ (π β π΅ = (Baseβπ)) β β’ (π β πΎ = ((π½ βko II) βΎt π΅)) | ||
Theorem | pi1val 24785 | The definition of the fundamental group. (Contributed by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) β β’ (π β πΊ = (π /s ( βphβπ½))) | ||
Theorem | pi1bas 24786 | The base set of the fundamental group of a topological space at a given base point. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β π΅ = (πΎ / ( βphβπ½))) | ||
Theorem | pi1blem 24787 | Lemma for pi1buni 24788. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β ((( βphβπ½) β πΎ) β πΎ β§ πΎ β (II Cn π½))) | ||
Theorem | pi1buni 24788 | Another way to write the loop space base in terms of the base of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π½ Ξ©1 π) & β’ (π β π΅ = (BaseβπΊ)) & β’ (π β πΎ = (Baseβπ)) β β’ (π β βͺ π΅ = πΎ) | ||
Theorem | pi1bas2 24789 | The base set of the fundamental group, written self-referentially. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) β β’ (π β π΅ = (βͺ π΅ / ( βphβπ½))) | ||
Theorem | pi1eluni 24790 | Elementhood in the base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) β β’ (π β (πΉ β βͺ π΅ β (πΉ β (II Cn π½) β§ (πΉβ0) = π β§ (πΉβ1) = π))) | ||
Theorem | pi1bas3 24791 | The base set of the fundamental group. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) & β’ π = (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)) β β’ (π β π΅ = (βͺ π΅ / π )) | ||
Theorem | pi1cpbl 24792 | The group operation, loop concatenation, is compatible with homotopy equivalence. (Contributed by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β π΅ = (BaseβπΊ)) & β’ π = (( βphβπ½) β© (βͺ π΅ Γ βͺ π΅)) & β’ π = (π½ Ξ©1 π) & β’ + = (+gβπ) β β’ (π β ((ππ π β§ ππ π) β (π + π)π (π + π))) | ||
Theorem | elpi1 24793* | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (πΉ β π΅ β βπ β (II Cn π½)(((πβ0) = π β§ (πβ1) = π) β§ πΉ = [π]( βphβπ½)))) | ||
Theorem | elpi1i 24794 | The elements of the fundamental group. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β πΉ β (II Cn π½)) & β’ (π β (πΉβ0) = π) & β’ (π β (πΉβ1) = π) β β’ (π β [πΉ]( βphβπ½) β π΅) | ||
Theorem | pi1addf 24795 | The group operation of Ο1 is a binary operation. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ + = (+gβπΊ) β β’ (π β + :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | pi1addval 24796 | The concatenation of two path-homotopy classes in the fundamental group. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Jul-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ + = (+gβπΊ) & β’ (π β π β βͺ π΅) & β’ (π β π β βͺ π΅) β β’ (π β ([π]( βphβπ½) + [π]( βphβπ½)) = [(π(*πβπ½)π)]( βphβπ½)) | ||
Theorem | pi1grplem 24797 | Lemma for pi1grp 24798. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π΅ = (BaseβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ 0 = ((0[,]1) Γ {π}) β β’ (π β (πΊ β Grp β§ [ 0 ]( βphβπ½) = (0gβπΊ))) | ||
Theorem | pi1grp 24798 | The fundamental group is a group. Proposition 1.3 of [Hatcher] p. 26. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) β β’ ((π½ β (TopOnβπ) β§ π β π) β πΊ β Grp) | ||
Theorem | pi1id 24799 | The identity element of the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ 0 = ((0[,]1) Γ {π}) β β’ ((π½ β (TopOnβπ) β§ π β π) β [ 0 ]( βphβπ½) = (0gβπΊ)) | ||
Theorem | pi1inv 24800* | An inverse in the fundamental group. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 10-Aug-2015.) |
β’ πΊ = (π½ Ο1 π) & β’ π = (invgβπΊ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β πΉ β (II Cn π½)) & β’ (π β (πΉβ0) = π) & β’ (π β (πΉβ1) = π) & β’ πΌ = (π₯ β (0[,]1) β¦ (πΉβ(1 β π₯))) β β’ (π β (πβ[πΉ]( βphβπ½)) = [πΌ]( βphβπ½)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |