Home | Metamath
Proof Explorer Theorem List (p. 322 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imlmhm 32101 | The image of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.) |
β’ πΌ = (π βΎs ran πΉ) β β’ ((π β LVec β§ πΉ β (π LMHom π)) β πΌ β LVec) | ||
Theorem | lindsunlem 32102 | Lemma for lindsun 32103. (Contributed by Thierry Arnoux, 9-May-2023.) |
β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π β (LIndSβπ)) & β’ (π β π β (LIndSβπ)) & β’ (π β ((πβπ) β© (πβπ)) = { 0 }) & β’ π = (0gβ(Scalarβπ)) & β’ πΉ = (Baseβ(Scalarβπ)) & β’ (π β πΆ β π) & β’ (π β πΎ β (πΉ β {π})) & β’ (π β (πΎ( Β·π βπ)πΆ) β (πβ((π βͺ π) β {πΆ}))) β β’ (π β β₯) | ||
Theorem | lindsun 32103 | Condition for the union of two independent sets to be an independent set. (Contributed by Thierry Arnoux, 9-May-2023.) |
β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π β (LIndSβπ)) & β’ (π β π β (LIndSβπ)) & β’ (π β ((πβπ) β© (πβπ)) = { 0 }) β β’ (π β (π βͺ π) β (LIndSβπ)) | ||
Theorem | lbsdiflsp0 32104 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 32103. (Contributed by Thierry Arnoux, 17-May-2023.) |
β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π΅ β π½ β§ π β π΅) β ((πβ(π΅ β π)) β© (πβπ)) = { 0 }) | ||
Theorem | dimkerim 32105 | Given a linear map πΉ between vector spaces π and π, the dimension of the vector space π is the sum of the dimension of πΉ 's kernel and the dimension of πΉ's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dimβπΌ) being the rank of πΉ (the dimension of its image), and (dimβπΎ) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.) |
β’ 0 = (0gβπ) & β’ πΎ = (π βΎs (β‘πΉ β { 0 })) & β’ πΌ = (π βΎs ran πΉ) β β’ ((π β LVec β§ πΉ β (π LMHom π)) β (dimβπ) = ((dimβπΎ) +π (dimβπΌ))) | ||
Theorem | qusdimsum 32106 | Let π be a vector space, and let π be a subspace. Then the dimension of π is the sum of the dimension of π and the dimension of the quotient space of π. First part of theorem 5.3 in [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (π βΎs π) & β’ π = (π /s (π ~QG π)) β β’ ((π β LVec β§ π β (LSubSpβπ)) β (dimβπ) = ((dimβπ) +π (dimβπ))) | ||
Theorem | fedgmullem1 32107* | Lemma for fedgmul 32109. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) & β’ π· = (π β π, π β π β¦ (π(.rβπΈ)π)) & β’ π» = (π β π, π β π β¦ ((πΊβπ)βπ)) & β’ (π β π β (LBasisβπΆ)) & β’ (π β π β (LBasisβπ΅)) & β’ (π β π β (Baseβπ΄)) & β’ (π β πΏ:πβΆ(Baseβ(Scalarβπ΅))) & β’ (π β πΏ finSupp (0gβ(Scalarβπ΅))) & β’ (π β π = (π΅ Ξ£g (π β π β¦ ((πΏβπ)( Β·π βπ΅)π)))) & β’ (π β πΊ:πβΆ((Baseβ(ScalarβπΆ)) βm π)) & β’ ((π β§ π β π) β (πΊβπ) finSupp (0gβ(ScalarβπΆ))) & β’ ((π β§ π β π) β (πΏβπ) = (πΆ Ξ£g (π β π β¦ (((πΊβπ)βπ)( Β·π βπΆ)π)))) β β’ (π β (π» finSupp (0gβ(Scalarβπ΄)) β§ π = (π΄ Ξ£g (π» βf ( Β·π βπ΄)π·)))) | ||
Theorem | fedgmullem2 32108* | Lemma for fedgmul 32109. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) & β’ π· = (π β π, π β π β¦ (π(.rβπΈ)π)) & β’ π» = (π β π, π β π β¦ ((πΊβπ)βπ)) & β’ (π β π β (LBasisβπΆ)) & β’ (π β π β (LBasisβπ΅)) & β’ (π β π β (Baseβ((Scalarβπ΄) freeLMod (π Γ π)))) & β’ (π β (π΄ Ξ£g (π βf ( Β·π βπ΄)π·)) = (0gβπ΄)) β β’ (π β π = ((π Γ π) Γ {(0gβ(Scalarβπ΄))})) | ||
Theorem | fedgmul 32109 | The multiplicativity formula for degrees of field extensions. Given πΈ a field extension of πΉ, itself a field extension of πΎ, we have [πΈ:πΎ] = [πΈ:πΉ][πΉ:πΎ]. Proposition 1.2 of [Lang], p. 224. Here (dimβπ΄) is the degree of the extension πΈ of πΎ, (dimβπ΅) is the degree of the extension πΈ of πΉ, and (dimβπΆ) is the degree of the extension πΉ of πΎ. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) β β’ (π β (dimβπ΄) = ((dimβπ΅) Β·e (dimβπΆ))) | ||
Syntax | cfldext 32110 | Syntax for the field extension relation. |
class /FldExt | ||
Syntax | cfinext 32111 | Syntax for the finite field extension relation. |
class /FinExt | ||
Syntax | calgext 32112 | Syntax for the algebraic field extension relation. |
class /AlgExt | ||
Syntax | cextdg 32113 | Syntax for the field extension degree operation. |
class [:] | ||
Definition | df-fldext 32114* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FldExt = {β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} | ||
Definition | df-extdg 32115* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ [:] = (π β V, π β (/FldExt β {π}) β¦ (dimβ((subringAlg βπ)β(Baseβπ)))) | ||
Definition | df-finext 32116* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FinExt = {β¨π, πβ© β£ (π/FldExtπ β§ (π[:]π) β β0)} | ||
Definition | df-algext 32117* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /AlgExt = {β¨π, πβ© β£ (π/FldExtπ β§ βπ₯ β (Baseβπ)βπ β (Poly1βπ)(((eval1βπ)βπ)βπ₯) = (0gβπ))} | ||
Theorem | relfldext 32118 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ Rel /FldExt | ||
Theorem | brfldext 32119 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ β Field β§ πΉ β Field) β (πΈ/FldExtπΉ β (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ)))) | ||
Theorem | ccfldextrr 32120 | The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ βfld/FldExtβfld | ||
Theorem | fldextfld1 32121 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΈ β Field) | ||
Theorem | fldextfld2 32122 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ β Field) | ||
Theorem | fldextsubrg 32123 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π = (BaseβπΉ) β β’ (πΈ/FldExtπΉ β π β (SubRingβπΈ)) | ||
Theorem | fldextress 32124 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ = (πΈ βΎs (BaseβπΉ))) | ||
Theorem | brfinext 32125 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ/FinExtπΉ β (πΈ[:]πΉ) β β0)) | ||
Theorem | extdgval 32126 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) = (dimβ((subringAlg βπΈ)β(BaseβπΉ)))) | ||
Theorem | fldextsralvec 32127 | The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((subringAlg βπΈ)β(BaseβπΉ)) β LVec) | ||
Theorem | extdgcl 32128 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) β β0*) | ||
Theorem | extdggt0 32129 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΈ/FldExtπΉ β 0 < (πΈ[:]πΉ)) | ||
Theorem | fldexttr 32130 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β πΈ/FldExtπΎ) | ||
Theorem | fldextid 32131 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΉ β Field β πΉ/FldExtπΉ) | ||
Theorem | extdgid 32132 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
β’ (πΈ β Field β (πΈ[:]πΈ) = 1) | ||
Theorem | extdgmul 32133 | The multiplicativity formula for degrees of field extensions. Given πΈ a field extension of πΉ, itself a field extension of πΎ, the degree of the extension πΈ/FldExtπΎ is the product of the degrees of the extensions πΈ/FldExtπΉ and πΉ/FldExtπΎ. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ[:]πΎ) = ((πΈ[:]πΉ) Β·e (πΉ[:]πΎ))) | ||
Theorem | finexttrb 32134 | The extension πΈ of πΎ is finite if and only if πΈ is finite over πΉ and πΉ is finite over πΎ. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ/FinExtπΎ β (πΈ/FinExtπΉ β§ πΉ/FinExtπΎ))) | ||
Theorem | extdg1id 32135 | If the degree of the extension πΈ/FldExtπΉ is 1, then πΈ and πΉ are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ ((πΈ/FldExtπΉ β§ (πΈ[:]πΉ) = 1) β πΈ = πΉ) | ||
Theorem | extdg1b 32136 | The degree of the extension πΈ/FldExtπΉ is 1 iff πΈ and πΉ are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((πΈ[:]πΉ) = 1 β πΈ = πΉ)) | ||
Theorem | fldextchr 32137 | The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (πΈ/FldExtπΉ β (chrβπΉ) = (chrβπΈ)) | ||
Theorem | ccfldsrarelvec 32138 | The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((subringAlg ββfld)ββ) β LVec | ||
Theorem | ccfldextdgrr 32139 | The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (βfld[:]βfld) = 2 | ||
Syntax | calgnb 32140 | Extend class notation with the algebraic number builder function. |
class AlgNb | ||
Syntax | cminply 32141 | Extend class notation with the minimal polynomial builder function. |
class minPoly | ||
Definition | df-algnb 32142* | Define the algebraic number builder function. This definition is similar to df-aa 25597. (Contributed by Thierry Arnoux, 19-Jan-2025.) |
β’ AlgNb = (π β V, π β V β¦ βͺ π β (dom (π evalSub1 π) β {(0gβ(Poly1βπ))})(β‘((π evalSub1 π)βπ) β {(0gβπ)})) | ||
Definition | df-minply 32143* | Define the minimal polynomial builder function . (Contributed by Thierry Arnoux, 19-Jan-2025.) |
β’ minPoly = (π β V, π β V β¦ (π₯ β (π AlgNb π) β¦ inf((β‘((π evalSub1 π)βπ) β {(0gβπ)}), (Monic1pβπ), (( deg1 βπ) βr < ( deg1 βπ))))) | ||
Theorem | algnbval 32144* | The algebraic numbers over a field πΉ within a field πΈ. That is, the numbers π which are roots of nonzero polynomials π(π) with coefficients in (BaseβπΉ). This is expressed by the idiom (β‘(πβπ) β { 0 }), which can be translated into {π₯ β (BaseβπΈ) β£ ((πβπ)βπ₯) = 0 } by fniniseg2 7007. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) β β’ (π β (πΈ AlgNb πΉ) = βͺ π β (dom π β {π})(β‘(πβπ) β { 0 })) | ||
Theorem | isalgnb 32145* | Property for an element π of a field πΈ to be algebraic over a subfield πΉ. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ π΅ = (BaseβπΈ) β β’ (π β (π β (πΈ AlgNb πΉ) β (π β π΅ β§ βπ β (dom π β {π})((πβπ)βπ) = 0 ))) | ||
Theorem | minplyeulem 32146* | An algebraic number π over πΉ is a root of some monic polynomial π with coefficients in πΉ. (Contributed by Thierry Arnoux, 26-Jan-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π β (πΈ AlgNb πΉ)) β β’ (π β βπ β (Monic1pβπΈ)((πβπ)βπ) = 0 ) | ||
Syntax | csmat 32147 | Syntax for a function generating submatrices. |
class subMat1 | ||
Definition | df-smat 32148* | Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...π) Γ (1...π)) into a new index in ((1...(π β 1)) Γ (1...(π β 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 21848. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
β’ subMat1 = (π β V β¦ (π β β, π β β β¦ (π β (π β β, π β β β¦ β¨if(π < π, π, (π + 1)), if(π < π, π, (π + 1))β©)))) | ||
Theorem | smatfval 32149* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ ((πΎ β β β§ πΏ β β β§ π β π) β (πΎ(subMat1βπ)πΏ) = (π β (π β β, π β β β¦ β¨if(π < πΎ, π, (π + 1)), if(π < πΏ, π, (π + 1))β©))) | ||
Theorem | smatrcl 32150 | Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) β β’ (π β π β (π΅ βm ((1...(π β 1)) Γ (1...(π β 1))))) | ||
Theorem | smatlem 32151 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β β) & β’ (π β π½ β β) & β’ (π β if(πΌ < πΎ, πΌ, (πΌ + 1)) = π) & β’ (π β if(π½ < πΏ, π½, (π½ + 1)) = π) β β’ (π β (πΌππ½) = (ππ΄π)) | ||
Theorem | smattl 32152 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = (πΌπ΄π½)) | ||
Theorem | smattr 32153 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (1..^πΏ)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄π½)) | ||
Theorem | smatbl 32154 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (1..^πΎ)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = (πΌπ΄(π½ + 1))) | ||
Theorem | smatbr 32155 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π = (πΎ(subMat1βπ΄)πΏ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π΄ β (π΅ βm ((1...π) Γ (1...π)))) & β’ (π β πΌ β (πΎ...π)) & β’ (π β π½ β (πΏ...π)) β β’ (π β (πΌππ½) = ((πΌ + 1)π΄(π½ + 1))) | ||
Theorem | smatcl 32156 | Closure of the square submatrix: if π is a square matrix of dimension π with indices in (1...π), then a submatrix of π is of dimension (π β 1). (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΆ = (Baseβ((1...(π β 1)) Mat π )) & β’ π = (πΎ(subMat1βπ)πΏ) & β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β πΏ β (1...π)) & β’ (π β π β π΅) β β’ (π β π β πΆ) | ||
Theorem | matmpo 32157* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β π = (π β π, π β π β¦ (πππ))) | ||
Theorem | 1smat1 32158 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 21854. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ 1 = (1rβ((1...π) Mat π )) & β’ (π β π β Ring) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) β β’ (π β (πΌ(subMat1β 1 )πΌ) = (1rβ((1...(π β 1)) Mat π ))) | ||
Theorem | submat1n 32159 | One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β β β§ π β π΅) β (π(subMat1βπ)π) = (π(((1...π) subMat π )βπ)π)) | ||
Theorem | submatres 32160 | Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β β β§ π β π΅) β (π(subMat1βπ)π) = (π βΎ ((1...(π β 1)) Γ (1...(π β 1))))) | ||
Theorem | submateqlem1 32161 | Lemma for submateq 32163. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β πΎ β€ π) β β’ (π β (π β (πΎ...π) β§ (π + 1) β ((1...π) β {πΎ}))) | ||
Theorem | submateqlem2 32162 | Lemma for submateq 32163. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΎ β (1...π)) & β’ (π β π β (1...(π β 1))) & β’ (π β π < πΎ) β β’ (π β (π β (1..^πΎ) β§ π β ((1...π) β {πΎ}))) | ||
Theorem | submateq 32163* | Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ ((π β§ π β ((1...π) β {πΌ}) β§ π β ((1...π) β {π½})) β (ππΈπ) = (ππΉπ)) β β’ (π β (πΌ(subMat1βπΈ)π½) = (πΌ(subMat1βπΉ)π½)) | ||
Theorem | submatminr1 32164 | If we take a submatrix by removing the row πΌ and column π½, then the result is the same on the matrix with row πΌ and column π½ modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
β’ π΄ = ((1...π) Mat π ) & β’ π΅ = (Baseβπ΄) & β’ (π β π β β) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ πΈ = (πΌ(((1...π) minMatR1 π )βπ)π½) β β’ (π β (πΌ(subMat1βπ)π½) = (πΌ(subMat1βπΈ)π½)) | ||
Syntax | clmat 32165 | Extend class notation with the literal matrix conversion function. |
class litMat | ||
Definition | df-lmat 32166* | Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ litMat = (π β V β¦ (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) | ||
Theorem | lmatval 32167* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ (π β π β (litMatβπ) = (π β (1...(β―βπ)), π β (1...(β―β(πβ0))) β¦ ((πβ(π β 1))β(π β 1)))) | ||
Theorem | lmatfval 32168* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) β β’ (π β (πΌππ½) = ((πβ(πΌ β 1))β(π½ β 1))) | ||
Theorem | lmatfvlem 32169* | Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ πΎ β β0 & β’ πΏ β β0 & β’ πΌ β€ π & β’ π½ β€ π & β’ (πΎ + 1) = πΌ & β’ (πΏ + 1) = π½ & β’ (πβπΎ) = π & β’ (π β (πβπΏ) = π) β β’ (π β (πΌππ½) = π) | ||
Theorem | lmatcl 32170* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatβπ) & β’ (π β π β β) & β’ (π β π β Word Word π) & β’ (π β (β―βπ) = π) & β’ ((π β§ π β (0..^π)) β (β―β(πβπ)) = π) & β’ π = (Baseβπ ) & β’ π = ((1...π) Mat π ) & β’ π = (Baseβπ) & β’ (π β π β π) β β’ (π β π β π) | ||
Theorem | lmat22lem 32171* | Lemma for lmat22e11 32172 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ ((π β§ π β (0..^2)) β (β―β(β¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©βπ)) = 2) | ||
Theorem | lmat22e11 32172 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π1) = π΄) | ||
Theorem | lmat22e12 32173 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (1π2) = π΅) | ||
Theorem | lmat22e21 32174 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π1) = πΆ) | ||
Theorem | lmat22e22 32175 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (2π2) = π·) | ||
Theorem | lmat22det 32176 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
β’ π = (litMatββ¨ββ¨βπ΄π΅ββ©β¨βπΆπ·ββ©ββ©) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ π = (Baseβπ ) & β’ π½ = ((1...2) maDet π ) & β’ (π β π β Ring) β β’ (π β (π½βπ) = ((π΄ Β· π·) β (πΆ Β· π΅))) | ||
Theorem | mdetpmtr1 32177* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)ππ)) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr2 32178* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ (ππ(πβπ))) β β’ (((π β CRing β§ π β Fin) β§ (π β π΅ β§ π β πΊ)) β (π·βπ) = (((π β π)βπ) Β· (π·βπΈ))) | ||
Theorem | mdetpmtr12 32179* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΊ = (Baseβ(SymGrpβπ)) & β’ π = (pmSgnβπ) & β’ π = (β€RHomβπ ) & β’ Β· = (.rβπ ) & β’ πΈ = (π β π, π β π β¦ ((πβπ)π(πβπ))) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ (π β π β π΅) & β’ (π β π β πΊ) & β’ (π β π β πΊ) β β’ (π β (π·βπ) = ((πβ((πβπ) Β· (πβπ))) Β· (π·βπΈ))) | ||
Theorem | mdetlap1 32180* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π· = (π maDet π ) & β’ πΎ = (π maAdju π ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ πΌ β π) β (π·βπ) = (π Ξ£g (π β π β¦ ((πΌππ) Β· (π(πΎβπ)πΌ))))) | ||
Theorem | madjusmdetlem1 32181* | Lemma for madjusmdet 32185. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ πΊ = (Baseβ(SymGrpβ(1...π))) & β’ π = (pmSgnβ(1...π)) & β’ π = (πΌ(((1...π) minMatR1 π )βπ)π½) & β’ π = (π β (1...π), π β (1...π) β¦ ((πβπ)π(πβπ))) & β’ (π β π β πΊ) & β’ (π β π β πΊ) & β’ (π β (πβπ) = πΌ) & β’ (π β (πβπ) = π½) & β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ((πβπ) Β· (πβπ))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdetlem2 32182* | Lemma for madjusmdet 32185. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ ((π β§ π β (1...(π β 1))) β if(π < πΌ, π, (π + 1)) = ((π β β‘π)βπ)) | ||
Theorem | madjusmdetlem3 32183* | Lemma for madjusmdet 32185. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π), π β (1...π) β¦ (((π β β‘π)βπ)π((π β β‘π)βπ))) & β’ (π β π β π΅) β β’ (π β (πΌ(subMat1βπ)π½) = (π(subMat1βπ)π)) | ||
Theorem | madjusmdetlem4 32184* | Lemma for madjusmdet 32185. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) & β’ π = (π β (1...π) β¦ if(π = 1, πΌ, if(π β€ πΌ, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π½, if(π β€ π½, (π β 1), π))) & β’ π = (π β (1...π) β¦ if(π = 1, π, if(π β€ π, (π β 1), π))) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | madjusmdet 32185 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π½(πΎβπ)πΌ) = ((πβ(-1β(πΌ + π½))) Β· (πΈβ(πΌ(subMat1βπ)π½)))) | ||
Theorem | mdetlap 32186* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
β’ π΅ = (Baseβπ΄) & β’ π΄ = ((1...π) Mat π ) & β’ π· = ((1...π) maDet π ) & β’ πΎ = ((1...π) maAdju π ) & β’ Β· = (.rβπ ) & β’ π = (β€RHomβπ ) & β’ πΈ = ((1...(π β 1)) maDet π ) & β’ (π β π β β) & β’ (π β π β CRing) & β’ (π β πΌ β (1...π)) & β’ (π β π½ β (1...π)) & β’ (π β π β π΅) β β’ (π β (π·βπ) = (π Ξ£g (π β (1...π) β¦ ((πβ(-1β(πΌ + π))) Β· ((πΌππ) Β· (πΈβ(πΌ(subMat1βπ)π))))))) | ||
Theorem | ist0cld 32187* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
β’ (π β π΅ = βͺ π½) & β’ (π β π· = (Clsdβπ½)) β β’ (π β (π½ β Kol2 β (π½ β Top β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π· (π₯ β π β π¦ β π) β π₯ = π¦)))) | ||
Theorem | txomap 32188* | Given two open maps πΉ and πΊ, π» mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΏ) & β’ ((π β§ π¦ β πΎ) β (πΊ β π¦) β π) & β’ (π β π΄ β (π½ Γt πΎ)) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) β β’ (π β (π» β π΄) β (πΏ Γt π)) | ||
Theorem | qtopt1 32189* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π½ β Fre) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π) β (β‘πΉ β {π₯}) β (Clsdβπ½)) β β’ (π β (π½ qTop πΉ) β Fre) | ||
Theorem | qtophaus 32190* | If an open map's graph in the product space (π½ Γt π½) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ π = βͺ π½ & β’ βΌ = (β‘πΉ β πΉ) & β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) & β’ (π β π½ β Haus) & β’ (π β πΉ:πβontoβπ) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β (π½ qTop πΉ)) & β’ (π β βΌ β (Clsdβ(π½ Γt π½))) β β’ (π β (π½ qTop πΉ) β Haus) | ||
Theorem | circtopn 32191* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ (π½ qTop πΉ) = (TopOpenβ(πΉ βs βfld)) | ||
Theorem | circcn 32192* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
β’ πΌ = (0[,](2 Β· Ο)) & β’ π½ = (topGenβran (,)) & β’ πΉ = (π₯ β β β¦ (expβ(i Β· π₯))) & β’ πΆ = (β‘abs β {1}) β β’ πΉ β (π½ Cn (π½ qTop πΉ)) | ||
Theorem | reff 32193* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10357. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
β’ (π΄ β π β (π΄Refπ΅ β (βͺ π΅ β βͺ π΄ β§ βπ(π:π΄βΆπ΅ β§ βπ£ β π΄ π£ β (πβπ£))))) | ||
Theorem | locfinreflem 32194* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ((Fun π β§ dom π β π β§ ran π β π½) β§ (ran πRefπ β§ ran π β (LocFinβπ½)))) | ||
Theorem | locfinref 32195* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function π from the original cover π, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ π = βͺ π½ & β’ (π β π β π½) & β’ (π β π = βͺ π) & β’ (π β π β π½) & β’ (π β πRefπ) & β’ (π β π β (LocFinβπ½)) β β’ (π β βπ(π:πβΆπ½ β§ ran πRefπ β§ ran π β (LocFinβπ½))) | ||
Syntax | ccref 32196 | The "every open cover has an π΄ refinement" predicate. |
class CovHasRefπ΄ | ||
Definition | df-cref 32197* | Define a statement "every open cover has an π΄ refinement" , where π΄ is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ CovHasRefπ΄ = {π β Top β£ βπ¦ β π« π(βͺ π = βͺ π¦ β βπ§ β (π« π β© π΄)π§Refπ¦)} | ||
Theorem | iscref 32198* | The property that every open cover has an π΄ refinement for the topological space π½. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ π = βͺ π½ β β’ (π½ β CovHasRefπ΄ β (π½ β Top β§ βπ¦ β π« π½(π = βͺ π¦ β βπ§ β (π« π½ β© π΄)π§Refπ¦))) | ||
Theorem | crefeq 32199 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π΄ = π΅ β CovHasRefπ΄ = CovHasRefπ΅) | ||
Theorem | creftop 32200 | A space where every open cover has an π΄ refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
β’ (π½ β CovHasRefπ΄ β π½ β Top) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |