:: On constructing topological spaces and Sorgenfrey line
:: by Grzegorz Bancerek
::
:: Copyright (c) 2004-2018 Association of Mizar Users

definition
let X be set ;
let B be Subset-Family of X;
attr B is point-filtered means :: 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 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 & x in U ) )
proof end;

::<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 & B is covering holds
for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T )
proof end;

::<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) & ( for x, U being set st x in X & U in B . x holds
x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ) holds
ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )
proof end;

::<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 & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( 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 & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
proof end;

scheme :: TOPGEN_3:sch 1
TopDefByClosedPred{ F1() -> set , P1[ set ] } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( for A being Subset of T holds
( A is closed iff P1[A] ) ) )
provided
A1: ( P1[ {} ] & P1[F1()] ) and
A2: for A, B being set st P1[A] & 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]
proof end;

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 & the topology of T1 c= the topology of T2 )

proof end;

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 #)
proof end;

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 & the topology of T1 c= the topology of T2 )

proof end;

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 #)
proof end;

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 . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds
( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )
proof end;

scheme :: TOPGEN_3:sch 2
TopDefByClosureOp{ F1() -> set , F2( object ) -> set } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( 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) & 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)
proof end;

theorem Th8: :: TOPGEN_3:8
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( 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
proof end;

::<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 & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = rng i holds
( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )
proof end;

scheme :: TOPGEN_3:sch 3
TopDefByInteriorOp{ F1() -> set , F2( object ) -> set } :
ex T being strict TopSpace st
( the carrier of T = F1() & ( 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)
proof end;

theorem Th10: :: TOPGEN_3:10
for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( 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
proof end;

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

Lm3:
by Def2;

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

BB c= the topology of Sorgenfrey-line
by ;

then Lm6: BB is Basis of Sorgenfrey-line
by ;

theorem Th11: :: TOPGEN_3:11
for x, y being Real holds [.x,y.[ is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:12
for x, y being Real holds ].x,y.[ is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:13
for x being Real holds left_open_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:14
for x being Real holds right_open_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem :: TOPGEN_3:15
for x being Real holds right_closed_halfline x is open Subset of Sorgenfrey-line
proof end;

theorem Th16: :: TOPGEN_3:16
proof end;

:: The Denumerability of the Rational Numbers
theorem Th17: :: TOPGEN_3:17
proof end;

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

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

:: deftheorem defines is_local_minimum_of TOPGEN_3:def 3 :
for X being set
for x being Real holds
( x is_local_minimum_of X iff ( x in X & ex y being Real st
( y < x & ].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
proof end;

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

definition
coherence ;
end;

:: deftheorem defines continuum TOPGEN_3:def 4 :

theorem Th20: :: TOPGEN_3:20
card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } = continuum
proof end;

definition
let X be set ;
let r be Real;
func X -powers r -> sequence of REAL means :Def5: :: TOPGEN_3:def 5
for i being Nat holds
( ( i in X & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );
existence
ex b1 being sequence of REAL st
for i being Nat holds
( ( i in X & b1 . i = r |^ i ) or ( not i in X & b1 . i = 0 ) )
proof end;
uniqueness
for b1, b2 being sequence of REAL st ( for i being Nat holds
( ( i in X & b1 . i = r |^ i ) or ( not i in X & b1 . i = 0 ) ) ) & ( for i being Nat holds
( ( i in X & b2 . i = r |^ i ) or ( not i in X & b2 . i = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
for X being set
for r being Real
for b3 being sequence of REAL holds
( b3 = X -powers r iff for i being Nat holds
( ( i in X & b3 . i = r |^ i ) or ( not i in X & b3 . i = 0 ) ) );

theorem Th21: :: TOPGEN_3:21
for X being set
for r being Real st 0 < r & r < 1 holds
X -powers r is summable
proof end;

theorem Th22: :: TOPGEN_3:22
for r being Real
for n being Element of NAT st 0 < r & r < 1 holds
Sum (() ^\ n) = (r |^ n) / (1 - r)
proof end;

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

theorem :: TOPGEN_3:24
for r being Real
for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum ()
proof end;

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
proof end;

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))
proof end;

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
proof end;

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

theorem Th29: :: TOPGEN_3:29
proof end;

:: The Non-Denumerability of the Continuum
theorem Th30: :: TOPGEN_3:30
proof end;

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 & x is_local_minimum_of U )
}
in continuum
proof end;

theorem Th32: :: TOPGEN_3:32
for X being Subset-Family of REAL st card X in continuum holds
ex x being Real ex q being Rational st
( x < q & not [.x,q.[ in UniCl X )
proof end;

theorem :: TOPGEN_3:33
proof end;

definition
let X be set ;
func ClFinTop X -> strict TopSpace means :Def6: :: TOPGEN_3:def 6
( the carrier of it = X & ( 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 & ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for F being Subset of b1 holds
( F is closed iff ( F is finite or F = X ) ) ) & the carrier of b2 = X & ( for F being Subset of b2 holds
( F is closed iff ( F is finite or F = X ) ) ) holds
b1 = b2
;
proof end;
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 & ( 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 () holds
( A is open iff ( A = {} or A  is finite ) )
proof end;

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

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 () holds U meets V
proof end;

definition
let X, x0 be set ;
func x0 -PointClTop X -> strict TopSpace means :Def7: :: TOPGEN_3:def 7
( the carrier of it = X & ( 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 & ( for A being Subset of b1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) holds
b1 = b2
;
proof end;
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 & ( 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 ;
cluster x0 -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}
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 & x <> x0 ) )
proof end;

definition
let X, X0 be set ;
func X0 -DiscreteTop X -> strict TopSpace means :Def8: :: TOPGEN_3:def 8
( the carrier of it = X & ( 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 & ( for A being Subset of b1 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) holds
b1 = b2
;
proof end;
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 & ( 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 ;
cluster X0 -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
proof end;

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 )
proof end;

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)
proof end;

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

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