![]() |
Intuitionistic Logic Explorer Theorem List (p. 138 of 152) | < 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 | ||
Syntax | cfg 13701 | Extend class definition to include the filter generating function. |
class filGen | ||
Syntax | cmopn 13702 | Extend class notation with a function mapping each metric space to the family of its open sets. |
class MetOpen | ||
Syntax | cmetu 13703 | Extend class notation with the function mapping metrics to the uniform structure generated by that metric. |
class metUnif | ||
Definition | df-psmet 13704* | 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 13705* | Define the set of all extended metrics on a given base set. The definition is similar to df-met 13706, but we also allow the metric to take on the value +β. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ βMet = (π₯ β V β¦ {π β (β* βπ (π₯ Γ π₯)) β£ βπ¦ β π₯ βπ§ β π₯ (((π¦ππ§) = 0 β π¦ = π§) β§ βπ€ β π₯ (π¦ππ§) β€ ((π€ππ¦) +π (π€ππ§)))}) | ||
Definition | df-met 13706* | 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 13707* | 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 13708 | 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 13709* | 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 13710* | 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 13711* | 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 13712 | Extend class notation with the field of complex numbers. |
class βfld | ||
Definition | df-icnfld 13713 |
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 13715, cnfldadd 13717, cnfldmul 13718, cnfldcj 13719, and cnfldbas 13716. 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 13714 | 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 13715 | 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 13716 | 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 13717 | 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 13718 | 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 13719 | 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 13720 | The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
β’ βfld β CRing | ||
Theorem | cnring 13721 | The complex numbers form a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ βfld β Ring | ||
Theorem | cnfld0 13722 | Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 0 = (0gββfld) | ||
Theorem | cnfld1 13723 | One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ 1 = (1rββfld) | ||
Theorem | cnfldneg 13724 | The additive inverse in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β ((invgββfld)βπ) = -π) | ||
Theorem | cnfldplusf 13725 | The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ + = (+πββfld) | ||
Theorem | cnfldsub 13726 | The subtraction operator in the field of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ β = (-gββfld) | ||
Theorem | cnfldmulg 13727 | The group multiple function in the field of complex numbers. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ ((π΄ β β€ β§ π΅ β β) β (π΄(.gββfld)π΅) = (π΄ Β· π΅)) | ||
Theorem | cnfldexp 13728 | 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 13729* | Lemma for nn0subm 13734 and friends. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ 0 β π΄ β β’ π΄ β (SubMndββfld) | ||
Theorem | cnsubglem 13730* | Lemma for cnsubrglem 13731 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ π΅ β π΄ β β’ π΄ β (SubGrpββfld) | ||
Theorem | cnsubrglem 13731* | Lemma for zsubrg 13732 and friends. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ (π₯ β π΄ β π₯ β β) & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ + π¦) β π΄) & β’ (π₯ β π΄ β -π₯ β π΄) & β’ 1 β π΄ & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯ Β· π¦) β π΄) β β’ π΄ β (SubRingββfld) | ||
Theorem | zsubrg 13732 | The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€ β (SubRingββfld) | ||
Theorem | gzsubrg 13733 | The gaussian integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ β€[i] β (SubRingββfld) | ||
Theorem | nn0subm 13734 | The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ β0 β (SubMndββfld) | ||
Theorem | rege0subm 13735 | The nonnegative reals form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (0[,)+β) β (SubMndββfld) | ||
Theorem | zsssubrg 13736 | 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 13740 it is shown that this restriction is a ring, and zringbas 13743 shows that its base set is the integers. As of June 2019, there is an abbreviation of this expression as Definition df-zring 13738 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) 13738). | ||
Syntax | czring 13737 | Extend class notation with the (unital) ring of integers. |
class β€ring | ||
Definition | df-zring 13738 | The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
β’ β€ring = (βfld βΎs β€) | ||
Theorem | zringcrng 13739 | The ring of integers is a commutative ring. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β CRing | ||
Theorem | zringring 13740 | 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 13741 | The ring of integers is an (additive) abelian group. (Contributed by AV, 13-Jun-2019.) |
β’ β€ring β Abel | ||
Theorem | zringgrp 13742 | The ring of integers is an (additive) group. (Contributed by AV, 10-Jun-2019.) |
β’ β€ring β Grp | ||
Theorem | zringbas 13743 | 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 13744 | 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 13745 | 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 13746 | 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 13747 | 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 13748 | 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 13749 | The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
β’ β€ring β NzRing | ||
Theorem | dvdsrzring 13750 | 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 13751 | 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 13752 | Subtraction in the ring of integers. (Contributed by AV, 3-Aug-2019.) |
β’ β = (-gββ€ring) β β’ ((π β β€ β§ π β β€) β (π β π) = (π β π)) | ||
Theorem | zringmpg 13753 | 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) | ||
Syntax | czrh 13754 | Map the rationals into a field, or the integers into a ring. |
class β€RHom | ||
Syntax | czlm 13755 | Augment an abelian group with vector space operations to turn it into a β€-module. |
class β€Mod | ||
Syntax | czn 13756 | The ring of integers modulo π. |
class β€/nβ€ | ||
Definition | df-zrh 13757 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of π = 1r + 1r + ... + 1r for integers (see also df-mulg 13014). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€RHom = (π β V β¦ βͺ (β€ring RingHom π)) | ||
Definition | df-zlm 13758 | Augment an abelian group with vector space operations to turn it into a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€Mod = (π β V β¦ ((π sSet β¨(Scalarβndx), β€ringβ©) sSet β¨( Β·π βndx), (.gβπ)β©)) | ||
Definition | df-zn 13759* | Define the ring of integers mod π. This is literally the quotient ring of β€ by the ideal πβ€, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
β’ β€/nβ€ = (π β β0 β¦ β¦β€ring / π§β¦β¦(π§ /s (π§ ~QG ((RSpanβπ§)β{π}))) / π β¦(π sSet β¨(leβndx), β¦((β€RHomβπ ) βΎ if(π = 0, β€, (0..^π))) / πβ¦((π β β€ ) β β‘π)β©)) | ||
Theorem | zlmval 13760 | Augment an abelian group with vector space operations to turn it into a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β π β π = ((πΊ sSet β¨(Scalarβndx), β€ringβ©) sSet β¨( Β·π βndx), Β· β©)) | ||
Theorem | zlmlemg 13761 | Lemma for zlmbasg 13762 and zlmplusgg 13763. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β β & β’ (πΈβndx) β (Scalarβndx) & β’ (πΈβndx) β ( Β·π βndx) β β’ (πΊ β π β (πΈβπΊ) = (πΈβπ)) | ||
Theorem | zlmbasg 13762 | Base set of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ π΅ = (BaseβπΊ) β β’ (πΊ β π β π΅ = (Baseβπ)) | ||
Theorem | zlmplusgg 13763 | Group operation of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β π β + = (+gβπ)) | ||
Theorem | zlmmulrg 13764 | Ring operation of a β€-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.rβπΊ) β β’ (πΊ β π β Β· = (.rβπ)) | ||
Theorem | zlmsca 13765 | Scalar ring of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.) |
β’ π = (β€ModβπΊ) β β’ (πΊ β π β β€ring = (Scalarβπ)) | ||
Theorem | zlmvscag 13766 | Scalar multiplication operation of a β€-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (β€ModβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β π β Β· = ( Β·π βπ)) | ||
Theorem | znlidl 13767 | The set πβ€ is an ideal in β€. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
β’ π = (RSpanββ€ring) β β’ (π β β€ β (πβ{π}) β (LIdealββ€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 13768 | Syntax for the class of topologies. |
class Top | ||
Definition | df-top 13769* |
Define the class of topologies. It is a proper class. See istopg 13770 and
istopfin 13771 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 13770* |
Express the predicate "π½ is a topology". See istopfin 13771 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 13771* | Express the predicate "π½ is a topology" using nonempty finite intersections instead of binary intersections as in istopg 13770. 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 13772 | 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 13773* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) |
β’ ((π½ β Top β§ βπ₯ β π΄ π΅ β π½) β βͺ π₯ β π΄ π΅ β π½) | ||
Theorem | inopn 13774 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ β© π΅) β π½) | ||
Theorem | fiinopn 13775 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) |
β’ (π½ β Top β ((π΄ β π½ β§ π΄ β β β§ π΄ β Fin) β β© π΄ β π½)) | ||
Theorem | unopn 13776 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π½ β Top β§ π΄ β π½ β§ π΅ β π½) β (π΄ βͺ π΅) β π½) | ||
Theorem | 0opn 13777 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) |
β’ (π½ β Top β β β π½) | ||
Theorem | 0ntop 13778 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) |
β’ Β¬ β β Top | ||
Theorem | topopn 13779 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β π β π½) | ||
Theorem | eltopss 13780 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π½) β π΄ β π) | ||
Syntax | ctopon 13781 | Syntax for the function of topologies on sets. |
class TopOn | ||
Definition | df-topon 13782* | 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 13783 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) |
β’ Fun TopOn | ||
Theorem | istopon 13784 | 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 13785 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π½ β Top) | ||
Theorem | toponuni 13786 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | ||
Theorem | topontopi 13787 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π½ β Top | ||
Theorem | toponunii 13788 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π½ β (TopOnβπ΅) β β’ π΅ = βͺ π½ | ||
Theorem | toptopon 13789 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β π½ β (TopOnβπ)) | ||
Theorem | toptopon2 13790 | 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 13791 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
β’ (π½ β (TopOnβπ) β π½ β (TopOnββͺ π½)) | ||
Theorem | toponrestid 13792 | 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 | toponsspwpwg 13793 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.) |
β’ (π΄ β π β (TopOnβπ΄) β π« π« π΄) | ||
Theorem | dmtopon 13794 | The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.) |
β’ dom TopOn = V | ||
Theorem | fntopon 13795 | The class TopOn is a function with domain V. (Contributed by BJ, 29-Apr-2021.) |
β’ TopOn Fn V | ||
Theorem | toponmax 13796 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ (π½ β (TopOnβπ΅) β π΅ β π½) | ||
Theorem | toponss 13797 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π½) β π΄ β π) | ||
Theorem | toponcom 13798 | 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 13799 | Biconditional form of toponcom 13798. (Contributed by BJ, 5-Dec-2021.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½ β (TopOnββͺ πΎ) β πΎ β (TopOnββͺ π½))) | ||
Theorem | topgele 13800 | 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βπ) β ({β , π} β π½ β§ π½ β π« π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |