HomeTheorem List (p. 227 of 480)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 227 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: | Metamath Proof Explorer
(1-30438) |
Hilbert Space Explorer
(30439-31961) |
Users' Mathboxes
(31962-47939) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cpmidgsum2 22601* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΌ = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π» = (πΎ Β· 1 ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))π» = (π Ξ£g (π β β0 β¦ ((π β π) Β· (πΊβπ))))) | ||
| Theorem | cpmidg2sum 22602* | Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ Β· = ( Β·π βπ) & β’ Γ = (.rβπ) & β’ 1 = (1rβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ πΌ = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ π = (algScβπ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(π Ξ£g (π β β0 β¦ ((π β π) Β· ((πβ((coe1βπΎ)βπ)) Β· 1 )))) = (π Ξ£g (π β β0 β¦ ((π β π) Β· (πΊβπ))))) | ||
| Theorem | cpmadumatpolylem1 22603* | Lemma 1 for cpmadumatpoly 22605. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (π ConstPolyMat π ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (var1βπ ) & β’ π· = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ π = (Baseβπ) & β’ π = (Poly1βπ΄) & β’ π = (var1βπ΄) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (π cPolyMatToMat π ) β β’ ((((π β Fin β§ π β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π β πΊ) β (π΅ βm β0)) | ||
| Theorem | cpmadumatpolylem2 22604* | Lemma 2 for cpmadumatpoly 22605. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (π ConstPolyMat π ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (var1βπ ) & β’ π· = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ π = (Baseβπ) & β’ π = (Poly1βπ΄) & β’ π = (var1βπ΄) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (π cPolyMatToMat π ) β β’ ((((π β Fin β§ π β CRing β§ π β π΅) β§ π β β) β§ π β (π΅ βm (0...π ))) β (π β πΊ) finSupp (0gβπ΄)) | ||
| Theorem | cpmadumatpoly 22605* | The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 7-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ π = (π matToPolyMat π ) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (π ConstPolyMat π ) & β’ Β· = ( Β·π βπ) & β’ 1 = (1rβπ) & β’ π = (var1βπ ) & β’ π· = ((π Β· 1 ) β (πβπ)) & β’ π½ = (π maAdju π) & β’ π = (Baseβπ) & β’ π = (Poly1βπ΄) & β’ π = (var1βπ΄) & β’ β = ( Β·π βπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π = (π cPolyMatToMat π ) & β’ πΌ = (π pMatToMatPoly π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(πΌβ(π· Γ (π½βπ·))) = (π Ξ£g (π β β0 β¦ ((πβ(πΊβπ)) β (π β π))))) | ||
| Theorem | cayhamlem2 22606 | Lemma for cayhamlem3 22609. (Contributed by AV, 24-Nov-2019.) |
| β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) & β’ Β· = (.rβπ΄) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π» β (πΎ βm β0) β§ πΏ β β0)) β ((π»βπΏ) β (πΏ β π)) = ((πΏ β π) Β· ((π»βπΏ) β 1 ))) | ||
| Theorem | chcoeffeqlem 22607* | Lemma for chcoeffeq 22608. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (Baseβπ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π cPolyMatToMat π ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (((Poly1βπ΄) Ξ£g (π β β0 β¦ ((πβ(πΊβπ))( Β·π β(Poly1βπ΄))(π(.gβ(mulGrpβ(Poly1βπ΄)))(var1βπ΄))))) = ((Poly1βπ΄) Ξ£g (π β β0 β¦ ((((coe1βπΎ)βπ) β 1 )( Β·π β(Poly1βπ΄))(π(.gβ(mulGrpβ(Poly1βπ΄)))(var1βπ΄))))) β βπ β β0 (πβ(πΊβπ)) = (((coe1βπΎ)βπ) β 1 ))) | ||
| Theorem | chcoeffeq 22608* | The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 8-Dec-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (Baseβπ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π cPolyMatToMat π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))βπ β β0 (πβ(πΊβπ)) = (((coe1βπΎ)βπ) β 1 )) | ||
| Theorem | cayhamlem3 22609* | Lemma for cayhamlem4 22610. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (Baseβπ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π cPolyMatToMat π ) & β’ β = (.gβ(mulGrpβπ΄)) & β’ Β· = (.rβπ΄) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(π΄ Ξ£g (π β β0 β¦ (((coe1βπΎ)βπ) β (π β π)))) = (π΄ Ξ£g (π β β0 β¦ ((π β π) Β· (πβ(πΊβπ)))))) | ||
| Theorem | cayhamlem4 22610* | Lemma for cayleyhamilton 22612. (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (π matToPolyMat π ) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (πΆβπ) & β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (Baseβπ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ π = (π cPolyMatToMat π ) & β’ β = (.gβ(mulGrpβπ΄)) & β’ πΈ = (.gβ(mulGrpβπ)) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β βπ β β βπ β (π΅ βm (0...π ))(π΄ Ξ£g (π β β0 β¦ (((coe1βπΎ)βπ) β (π β π)))) = (πβ(π Ξ£g (π β β0 β¦ ((ππΈ(πβπ)) Γ (πΊβπ)))))) | ||
| Theorem | cayleyhamilton0 22611* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 22612 provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT 22613)! (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (coe1β(πΆβπ)) & β’ π = (Poly1βπ ) & β’ π = (π Mat π) & β’ Γ = (.rβπ) & β’ β = (-gβπ) & β’ π = (0gβπ) & β’ π = (Baseβπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (π matToPolyMat π ) & β’ πΊ = (π β β0 β¦ if(π = 0, (π β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, π, ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) & β’ π = (π cPolyMatToMat π ) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (π΄ Ξ£g (π β β0 β¦ ((πΎβπ) β (π β π)))) = 0 ) | ||
| Theorem | cayleyhamilton 22612* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", see theorem 7.8 in [Roman] p. 170 (without proof!), or theorem 3.1 in [Lang] p. 561. In other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. This is Metamath 100 proof #49. (Contributed by Alexander van der Vekens, 25-Nov-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (coe1β(πΆβπ)) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (π΄ Ξ£g (π β β0 β¦ ((πΎβπ) β (π β π)))) = 0 ) | ||
| Theorem | cayleyhamiltonALT 22613* | Alternate proof of cayleyhamilton 22612, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 22611 directly, but has the same structure as the proof of cayleyhamilton0 22611. In contrast to the proof of cayleyhamilton0 22611, only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (coe1β(πΆβπ)) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) β β’ ((π β Fin β§ π β CRing β§ π β π΅) β (π΄ Ξ£g (π β β0 β¦ ((πΎβπ) β (π β π)))) = 0 ) | ||
| Theorem | cayleyhamilton1 22614* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton 22612, the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients (πΉβπ), then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019.) |
| β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ 0 = (0gβπ΄) & β’ πΆ = (π CharPlyMat π ) & β’ πΎ = (coe1β(πΆβπ)) & β’ β = ( Β·π βπ΄) & β’ β = (.gβ(mulGrpβπ΄)) & β’ πΏ = (Baseβπ ) & β’ π = (var1βπ ) & β’ π = (Poly1βπ ) & β’ Β· = ( Β·π βπ) & β’ πΈ = (.gβ(mulGrpβπ)) & β’ π = (0gβπ ) β β’ (((π β Fin β§ π β CRing β§ π β π΅) β§ (πΉ β (πΏ βm β0) β§ πΉ finSupp π)) β ((πΆβπ) = (π Ξ£g (π β β0 β¦ ((πΉβπ) Β· (ππΈπ)))) β (π΄ Ξ£g (π β β0 β¦ ((πΉβπ) β (π β π)))) = 0 )) | ||
A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union, see toponuni 22636), and it may sometimes be more convenient to consider topologies without reference to the underlying set. This is why we define successively the class of topologies (df-top 22616), then the function which associates with a set the set of topologies on it (df-topon 22633), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp 22655). Of course, a topology is the same thing as a topology on a set (see toprntopon 22647). | ||
| Syntax | ctop 22615 | Syntax for the class of topologies. |
| class Top | ||
| Definition | df-top 22616* |
Define the class of topologies. It is a proper class (see topnex 22719).
See istopg 22617 and istop2g 22618 for the corresponding characterizations,
using respectively binary intersections like in this definition and
nonempty finite intersections.
The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.) |
| β’ Top = {π₯ β£ (βπ¦ β π« π₯βͺ π¦ β π₯ β§ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β π₯)} | ||
| Theorem | istopg 22617* |
Express the predicate "π½ is a topology". See istop2g 22618 for another
characterization using nonempty finite intersections instead of binary
intersections.
Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use π to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
| β’ (π½ β π΄ β (π½ β Top β (βπ₯(π₯ β π½ β βͺ π₯ β π½) β§ βπ₯ β π½ βπ¦ β π½ (π₯ β© π¦) β π½))) | ||
| Theorem | istop2g 22618* | Express the predicate "π½ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 22617. (Contributed by NM, 19-Jul-2006.) |
| β’ (π½ β π΄ β (π½ β Top β (βπ₯(π₯ β π½ β βͺ π₯ β π½) β§ βπ₯((π₯ β π½ β§ π₯ β β β§ π₯ β Fin) β β© π₯ β π½)))) | ||
| Theorem | uniopn 22619 | The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.) |
| β’ ((π½ β Top β§ π΄ β π½) β βͺ π΄ β π½) | ||
| Theorem | iunopn 22620* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
| β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β π½) β βͺ π₯ β π΄ π΅ β π½) | ||
| Theorem | inopn 22621 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
| β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||
| Theorem | fitop 22622 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) |
| β’ (π½ β Top β (fiβπ½) = π½) | ||
| Theorem | fiinopn 22623 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
| β’ (π½ β Top β ((π΄ β π½ β§ π΄ β β β§ π΄ β Fin) β β© π΄ β π½)) | ||
| Theorem | iinopn 22624* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) |
| β’ ((π½ β Top β§ (π΄ β Fin β§ π΄ β β β§ βπ₯ β π΄ π΅ β π½)) β β© π₯ β π΄ π΅ β π½) | ||
| Theorem | unopn 22625 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ βͺ π΅) β π½) | ||
| Theorem | 0opn 22626 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
| β’ (π½ β Top β β β π½) | ||
| Theorem | 0ntop 22627 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
| β’ Β¬ β β Top | ||
| Theorem | topopn 22628 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
| β’ π = βͺ π½ β β’ (π½ β Top β π β π½) | ||
| Theorem | eltopss 22629 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
| β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½) β π΄ β π) | ||
| Theorem | riinopn 22630* | A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β Fin β§ βπ₯ β π΄ π΅ β π½) β (π β© β© π₯ β π΄ π΅) β π½) | ||
| Theorem | rintopn 22631 | A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½ β§ π΄ β Fin) β (π β© β© π΄) β π½) | ||
| Syntax | ctopon 22632 | Syntax for the function of topologies on sets. |
| class TopOn | ||
| Definition | df-topon 22633* | Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| β’ TopOn = (π β V β¦ {π β Top β£ π = βͺ π}) | ||
| Theorem | istopon 22634 | Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.) |
| β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) | ||
| Theorem | topontop 22635 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||
| Theorem | toponuni 22636 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | ||
| Theorem | topontopi 22637 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π½ β (TopOnβπ΅) β β’ π½ β Top | ||
| Theorem | toponunii 22638 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π½ β (TopOnβπ΅) β β’ π΅ = βͺ π½ | ||
| Theorem | toptopon 22639 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π = βͺ π½ β β’ (π½ β Top β π½ β (TopOnβπ)) | ||
| Theorem | toptopon2 22640 | A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
| β’ (π½ β Top β π½ β (TopOnββͺ π½)) | ||
| Theorem | topontopon 22641 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
| β’ (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½)) | ||
| Theorem | funtopon 22642 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
| β’ Fun TopOn | ||
| Theorem | toponrestid 22643 | Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.) |
| β’ π΄ β (TopOnβπ΅) β β’ π΄ = (π΄ βΎt π΅) | ||
| Theorem | toponsspwpw 22644 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) |
| β’ (TopOnβπ΄) β π« π« π΄ | ||
| Theorem | dmtopon 22645 | The domain of TopOn is the universal class V. (Contributed by BJ, 29-Apr-2021.) |
| β’ dom TopOn = V | ||
| Theorem | fntopon 22646 | The class TopOn is a function with domain the universal class V. Analogue for topologies of fnmre 17539 for Moore collections. (Contributed by BJ, 29-Apr-2021.) |
| β’ TopOn Fn V | ||
| Theorem | toprntopon 22647 | A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.) |
| β’ Top = βͺ ran TopOn | ||
| Theorem | toponmax 22648 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ (π½ β (TopOnβπ΅) β π΅ β π½) | ||
| Theorem | toponss 22649 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| β’ ((π½ β (TopOnβπ) β§ π΄ β π½) β π΄ β π) | ||
| Theorem | toponcom 22650 | If πΎ is a topology on the base set of topology π½, then π½ is a topology on the base of πΎ. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| β’ ((π½ β Top β§ πΎ β (TopOnββͺ π½)) β π½ β (TopOnββͺ πΎ)) | ||
| Theorem | toponcomb 22651 | Biconditional form of toponcom 22650. (Contributed by BJ, 5-Dec-2021.) |
| β’ ((π½ β Top β§ πΎ β Top) β (π½ β (TopOnββͺ πΎ) β πΎ β (TopOnββͺ π½))) | ||
| Theorem | topgele 22652 | The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.) |
| β’ (π½ β (TopOnβπ) β ({β , π} β π½ β§ π½ β π« π)) | ||
| Theorem | topsn 22653 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4899). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
| β’ (π½ β (TopOnβ{π΄}) β π½ = π« {π΄}) | ||
| Syntax | ctps 22654 | Syntax for the class of topological spaces. |
| class TopSp | ||
| Definition | df-topsp 22655 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) |
| β’ TopSp = {π β£ (TopOpenβπ) β (TopOnβ(Baseβπ))} | ||
| Theorem | istps 22656 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β (TopOnβπ΄)) | ||
| Theorem | istps2 22657 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) |
| β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β (π½ β Top β§ π΄ = βͺ π½)) | ||
| Theorem | tpsuni 22658 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) |
| β’ π΄ = (BaseβπΎ) & β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π΄ = βͺ π½) | ||
| Theorem | tpstop 22659 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) |
| β’ π½ = (TopOpenβπΎ) β β’ (πΎ β TopSp β π½ β Top) | ||
| Theorem | tpspropd 22660 | A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
| β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β TopSp β πΏ β TopSp)) | ||
| Theorem | tpsprop2d 22661 | A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (TopSetβπΎ) = (TopSetβπΏ)) β β’ (π β (πΎ β TopSp β πΏ β TopSp)) | ||
| Theorem | topontopn 22662 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π΄ = (BaseβπΎ) & β’ π½ = (TopSetβπΎ) β β’ (π½ β (TopOnβπ΄) β π½ = (TopOpenβπΎ)) | ||
| Theorem | tsettps 22663 | If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015.) |
| β’ π΄ = (BaseβπΎ) & β’ π½ = (TopSetβπΎ) β β’ (π½ β (TopOnβπ΄) β πΎ β TopSp) | ||
| Theorem | istpsi 22664 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) |
| β’ (BaseβπΎ) = π΄ & β’ (TopOpenβπΎ) = π½ & β’ π΄ = βͺ π½ & β’ π½ β Top β β’ πΎ β TopSp | ||
| Theorem | eltpsg 22665 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by AV, 31-Oct-2024.) |
| β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), π½β©} β β’ (π½ β (TopOnβπ΄) β πΎ β TopSp) | ||
| Theorem | eltpsgOLD 22666 | Obsolete version of eltpsg 22665 as of 31-Oct-2024. Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), π½β©} β β’ (π½ β (TopOnβπ΄) β πΎ β TopSp) | ||
| Theorem | eltpsi 22667 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.) |
| β’ πΎ = {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), π½β©} & β’ π΄ = βͺ π½ & β’ π½ β Top β β’ πΎ β TopSp | ||
| Syntax | ctb 22668 | Syntax for the class of topological bases. |
| class TopBases | ||
| Definition | df-bases 22669* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22671). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) |
| β’ TopBases = {π₯ β£ βπ¦ β π₯ βπ§ β π₯ (π¦ β© π§) β βͺ (π₯ β© π« (π¦ β© π§))} | ||
| Theorem | isbasisg 22670* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
| β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β βͺ (π΅ β© π« (π₯ β© π¦)))) | ||
| Theorem | isbasis2g 22671* | Express the predicate "the set π΅ is a basis for a topology". (Contributed by NM, 17-Jul-2006.) |
| β’ (π΅ β πΆ β (π΅ β TopBases β βπ₯ β π΅ βπ¦ β π΅ βπ§ β (π₯ β© π¦)βπ€ β π΅ (π§ β π€ β§ π€ β (π₯ β© π¦)))) | ||
| Theorem | isbasis3g 22672* | Express the predicate "the set π΅ is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.) |
| β’ (π΅ β πΆ β (π΅ β TopBases β (βπ₯ β π΅ π₯ β βͺ π΅ β§ βπ₯ β βͺ π΅βπ¦ β π΅ π₯ β π¦ β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β (π₯ β© π¦)βπ€ β π΅ (π§ β π€ β§ π€ β (π₯ β© π¦))))) | ||
| Theorem | basis1 22673 | Property of a basis. (Contributed by NM, 16-Jul-2006.) |
| β’ ((π΅ β TopBases β§ πΆ β π΅ β§ π· β π΅) β (πΆ β© π·) β βͺ (π΅ β© π« (πΆ β© π·))) | ||
| Theorem | basis2 22674* | Property of a basis. (Contributed by NM, 17-Jul-2006.) |
| β’ (((π΅ β TopBases β§ πΆ β π΅) β§ (π· β π΅ β§ π΄ β (πΆ β© π·))) β βπ₯ β π΅ (π΄ β π₯ β§ π₯ β (πΆ β© π·))) | ||
| Theorem | fiinbas 22675* | If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| β’ ((π΅ β πΆ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β© π¦) β π΅) β π΅ β TopBases) | ||
| Theorem | basdif0 22676 | A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| β’ ((π΅ β {β }) β TopBases β π΅ β TopBases) | ||
| Theorem | baspartn 22677* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| β’ ((π β π β§ βπ₯ β π βπ¦ β π (π₯ = π¦ β¨ (π₯ β© π¦) = β )) β π β TopBases) | ||
| Theorem | tgval 22678* | The topology generated by a basis. See also tgval2 22679 and tgval3 22686. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) | ||
| Theorem | tgval2 22679* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22692) that (topGenβπ΅) is indeed a topology (on βͺ π΅, see unitg 22690). See also tgval 22678 and tgval3 22686. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))}) | ||
| Theorem | eltg 22680 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β (π΄ β (topGenβπ΅) β π΄ β βͺ (π΅ β© π« π΄))) | ||
| Theorem | eltg2 22681* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β (π΄ β (topGenβπ΅) β (π΄ β βͺ π΅ β§ βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π¦ β π΄)))) | ||
| Theorem | eltg2b 22682* | Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β (π΄ β (topGenβπ΅) β βπ₯ β π΄ βπ¦ β π΅ (π₯ β π¦ β§ π¦ β π΄))) | ||
| Theorem | eltg4i 22683 | An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| β’ (π΄ β (topGenβπ΅) β π΄ = βͺ (π΅ β© π« π΄)) | ||
| Theorem | eltg3i 22684 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
| β’ ((π΅ β π β§ π΄ β π΅) β βͺ π΄ β (topGenβπ΅)) | ||
| Theorem | eltg3 22685* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
| β’ (π΅ β π β (π΄ β (topGenβπ΅) β βπ₯(π₯ β π΅ β§ π΄ = βͺ π₯))) | ||
| Theorem | tgval3 22686* | Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22678 and tgval2 22679. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.) |
| β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)}) | ||
| Theorem | tg1 22687 | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
| β’ (π΄ β (topGenβπ΅) β π΄ β βͺ π΅) | ||
| Theorem | tg2 22688* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
| β’ ((π΄ β (topGenβπ΅) β§ πΆ β π΄) β βπ₯ β π΅ (πΆ β π₯ β§ π₯ β π΄)) | ||
| Theorem | bastg 22689 | A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) |
| β’ (π΅ β π β π΅ β (topGenβπ΅)) | ||
| Theorem | unitg 22690 | The topology generated by a basis π΅ is a topology on βͺ π΅. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.) |
| β’ (π΅ β π β βͺ (topGenβπ΅) = βͺ π΅) | ||
| Theorem | tgss 22691 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
| β’ ((πΆ β π β§ π΅ β πΆ) β (topGenβπ΅) β (topGenβπΆ)) | ||
| Theorem | tgcl 22692 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
| β’ (π΅ β TopBases β (topGenβπ΅) β Top) | ||
| Theorem | tgclb 22693 | The property tgcl 22692 can be reversed: if the topology generated by π΅ is actually a topology, then π΅ must be a topological basis. This yields an alternative definition of TopBases. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| β’ (π΅ β TopBases β (topGenβπ΅) β Top) | ||
| Theorem | tgtopon 22694 | A basis generates a topology on βͺ π΅. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| β’ (π΅ β TopBases β (topGenβπ΅) β (TopOnββͺ π΅)) | ||
| Theorem | topbas 22695 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
| β’ (π½ β Top β π½ β TopBases) | ||
| Theorem | tgtop 22696 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
| β’ (π½ β Top β (topGenβπ½) = π½) | ||
| Theorem | eltop 22697 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
| β’ (π½ β Top β (π΄ β π½ β π΄ β βͺ (π½ β© π« π΄))) | ||
| Theorem | eltop2 22698* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
| β’ (π½ β Top β (π΄ β π½ β βπ₯ β π΄ βπ¦ β π½ (π₯ β π¦ β§ π¦ β π΄))) | ||
| Theorem | eltop3 22699* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
| β’ (π½ β Top β (π΄ β π½ β βπ₯(π₯ β π½ β§ π΄ = βͺ π₯))) | ||
| Theorem | fibas 22700 | A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
| β’ (fiβπ΄) β TopBases | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |