![]() |
Metamath
Proof Explorer Theorem List (p. 238 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 | fbflim 23701* | A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ₯ β π½ (π΄ β π₯ β βπ¦ β π΅ π¦ β π₯)))) | ||
Theorem | fbflim2 23702* | A condition for a filter base π΅ to converge to a point π΄. Use neighborhoods instead of open neighborhoods. Compare fbflim 23701. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π))) | ||
Theorem | flimclsi 23703 | The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (π β πΉ β (π½ fLim πΉ) β ((clsβπ½)βπ)) | ||
Theorem | hausflimlem 23704 | If π΄ and π΅ are both limits of the same filter, then all neighborhoods of π΄ and π΅ intersect. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β (π β© π) β β ) | ||
Theorem | hausflimi 23705* | One direction of hausflim 23706. A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010.) (Revised by Mario Carneiro, 21-Sep-2015.) |
β’ (π½ β Haus β β*π₯ π₯ β (π½ fLim πΉ)) | ||
Theorem | hausflim 23706* | A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ β (Filβπ)β*π₯ π₯ β (π½ fLim π))) | ||
Theorem | flimcf 23707* | Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ β πΎ β βπ β (Filβπ)(πΎ fLim π) β (π½ fLim π))) | ||
Theorem | flimrest 23708 | The set of limit points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fLim (πΉ βΎt π)) = ((π½ fLim πΉ) β© π)) | ||
Theorem | flimclslem 23709 | Lemma for flimcls 23710. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) β β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (πΉ β (Filβπ) β§ π β πΉ β§ π΄ β (π½ fLim πΉ))) | ||
Theorem | flimcls 23710* | Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π β π) β (π΄ β ((clsβπ½)βπ) β βπ β (Filβπ)(π β π β§ π΄ β (π½ fLim π)))) | ||
Theorem | flimsncls 23711 | If π΄ is a limit point of the filter πΉ, then all the points which specialize π΄ (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β (π½ fLim πΉ)) | ||
Theorem | hauspwpwf1 23712* | Lemma for hauspwpwdom 23713. Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015.) |
β’ π = βͺ π½ & β’ πΉ = (π₯ β ((clsβπ½)βπ΄) β¦ {π β£ βπ β π½ (π₯ β π β§ π = (π β© π΄))}) β β’ ((π½ β Haus β§ π΄ β π) β πΉ:((clsβπ½)βπ΄)β1-1βπ« π« π΄) | ||
Theorem | hauspwpwdom 23713 | If π is a Hausdorff space, then the cardinality of the closure of a set π΄ is bounded by the double powerset of π΄. In particular, a Hausdorff space with a dense subset π΄ has cardinality at most π« π« π΄, and a separable Hausdorff space has cardinality at most π« π« β. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π΄ β π) β ((clsβπ½)βπ΄) βΌ π« π« π΄) | ||
Theorem | flffval 23714* | Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLimf πΏ) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))) | ||
Theorem | flfval 23715 | Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) | ||
Theorem | flfnei 23716* | The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (πΉ β π ) β π))) | ||
Theorem | flfneii 23717* | A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fLimf πΏ)βπΉ) β§ π β ((neiβπ½)β{π΄})) β βπ β πΏ (πΉ β π ) β π) | ||
Theorem | isflf 23718* | The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (πΉ β π ) β π)))) | ||
Theorem | flfelbas 23719 | A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fLimf πΏ)βπΉ)) β π΄ β π) | ||
Theorem | flffbas 23720* | Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (πΉ β π ) β π)))) | ||
Theorem | flftg 23721* | Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (topGenβπ΅) β β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π΅ (π΄ β π β βπ β πΏ (πΉ β π ) β π)))) | ||
Theorem | hausflf 23722* | If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β β*π₯ π₯ β ((π½ fLimf πΏ)βπΉ)) | ||
Theorem | hausflf2 23723 | If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Haus β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ ((π½ fLimf πΏ)βπΉ) β β ) β ((π½ fLimf πΏ)βπΉ) β 1o) | ||
Theorem | cnpflfi 23724 | Forward direction of cnpflf 23726. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)) | ||
Theorem | cnpflf2 23725 | πΉ is continuous at point π΄ iff a limit of πΉ when π₯ tends to π΄ is (πΉβπ΄). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ πΏ = ((neiβπ½)β{π΄}) β β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)))) | ||
Theorem | cnpflf 23726* | Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) | ||
Theorem | cnflf 23727* | A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) | ||
Theorem | cnflf2 23728* | A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)(πΉ β (π½ fLim π)) β ((πΎ fLimf π)βπΉ)))) | ||
Theorem | flfcnp 23729 | A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΊβπ΄) β ((πΎ fLimf πΏ)β(πΊ β πΉ))) | ||
Theorem | lmflf 23730 | The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ πΏ = (πfilGen(β€β₯ β π)) β β’ ((π½ β (TopOnβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ(βπ‘βπ½)π β π β ((π½ fLimf πΏ)βπΉ))) | ||
Theorem | txflf 23731* | Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ π» = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) β β’ (π β (β¨π , πβ© β (((π½ Γt πΎ) fLimf πΏ)βπ») β (π β ((π½ fLimf πΏ)βπΉ) β§ π β ((πΎ fLimf πΏ)βπΊ)))) | ||
Theorem | flfcnp2 23732* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (Filβπ)) & β’ ((π β§ π₯ β π) β π΄ β π) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β π β ((π½ fLimf πΏ)β(π₯ β π β¦ π΄))) & β’ (π β π β ((πΎ fLimf πΏ)β(π₯ β π β¦ π΅))) & β’ (π β π β (((π½ Γt πΎ) CnP π)ββ¨π , πβ©)) β β’ (π β (π ππ) β ((π fLimf πΏ)β(π₯ β π β¦ (π΄ππ΅)))) | ||
Theorem | fclsval 23733* | The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = if(π = π, β© π‘ β πΉ ((clsβπ½)βπ‘), β )) | ||
Theorem | isfcls 23734* | A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β (π½ β Top β§ πΉ β (Filβπ) β§ βπ β πΉ π΄ β ((clsβπ½)βπ ))) | ||
Theorem | fclsfil 23735 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β πΉ β (Filβπ)) | ||
Theorem | fclstop 23736 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) | ||
Theorem | fclstopon 23737 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π΄ β (π½ fClus πΉ) β (π½ β (TopOnβπ) β πΉ β (Filβπ))) | ||
Theorem | isfcls2 23738* | A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β βπ β πΉ π΄ β ((clsβπ½)βπ ))) | ||
Theorem | fclsopn 23739* | Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β )))) | ||
Theorem | fclsopni 23740 | An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π΄ β (π½ fClus πΉ) β§ (π β π½ β§ π΄ β π β§ π β πΉ)) β (π β© π) β β ) | ||
Theorem | fclselbas 23741 | A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β π΄ β π) | ||
Theorem | fclsneii 23742 | A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (π β© π) β β ) | ||
Theorem | fclssscls 23743 | The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β πΉ β (π½ fClus πΉ) β ((clsβπ½)βπ)) | ||
Theorem | fclsnei 23744* | Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΉ (π β© π ) β β ))) | ||
Theorem | supnfcls 23745* | The filter of supersets of π β π does not cluster at any point of the open set π. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β Β¬ π΄ β (π½ fClus {π₯ β π« π β£ (π β π) β π₯})) | ||
Theorem | fclsbas 23746* | Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (π β© π ) β β )))) | ||
Theorem | fclsss1 23747 | A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β (πΎ fClus πΉ) β (π½ fClus πΉ)) | ||
Theorem | fclsss2 23748 | A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΉ β πΊ) β (π½ fClus πΊ) β (π½ fClus πΉ)) | ||
Theorem | fclsrest 23749 | The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fClus (πΉ βΎt π)) = ((π½ fClus πΉ) β© π)) | ||
Theorem | fclscf 23750* | Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ β πΎ β βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π))) | ||
Theorem | flimfcls 23751 | A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π½ fLim πΉ) β (π½ fClus πΉ) | ||
Theorem | fclsfnflim 23752* | A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) | ||
Theorem | flimfnfcls 23753* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23752, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (πΉ β (Filβπ) β (π΄ β (π½ fLim πΉ) β βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)))) | ||
Theorem | fclscmpi 23754 | Forward direction of fclscmp 23755. Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π½ fClus πΉ) β β ) | ||
Theorem | fclscmp 23755* | A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β )) | ||
Theorem | uffclsflim 23756 | The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (π½ fClus πΉ) = (π½ fLim πΉ)) | ||
Theorem | ufilcmp 23757* | A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009.) (Proof shortened by Mario Carneiro, 12-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fLim π) β β )) | ||
Theorem | fcfval 23758 | The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fClusf πΏ)βπΉ) = (π½ fClus ((π FilMap πΉ)βπΏ))) | ||
Theorem | isfcf 23759* | The property of being a cluster point of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β )))) | ||
Theorem | fcfnei 23760* | The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β ))) | ||
Theorem | fcfelbas 23761 | A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fClusf πΏ)βπΉ)) β π΄ β π) | ||
Theorem | fcfneii 23762 | A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fClusf πΏ)βπΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΏ)) β (π β© (πΉ β π)) β β ) | ||
Theorem | flfssfcf 23763 | A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) β ((π½ fClusf πΏ)βπΉ)) | ||
Theorem | uffcfflf 23764 | If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (UFilβπ) β§ πΉ:πβΆπ) β ((π½ fClusf πΏ)βπΉ) = ((π½ fLimf πΏ)βπΉ)) | ||
Theorem | cnpfcfi 23765 | Lemma for cnpfcf 23766. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((πΎ β Top β§ π΄ β (π½ fClus πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fClusf πΏ)βπΉ)) | ||
Theorem | cnpfcf 23766* | A function πΉ is continuous at point π΄ iff πΉ respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))))) | ||
Theorem | cnfcf 23767* | Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fClus π)(πΉβπ₯) β ((πΎ fClusf π)βπΉ)))) | ||
Theorem | flfcntr 23768 | A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β π΄ β πΆ) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β π β π΄) β β’ (π β (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) | ||
Theorem | alexsublem 23769* | Lemma for alexsub 23770. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β UFL) & β’ (π β π = βͺ π΅) & β’ (π β π½ = (topGenβ(fiβπ΅))) & β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) & β’ (π β πΉ β (UFilβπ)) & β’ (π β (π½ fLim πΉ) = β ) β β’ Β¬ π | ||
Theorem | alexsub 23770* | The Alexander Subbase Theorem: If π΅ is a subbase for the topology π½, and any cover taken from π΅ has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT 23776 for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β UFL) & β’ (π β π = βͺ π΅) & β’ (π β π½ = (topGenβ(fiβπ΅))) & β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β β’ (π β π½ β Comp) | ||
Theorem | alexsubb 23771* | Biconditional form of the Alexander Subbase Theorem alexsub 23770. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((π β UFL β§ π = βͺ π΅) β ((topGenβ(fiβπ΅)) β Comp β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) | ||
Theorem | alexsubALTlem1 23772* | Lemma for alexsubALT 23776. A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010.) |
β’ π = βͺ π½ β β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | alexsubALTlem2 23773* | Lemma for alexsubALT 23776. Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010.) |
β’ π = βͺ π½ β β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ π) β βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β })βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β }) Β¬ π’ β π£) | ||
Theorem | alexsubALTlem3 23774* | Lemma for alexsubALT 23776. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ π = βͺ π½ β β’ (((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ β π‘ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) | ||
Theorem | alexsubALTlem4 23775* | Lemma for alexsubALT 23776. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ π = βͺ π½ β β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π« (fiβπ₯)(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | alexsubALT 23776* | The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = βͺ π½ β β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | ptcmplem1 23777* | Lemma for ptcmp 23783. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (π = βͺ (ran π βͺ {π}) β§ (βtβπΉ) = (topGenβ(fiβ(ran π βͺ {π}))))) | ||
Theorem | ptcmplem2 23778* | Lemma for ptcmp 23783. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) β β’ (π β βͺ π β {π β π΄ β£ Β¬ βͺ (πΉβπ) β 1o}βͺ (πΉβπ) β dom card) | ||
Theorem | ptcmplem3 23779* | Lemma for ptcmp 23783. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ (π β βπ(π Fn π΄ β§ βπ β π΄ (πβπ) β (βͺ (πΉβπ) β βͺ πΎ))) | ||
Theorem | ptcmplem4 23780* | Lemma for ptcmp 23783. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ Β¬ π | ||
Theorem | ptcmplem5 23781* | Lemma for ptcmp 23783. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (βtβπΉ) β Comp) | ||
Theorem | ptcmpg 23782 | Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if π« π« π is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 23783). (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π½ = (βtβπΉ) & β’ π = βͺ π½ β β’ ((π΄ β π β§ πΉ:π΄βΆComp β§ π β (UFL β© dom card)) β π½ β Comp) | ||
Theorem | ptcmp 23783 | Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆComp) β (βtβπΉ) β Comp) | ||
Syntax | ccnext 23784 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 23785* | Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ CnExt = (π β Top, π β Top β¦ (π β (βͺ π βpm βͺ π) β¦ βͺ π₯ β ((clsβπ)βdom π)({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ)))) | ||
Theorem | cnextval 23786* | The function applying continuous extension to a given function π. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½CnExtπΎ) = (π β (βͺ πΎ βpm βͺ π½) β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) | ||
Theorem | cnextfval 23787* | The continuous extension of a given function πΉ. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ π = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β ((π½CnExtπΎ)βπΉ) = βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) | ||
Theorem | cnextrel 23788 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) | ||
Theorem | cnextfun 23789 | If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) | ||
Theorem | cnextfvval 23790* | The value of the continuous extension of a given function πΉ at a point π. (Contributed by Thierry Arnoux, 21-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) β β’ ((π β§ π β πΆ) β (((π½CnExtπΎ)βπΉ)βπ) = βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) | ||
Theorem | cnextf 23791* | Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) β β’ (π β ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) | ||
Theorem | cnextcn 23792* | Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology π½ on πΆ, a subset π΄ dense in πΆ, this states a condition for πΉ from π΄ to a regular space πΎ to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) & β’ (π β πΎ β Reg) β β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) | ||
Theorem | cnextfres1 23793* | πΉ and its extension by continuity agree on the domain of πΉ. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) & β’ (π β πΎ β Reg) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) β β’ (π β (((π½CnExtπΎ)βπΉ) βΎ π΄) = πΉ) | ||
Theorem | cnextfres 23794 | πΉ and its extension by continuity agree on the domain of πΉ. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β π΄ β πΆ) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β π β π΄) β β’ (π β (((π½CnExtπΎ)βπΉ)βπ) = (πΉβπ)) | ||
Syntax | ctmd 23795 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 23796 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 23797* | Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ TopMnd = {π β (Mnd β© TopSp) β£ [(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π)} | ||
Definition | df-tgp 23798* | Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.) |
β’ TopGrp = {π β (Grp β© TopMnd) β£ [(TopOpenβπ) / π](invgβπ) β (π Cn π)} | ||
Theorem | istmd 23799 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ πΉ = (+πβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopMnd β (πΊ β Mnd β§ πΊ β TopSp β§ πΉ β ((π½ Γt π½) Cn π½))) | ||
Theorem | tmdmnd 23800 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopMnd β πΊ β Mnd) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |