HomeHome Intuitionistic Logic Explorer
Theorem List (p. 122 of 132)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12101-12200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem0ntop 12101 The empty set is not a topology. (Contributed by FL, 1-Jun-2008.)
 |- 
 -.  (/)  e.  Top
 
Theoremtopopn 12102 The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  ->  X  e.  J )
 
Theoremeltopss 12103 A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
 |-  X  =  U. J   =>    |-  (
 ( J  e.  Top  /\  A  e.  J ) 
 ->  A  C_  X )
 
7.1.1.2  Topologies on sets
 
Syntaxctopon 12104 Syntax for the function of topologies on sets.
 class TopOn
 
Definitiondf-topon 12105* Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.)
 |- TopOn  =  ( b  e.  _V  |->  { j  e.  Top  |  b  =  U. j }
 )
 
Theoremfuntopon 12106 The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
 |- 
 Fun TopOn
 
Theoremistopon 12107 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.)
 |-  ( J  e.  (TopOn `  B )  <->  ( J  e.  Top  /\  B  =  U. J ) )
 
Theoremtopontop 12108 A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  ( J  e.  (TopOn `  B )  ->  J  e.  Top )
 
Theoremtoponuni 12109 The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  ( J  e.  (TopOn `  B )  ->  B  =  U. J )
 
Theoremtopontopi 12110 A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  J  e.  (TopOn `  B )   =>    |-  J  e.  Top
 
Theoremtoponunii 12111 The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  J  e.  (TopOn `  B )   =>    |-  B  =  U. J
 
Theoremtoptopon 12112 Alternative definition of  Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
 
Theoremtoptopon2 12113 A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
 |-  ( J  e.  Top  <->  J  e.  (TopOn `  U. J ) )
 
Theoremtopontopon 12114 A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
 |-  ( J  e.  (TopOn `  X )  ->  J  e.  (TopOn `  U. J ) )
 
Theoremtoponrestid 12115 Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
 |-  A  e.  (TopOn `  B )   =>    |-  A  =  ( At  B )
 
Theoremtoponsspwpwg 12116 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.)
 |-  ( A  e.  V  ->  (TopOn `  A )  C_ 
 ~P ~P A )
 
Theoremdmtopon 12117 The domain of TopOn is  _V. (Contributed by BJ, 29-Apr-2021.)
 |- 
 dom TopOn  =  _V
 
Theoremfntopon 12118 The class TopOn is a function with domain  _V. (Contributed by BJ, 29-Apr-2021.)
 |- TopOn  Fn  _V
 
Theoremtoponmax 12119 The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  ( J  e.  (TopOn `  B )  ->  B  e.  J )
 
Theoremtoponss 12120 A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
 |-  ( ( J  e.  (TopOn `  X )  /\  A  e.  J )  ->  A  C_  X )
 
Theoremtoponcom 12121 If  K is a topology on the base set of topology  J, then  J is a topology on the base of  K. (Contributed by Mario Carneiro, 22-Aug-2015.)
 |-  ( ( J  e.  Top  /\  K  e.  (TopOn `  U. J ) )  ->  J  e.  (TopOn `  U. K ) )
 
Theoremtoponcomb 12122 Biconditional form of toponcom 12121. (Contributed by BJ, 5-Dec-2021.)
 |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( J  e.  (TopOn ` 
 U. K )  <->  K  e.  (TopOn ` 
 U. J ) ) )
 
Theoremtopgele 12123 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.)
 |-  ( J  e.  (TopOn `  X )  ->  ( { (/) ,  X }  C_  J  /\  J  C_  ~P X ) )
 
7.1.1.3  Topological spaces
 
Syntaxctps 12124 Syntax for the class of topological spaces.
 class  TopSp
 
Definitiondf-topsp 12125 Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
 |- 
 TopSp  =  { f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) ) }
 
Theoremistps 12126 Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  A  =  ( Base `  K )   &    |-  J  =  (
 TopOpen `  K )   =>    |-  ( K  e.  TopSp  <->  J  e.  (TopOn `  A ) )
 
Theoremistps2 12127 Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.)
 |-  A  =  ( Base `  K )   &    |-  J  =  (
 TopOpen `  K )   =>    |-  ( K  e.  TopSp  <->  ( J  e.  Top  /\  A  =  U. J ) )
 
Theoremtpsuni 12128 The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
 |-  A  =  ( Base `  K )   &    |-  J  =  (
 TopOpen `  K )   =>    |-  ( K  e.  TopSp  ->  A  =  U. J )
 
Theoremtpstop 12129 The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
 |-  J  =  ( TopOpen `  K )   =>    |-  ( K  e.  TopSp  ->  J  e.  Top )
 
Theoremtpspropd 12130 A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
 |-  ( ph  ->  ( Base `  K )  =  ( Base `  L )
 )   &    |-  ( ph  ->  ( TopOpen `  K )  =  (
 TopOpen `  L ) )   =>    |-  ( ph  ->  ( K  e.  TopSp 
 <->  L  e.  TopSp ) )
 
Theoremtopontopn 12131 Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  A  =  ( Base `  K )   &    |-  J  =  (TopSet `  K )   =>    |-  ( J  e.  (TopOn `  A )  ->  J  =  ( TopOpen `  K )
 )
 
Theoremtsettps 12132 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.)
 |-  A  =  ( Base `  K )   &    |-  J  =  (TopSet `  K )   =>    |-  ( J  e.  (TopOn `  A )  ->  K  e.  TopSp )
 
Theoremistpsi 12133 Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
 |-  ( Base `  K )  =  A   &    |-  ( TopOpen `  K )  =  J   &    |-  A  =  U. J   &    |-  J  e.  Top   =>    |-  K  e.  TopSp
 
Theoremeltpsg 12134 Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  K  =  { <. (
 Base `  ndx ) ,  A >. ,  <. (TopSet `  ndx ) ,  J >. }   =>    |-  ( J  e.  (TopOn `  A )  ->  K  e.  TopSp )
 
Theoremeltpsi 12135 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.)
 |-  K  =  { <. (
 Base `  ndx ) ,  A >. ,  <. (TopSet `  ndx ) ,  J >. }   &    |-  A  =  U. J   &    |-  J  e.  Top   =>    |-  K  e.  TopSp
 
7.1.2  Topological bases
 
Syntaxctb 12136 Syntax for the class of topological bases.
 class  TopBases
 
Definitiondf-bases 12137* Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 12139). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
 |-  TopBases 
 =  { x  |  A. y  e.  x  A. z  e.  x  ( y  i^i  z ) 
 C_  U. ( x  i^i  ~P ( y  i^i  z
 ) ) }
 
Theoremisbasisg 12138* Express the predicate "the set 
B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
 |-  ( B  e.  C  ->  ( B  e.  TopBases  <->  A. x  e.  B  A. y  e.  B  ( x  i^i  y ) 
 C_  U. ( B  i^i  ~P ( x  i^i  y
 ) ) ) )
 
Theoremisbasis2g 12139* Express the predicate "the set 
B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
 |-  ( B  e.  C  ->  ( B  e.  TopBases  <->  A. x  e.  B  A. y  e.  B  A. z  e.  ( x  i^i  y ) E. w  e.  B  ( z  e.  w  /\  w  C_  ( x  i^i  y ) ) ) )
 
Theoremisbasis3g 12140* Express the predicate "the set 
B is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
 |-  ( B  e.  C  ->  ( B  e.  TopBases  <->  ( A. x  e.  B  x  C_  U. B  /\  A. x  e.  U. B E. y  e.  B  x  e.  y  /\  A. x  e.  B  A. y  e.  B  A. z  e.  ( x  i^i  y
 ) E. w  e.  B  ( z  e.  w  /\  w  C_  ( x  i^i  y ) ) ) ) )
 
Theorembasis1 12141 Property of a basis. (Contributed by NM, 16-Jul-2006.)
 |-  ( ( B  e.  TopBases  /\  C  e.  B  /\  D  e.  B )  ->  ( C  i^i  D )  C_  U. ( B  i^i  ~P ( C  i^i  D ) ) )
 
Theorembasis2 12142* Property of a basis. (Contributed by NM, 17-Jul-2006.)
 |-  ( ( ( B  e.  TopBases  /\  C  e.  B )  /\  ( D  e.  B  /\  A  e.  ( C  i^i  D ) ) )  ->  E. x  e.  B  ( A  e.  x  /\  x  C_  ( C  i^i  D ) ) )
 
Theoremfiinbas 12143* If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
 |-  ( ( B  e.  C  /\  A. x  e.  B  A. y  e.  B  ( x  i^i  y )  e.  B )  ->  B  e.  TopBases )
 
Theorembaspartn 12144* A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
 |-  ( ( P  e.  V  /\  A. x  e.  P  A. y  e.  P  ( x  =  y  \/  ( x  i^i  y )  =  (/) ) )  ->  P  e. 
 TopBases )
 
Theoremtgval 12145* The topology generated by a basis. See also tgval2 12147 and tgval3 12154. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
 |-  ( B  e.  V  ->  ( topGen `  B )  =  { x  |  x  C_ 
 U. ( B  i^i  ~P x ) } )
 
Theoremtgvalex 12146 The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
 |-  ( B  e.  V  ->  ( topGen `  B )  e.  _V )
 
Theoremtgval2 12147* Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 12160) that  ( topGen `  B ) is indeed a topology (on  U. B, see unitg 12158). See also tgval 12145 and tgval3 12154. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
 |-  ( B  e.  V  ->  ( topGen `  B )  =  { x  |  ( x  C_  U. B  /\  A. y  e.  x  E. z  e.  B  (
 y  e.  z  /\  z  C_  x ) ) } )
 
Theoremeltg 12148 Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
 |-  ( B  e.  V  ->  ( A  e.  ( topGen `
  B )  <->  A  C_  U. ( B  i^i  ~P A ) ) )
 
Theoremeltg2 12149* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
 |-  ( B  e.  V  ->  ( A  e.  ( topGen `
  B )  <->  ( A  C_  U. B  /\  A. x  e.  A  E. y  e.  B  ( x  e.  y  /\  y  C_  A ) ) ) )
 
Theoremeltg2b 12150* Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
 |-  ( B  e.  V  ->  ( A  e.  ( topGen `
  B )  <->  A. x  e.  A  E. y  e.  B  ( x  e.  y  /\  y  C_  A ) ) )
 
Theoremeltg4i 12151 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.)
 |-  ( A  e.  ( topGen `
  B )  ->  A  =  U. ( B  i^i  ~P A ) )
 
Theoremeltg3i 12152 The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
 |-  ( ( B  e.  V  /\  A  C_  B )  ->  U. A  e.  ( topGen `
  B ) )
 
Theoremeltg3 12153* Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
 |-  ( B  e.  V  ->  ( A  e.  ( topGen `
  B )  <->  E. x ( x 
 C_  B  /\  A  =  U. x ) ) )
 
Theoremtgval3 12154* Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12145 and tgval2 12147. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
 |-  ( B  e.  V  ->  ( topGen `  B )  =  { x  |  E. y ( y  C_  B  /\  x  =  U. y ) } )
 
Theoremtg1 12155 Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
 |-  ( A  e.  ( topGen `
  B )  ->  A  C_  U. B )
 
Theoremtg2 12156* Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
 |-  ( ( A  e.  ( topGen `  B )  /\  C  e.  A ) 
 ->  E. x  e.  B  ( C  e.  x  /\  x  C_  A ) )
 
Theorembastg 12157 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.)
 |-  ( B  e.  V  ->  B  C_  ( topGen `  B ) )
 
Theoremunitg 12158 The topology generated by a basis 
B is a topology on 
U. B. 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.)
 |-  ( B  e.  V  ->  U. ( topGen `  B )  =  U. B )
 
Theoremtgss 12159 Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
 |-  ( ( C  e.  V  /\  B  C_  C )  ->  ( topGen `  B )  C_  ( topGen `  C ) )
 
Theoremtgcl 12160 Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
 |-  ( B  e.  TopBases  ->  (
 topGen `  B )  e. 
 Top )
 
Theoremtgclb 12161 The property tgcl 12160 can be reversed: if the topology generated by  B is actually a topology, then 
B must be a topological basis. This yields an alternative definition of  TopBases. (Contributed by Mario Carneiro, 2-Sep-2015.)
 |-  ( B  e.  TopBases  <->  ( topGen `  B )  e.  Top )
 
Theoremtgtopon 12162 A basis generates a topology on 
U. B. (Contributed by Mario Carneiro, 14-Aug-2015.)
 |-  ( B  e.  TopBases  ->  (
 topGen `  B )  e.  (TopOn `  U. B ) )
 
Theoremtopbas 12163 A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
 |-  ( J  e.  Top  ->  J  e.  TopBases )
 
Theoremtgtop 12164 A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
 |-  ( J  e.  Top  ->  ( topGen `  J )  =  J )
 
Theoremeltop 12165 Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
 |-  ( J  e.  Top  ->  ( A  e.  J  <->  A 
 C_  U. ( J  i^i  ~P A ) ) )
 
Theoremeltop2 12166* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
 |-  ( J  e.  Top  ->  ( A  e.  J  <->  A. x  e.  A  E. y  e.  J  ( x  e.  y  /\  y  C_  A ) ) )
 
Theoremeltop3 12167* Membership in a topology. (Contributed by NM, 19-Jul-2006.)
 |-  ( J  e.  Top  ->  ( A  e.  J  <->  E. x ( x  C_  J  /\  A  =  U. x ) ) )
 
Theoremtgdom 12168 A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 9-Apr-2015.)
 |-  ( B  e.  V  ->  ( topGen `  B )  ~<_  ~P B )
 
Theoremtgiun 12169* The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( B  e.  V  /\  A. x  e.  A  C  e.  B )  ->  U_ x  e.  A  C  e.  ( topGen `  B ) )
 
Theoremtgidm 12170 The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
 |-  ( B  e.  V  ->  ( topGen `  ( topGen `  B ) )  =  ( topGen `
  B ) )
 
Theorembastop 12171 Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
 |-  ( B  e.  TopBases  ->  ( B  e.  Top  <->  ( topGen `  B )  =  B )
 )
 
Theoremtgtop11 12172 The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
 |-  ( ( J  e.  Top  /\  K  e.  Top  /\  ( topGen `  J )  =  ( topGen `  K )
 )  ->  J  =  K )
 
Theoremen1top 12173  { (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
 |-  ( J  e.  Top  ->  ( J  ~~  1o  <->  J  =  { (/)
 } ) )
 
Theoremtgss3 12174 A criterion for determining whether one topology is finer than another. Lemma 2.2 of [Munkres] p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( B  e.  V  /\  C  e.  W )  ->  ( ( topGen `  B )  C_  ( topGen `  C )  <->  B  C_  ( topGen `  C ) ) )
 
Theoremtgss2 12175* A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( B  e.  V  /\  U. B  =  U. C )  ->  (
 ( topGen `  B )  C_  ( topGen `  C )  <->  A. x  e.  U. B A. y  e.  B  ( x  e.  y  ->  E. z  e.  C  ( x  e.  z  /\  z  C_  y ) ) ) )
 
Theorembasgen 12176 Given a topology  J, show that a subset  B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using abbreviations. (Contributed by NM, 22-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( J  e.  Top  /\  B  C_  J  /\  J  C_  ( topGen `  B ) )  ->  ( topGen `  B )  =  J )
 
Theorembasgen2 12177* Given a topology  J, show that a subset  B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( J  e.  Top  /\  B  C_  J  /\  A. x  e.  J  A. y  e.  x  E. z  e.  B  (
 y  e.  z  /\  z  C_  x ) ) 
 ->  ( topGen `  B )  =  J )
 
Theorem2basgeng 12178 Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.)
 |-  ( ( B  e.  V  /\  B  C_  C  /\  C  C_  ( topGen `  B ) )  ->  ( topGen `  B )  =  ( topGen `  C )
 )
 
Theorembastop1 12179* A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom " ( topGen `  B
)  =  J " to express " B is a basis for topology  J " since we do not have a separate notation for this. Definition 15.35 of [Schechter] p. 428. (Contributed by NM, 2-Feb-2008.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
 |-  ( ( J  e.  Top  /\  B  C_  J )  ->  ( ( topGen `  B )  =  J  <->  A. x  e.  J  E. y ( y  C_  B  /\  x  =  U. y ) ) )
 
Theorembastop2 12180* A version of bastop1 12179 that doesn't have  B  C_  J in the antecedent. (Contributed by NM, 3-Feb-2008.)
 |-  ( J  e.  Top  ->  ( ( topGen `  B )  =  J  <->  ( B  C_  J  /\  A. x  e.  J  E. y ( y  C_  B  /\  x  =  U. y ) ) ) )
 
7.1.3  Examples of topologies
 
Theoremdistop 12181 The discrete topology on a set  A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.)
 |-  ( A  e.  V  ->  ~P A  e.  Top )
 
Theoremtopnex 12182 The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4340. (Contributed by BJ, 2-May-2021.)
 |- 
 Top  e/  _V
 
Theoremdistopon 12183 The discrete topology on a set  A, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |-  ( A  e.  V  ->  ~P A  e.  (TopOn `  A ) )
 
Theoremsn0topon 12184 The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
 |- 
 { (/) }  e.  (TopOn `  (/) )
 
Theoremsn0top 12185 The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro, 13-Aug-2015.)
 |- 
 { (/) }  e.  Top
 
Theoremepttop 12186* The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
 |-  ( ( A  e.  V  /\  P  e.  A )  ->  { x  e. 
 ~P A  |  ( P  e.  x  ->  x  =  A ) }  e.  (TopOn `  A ) )
 
Theoremdistps 12187 The discrete topology on a set  A expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
 |-  A  e.  _V   &    |-  K  =  { <. ( Base `  ndx ) ,  A >. , 
 <. (TopSet `  ndx ) ,  ~P A >. }   =>    |-  K  e.  TopSp
 
7.1.4  Closure and interior
 
Syntaxccld 12188 Extend class notation with the set of closed sets of a topology.
 class  Clsd
 
Syntaxcnt 12189 Extend class notation with interior of a subset of a topology base set.
 class  int
 
Syntaxccl 12190 Extend class notation with closure of a subset of a topology base set.
 class  cls
 
Definitiondf-cld 12191* Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
 |- 
 Clsd  =  ( j  e.  Top  |->  { x  e.  ~P U. j  |  ( U. j  \  x )  e.  j } )
 
Definitiondf-ntr 12192* Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 12206. (Contributed by NM, 10-Sep-2006.)
 |- 
 int  =  ( j  e.  Top  |->  ( x  e. 
 ~P U. j  |->  U. (
 j  i^i  ~P x ) ) )
 
Definitiondf-cls 12193* Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 12207. (Contributed by NM, 3-Oct-2006.)
 |- 
 cls  =  ( j  e.  Top  |->  ( x  e. 
 ~P U. j  |->  |^| { y  e.  ( Clsd `  j )  |  x  C_  y }
 ) )
 
Theoremfncld 12194 The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
 |- 
 Clsd  Fn  Top
 
Theoremcldval 12195* The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  ->  ( Clsd `  J )  =  { x  e.  ~P X  |  ( X  \  x )  e.  J } )
 
Theoremntrfval 12196* The interior function on the subsets of a topology's base set. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  ->  ( int `  J )  =  ( x  e.  ~P X  |->  U. ( J  i^i  ~P x ) ) )
 
Theoremclsfval 12197* The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  ->  ( cls `  J )  =  ( x  e.  ~P X  |->  |^| { y  e.  ( Clsd `  J )  |  x  C_  y }
 ) )
 
Theoremcldrcl 12198 Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
 |-  ( C  e.  ( Clsd `  J )  ->  J  e.  Top )
 
Theoremiscld 12199 The predicate "the class  S is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
 |-  X  =  U. J   =>    |-  ( J  e.  Top  ->  ( S  e.  ( Clsd `  J )  <->  ( S  C_  X  /\  ( X  \  S )  e.  J ) ) )
 
Theoremiscld2 12200 A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
 |-  X  =  U. J   =>    |-  (
 ( J  e.  Top  /\  S  C_  X )  ->  ( S  e.  ( Clsd `  J )  <->  ( X  \  S )  e.  J ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13177
  Copyright terms: Public domain < Previous  Next >