:: On constructing topological spaces and Sorgenfrey line
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let X be set ;
let B be Subset-Family of X;
attrB is point-filtered  means :Def1: :: TOPGEN_3:def 1
 for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 );
end;

:: deftheorem Def1 defines point-filtered TOPGEN_3:def_1_:_
 for X being set
for B being Subset-Family of X holds
( B is point-filtered iff for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 ) );

::<DSCR monograph="topology" name="condition (B2)"/>
theorem Th1: :: TOPGEN_3:1
for X being set
for B being Subset-Family of X holds
( B is covering iff for x being set st x in X holds
ex U being Subset of X st
( U in B &amp; x in U ) )
proofend;

::<DSCR monograph="topology" label="1.2.1."/>
theorem Th2: :: TOPGEN_3:2
for X being set
for B being Subset-Family of X st B is point-filtered &amp; B is covering holds
for T being TopStruct st the carrier of T = X &amp; the topology of T = UniCl B holds
( T is TopSpace &amp; B is Basis of T )
proofend;

::<DSCR monograph="topology" label="1.2.3."/>
theorem :: TOPGEN_3:3
for X being set
for B being non-empty ManySortedSet of X st rng B c= bool (bool X) &amp; ( for x, U being set st x in X &amp; U in B . x holds
x in U ) &amp; ( for x, y, U being set st x in U &amp; U in B . y &amp; y in X holds
ex V being set st
( V in B . x &amp; V c= U ) ) &amp; ( for x, U1, U2 being set st x in X &amp; U1 in B . x &amp; U2 in B . x holds
ex U being set st
( U in B . x &amp; U c= U1 /\ U2 ) ) holds
ex P being Subset-Family of X st
( P = Union B &amp; ( for T being TopStruct st the carrier of T = X &amp; the topology of T = UniCl P holds
( T is TopSpace &amp; ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )
proofend;

::<DSCR monograph="topology" label="1.2.5."/>
theorem Th4: :: TOPGEN_3:4
for X being set
for F being Subset-Family of X st {} in F &amp; ( for A, B being set st A in F &amp; B in F holds
A \/ B in F ) &amp; ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) holds
for T being TopStruct st the carrier of T = X &amp; the topology of T = COMPLEMENT F holds
( T is TopSpace &amp; ( for A being Subset of T holds
( A is closed iff A in F ) ) )
proofend;

scheme :: TOPGEN_3:sch 1
TopDefByClosedPred{ F1() ->  set , P1[ set ] } :
 ex T being strict TopSpace st
( the carrier of T = F1() &amp; ( for A being Subset of T holds
( A is closed iff P1[A] ) ) )
provided
A1: ( P1[ {} ] &amp; P1[F1()] ) and
A2: for A, B being set st P1[A] &amp; P1[B] holds
P1[A \/ B] and
A3: for G being Subset-Family of F1() st ( for A being set st A in G holds
P1[A] ) holds
P1[ Intersect G]
proofend;

Lm1:  for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 &amp; the topology of T1 c= the topology of T2 )
proofend;

theorem :: TOPGEN_3:5
for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
proofend;

Lm2:  for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 &amp; the topology of T1 c= the topology of T2 )
proofend;

theorem Th6: :: TOPGEN_3:6
for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
proofend;

definition
let X, Y be set ;
let r be Subset of [:X,(bool Y):];
:: original:rng
redefine func rng r ->  Subset-Family of Y;
coherence
 rng r is Subset-Family of Y by RELAT_1:def_19;
end;

::<DSCR monograph="topology" label="1.2.7."/>
theorem Th7: :: TOPGEN_3:7
for X being set
for c being Function of (bool X),(bool X) st c . {} = {} &amp; ( for A being Subset of X holds A c= c . A ) &amp; ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) &amp; ( for A being Subset of X holds c . (c . A) = c . A ) holds
for T being TopStruct st the carrier of T = X &amp; the topology of T = COMPLEMENT (rng c) holds
( T is TopSpace &amp; ( for A being Subset of T holds Cl A = c . A ) )
proofend;

scheme :: TOPGEN_3:sch 2
TopDefByClosureOp{ F1() ->  set , F2( set ) ->  set } :
 ex T being strict TopSpace st
( the carrier of T = F1() &amp; ( for A being Subset of T holds Cl A = F2(A) ) )
provided
A1: F2({}) = {} and
A2: for A being Subset of F1() holds
( A c= F2(A) &amp; F2(A) c= F1() ) and
A3: for A, B being Subset of F1() holds F2((A \/ B)) = F2(A) \/ F2(B) and
A4: for A being Subset of F1() holds F2(F2(A)) = F2(A)
proofend;

theorem Th8: :: TOPGEN_3:8
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 &amp; ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2 ) holds
the topology of T1 = the topology of T2
proofend;

::<DSCR monograph="topology" label="1.2.9."/>
theorem Th9: :: TOPGEN_3:9
for X being set
for i being Function of (bool X),(bool X) st i . X = X &amp; ( for A being Subset of X holds i . A c= A ) &amp; ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) &amp; ( for A being Subset of X holds i . (i . A) = i . A ) holds
for T being TopStruct st the carrier of T = X &amp; the topology of T = rng i holds
( T is TopSpace &amp; ( for A being Subset of T holds Int A = i . A ) )
proofend;

scheme :: TOPGEN_3:sch 3
TopDefByInteriorOp{ F1() ->  set , F2( set ) ->  set } :
 ex T being strict TopSpace st
( the carrier of T = F1() &amp; ( for A being Subset of T holds Int A = F2(A) ) )
provided
A1: F2(F1()) = F1() and
A2: for A being Subset of F1() holds F2(A) c= A and
A3: for A, B being Subset of F1() holds F2((A /\ B)) = F2(A) /\ F2(B) and
A4: for A being Subset of F1() holds F2(F2(A)) = F2(A)
proofend;

theorem Th10: :: TOPGEN_3:10
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 &amp; ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2 ) holds
the topology of T1 = the topology of T2
proofend;

begin

definition
func Sorgenfrey-line  ->  non empty strict TopSpace means :Def2: :: TOPGEN_3:def 2
( the carrier of it = REAL &amp; ex B being Subset-Family of REAL st
( the topology of it = UniCl B &amp; B =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  ) );
uniqueness
 for b1, b2 being non empty strict TopSpace st the carrier of b1 = REAL &amp; ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B &amp; B =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  ) &amp; the carrier of b2 = REAL &amp; ex B being Subset-Family of REAL st
( the topology of b2 = UniCl B &amp; B =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  ) holds
b1 = b2 ;
existence
 ex b1 being non empty strict TopSpace st
( the carrier of b1 = REAL &amp; ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B &amp; B =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  ) )
proofend;
end;

:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def_2_:_
 for b1 being non empty strict TopSpace holds
( b1 = Sorgenfrey-line iff ( the carrier of b1 = REAL &amp; ex B being Subset-Family of REAL st
( the topology of b1 = UniCl B &amp; B =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  ) ) );

Lm3:  the carrier of Sorgenfrey-line = REAL
by Def2;

consider BB being Subset-Family of REAL such that
Lm4:  the topology of Sorgenfrey-line = UniCl BB and
Lm5:  BB =  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  by Def2;

 BB c= the topology of Sorgenfrey-line
by Lm4, CANTOR_1:1;

then Lm6:  BB is Basis of Sorgenfrey-line
by Lm3, Lm4, CANTOR_1:def_2, TOPS_2:64;

theorem Th11: :: TOPGEN_3:11
for x, y being real number holds [.x,y.[ is open Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_3:12
for x, y being real number holds ].x,y.[ is open Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_3:13
for x being real number holds left_open_halfline x is open Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_3:14
for x being real number holds right_open_halfline x is open Subset of Sorgenfrey-line
proofend;

theorem :: TOPGEN_3:15
for x being real number holds right_closed_halfline x is open Subset of Sorgenfrey-line
proofend;

theorem Th16: :: TOPGEN_3:16
card INT = omega
proofend;

:: [WP: ] The_Denumerability_of_the_Rational_Numbers
theorem Th17: :: TOPGEN_3:17
card RAT = omega
proofend;

theorem Th18: :: TOPGEN_3:18
for A being set st A is mutually-disjoint &amp; ( for a being set st a in A holds
ex x, y being real number st
( x < y &amp; ].x,y.[ c= a ) ) holds
A is countable
proofend;

definition
let X be set ;
let x be real number ;
predx is_local_minimum_of X means :Def3: :: TOPGEN_3:def 3
( x in X &amp; ex y being real number st
( y < x &amp; ].y,x.[ misses X ) );
end;

:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def_3_:_
 for X being set
for x being real number holds
( x is_local_minimum_of X iff ( x in X &amp; ex y being real number st
( y < x &amp; ].y,x.[ misses X ) ) );

theorem Th19: :: TOPGEN_3:19
for U being Subset of REAL holds  {  x where x is Element of REAL : x is_local_minimum_of U  }  is countable
proofend;

registration
let M be Aleph;
cluster exp (2,M) ->  infinite ;
coherence
 not exp (2,M) is finite
proofend;
end;

definition
func continuum  ->  infinite cardinal number  equals :: TOPGEN_3:def 4
 card REAL;
coherence
 card REAL is infinite cardinal number ;
end;

:: deftheorem  defines continuum TOPGEN_3:def_4_:_
 continuum = card REAL;

theorem Th20: :: TOPGEN_3:20
card  {  [.x,q.[ where x, q is Element of REAL : ( x < q &amp; q is rational )  }  = continuum
proofend;

definition
let X be set ;
let r be real number ;
funcX -powers r ->  Function of NAT,REAL means :Def5: :: TOPGEN_3:def 5
 for i being Nat holds
( ( i in X &amp; it . i = r |^ i ) or ( not i in X &amp; it . i = 0 ) );
existence
 ex b1 being Function of NAT,REAL st
for i being Nat holds
( ( i in X &amp; b1 . i = r |^ i ) or ( not i in X &amp; b1 . i = 0 ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,REAL st ( for i being Nat holds
( ( i in X &amp; b1 . i = r |^ i ) or ( not i in X &amp; b1 . i = 0 ) ) ) &amp; ( for i being Nat holds
( ( i in X &amp; b2 . i = r |^ i ) or ( not i in X &amp; b2 . i = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines -powers TOPGEN_3:def_5_:_
 for X being set
for r being real number
for b3 being Function of NAT,REAL holds
( b3 = X -powers r iff for i being Nat holds
( ( i in X &amp; b3 . i = r |^ i ) or ( not i in X &amp; b3 . i = 0 ) ) );

theorem Th21: :: TOPGEN_3:21
for X being set
for r being real number st 0 < r &amp; r < 1 holds
X -powers r is summable
proofend;

theorem Th22: :: TOPGEN_3:22
for r being real number
for n being Element of NAT st 0 < r &amp; r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
proofend;

theorem Th23: :: TOPGEN_3:23
for n being Element of NAT holds Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n
proofend;

theorem :: TOPGEN_3:24
for r being real number
for X being set st 0 < r &amp; r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq)
proofend;

theorem Th25: :: TOPGEN_3:25
for X being set
for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
proofend;

theorem Th26: :: TOPGEN_3:26
for X being infinite Subset of NAT
for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
proofend;

theorem Th27: :: TOPGEN_3:27
for X, Y being infinite Subset of NAT st Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) holds
X = Y
proofend;

theorem Th28: :: TOPGEN_3:28
for X being set st X is countable holds
Fin X is countable
proofend;

theorem Th29: :: TOPGEN_3:29
continuum = exp (2,omega)
proofend;

:: [WP: ] The_Non-Denumerability_of_the_Continuum
theorem Th30: :: TOPGEN_3:30
omega in continuum
proofend;

theorem Th31: :: TOPGEN_3:31
for A being Subset-Family of REAL st card A in continuum holds
card  {  x where x is Element of REAL : ex U being set st
( U in UniCl A &amp; x is_local_minimum_of U )  }  in continuum
proofend;

theorem Th32: :: TOPGEN_3:32
for X being Subset-Family of REAL st card X in continuum holds
ex x being real number ex q being rational number st
( x < q &amp; not [.x,q.[ in UniCl X )
proofend;

theorem :: TOPGEN_3:33
weight Sorgenfrey-line = continuum
proofend;

begin

definition
let X be set ;
func ClFinTop X ->  strict TopSpace means :Def6: :: TOPGEN_3:def 6
( the carrier of it = X &amp; ( for F being Subset of it holds
( F is closed iff ( F is finite or F = X ) ) ) );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = X &amp; ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) )
proofend;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X &amp; ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) &amp; the carrier of b2 = X &amp; ( for F being Subset of b2 holds
( F is closed iff ( F is finite or F = X ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def6 defines ClFinTop TOPGEN_3:def_6_:_
 for X being set
for b2 being strict TopSpace holds
( b2 = ClFinTop X iff ( the carrier of b2 = X &amp; ( for F being Subset of b2 holds
( F is closed iff ( F is finite or F = X ) ) ) ) );

theorem Th34: :: TOPGEN_3:34
for X being set
for A being Subset of (ClFinTop X) holds
( A is open iff ( A = {} or A ` is finite ) )
proofend;

theorem Th35: :: TOPGEN_3:35
for X being infinite set
for A being Subset of X st A is finite holds
A ` is infinite
proofend;

registration
let X be non empty set ;
cluster ClFinTop X ->  non empty strict ;
coherence
 not ClFinTop X is empty by Def6;
end;

theorem :: TOPGEN_3:36
for X being infinite set
for U, V being non empty open Subset of (ClFinTop X) holds U meets V
proofend;

begin

definition
let X, x0 be set ;
funcx0 -PointClTop X ->  strict TopSpace means :Def7: :: TOPGEN_3:def 7
( the carrier of it = X &amp; ( for A being Subset of it holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = X &amp; ( for A being Subset of b1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) )
proofend;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X &amp; ( for A being Subset of b1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) &amp; the carrier of b2 = X &amp; ( for A being Subset of b2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def7 defines -PointClTop TOPGEN_3:def_7_:_
 for X, x0 being set
for b3 being strict TopSpace holds
( b3 = x0 -PointClTop X iff ( the carrier of b3 = X &amp; ( for A being Subset of b3 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) ) );

registration
let X be non empty set ;
let x0 be set ;
clusterx0 -PointClTop X ->  non empty strict ;
coherence
 not x0 -PointClTop X is empty by Def7;
end;

theorem Th37: :: TOPGEN_3:37
for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
proofend;

theorem Th38: :: TOPGEN_3:38
for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds
( A is closed iff x0 in A )
proofend;

theorem Th39: :: TOPGEN_3:39
for X being non empty set
for x0 being Element of X
for A being proper Subset of (x0 -PointClTop X) holds
( A is open iff not x0 in A )
proofend;

theorem :: TOPGEN_3:40
for X, x0, x being set st x0 in X holds
( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 )
proofend;

theorem :: TOPGEN_3:41
for X, x0, x being set st {x0} c< X holds
( {x} is open Subset of (x0 -PointClTop X) iff ( x in X &amp; x <> x0 ) )
proofend;

begin

definition
let X, X0 be set ;
funcX0 -DiscreteTop X ->  strict TopSpace means :Def8: :: TOPGEN_3:def 8
( the carrier of it = X &amp; ( for A being Subset of it holds Int A = IFEQ (A,X,A,(A /\ X0)) ) );
existence
 ex b1 being strict TopSpace st
( the carrier of b1 = X &amp; ( for A being Subset of b1 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) )
proofend;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X &amp; ( for A being Subset of b1 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) &amp; the carrier of b2 = X &amp; ( for A being Subset of b2 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def_8_:_
 for X, X0 being set
for b3 being strict TopSpace holds
( b3 = X0 -DiscreteTop X iff ( the carrier of b3 = X &amp; ( for A being Subset of b3 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) ) );

registration
let X be non empty set ;
let X0 be set ;
clusterX0 -DiscreteTop X ->  non empty strict ;
coherence
 not X0 -DiscreteTop X is empty by Def8;
end;

theorem Th42: :: TOPGEN_3:42
for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
proofend;

theorem Th43: :: TOPGEN_3:43
for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds
( A is open iff A c= X0 )
proofend;

theorem Th44: :: TOPGEN_3:44
for X being set
for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
proofend;

theorem :: TOPGEN_3:45
for X being set holds ADTS X = {} -DiscreteTop X
proofend;

theorem :: TOPGEN_3:46
for X being set holds 1TopSp X = X -DiscreteTop X
proofend;