![]() |
Intuitionistic Logic Explorer Theorem List (p. 136 of 150) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lspsnel5a 13501 | Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{π}) β π) | ||
Theorem | lspprid1 13502 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprid2 13503 | A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π β (πβ{π, π})) | ||
Theorem | lspprvacl 13504 | The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π + π) β (πβ{π, π})) | ||
Theorem | lssats2 13505* | A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β π = βͺ π₯ β π (πβ{π₯})) | ||
Theorem | lspsneli 13506 | A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 2-Jul-2014.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π΄ β πΎ) & β’ (π β π β π) β β’ (π β (π΄ Β· π) β (πβ{π})) | ||
Theorem | lspsn 13507* | Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{π}) = {π£ β£ βπ β πΎ π£ = (π Β· π)}) | ||
Theorem | lspsnel 13508* | Member of span of the singleton of a vector. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (π β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnvsi 13509 | Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.) |
β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β πΎ β§ π β π) β (πβ{(π Β· π)}) β (πβ{π})) | ||
Theorem | lspsnss2 13510* | Comparable spans of singletons must have proportional vectors. (Contributed by NM, 7-Jun-2015.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ{π}) β (πβ{π}) β βπ β πΎ π = (π Β· π))) | ||
Theorem | lspsnneg 13511 | Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β (πβ{(πβπ)}) = (πβ{π})) | ||
Theorem | lspsnsub 13512 | Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ{(π β π)}) = (πβ{(π β π)})) | ||
Theorem | lspsn0 13513 | Span of the singleton of the zero vector. (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πβ{ 0 }) = { 0 }) | ||
Theorem | lsp0 13514 | Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β (πββ ) = { 0 }) | ||
Theorem | lspuni0 13515 | Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ (π β LMod β βͺ (πββ ) = 0 ) | ||
Theorem | lspun0 13516 | The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β (πβ(π βͺ { 0 })) = (πβπ)) | ||
Theorem | lspsneq0 13517 | Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) | ||
Theorem | lspsneq0b 13518 | Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) = (πβ{π})) β β’ (π β (π = 0 β π = 0 )) | ||
Theorem | lmodindp1 13519 | Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π + π) β 0 ) | ||
Theorem | lsslsp 13520 | Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) TODO: Shouldn't we swap πβπΊ and πβπΊ since we are computing a property of πβπΊ? (Like we say sin 0 = 0 and not 0 = sin 0.) - NM 15-Mar-2015. |
β’ π = (π βΎs π) & β’ π = (LSpanβπ) & β’ π = (LSpanβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) = (πβπΊ)) | ||
Theorem | lss0v 13521 | The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.) |
β’ π = (π βΎs π) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ πΏ = (LSubSpβπ) β β’ ((π β LMod β§ π β πΏ) β π = 0 ) | ||
Theorem | lsspropdg 13522* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (LSubSpβπΎ) = (LSubSpβπΏ)) | ||
Theorem | lsppropd 13523* | If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β π = (Baseβ(ScalarβπΎ))) & β’ (π β π = (Baseβ(ScalarβπΏ))) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (LSpanβπΎ) = (LSpanβπΏ)) | ||
Syntax | cpsmet 13524 | Extend class notation with the class of all pseudometric spaces. |
class PsMet | ||
Syntax | cxmet 13525 | Extend class notation with the class of all extended metric spaces. |
class βMet | ||
Syntax | cmet 13526 | Extend class notation with the class of all metrics. |
class Met | ||
Syntax | cbl 13527 | Extend class notation with the metric space ball function. |
class ball | ||
Syntax | cfbas 13528 | Extend class definition to include the class of filter bases. |
class fBas | ||
Syntax | cfg 13529 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 13530 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 13531 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 13532* | Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
β’ PsMet = (π₯ β V β¦ {π β (β* βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ ((π¦ππ¦) = 0 β§ βπ§ β π₯ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) +π (π€ππ§)))}) | ||
Definition | df-xmet 13533* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 13534, but we also allow the metric to take on the value +β. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ βMet = (π₯ β V β¦ {π β (β* βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ βπ§ β π₯ (((π¦ππ§) = 0 β π¦ = π§) β§ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) +π (π€ππ§)))}) | ||
Definition | df-met 13534* | Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.) |
β’ Met = (π₯ β V β¦ {π β (β βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ βπ§ β π₯ (((π¦ππ§) = 0 β π¦ = π§) β§ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) + (π€ππ§)))}) | ||
Definition | df-bl 13535* | Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ball = (π β V β¦ (π₯ β dom dom π, π§ β β* β¦ {π¦ β dom dom π β£ (π₯ππ¦) < π§})) | ||
Definition | df-mopn 13536 | Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.) |
β’ MetOpen = (π β βͺ ran βMet β¦ (topGenβran (ballβπ))) | ||
Definition | df-fbas 13537* | Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.) |
β’ fBas = (π€ β V β¦ {π₯ β π« π« π€ β£ (π₯ β β β§ β β π₯ β§ βπ¦ β π₯ βπ§ β π₯ (π₯ β© π« (π¦ β© π§)) β β )}) | ||
Definition | df-fg 13538* | Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.) |
β’ filGen = (π€ β V, π₯ β (fBasβπ€) β¦ {π¦ β π« π€ β£ (π₯ β© π« π¦) β β }) | ||
Definition | df-metu 13539* | Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ metUnif = (π β βͺ ran PsMet β¦ ((dom dom π Γ dom dom π)filGenran (π β β+ β¦ (β‘π β (0[,)π))))) | ||
Syntax | ccnfld 13540 | Extend class notation with the field of complex numbers. |
class βfld | ||
Definition | df-icnfld 13541 |
The field of complex numbers. Other number fields and rings can be
constructed by applying the βΎs
restriction operator.
The contract of this set is defined entirely by cnfldex 13543, cnfldadd 13545, cnfldmul 13546, cnfldcj 13547, and cnfldbas 13544. We may add additional members to this in the future. At least for now, this structure does not include a topology, order, a distance function, or function mapping metrics. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (New usage is discouraged.) |
β’ βfld = ({β¨(Baseβndx), ββ©, β¨(+gβndx), + β©, β¨(.rβndx), Β· β©} βͺ {β¨(*πβndx), ββ©}) | ||
Theorem | cnfldstr 13542 | The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld Struct β¨1, ;13β© | ||
Theorem | cnfldex 13543 | The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ βfld β V | ||
Theorem | cnfldbas 13544 | The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ β = (Baseββfld) | ||
Theorem | cnfldadd 13545 | The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ + = (+gββfld) | ||
Theorem | cnfldmul 13546 | The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ Β· = (.rββfld) | ||
Theorem | cnfldcj 13547 | The conjugation operation of the field of complex numbers. (Contributed by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 17-Dec-2017.) |
β’ β = (*πββfld) | ||
Theorem | cncrng 13548 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
β’ βfld β CRing | ||
Theorem | cnring 13549 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ βfld β Ring | ||
Theorem | cnfld0 13550 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 0 = (0gββfld) | ||
Theorem | cnfld1 13551 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 1 = (1rββfld) | ||
Theorem | cnfldneg 13552 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β ((invgββfld)βπ) = -π) | ||
Theorem | cnfldplusf 13553 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ + = (+πββfld) | ||
Theorem | cnfldsub 13554 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ β = (-gββfld) | ||
Theorem | cnfldmulg 13555 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ ((π΄ β β€ β§ π΅ β β) β (π΄(.gββfld)π΅) = (π΄ Β· π΅)) | ||
Theorem | cnfldexp 13556 | The exponentiation operator in the field of complex numbers (for nonnegative exponents). (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ ((π΄ β β β§ π΅ β β0) β (π΅(.gβ(mulGrpββfld))π΄) = (π΄βπ΅)) | ||
Theorem | cnsubmlem 13557* | Lemma for nn0subm 13562 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ 0 β π΄ β β’ π΄ β (SubMndββfld) | ||
Theorem | cnsubglem 13558* | Lemma for cnsubrglem 13559 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ π΅ β π΄ β β’ π΄ β (SubGrpββfld) | ||
Theorem | cnsubrglem 13559* | Lemma for zsubrg 13560 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ 1 β π΄ & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ Β· π¦) β π΄) β β’ π΄ β (SubRingββfld) | ||
Theorem | zsubrg 13560 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€ β (SubRingββfld) | ||
Theorem | gzsubrg 13561 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€[i] β (SubRingββfld) | ||
Theorem | nn0subm 13562 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ β0 β (SubMndββfld) | ||
Theorem | rege0subm 13563 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (0[,)+β) β (SubMndββfld) | ||
Theorem | zsssubrg 13564 | The integers are a subset of any subring of the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β (SubRingββfld) β β€ β π ) | ||
According to Wikipedia ("Integer", 25-May-2019, https://en.wikipedia.org/wiki/Integer) "The integers form a unital ring which is the most basic one, in the following sense: for any unital ring, there is a unique ring homomorphism from the integers into this ring. This universal property, namely to be an initial object in the category of [unital] rings, characterizes the ring π." In set.mm, there was no explicit definition for the ring of integers until June 2019, but it was denoted by (βfld βΎs β€), the field of complex numbers restricted to the integers. In zringring 13568 it is shown that this restriction is a ring, and zringbas 13571 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 13566 of the ring of integers. Remark: Instead of using the symbol "ZZrng" analogous to βfld used for the field of complex numbers, we have chosen the version with an "i" to indicate that the ring of integers is a unital ring, see also Wikipedia ("Rng (algebra)", 9-Jun-2019, https://en.wikipedia.org/wiki/Rng_(algebra) 13566). | ||
Syntax | czring 13565 | Extend class notation with the (unital) ring of integers. |
class β€ring | ||
Definition | df-zring 13566 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
β’ β€ring = (βfld βΎs β€) | ||
Theorem | zringcrng 13567 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β CRing | ||
Theorem | zringring 13568 | The ring of integers is a ring. (Contributed by AV, 20-May-2019.) (Revised by AV, 9-Jun-2019.) (Proof shortened by AV, 13-Jun-2019.) |
β’ β€ring β Ring | ||
Theorem | zringabl 13569 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β Abel | ||
Theorem | zringgrp 13570 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
β’ β€ring β Grp | ||
Theorem | zringbas 13571 | The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
β’ β€ = (Baseββ€ring) | ||
Theorem | zringplusg 13572 | The addition operation of the ring of integers. (Contributed by Thierry Arnoux, 8-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ + = (+gββ€ring) | ||
Theorem | zringmulg 13573 | The multiplication (group power) operation of the group of integers. (Contributed by Thierry Arnoux, 31-Oct-2017.) (Revised by AV, 9-Jun-2019.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄(.gββ€ring)π΅) = (π΄ Β· π΅)) | ||
Theorem | zringmulr 13574 | The multiplication operation of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ Β· = (.rββ€ring) | ||
Theorem | zring0 13575 | The zero element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ 0 = (0gββ€ring) | ||
Theorem | zring1 13576 | The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017.) (Revised by AV, 9-Jun-2019.) |
β’ 1 = (1rββ€ring) | ||
Theorem | zringnzr 13577 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
β’ β€ring β NzRing | ||
Theorem | dvdsrzring 13578 | Ring divisibility in the ring of integers corresponds to ordinary divisibility in β€. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by AV, 9-Jun-2019.) |
β’ β₯ = (β₯rββ€ring) | ||
Theorem | zringinvg 13579 | The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.) |
β’ (π΄ β β€ β -π΄ = ((invgββ€ring)βπ΄)) | ||
Theorem | zringsubgval 13580 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
β’ β = (-gββ€ring) β β’ ((π β β€ β§ π β β€) β (π β π) = (π β π)) | ||
Theorem | zringmpg 13581 | The multiplicative group of the ring of integers is the restriction of the multiplicative group of the complex numbers to the integers. (Contributed by AV, 15-Jun-2019.) |
β’ ((mulGrpββfld) βΎs β€) = (mulGrpββ€ring) | ||
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), and it may sometimes be more convenient to consider topologies without reference to the underlying set. | ||
Syntax | ctop 13582 | Syntax for the class of topologies. |
class Top | ||
Definition | df-top 13583* |
Define the class of topologies. It is a proper class. See istopg 13584 and
istopfin 13585 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 13584* |
Express the predicate "π½ is a topology". See istopfin 13585 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 | istopfin 13585* | Express the predicate "π½ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 13584. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.) |
β’ (π½ β Top β (βπ₯(π₯ β π½ β βͺ π₯ β π½) β§ βπ₯((π₯ β π½ β§ π₯ β β β§ π₯ β Fin) β β© π₯ β π½))) | ||
Theorem | uniopn 13586 | 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 13587* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β π½) β βͺ π₯ β π΄ π΅ β π½) | ||
Theorem | inopn 13588 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||
Theorem | fiinopn 13589 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
β’ (π½ β Top β ((π΄ β π½ β§ π΄ β β β§ π΄ β Fin) β β© π΄ β π½)) | ||
Theorem | unopn 13590 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ βͺ π΅) β π½) | ||
Theorem | 0opn 13591 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
β’ (π½ β Top β β β π½) | ||
Theorem | 0ntop 13592 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
β’ Β¬ β β Top | ||
Theorem | topopn 13593 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β π β π½) | ||
Theorem | eltopss 13594 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½) β π΄ β π) | ||
Syntax | ctopon 13595 | Syntax for the function of topologies on sets. |
class TopOn | ||
Definition | df-topon 13596* | 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 | funtopon 13597 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
β’ Fun TopOn | ||
Theorem | istopon 13598 | 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 13599 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||
Theorem | toponuni 13600 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |