:: TOPGEN_3 semantic presentation
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 ) );
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
let X be set ; ::_thesis: 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 ) )
let B be Subset-Family of X; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) ) implies B is covering )
assume B is covering ; ::_thesis: for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U )
then A1: union B = X by ABIAN:4;
let x be set ; ::_thesis: ( x in X implies ex U being Subset of X st
( U in B & x in U ) )
assume x in X ; ::_thesis: ex U being Subset of X st
( U in B & x in U )
then consider U being set such that
A2: x in U and
A3: U in B by A1, TARSKI:def_4;
reconsider U = U as Subset of X by A3;
take U = U; ::_thesis: ( U in B & x in U )
thus ( U in B & x in U ) by A2, A3; ::_thesis: verum
end;
assume A4: for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) ; ::_thesis: B is covering
union B = X
proof
thus union B c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= union B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in union B )
assume a in X ; ::_thesis: a in union B
then ex U being Subset of X st
( U in B & a in U ) by A4;
hence a in union B by TARSKI:def_4; ::_thesis: verum
end;
hence B is covering by ABIAN:4; ::_thesis: verum
end;
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
let X be set ; ::_thesis: 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 )
let B be Subset-Family of X; ::_thesis: ( B is point-filtered & B is covering implies 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 ) )
assume A1: ( B is point-filtered & B is covering ) ; ::_thesis: 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 )
let T be TopStruct ; ::_thesis: ( the carrier of T = X & the topology of T = UniCl B implies ( T is TopSpace & B is Basis of T ) )
assume that
A2: the carrier of T = X and
A3: the topology of T = UniCl B ; ::_thesis: ( T is TopSpace & B is Basis of T )
T is TopSpace-like
proof
union B in UniCl B by CANTOR_1:def_1;
hence the carrier of T in the topology of T by A1, A2, A3, ABIAN:4; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
hereby ::_thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T )
let a be Subset-Family of T; ::_thesis: ( a c= the topology of T implies union a in the topology of T )
assume a c= the topology of T ; ::_thesis: union a in the topology of T
then union a in UniCl the topology of T by CANTOR_1:def_1;
hence union a in the topology of T by A2, A3, YELLOW_9:15; ::_thesis: verum
end;
let a, b be Subset of T; ::_thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
set Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } ;
{ c where c is Subset of T : ( c in B & c c= a /\ b ) } c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } or x in bool X )
assume x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } ; ::_thesis: x in bool X
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in bool X ; ::_thesis: verum
end;
then reconsider Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } as Subset-Family of T by A2;
assume a in the topology of T ; ::_thesis: ( not b in the topology of T or a /\ b in the topology of T )
then consider Ba being Subset-Family of T such that
A4: Ba c= B and
A5: a = union Ba by A2, A3, CANTOR_1:def_1;
assume b in the topology of T ; ::_thesis: a /\ b in the topology of T
then consider Bb being Subset-Family of T such that
A6: Bb c= B and
A7: b = union Bb by A2, A3, CANTOR_1:def_1;
A8: union Bc = a /\ b
proof
Bc c= bool (a /\ b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Bc or x in bool (a /\ b) )
assume x in Bc ; ::_thesis: x in bool (a /\ b)
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in bool (a /\ b) ; ::_thesis: verum
end;
then union Bc c= union (bool (a /\ b)) by ZFMISC_1:77;
hence union Bc c= a /\ b by ZFMISC_1:81; :: according to XBOOLE_0:def_10 ::_thesis: a /\ b c= union Bc
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a /\ b or x in union Bc )
assume A9: x in a /\ b ; ::_thesis: x in union Bc
then x in a by XBOOLE_0:def_4;
then consider U1 being set such that
A10: x in U1 and
A11: U1 in Ba by A5, TARSKI:def_4;
x in b by A9, XBOOLE_0:def_4;
then consider U2 being set such that
A12: x in U2 and
A13: U2 in Bb by A7, TARSKI:def_4;
A14: U2 c= b by A7, A13, ZFMISC_1:74;
x in U1 /\ U2 by A10, A12, XBOOLE_0:def_4;
then consider U being Subset of X such that
A15: U in B and
A16: x in U and
A17: U c= U1 /\ U2 by A4, A11, A6, A13, A1, Def1;
U1 c= a by A5, A11, ZFMISC_1:74;
then U1 /\ U2 c= a /\ b by A14, XBOOLE_1:27;
then U c= a /\ b by A17, XBOOLE_1:1;
then U in Bc by A2, A15;
hence x in union Bc by A16, TARSKI:def_4; ::_thesis: verum
end;
Bc c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Bc or x in B )
assume x in Bc ; ::_thesis: x in B
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in B ; ::_thesis: verum
end;
hence a /\ b in the topology of T by A8, A2, A3, CANTOR_1:def_1; ::_thesis: verum
end;
hence T is TopSpace ; ::_thesis: B is Basis of T
reconsider B9 = B as Subset-Family of T by A2;
B9 c= the topology of T by A3, CANTOR_1:1;
hence B is Basis of T by A2, A3, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;
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
let X be set ; ::_thesis: 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 ) ) ) )
let B be non-empty ManySortedSet of X; ::_thesis: ( 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 ) ) implies 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 ) ) ) ) )
assume A1: rng B c= bool (bool X) ; ::_thesis: ( ex x, U being set st
( x in X & U in B . x & not x in U ) or ex x, y, U being set st
( x in U & U in B . y & y in X & ( for V being set holds
( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or 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 ) ) ) ) )
Union B c= union (bool (bool X)) by A1, ZFMISC_1:77;
then reconsider P = Union B as Subset-Family of X by ZFMISC_1:81;
A2: dom B = X by PARTFUN1:def_2;
assume A3: for x, U being set st x in X & U in B . x holds
x in U ; ::_thesis: ( ex x, y, U being set st
( x in U & U in B . y & y in X & ( for V being set holds
( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or 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 ) ) ) ) )
assume A4: 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 ) ; ::_thesis: ( ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or 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 ) ) ) ) )
assume A5: 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 ) ; ::_thesis: 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 ) ) ) )
A6: P is point-filtered
proof
let x, U1, U2 be set ; :: according to TOPGEN_3:def_1 ::_thesis: ( U1 in P & U2 in P & x in U1 /\ U2 implies ex U being Subset of X st
( U in P & x in U & U c= U1 /\ U2 ) )
assume that
A7: U1 in P and
A8: U2 in P and
A9: x in U1 /\ U2 ; ::_thesis: ex U being Subset of X st
( U in P & x in U & U c= U1 /\ U2 )
A10: x in U2 by A9, XBOOLE_0:def_4;
ex y2 being set st
( y2 in X & U2 in B . y2 ) by A2, A8, CARD_5:2;
then consider V2 being set such that
A11: V2 in B . x and
A12: V2 c= U2 by A10, A4;
A13: x in U1 by A9, XBOOLE_0:def_4;
ex y1 being set st
( y1 in X & U1 in B . y1 ) by A7, A2, CARD_5:2;
then consider V1 being set such that
A14: V1 in B . x and
A15: V1 c= U1 by A13, A4;
A16: x in X by A2, A14, FUNCT_1:def_2;
then consider U being set such that
A17: U in B . x and
A18: U c= V1 /\ V2 by A5, A14, A11;
U in P by A2, A16, A17, CARD_5:2;
then reconsider U = U as Subset of X ;
take U ; ::_thesis: ( U in P & x in U & U c= U1 /\ U2 )
thus U in P by A2, A16, A17, CARD_5:2; ::_thesis: ( x in U & U c= U1 /\ U2 )
thus x in U by A3, A16, A17; ::_thesis: U c= U1 /\ U2
V1 /\ V2 c= U1 /\ U2 by A15, A12, XBOOLE_1:27;
hence U c= U1 /\ U2 by A18, XBOOLE_1:1; ::_thesis: verum
end;
take P ; ::_thesis: ( 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 ) ) ) )
thus P = Union B ; ::_thesis: 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 ) )
let T be TopStruct ; ::_thesis: ( the carrier of T = X & the topology of T = UniCl P implies ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) )
assume that
A19: the carrier of T = X and
A20: the topology of T = UniCl P ; ::_thesis: ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) )
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
ex_U_being_Subset_of_X_st_
(_U_in_P_&_x_in_U_)
let x be set ; ::_thesis: ( x in X implies ex U being Subset of X st
( U in P & x in U ) )
set U = the Element of B . x;
assume A21: x in X ; ::_thesis: ex U being Subset of X st
( U in P & x in U )
then A22: the Element of B . x in P by A2, CARD_5:2;
x in the Element of B . x by A3, A21;
hence ex U being Subset of X st
( U in P & x in U ) by A22; ::_thesis: verum
end;
then P is covering by Th1;
hence T is TopSpace by A19, A20, A6, Th2; ::_thesis: for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9
let T9 be non empty TopSpace; ::_thesis: ( T9 = T implies B is Neighborhood_System of T9 )
assume A23: T9 = T ; ::_thesis: B is Neighborhood_System of T9
then reconsider B9 = B as ManySortedSet of T9 by A19;
B9 is Neighborhood_System of T9
proof
let x be Point of T9; :: according to TOPGEN_2:def_3 ::_thesis: B9 . x is Element of bool (bool the carrier of T9)
A24: B9 . x in rng B by A2, A19, A23, FUNCT_1:def_3;
then reconsider Bx = B9 . x as Subset-Family of T9 by A1, A19, A23;
Bx is Basis of x
proof
A25: P c= UniCl P by CANTOR_1:1;
Bx c= P by A24, ZFMISC_1:74;
then Bx c= the topology of T9 by A25, A20, A23, XBOOLE_1:1;
then A26: Bx is open by TOPS_2:64;
Bx is x -quasi_basis
proof
for a being set st a in Bx holds
x in a by A3, A19, A23;
hence x in Intersect Bx by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of T9 holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of T9 st
( b2 in Bx & b2 c= b1 ) )
let A be Subset of T9; ::_thesis: ( not A is open or not x in A or ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A ) )
assume A in the topology of T9 ; :: according to PRE_TOPC:def_2 ::_thesis: ( not x in A or ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A ) )
then consider Y being Subset-Family of T9 such that
A27: Y c= P and
A28: A = union Y by A19, A20, A23, CANTOR_1:def_1;
assume x in A ; ::_thesis: ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A )
then consider a being set such that
A29: x in a and
A30: a in Y by A28, TARSKI:def_4;
ex b being set st
( b in dom B & a in B . b ) by A27, A30, CARD_5:2;
then A31: ex V being set st
( V in B . x & V c= a ) by A4, A29;
a c= A by A28, A30, ZFMISC_1:74;
hence ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A ) by A31, XBOOLE_1:1; ::_thesis: verum
end;
hence Bx is Basis of x by A26; ::_thesis: verum
end;
hence B9 . x is Element of bool (bool the carrier of T9) ; ::_thesis: verum
end;
hence B is Neighborhood_System of T9 ; ::_thesis: verum
end;
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
let X be set ; ::_thesis: 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 ) ) )
let F be Subset-Family of X; ::_thesis: ( {} 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 ) implies 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 ) ) ) )
assume A1: {} in F ; ::_thesis: ( ex A, B being set st
( A in F & B in F & not A \/ B in F ) or ex G being Subset-Family of X st
( G c= F & not Intersect G in F ) or 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 ) ) ) )
set O = COMPLEMENT F;
assume A2: for A, B being set st A in F & B in F holds
A \/ B in F ; ::_thesis: ( ex G being Subset-Family of X st
( G c= F & not Intersect G in F ) or 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 ) ) ) )
assume A3: for G being Subset-Family of X st G c= F holds
Intersect G in F ; ::_thesis: 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 ) ) )
let T be TopStruct ; ::_thesis: ( the carrier of T = X & the topology of T = COMPLEMENT F implies ( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) ) )
assume that
A4: the carrier of T = X and
A5: the topology of T = COMPLEMENT F ; ::_thesis: ( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )
T is TopSpace-like
proof
({} T) ` in COMPLEMENT F by A1, A4, SETFAM_1:35;
hence the carrier of T in the topology of T by A5; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
hereby ::_thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T )
let a be Subset-Family of T; ::_thesis: ( a c= the topology of T implies union a in the topology of T )
assume a c= the topology of T ; ::_thesis: union a in the topology of T
then COMPLEMENT a c= F by A4, A5, SETFAM_1:37;
then Intersect (COMPLEMENT a) in F by A3, A4;
then (union a) ` in F by YELLOW_8:6;
hence union a in the topology of T by A4, A5, SETFAM_1:def_7; ::_thesis: verum
end;
let a, b be Subset of T; ::_thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
assume that
A6: a in the topology of T and
A7: b in the topology of T ; ::_thesis: a /\ b in the topology of T
A8: b ` in F by A7, A4, A5, SETFAM_1:def_7;
a ` in F by A6, A4, A5, SETFAM_1:def_7;
then (a `) \/ (b `) in F by A8, A2;
then (a /\ b) ` in F by XBOOLE_1:54;
hence a /\ b in the topology of T by A4, A5, SETFAM_1:def_7; ::_thesis: verum
end;
hence T is TopSpace ; ::_thesis: for A being Subset of T holds
( A is closed iff A in F )
let A be Subset of T; ::_thesis: ( A is closed iff A in F )
( A is closed iff A ` is open ) by TOPS_1:3;
then ( A is closed iff A ` in COMPLEMENT F ) by A5, PRE_TOPC:def_2;
hence ( A is closed iff A in F ) by A4, SETFAM_1:35; ::_thesis: verum
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
set X = F1();
set F = { A where A is Subset of F1() : P1[A] } ;
{ A where A is Subset of F1() : P1[A] } c= bool F1()
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { A where A is Subset of F1() : P1[A] } or a in bool F1() )
assume a in { A where A is Subset of F1() : P1[A] } ; ::_thesis: a in bool F1()
then ex B being Subset of F1() st
( a = B & P1[B] ) ;
hence a in bool F1() ; ::_thesis: verum
end;
then reconsider F = { A where A is Subset of F1() : P1[A] } as Subset-Family of F1() ;
set T = TopStruct(# F1(),(COMPLEMENT F) #);
A4: for A, B being set st A in F & B in F holds
A \/ B in F
proof
let A, B be set ; ::_thesis: ( A in F & B in F implies A \/ B in F )
assume A in F ; ::_thesis: ( not B in F or A \/ B in F )
then consider A9 being Subset of F1() such that
A5: A = A9 and
A6: P1[A9] ;
assume B in F ; ::_thesis: A \/ B in F
then consider B9 being Subset of F1() such that
A7: B = B9 and
A8: P1[B9] ;
P1[A9 \/ B9] by A2, A6, A8;
hence A \/ B in F by A5, A7; ::_thesis: verum
end;
A9: for G being Subset-Family of F1() st G c= F holds
Intersect G in F
proof
let G be Subset-Family of F1(); ::_thesis: ( G c= F implies Intersect G in F )
assume A10: G c= F ; ::_thesis: Intersect G in F
now__::_thesis:_for_A_being_set_st_A_in_G_holds_
P1[A]
let A be set ; ::_thesis: ( A in G implies P1[A] )
assume A in G ; ::_thesis: P1[A]
then A in F by A10;
then ex B being Subset of F1() st
( A = B & P1[B] ) ;
hence P1[A] ; ::_thesis: verum
end;
then P1[ Intersect G] by A3;
hence Intersect G in F ; ::_thesis: verum
end;
{} c= F1() by XBOOLE_1:2;
then A11: {} in F by A1;
then reconsider T = TopStruct(# F1(),(COMPLEMENT F) #) as strict TopSpace by A9, A4, Th4;
take T ; ::_thesis: ( the carrier of T = F1() & ( for A being Subset of T holds
( A is closed iff P1[A] ) ) )
thus the carrier of T = F1() ; ::_thesis: for A being Subset of T holds
( A is closed iff P1[A] )
let A be Subset of T; ::_thesis: ( A is closed iff P1[A] )
( A in F iff ex B being Subset of F1() st
( A = B & P1[B] ) ) ;
hence ( A is closed iff P1[A] ) by A11, A4, A9, Th4; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) implies ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 ) )
assume A1: for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ; ::_thesis: ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
the carrier of T2 = [#] T2 ;
then A2: the carrier of T2 is Subset of T1 by A1;
the carrier of T1 = [#] T1 ;
then A3: the carrier of T1 is Subset of T2 by A1;
hence the carrier of T1 = the carrier of T2 by A2, XBOOLE_0:def_10; ::_thesis: the topology of T1 c= the topology of T2
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of T1 or a in the topology of T2 )
assume A4: a in the topology of T1 ; ::_thesis: a in the topology of T2
then reconsider a = a as Subset of T1 ;
reconsider b = a as Subset of T2 by A3, A2, XBOOLE_0:def_10;
a is open by A4, PRE_TOPC:def_2;
then b is open by A1;
hence a in the topology of T2 by PRE_TOPC:def_2; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) implies TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) )
assume A1: for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ; ::_thesis: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
A2: the topology of T2 c= the topology of T1 by A1, Lm1;
the topology of T1 c= the topology of T2 by A1, Lm1;
then the topology of T1 = the topology of T2 by A2, XBOOLE_0:def_10;
hence TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) by A1, Lm1; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) implies ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 ) )
assume A1: for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ; ::_thesis: ( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
the carrier of T2 = [#] T2 ;
then A2: the carrier of T2 is Subset of T1 by A1;
the carrier of T1 = [#] T1 ;
then A3: the carrier of T1 is Subset of T2 by A1;
hence A4: the carrier of T1 = the carrier of T2 by A2, XBOOLE_0:def_10; ::_thesis: the topology of T1 c= the topology of T2
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of T1 or a in the topology of T2 )
assume A5: a in the topology of T1 ; ::_thesis: a in the topology of T2
then reconsider a = a as Subset of T1 ;
reconsider b = a as Subset of T2 by A3, A2, XBOOLE_0:def_10;
a is open by A5, PRE_TOPC:def_2;
then b ` is closed by A1, A4;
then b is open by TOPS_1:4;
hence a in the topology of T2 by PRE_TOPC:def_2; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) implies TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) )
assume A1: for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ; ::_thesis: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
A2: the topology of T2 c= the topology of T1 by A1, Lm2;
the topology of T1 c= the topology of T2 by A1, Lm2;
then the topology of T1 = the topology of T2 by A2, XBOOLE_0:def_10;
hence TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) by A1, Lm2; ::_thesis: verum
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;
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
let X be set ; ::_thesis: 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 ) )
let c be Function of (bool X),(bool X); ::_thesis: ( 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 ) implies 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 ) ) )
assume that
A1: c . {} = {} and
A2: for A being Subset of X holds A c= c . A and
A3: for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) and
A4: for A being Subset of X holds c . (c . A) = c . A ; ::_thesis: 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 ) )
set F = rng c;
A5: dom c = bool X by FUNCT_2:def_1;
A6: now__::_thesis:_for_A,_B_being_set_st_A_in_rng_c_&_B_in_rng_c_holds_
A_\/_B_in_rng_c
let A, B be set ; ::_thesis: ( A in rng c & B in rng c implies A \/ B in rng c )
assume that
A7: A in rng c and
A8: B in rng c ; ::_thesis: A \/ B in rng c
consider a being set such that
A9: a in dom c and
A10: A = c . a by A7, FUNCT_1:def_3;
consider b being set such that
A11: b in dom c and
A12: B = c . b by A8, FUNCT_1:def_3;
reconsider a = a, b = b as Subset of X by A9, A11;
A \/ B = (c . A) \/ B by A4, A9, A10
.= (c . A) \/ (c . B) by A4, A11, A12
.= c . ((c . a) \/ (c . b)) by A3, A10, A12 ;
hence A \/ B in rng c by A5, FUNCT_1:def_3; ::_thesis: verum
end;
A13: now__::_thesis:_for_A,_B_being_Subset_of_X_st_A_c=_B_holds_
c_._A_c=_c_._B
let A, B be Subset of X; ::_thesis: ( A c= B implies c . A c= c . B )
assume A c= B ; ::_thesis: c . A c= c . B
then A \/ B = B by XBOOLE_1:12;
then c . B = (c . A) \/ (c . B) by A3;
hence c . A c= c . B by XBOOLE_1:11; ::_thesis: verum
end;
A14: now__::_thesis:_for_G_being_Subset-Family_of_X_st_G_c=_rng_c_holds_
Intersect_G_in_rng_c
let G be Subset-Family of X; ::_thesis: ( G c= rng c implies Intersect G in rng c )
assume A15: G c= rng c ; ::_thesis: Intersect G in rng c
now__::_thesis:_for_a_being_set_st_a_in_G_holds_
c_._(Intersect_G)_c=_a
let a be set ; ::_thesis: ( a in G implies c . (Intersect G) c= a )
assume A16: a in G ; ::_thesis: c . (Intersect G) c= a
then reconsider A = a as Subset of X ;
A17: c . (Intersect G) c= c . A by A13, A16, MSSUBFAM:2;
ex b being set st
( b in dom c & A = c . b ) by A15, A16, FUNCT_1:def_3;
hence c . (Intersect G) c= a by A17, A4; ::_thesis: verum
end;
then A18: c . (Intersect G) c= Intersect G by MSSUBFAM:4;
Intersect G c= c . (Intersect G) by A2;
then c . (Intersect G) = Intersect G by A18, XBOOLE_0:def_10;
hence Intersect G in rng c by A5, FUNCT_1:def_3; ::_thesis: verum
end;
let T be TopStruct ; ::_thesis: ( the carrier of T = X & the topology of T = COMPLEMENT (rng c) implies ( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) ) )
assume that
A19: the carrier of T = X and
A20: the topology of T = COMPLEMENT (rng c) ; ::_thesis: ( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )
{} = {} X ;
then A21: {} in rng c by A1, A5, FUNCT_1:def_3;
hence A22: T is TopSpace by A14, A19, A20, A6, Th4; ::_thesis: for A being Subset of T holds Cl A = c . A
let A be Subset of T; ::_thesis: Cl A = c . A
reconsider B = A, ClA = Cl A as Subset of X by A19;
reconsider cB = c . B as Subset of T by A19;
cB in rng c by A5, FUNCT_1:def_3;
then cB is closed by A19, A20, A21, A6, A14, Th4;
hence Cl A c= c . A by A2, TOPS_1:5; :: according to XBOOLE_0:def_10 ::_thesis: c . A c= Cl A
ClA in rng c by A22, A19, A20, A21, A6, A14, Th4;
then ex a being set st
( a in dom c & ClA = c . a ) by FUNCT_1:def_3;
then c . ClA = ClA by A4;
hence c . A c= Cl A by A19, A13, PRE_TOPC:18; ::_thesis: verum
end;
scheme :: TOPGEN_3:sch 2
TopDefByClosureOp{ F1() -> set , F2( set ) -> 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
set X = F1();
consider c being Function such that
A5: ( dom c = bool F1() & ( for a being set st a in bool F1() holds
c . a = F2(a) ) ) from FUNCT_1:sch_3();
now__::_thesis:_for_a_being_set_st_a_in_bool_F1()_holds_
c_._a_in_bool_F1()
let a be set ; ::_thesis: ( a in bool F1() implies c . a in bool F1() )
assume A6: a in bool F1() ; ::_thesis: c . a in bool F1()
then A7: F2(a) c= F1() by A2;
c . a = F2(a) by A6, A5;
hence c . a in bool F1() by A7; ::_thesis: verum
end;
then reconsider c = c as Function of (bool F1()),(bool F1()) by A5, FUNCT_2:3;
A8: for A being Subset of F1() holds A c= c . A
proof
let A be Subset of F1(); ::_thesis: A c= c . A
c . A = F2(A) by A5;
hence A c= c . A by A2; ::_thesis: verum
end;
A9: for A, B being Subset of F1() holds c . (A \/ B) = (c . A) \/ (c . B)
proof
let A, B be Subset of F1(); ::_thesis: c . (A \/ B) = (c . A) \/ (c . B)
A10: c . B = F2(B) by A5;
A11: F2((A \/ B)) = c . (A \/ B) by A5;
c . A = F2(A) by A5;
hence c . (A \/ B) = (c . A) \/ (c . B) by A10, A11, A3; ::_thesis: verum
end;
A12: for A being Subset of F1() holds c . (c . A) = c . A
proof
let A be Subset of F1(); ::_thesis: c . (c . A) = c . A
A13: F2((c . A)) = c . (c . A) by A5;
c . A = F2(A) by A5;
hence c . (c . A) = c . A by A13, A4; ::_thesis: verum
end;
{} c= F1() by XBOOLE_1:2;
then A14: c . {} = {} by A1, A5;
then reconsider T = TopStruct(# F1(),(COMPLEMENT (rng c)) #) as strict TopSpace by A12, A8, A9, Th7;
take T ; ::_thesis: ( the carrier of T = F1() & ( for A being Subset of T holds Cl A = F2(A) ) )
thus the carrier of T = F1() ; ::_thesis: for A being Subset of T holds Cl A = F2(A)
let A be Subset of T; ::_thesis: Cl A = F2(A)
thus Cl A = c . A by A14, A8, A9, A12, Th7
.= F2(A) by A5 ; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( 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 ) implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2 ; ::_thesis: the topology of T1 = the topology of T2
now__::_thesis:_for_A_being_set_holds_
(_(_A_is_closed_Subset_of_T1_implies_A_is_closed_Subset_of_T2_)_&_(_A_is_closed_Subset_of_T2_implies_A_is_closed_Subset_of_T1_)_)
let A be set ; ::_thesis: ( ( A is closed Subset of T1 implies A is closed Subset of T2 ) & ( A is closed Subset of T2 implies A is closed Subset of T1 ) )
thus ( A is closed Subset of T1 implies A is closed Subset of T2 ) ::_thesis: ( A is closed Subset of T2 implies A is closed Subset of T1 )
proof
assume A is closed Subset of T1 ; ::_thesis: A is closed Subset of T2
then reconsider A1 = A as closed Subset of T1 ;
reconsider A2 = A1 as Subset of T2 by A1;
Cl A1 = A1 by PRE_TOPC:22;
then Cl A2 = A2 by A2;
hence A is closed Subset of T2 ; ::_thesis: verum
end;
assume A is closed Subset of T2 ; ::_thesis: A is closed Subset of T1
then reconsider A2 = A as closed Subset of T2 ;
reconsider A1 = A2 as Subset of T1 by A1;
Cl A2 = A2 by PRE_TOPC:22;
then Cl A1 = A1 by A2;
hence A is closed Subset of T1 ; ::_thesis: verum
end;
then TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) by Th6;
hence the topology of T1 = the topology of T2 ; ::_thesis: verum
end;
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
let X be set ; ::_thesis: 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 ) )
let c be Function of (bool X),(bool X); ::_thesis: ( c . X = X & ( for A being Subset of X holds c . A 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 ) implies for T being TopStruct st the carrier of T = X & the topology of T = rng c holds
( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) ) )
assume that
A1: c . X = X and
A2: for A being Subset of X holds c . A c= A and
A3: for A, B being Subset of X holds c . (A /\ B) = (c . A) /\ (c . B) and
A4: for A being Subset of X holds c . (c . A) = c . A ; ::_thesis: for T being TopStruct st the carrier of T = X & the topology of T = rng c holds
( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) )
set F = rng c;
let T be TopStruct ; ::_thesis: ( the carrier of T = X & the topology of T = rng c implies ( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) ) )
assume that
A5: the carrier of T = X and
A6: the topology of T = rng c ; ::_thesis: ( T is TopSpace & ( for A being Subset of T holds Int A = c . A ) )
A7: dom c = bool X by FUNCT_2:def_1;
A8: now__::_thesis:_for_A,_B_being_Subset_of_T_st_A_in_rng_c_&_B_in_rng_c_holds_
A_/\_B_in_rng_c
let A, B be Subset of T; ::_thesis: ( A in rng c & B in rng c implies A /\ B in rng c )
assume that
A9: A in rng c and
A10: B in rng c ; ::_thesis: A /\ B in rng c
consider a being set such that
A11: a in dom c and
A12: A = c . a by A9, FUNCT_1:def_3;
consider b being set such that
A13: b in dom c and
A14: B = c . b by A10, FUNCT_1:def_3;
reconsider a = a, b = b as Subset of X by A11, A13;
A /\ B = (c . A) /\ B by A4, A11, A12
.= (c . A) /\ (c . B) by A4, A13, A14
.= c . ((c . a) /\ (c . b)) by A3, A12, A14 ;
hence A /\ B in rng c by A7, FUNCT_1:def_3; ::_thesis: verum
end;
A15: now__::_thesis:_for_A,_B_being_Subset_of_X_st_A_c=_B_holds_
c_._A_c=_c_._B
let A, B be Subset of X; ::_thesis: ( A c= B implies c . A c= c . B )
assume A c= B ; ::_thesis: c . A c= c . B
then A /\ B = A by XBOOLE_1:28;
then c . A = (c . A) /\ (c . B) by A3;
hence c . A c= c . B by XBOOLE_1:17; ::_thesis: verum
end;
A16: now__::_thesis:_for_G_being_Subset-Family_of_X_st_G_c=_rng_c_holds_
union_G_in_rng_c
let G be Subset-Family of X; ::_thesis: ( G c= rng c implies union G in rng c )
assume A17: G c= rng c ; ::_thesis: union G in rng c
now__::_thesis:_for_a_being_set_st_a_in_G_holds_
a_c=_c_._(union_G)
let a be set ; ::_thesis: ( a in G implies a c= c . (union G) )
assume A18: a in G ; ::_thesis: a c= c . (union G)
then reconsider A = a as Subset of X ;
A19: c . A c= c . (union G) by A15, A18, ZFMISC_1:74;
ex b being set st
( b in dom c & A = c . b ) by A17, A18, FUNCT_1:def_3;
hence a c= c . (union G) by A19, A4; ::_thesis: verum
end;
then A20: union G c= c . (union G) by ZFMISC_1:76;
c . (union G) c= union G by A2;
then c . (union G) = union G by A20, XBOOLE_0:def_10;
hence union G in rng c by A7, FUNCT_1:def_3; ::_thesis: verum
end;
X = [#] X ;
then X in rng c by A1, A7, FUNCT_1:def_3;
hence A21: T is TopSpace by A16, A5, A6, A8, PRE_TOPC:def_1; ::_thesis: for A being Subset of T holds Int A = c . A
let A be Subset of T; ::_thesis: Int A = c . A
reconsider B = A, IntA = Int A as Subset of X by A5;
IntA in rng c by A21, A6, PRE_TOPC:def_2;
then ex a being set st
( a in dom c & IntA = c . a ) by FUNCT_1:def_3;
then c . IntA = IntA by A4;
hence Int A c= c . A by A5, A15, TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: c . A c= Int A
reconsider cB = c . B as Subset of T by A5;
cB in rng c by A7, FUNCT_1:def_3;
then cB is open by A6, PRE_TOPC:def_2;
hence c . A c= Int A by A2, TOPS_1:24; ::_thesis: verum
end;
scheme :: TOPGEN_3:sch 3
TopDefByInteriorOp{ F1() -> set , F2( set ) -> 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
set X = F1();
consider c being Function such that
A5: ( dom c = bool F1() & ( for a being set st a in bool F1() holds
c . a = F2(a) ) ) from FUNCT_1:sch_3();
now__::_thesis:_for_a_being_set_st_a_in_bool_F1()_holds_
c_._a_in_bool_F1()
let a be set ; ::_thesis: ( a in bool F1() implies c . a in bool F1() )
assume A6: a in bool F1() ; ::_thesis: c . a in bool F1()
then A7: F2(a) c= a by A2;
c . a = F2(a) by A6, A5;
then c . a c= F1() by A7, A6, XBOOLE_1:1;
hence c . a in bool F1() ; ::_thesis: verum
end;
then reconsider c = c as Function of (bool F1()),(bool F1()) by A5, FUNCT_2:3;
A8: for A being Subset of F1() holds c . A c= A
proof
let A be Subset of F1(); ::_thesis: c . A c= A
c . A = F2(A) by A5;
hence c . A c= A by A2; ::_thesis: verum
end;
A9: for A, B being Subset of F1() holds c . (A /\ B) = (c . A) /\ (c . B)
proof
let A, B be Subset of F1(); ::_thesis: c . (A /\ B) = (c . A) /\ (c . B)
A10: c . B = F2(B) by A5;
A11: F2((A /\ B)) = c . (A /\ B) by A5;
c . A = F2(A) by A5;
hence c . (A /\ B) = (c . A) /\ (c . B) by A10, A11, A3; ::_thesis: verum
end;
A12: for A being Subset of F1() holds c . (c . A) = c . A
proof
let A be Subset of F1(); ::_thesis: c . (c . A) = c . A
A13: F2((c . A)) = c . (c . A) by A5;
c . A = F2(A) by A5;
hence c . (c . A) = c . A by A13, A4; ::_thesis: verum
end;
F1() c= F1() ;
then A14: c . F1() = F1() by A1, A5;
then reconsider T = TopStruct(# F1(),(rng c) #) as strict TopSpace by A12, A8, A9, Th9;
take T ; ::_thesis: ( the carrier of T = F1() & ( for A being Subset of T holds Int A = F2(A) ) )
thus the carrier of T = F1() ; ::_thesis: for A being Subset of T holds Int A = F2(A)
let A be Subset of T; ::_thesis: Int A = F2(A)
thus Int A = c . A by A14, A8, A9, A12, Th9
.= F2(A) by A5 ; ::_thesis: verum
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
let T1, T2 be TopSpace; ::_thesis: ( 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 ) implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2 ; ::_thesis: the topology of T1 = the topology of T2
now__::_thesis:_for_A1_being_Subset_of_T1
for_A2_being_Subset_of_T2_st_A1_=_A2_holds_
Cl_A1_=_Cl_A2
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2
let A2 be Subset of T2; ::_thesis: ( A1 = A2 implies Cl A1 = Cl A2 )
assume A1 = A2 ; ::_thesis: Cl A1 = Cl A2
then Int (A1 `) = Int (A2 `) by A1, A2;
hence Cl A1 = (Int (A2 `)) ` by A1, TDLAT_3:1
.= Cl A2 by TDLAT_3:1 ;
::_thesis: verum
end;
hence the topology of T1 = the topology of T2 by A1, Th8; ::_thesis: verum
end;
begin
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 Element of 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 Element of 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 Element of 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 Element of REAL : ( x < q & q is rational ) } ) )
proof
set B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ;
{ [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } c= bool REAL
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } or a in bool REAL )
assume a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ; ::_thesis: a in bool REAL
then ex x, q being Element of REAL st
( a = [.x,q.[ & x < q & q is rational ) ;
hence a in bool REAL ; ::_thesis: verum
end;
then reconsider B = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } as Subset-Family of REAL ;
A1: B is point-filtered
proof
let x, U1, U2 be set ; :: according to TOPGEN_3:def_1 ::_thesis: ( U1 in B & U2 in B & x in U1 /\ U2 implies ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 ) )
assume that
A2: U1 in B and
A3: U2 in B and
A4: x in U1 /\ U2 ; ::_thesis: ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 )
consider x1, q1 being Element of REAL such that
A5: U1 = [.x1,q1.[ and
A6: x1 < q1 and
A7: q1 is rational by A2;
consider x2, q2 being Element of REAL such that
A8: U2 = [.x2,q2.[ and
A9: x2 < q2 and
A10: q2 is rational by A3;
set y = max (x1,x2);
set q = min (q1,q2);
A11: min (q1,q2) is rational by A7, A10, XXREAL_0:15;
A12: x in U1 by A4, XBOOLE_0:def_4;
then reconsider x9 = x as Element of REAL by A5;
A13: x in U2 by A4, XBOOLE_0:def_4;
then A14: x2 <= x9 by A8, XXREAL_1:3;
A15: x9 < q2 by A8, A13, XXREAL_1:3;
A16: min (q1,q2) <= q2 by XXREAL_0:17;
x2 <= max (x1,x2) by XXREAL_0:31;
then A17: [.(max (x1,x2)),(min (q1,q2)).[ c= U2 by A16, A8, XXREAL_1:38;
A18: min (q1,q2) <= q1 by XXREAL_0:17;
x1 <= max (x1,x2) by XXREAL_0:31;
then A19: [.(max (x1,x2)),(min (q1,q2)).[ c= U1 by A18, A5, XXREAL_1:38;
A20: x1 <= x9 by A5, A12, XXREAL_1:3;
then x1 < q2 by A15, XXREAL_0:2;
then A21: max (x1,x2) < q2 by A9, XXREAL_0:29;
A22: x9 < q1 by A5, A12, XXREAL_1:3;
then A23: x9 < min (q1,q2) by A15, XXREAL_0:15;
x2 < q1 by A14, A22, XXREAL_0:2;
then max (x1,x2) < q1 by A6, XXREAL_0:29;
then max (x1,x2) < min (q1,q2) by A21, XXREAL_0:15;
then A24: [.(max (x1,x2)),(min (q1,q2)).[ in B by A11;
max (x1,x2) <= x9 by A20, A14, XXREAL_0:28;
then x9 in [.(max (x1,x2)),(min (q1,q2)).[ by A23, XXREAL_1:3;
hence ex U being Subset of REAL st
( U in B & x in U & U c= U1 /\ U2 ) by A24, A19, A17, XBOOLE_1:19; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_REAL_holds_
ex_U_being_Element_of_bool_REAL_st_
(_U_in_B_&_x_in_U_)
let x be set ; ::_thesis: ( x in REAL implies ex U being Element of bool REAL st
( U in B & x in U ) )
assume x in REAL ; ::_thesis: ex U being Element of bool REAL st
( U in B & x in U )
then reconsider x9 = x as Element of REAL ;
x9 + 0 < x9 + 1 by XREAL_1:6;
then consider q being rational number such that
A25: x9 < q and
q < x9 + 1 by RAT_1:7;
take U = [.x9,q.[; ::_thesis: ( U in B & x in U )
q in REAL by XREAL_0:def_1;
hence U in B by A25; ::_thesis: x in U
thus x in U by A25, XXREAL_1:3; ::_thesis: verum
end;
then B is covering by Th1;
then TopStruct(# REAL,(UniCl B) #) is non empty TopSpace by A1, Th2;
hence 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 Element of REAL : ( x < q & q is rational ) } ) ) ; ::_thesis: verum
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 Element of REAL : ( x < q & 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 & 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
proof
let x, y be real number ; ::_thesis: [.x,y.[ is open Subset of Sorgenfrey-line
reconsider V = [.x,y.[ as Subset of Sorgenfrey-line by Def2;
now__::_thesis:_for_p_being_Point_of_Sorgenfrey-line_st_p_in_[.x,y.[_holds_
ex_U_being_Subset_of_Sorgenfrey-line_st_
(_U_in_BB_&_p_in_U_&_U_c=_V_)
let p be Point of Sorgenfrey-line; ::_thesis: ( p in [.x,y.[ implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )
reconsider a = p as Element of REAL by Def2;
A1: x is Element of REAL by XREAL_0:def_1;
assume A2: p in [.x,y.[ ; ::_thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then A3: x <= a by XXREAL_1:3;
a < y by A2, XXREAL_1:3;
then consider q being rational number such that
A4: a < q and
A5: q < y by RAT_1:7;
reconsider U = [.x,q.[ as Subset of Sorgenfrey-line by Def2;
take U = U; ::_thesis: ( U in BB & p in U & U c= V )
A6: q is Element of REAL by XREAL_0:def_1;
x < q by A3, A4, XXREAL_0:2;
hence U in BB by A1, A6, Lm5; ::_thesis: ( p in U & U c= V )
thus p in U by A3, A4, XXREAL_1:3; ::_thesis: U c= V
thus U c= V by A5, XXREAL_1:38; ::_thesis: verum
end;
hence [.x,y.[ is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; ::_thesis: verum
end;
theorem :: TOPGEN_3:12
for x, y being real number holds ].x,y.[ is open Subset of Sorgenfrey-line
proof
let x, y be real number ; ::_thesis: ].x,y.[ is open Subset of Sorgenfrey-line
reconsider V = ].x,y.[ as Subset of Sorgenfrey-line by Def2;
now__::_thesis:_for_p_being_Point_of_Sorgenfrey-line_st_p_in_V_holds_
ex_U_being_Subset_of_Sorgenfrey-line_st_
(_U_in_BB_&_p_in_U_&_U_c=_V_)
let p be Point of Sorgenfrey-line; ::_thesis: ( p in V implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )
reconsider a = p as Element of REAL by Def2;
assume A1: p in V ; ::_thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then a < y by XXREAL_1:4;
then consider q being rational number such that
A2: a < q and
A3: q < y by RAT_1:7;
reconsider U = [.a,q.[ as Subset of Sorgenfrey-line by Def2;
take U = U; ::_thesis: ( U in BB & p in U & U c= V )
q is Element of REAL by XREAL_0:def_1;
hence U in BB by A2, Lm5; ::_thesis: ( p in U & U c= V )
thus p in U by A2, XXREAL_1:3; ::_thesis: U c= V
x < a by A1, XXREAL_1:4;
hence U c= V by A3, XXREAL_1:48; ::_thesis: verum
end;
hence ].x,y.[ is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; ::_thesis: verum
end;
theorem :: TOPGEN_3:13
for x being real number holds left_open_halfline x is open Subset of Sorgenfrey-line
proof
let x be real number ; ::_thesis: left_open_halfline x is open Subset of Sorgenfrey-line
reconsider V = left_open_halfline x as Subset of Sorgenfrey-line by Def2;
now__::_thesis:_for_p_being_Point_of_Sorgenfrey-line_st_p_in_V_holds_
ex_U_being_Subset_of_Sorgenfrey-line_st_
(_U_in_BB_&_p_in_U_&_U_c=_V_)
let p be Point of Sorgenfrey-line; ::_thesis: ( p in V implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )
reconsider a = p as Element of REAL by Def2;
assume A1: p in V ; ::_thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then A2: {a} c= V by ZFMISC_1:31;
a < x by A1, XXREAL_1:233;
then consider q being rational number such that
A3: a < q and
A4: q < x by RAT_1:7;
reconsider U = [.a,q.[ as Subset of Sorgenfrey-line by Def2;
take U = U; ::_thesis: ( U in BB & p in U & U c= V )
q is Element of REAL by XREAL_0:def_1;
hence U in BB by A3, Lm5; ::_thesis: ( p in U & U c= V )
thus p in U by A3, XXREAL_1:3; ::_thesis: U c= V
A5: ].a,q.[ c= V by A4, XXREAL_1:263;
U = {a} \/ ].a,q.[ by A3, XXREAL_1:131;
hence U c= V by A2, A5, XBOOLE_1:8; ::_thesis: verum
end;
hence left_open_halfline x is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; ::_thesis: verum
end;
theorem :: TOPGEN_3:14
for x being real number holds right_open_halfline x is open Subset of Sorgenfrey-line
proof
let x be real number ; ::_thesis: right_open_halfline x is open Subset of Sorgenfrey-line
reconsider V = right_open_halfline x as Subset of Sorgenfrey-line by Def2;
now__::_thesis:_for_p_being_Point_of_Sorgenfrey-line_st_p_in_V_holds_
ex_U_being_Subset_of_Sorgenfrey-line_st_
(_U_in_BB_&_p_in_U_&_U_c=_V_)
let p be Point of Sorgenfrey-line; ::_thesis: ( p in V implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )
reconsider a = p as Element of REAL by Def2;
assume A1: p in V ; ::_thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then A2: {a} c= V by ZFMISC_1:31;
a + 0 < a + 1 by XREAL_1:6;
then consider q being rational number such that
A3: a < q and
q < a + 1 by RAT_1:7;
reconsider U = [.a,q.[ as Subset of Sorgenfrey-line by Def2;
take U = U; ::_thesis: ( U in BB & p in U & U c= V )
q is Element of REAL by XREAL_0:def_1;
hence U in BB by A3, Lm5; ::_thesis: ( p in U & U c= V )
thus p in U by A3, XXREAL_1:3; ::_thesis: U c= V
a > x by A1, XXREAL_1:235;
then A4: ].a,q.[ c= V by XXREAL_1:247;
U = {a} \/ ].a,q.[ by A3, XXREAL_1:131;
hence U c= V by A2, A4, XBOOLE_1:8; ::_thesis: verum
end;
hence right_open_halfline x is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; ::_thesis: verum
end;
theorem :: TOPGEN_3:15
for x being real number holds right_closed_halfline x is open Subset of Sorgenfrey-line
proof
let x be real number ; ::_thesis: right_closed_halfline x is open Subset of Sorgenfrey-line
reconsider V = right_closed_halfline x as Subset of Sorgenfrey-line by Def2;
now__::_thesis:_for_p_being_Point_of_Sorgenfrey-line_st_p_in_V_holds_
ex_U_being_Subset_of_Sorgenfrey-line_st_
(_U_in_BB_&_p_in_U_&_U_c=_V_)
let p be Point of Sorgenfrey-line; ::_thesis: ( p in V implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )
reconsider a = p as Element of REAL by Def2;
a + 0 < a + 1 by XREAL_1:6;
then consider q being rational number such that
A1: a < q and
q < a + 1 by RAT_1:7;
a in [.a,q.] by A1, XXREAL_1:1;
then A2: {a} c= [.a,q.] by ZFMISC_1:31;
reconsider U = [.a,q.[ as Subset of Sorgenfrey-line by Def2;
assume p in V ; ::_thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then a >= x by XXREAL_1:236;
then A3: [.a,q.] c= V by XXREAL_1:251;
take U = U; ::_thesis: ( U in BB & p in U & U c= V )
q is Element of REAL by XREAL_0:def_1;
hence U in BB by A1, Lm5; ::_thesis: ( p in U & U c= V )
thus p in U by A1, XXREAL_1:3; ::_thesis: U c= V
A4: ].a,q.[ c= [.a,q.] by XXREAL_1:37;
U = {a} \/ ].a,q.[ by A1, XXREAL_1:131;
then U c= [.a,q.] by A2, A4, XBOOLE_1:8;
hence U c= V by A3, XBOOLE_1:1; ::_thesis: verum
end;
hence right_closed_halfline x is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; ::_thesis: verum
end;
theorem Th16: :: TOPGEN_3:16
card INT = omega
proof
A1: card INT c= card (NAT \/ [:{0},NAT:]) by CARD_1:11, NUMBERS:def_4;
A2: card [:NAT,{0}:] = card [:{0},NAT:] by CARD_2:4;
A3: card [:NAT,{0}:] = card NAT by CARD_1:69;
omega +` omega = omega by CARD_2:75;
then card (NAT \/ [:{0},NAT:]) c= omega by A3, A2, CARD_1:47, CARD_2:34;
hence card INT c= omega by A1, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: omega c= card INT
thus omega c= card INT by CARD_1:11, CARD_1:47, NUMBERS:17; ::_thesis: verum
end;
theorem Th17: :: TOPGEN_3:17
card RAT = omega
proof
defpred S1[ set , set ] means ex i being integer number ex n being Nat st
( $1 = [i,n] & $2 = i / n );
A1: for a being set st a in [:INT,NAT:] holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in [:INT,NAT:] implies ex b being set st S1[a,b] )
assume a in [:INT,NAT:] ; ::_thesis: ex b being set st S1[a,b]
then consider x, y being set such that
A2: x in INT and
A3: y in NAT and
A4: a = [x,y] by ZFMISC_1:def_2;
reconsider y = y as Nat by A3;
reconsider x = x as integer number by A2;
x / y = x / y ;
hence ex b being set st S1[a,b] by A4; ::_thesis: verum
end;
consider f being Function such that
A5: ( dom f = [:INT,NAT:] & ( for a being set st a in [:INT,NAT:] holds
S1[a,f . a] ) ) from CLASSES1:sch_1(A1);
A6: RAT c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in RAT or a in rng f )
assume a in RAT ; ::_thesis: a in rng f
then consider i, j being Integer such that
A7: a = i / j by RAT_1:def_1;
consider n being Element of NAT such that
A8: ( j = n or j = - n ) by INT_1:2;
i / (- n) = - (i / n) by XCMPLX_1:188;
then ( a = i / n or a = (- i) / n ) by A7, A8, XCMPLX_1:187;
then consider k being Integer such that
A9: a = k / n ;
k in INT by INT_1:def_2;
then A10: [k,n] in [:INT,NAT:] by ZFMISC_1:def_2;
then consider i1 being integer number , n1 being Nat such that
A11: [k,n] = [i1,n1] and
A12: f . [k,n] = i1 / n1 by A5;
A13: n = n1 by A11, XTUPLE_0:1;
i1 = k by A11, XTUPLE_0:1;
hence a in rng f by A13, A5, A9, A10, A12, FUNCT_1:def_3; ::_thesis: verum
end;
card [:INT,NAT:] = card [:omega,omega:] by Th16, CARD_2:7
.= omega by CARD_2:def_2, CARD_4:6 ;
hence card RAT c= omega by A5, A6, CARD_1:12; :: according to XBOOLE_0:def_10 ::_thesis: omega c= card RAT
thus omega c= card RAT by CARD_1:11, CARD_1:47, NUMBERS:18; ::_thesis: verum
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 number st
( x < y & ].x,y.[ c= a ) ) holds
A is countable
proof
defpred S1[ set , set ] means $2 in $1;
let A be set ; ::_thesis: ( A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being real number st
( x < y & ].x,y.[ c= a ) ) implies A is countable )
assume A1: for a, b being set st a in A & b in A & a <> b holds
a misses b ; :: according to TAXONOM2:def_5 ::_thesis: ( ex a being set st
( a in A & ( for x, y being real number holds
( not x < y or not ].x,y.[ c= a ) ) ) or A is countable )
assume A2: for a being set st a in A holds
ex x, y being real number st
( x < y & ].x,y.[ c= a ) ; ::_thesis: A is countable
A3: now__::_thesis:_for_a_being_set_st_a_in_A_holds_
ex_q_being_set_st_
(_q_in_RAT_&_S1[a,q]_)
let a be set ; ::_thesis: ( a in A implies ex q being set st
( q in RAT & S1[a,q] ) )
assume a in A ; ::_thesis: ex q being set st
( q in RAT & S1[a,q] )
then consider x, y being real number such that
A4: x < y and
A5: ].x,y.[ c= a by A2;
consider q being rational number such that
A6: x < q and
A7: q < y by A4, RAT_1:7;
A8: q in RAT by RAT_1:def_2;
q in ].x,y.[ by A6, A7, XXREAL_1:4;
hence ex q being set st
( q in RAT & S1[a,q] ) by A5, A8; ::_thesis: verum
end;
consider f being Function such that
A9: ( dom f = A & rng f c= RAT ) and
A10: for a being set st a in A holds
S1[a,f . a] from FUNCT_1:sch_5(A3);
f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom f or not b1 in dom f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A11: a in dom f and
A12: b in dom f and
A13: f . a = f . b and
A14: a <> b ; ::_thesis: contradiction
A15: f . a in b by A12, A13, A9, A10;
A16: f . a in a by A11, A9, A10;
a misses b by A11, A12, A14, A1, A9;
hence contradiction by A16, A15, XBOOLE_0:3; ::_thesis: verum
end;
then card A c= card RAT by A9, CARD_1:10;
hence A is countable by Th17, CARD_3:def_14; ::_thesis: verum
end;
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 & ex y being real number st
( y < x & ].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 & ex y being real number 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
let U be Subset of REAL; ::_thesis: { x where x is Element of REAL : x is_local_minimum_of U } is countable
set X = { x where x is Element of REAL : x is_local_minimum_of U } ;
defpred S1[ set , set ] means ex x, y being real number st
( $1 = x & $2 = ].y,x.[ & y < x & ].y,x.[ misses U );
A1: now__::_thesis:_for_a_being_set_st_a_in__{__x_where_x_is_Element_of_REAL_:_x_is_local_minimum_of_U__}__holds_
ex_b_being_set_st_
(_b_in_bool_REAL_&_S1[a,b]_)
let a be set ; ::_thesis: ( a in { x where x is Element of REAL : x is_local_minimum_of U } implies ex b being set st
( b in bool REAL & S1[a,b] ) )
assume a in { x where x is Element of REAL : x is_local_minimum_of U } ; ::_thesis: ex b being set st
( b in bool REAL & S1[a,b] )
then consider x being Element of REAL such that
A2: a = x and
A3: x is_local_minimum_of U ;
ex y being real number st
( y < x & ].y,x.[ misses U ) by A3, Def3;
hence ex b being set st
( b in bool REAL & S1[a,b] ) by A2; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = { x where x is Element of REAL : x is_local_minimum_of U } & rng f c= bool REAL ) and
A5: for a being set st a in { x where x is Element of REAL : x is_local_minimum_of U } holds
S1[a,f . a] from FUNCT_1:sch_5(A1);
f is one-to-one
proof
let a9, b9 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a9 in dom f or not b9 in dom f or not f . a9 = f . b9 or a9 = b9 )
set a = f . a9;
set b = f . b9;
assume that
A6: a9 in dom f and
A7: b9 in dom f ; ::_thesis: ( not f . a9 = f . b9 or a9 = b9 )
consider xb, yb being real number such that
A8: b9 = xb and
A9: f . b9 = ].yb,xb.[ and
yb < xb and
A10: ].yb,xb.[ misses U by A4, A5, A7;
ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) by A4, A7, A8;
then A11: xb in U by Def3;
assume that
A12: f . a9 = f . b9 and
A13: a9 <> b9 ; ::_thesis: contradiction
consider xa, ya being real number such that
A14: a9 = xa and
A15: f . a9 = ].ya,xa.[ and
A16: ya < xa and
A17: ].ya,xa.[ misses U by A4, A5, A6;
consider c being rational number such that
A18: ya < c and
A19: c < xa by A16, RAT_1:7;
A20: c in f . a9 by A15, A18, A19, XXREAL_1:4;
then A21: c < xb by A9, A12, XXREAL_1:4;
ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) by A4, A6, A14;
then A22: xa in U by Def3;
yb < c by A9, A12, A20, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A19, A18, A21, A14, A8, A13, XXREAL_0:1, XXREAL_0:2;
then ( xa in f . b9 or xb in f . a9 ) by A15, A9, XXREAL_1:4;
hence contradiction by A15, A17, A9, A10, A11, A22, XBOOLE_0:3; ::_thesis: verum
end;
then A23: card { x where x is Element of REAL : x is_local_minimum_of U } c= card (rng f) by A4, CARD_1:10;
A24: rng f is mutually-disjoint
proof
let a be set ; :: according to TAXONOM2:def_5 ::_thesis: for b1 being set holds
( not a in rng f or not b1 in rng f or a = b1 or a misses b1 )
let b be set ; ::_thesis: ( not a in rng f or not b in rng f or a = b or a misses b )
assume a in rng f ; ::_thesis: ( not b in rng f or a = b or a misses b )
then consider a9 being set such that
A25: a9 in dom f and
A26: a = f . a9 by FUNCT_1:def_3;
consider xa, ya being real number such that
A27: a9 = xa and
A28: a = ].ya,xa.[ and
ya < xa and
A29: ].ya,xa.[ misses U by A4, A5, A25, A26;
ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) by A4, A25, A27;
then A30: xa in U by Def3;
assume b in rng f ; ::_thesis: ( a = b or a misses b )
then consider b9 being set such that
A31: b9 in dom f and
A32: b = f . b9 by FUNCT_1:def_3;
consider xb, yb being real number such that
A33: b9 = xb and
A34: b = ].yb,xb.[ and
yb < xb and
A35: ].yb,xb.[ misses U by A4, A5, A31, A32;
assume that
A36: a <> b and
A37: a meets b ; ::_thesis: contradiction
consider c being set such that
A38: c in a and
A39: c in b by A37, XBOOLE_0:3;
reconsider c = c as Element of REAL by A28, A38;
A40: c < xa by A28, A38, XXREAL_1:4;
ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) by A4, A31, A33;
then A41: xb in U by Def3;
A42: c < xb by A34, A39, XXREAL_1:4;
A43: ya < c by A28, A38, XXREAL_1:4;
yb < c by A34, A39, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A40, A43, A42, A26, A32, A27, A33, A36, XXREAL_0:1, XXREAL_0:2;
then ( xa in b or xb in a ) by A28, A34, XXREAL_1:4;
hence contradiction by A28, A29, A34, A35, A41, A30, XBOOLE_0:3; ::_thesis: verum
end;
now__::_thesis:_for_a_being_set_st_a_in_rng_f_holds_
ex_y,_x_being_real_number_st_
(_y_<_x_&_].y,x.[_c=_a_)
let a be set ; ::_thesis: ( a in rng f implies ex y, x being real number st
( y < x & ].y,x.[ c= a ) )
assume a in rng f ; ::_thesis: ex y, x being real number st
( y < x & ].y,x.[ c= a )
then consider b being set such that
A44: b in dom f and
A45: a = f . b by FUNCT_1:def_3;
consider x, y being real number such that
b = x and
A46: a = ].y,x.[ and
A47: y < x and
].y,x.[ misses U by A4, A5, A44, A45;
take y = y; ::_thesis: ex x being real number st
( y < x & ].y,x.[ c= a )
take x = x; ::_thesis: ( y < x & ].y,x.[ c= a )
thus ( y < x & ].y,x.[ c= a ) by A46, A47; ::_thesis: verum
end;
then rng f is countable by A24, Th18;
then card (rng f) c= omega by CARD_3:def_14;
hence card { x where x is Element of REAL : x is_local_minimum_of U } c= omega by A23, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;
registration
let M be Aleph;
cluster exp (2,M) -> infinite ;
coherence
not exp (2,M) is finite
proof
card M = M by CARD_1:def_2;
then exp (2,M) = card (bool M) by CARD_2:31;
hence not exp (2,M) is finite ; ::_thesis: verum
end;
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 & q is rational ) } = continuum
proof
defpred S1[ set , set ] means ex x, q being Element of REAL st
( $1 = x & $2 = [.x,q.[ & x < q & q is rational );
deffunc H1( Element of [:REAL,RAT:]) -> Element of bool REAL = [.($1 `1),($1 `2).[;
set X = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ;
consider f being Function such that
A1: dom f = [:REAL,RAT:] and
A2: for z being Element of [:REAL,RAT:] holds f . z = H1(z) from FUNCT_1:sch_4();
A3: { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } or a in rng f )
assume a in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } ; ::_thesis: a in rng f
then consider x, q being Element of REAL such that
A4: a = [.x,q.[ and
x < q and
A5: q is rational ;
q in RAT by A5, RAT_1:def_2;
then reconsider b = [x,q] as Element of [:REAL,RAT:] by ZFMISC_1:def_2;
A6: b `2 = q by MCART_1:7;
b `1 = x by MCART_1:7;
then f . b = [.x,q.[ by A6, A2;
hence a in rng f by A1, A4, FUNCT_1:def_3; ::_thesis: verum
end;
0 in omega ;
then A7: omega c= continuum by CARD_1:11, CARD_1:47;
card [:REAL,RAT:] = card [:(card REAL),(card RAT):] by CARD_2:7
.= continuum *` omega by Th17, CARD_2:def_2
.= continuum by A7, CARD_4:16 ;
hence card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } c= continuum by A1, A3, CARD_1:12; :: according to XBOOLE_0:def_10 ::_thesis: continuum c= card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) }
A8: for a being set st a in REAL holds
ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S1[a,b] )
proof
let a be set ; ::_thesis: ( a in REAL implies ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S1[a,b] ) )
assume a in REAL ; ::_thesis: ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S1[a,b] )
then reconsider x = a as Element of REAL ;
x + 0 < x + 1 by XREAL_1:6;
then consider q being rational number such that
A9: x < q and
q < x + 1 by RAT_1:7;
q in RAT by RAT_1:def_2;
then reconsider q = q as Element of REAL by NUMBERS:12;
[.x,q.[ in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by A9;
hence ex b being set st
( b in { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & S1[a,b] ) by A9; ::_thesis: verum
end;
consider f being Function such that
A10: ( dom f = REAL & rng f c= { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } & ( for a being set st a in REAL holds
S1[a,f . a] ) ) from FUNCT_1:sch_5(A8);
f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom f or not b1 in dom f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume a in dom f ; ::_thesis: ( not b in dom f or not f . a = f . b or a = b )
then consider x, q being Element of REAL such that
A11: a = x and
A12: f . a = [.x,q.[ and
A13: x < q and
q is rational by A10;
assume b in dom f ; ::_thesis: ( not f . a = f . b or a = b )
then consider y, r being Element of REAL such that
A14: b = y and
A15: f . b = [.y,r.[ and
A16: y < r and
r is rational by A10;
assume A17: f . a = f . b ; ::_thesis: a = b
then y in [.x,q.[ by A12, A15, A16, XXREAL_1:3;
then A18: x <= y by XXREAL_1:3;
x in [.y,r.[ by A17, A12, A13, A15, XXREAL_1:3;
then y <= x by XXREAL_1:3;
hence a = b by A18, A11, A14, XXREAL_0:1; ::_thesis: verum
end;
hence continuum c= card { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) } by A10, CARD_1:10; ::_thesis: verum
end;
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 & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );
existence
ex b1 being Function of NAT,REAL st
for i being Nat holds
( ( i in X & b1 . i = r |^ i ) or ( not i in X & b1 . i = 0 ) )
proof
deffunc H1( set ) -> Element of NAT = 0 ;
deffunc H2( set ) -> set = r |^ (In ($1,NAT));
defpred S1[ set ] means $1 in X;
A1: for a being set st a in NAT holds
( ( S1[a] implies H2(a) in REAL ) & ( not S1[a] implies H1(a) in REAL ) ) by XREAL_0:def_1;
consider f being Function of NAT,REAL such that
A2: for a being set st a in NAT holds
( ( S1[a] implies f . a = H2(a) ) & ( not S1[a] implies f . a = H1(a) ) ) from FUNCT_2:sch_5(A1);
take f ; ::_thesis: for i being Nat holds
( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )
let i be Nat; ::_thesis: ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) )
i in NAT by ORDINAL1:def_12;
then In (i,NAT) = i by FUNCT_7:def_1;
hence ( ( i in X & f . i = r |^ i ) or ( not i in X & f . i = 0 ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of NAT,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
let f1, f2 be Function of NAT,REAL; ::_thesis: ( ( for i being Nat holds
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) ) & ( for i being Nat holds
( ( i in X & f2 . i = r |^ i ) or ( not i in X & f2 . i = 0 ) ) ) implies f1 = f2 )
assume that
A3: for i being Nat holds
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) and
A4: for i being Nat holds
( ( i in X & f2 . i = r |^ i ) or ( not i in X & f2 . i = 0 ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_i_being_Element_of_NAT_holds_f1_._i_=_f2_._i
let i be Element of NAT ; ::_thesis: f1 . i = f2 . i
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) by A3;
hence f1 . i = f2 . i by A4; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
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 & 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 number st 0 < r & r < 1 holds
X -powers r is summable
proof
let X be set ; ::_thesis: for r being real number st 0 < r & r < 1 holds
X -powers r is summable
let r be real number ; ::_thesis: ( 0 < r & r < 1 implies X -powers r is summable )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: X -powers r is summable
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(X_-powers_r)_._n
let n be Element of NAT ; ::_thesis: 0 <= (X -powers r) . n
( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;
hence 0 <= (X -powers r) . n by A1, PREPOWER:6; ::_thesis: verum
end;
A4: now__::_thesis:_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
(X_-powers_r)_._n_<=_(r_GeoSeq)_._n
take m = 1; ::_thesis: for n being Element of NAT st m <= n holds
(X -powers r) . n <= (r GeoSeq) . n
let n be Element of NAT ; ::_thesis: ( m <= n implies (X -powers r) . n <= (r GeoSeq) . n )
assume m <= n ; ::_thesis: (X -powers r) . n <= (r GeoSeq) . n
A5: (r GeoSeq) . n = r |^ n by PREPOWER:def_1;
( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;
hence (X -powers r) . n <= (r GeoSeq) . n by A1, A5, PREPOWER:6; ::_thesis: verum
end;
abs r = r by A1, ABSVALUE:def_1;
then r GeoSeq is summable by A2, SERIES_1:24;
hence X -powers r is summable by A4, A3, SERIES_1:19; ::_thesis: verum
end;
theorem Th22: :: TOPGEN_3:22
for r being real number
for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
proof
let r be real number ; ::_thesis: for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
let n be Element of NAT ; ::_thesis: ( 0 < r & r < 1 implies Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r) )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
A3: abs r = r by A1, ABSVALUE:def_1;
then A4: r GeoSeq is summable by A2, SERIES_1:24;
A5: dom ((r |^ n) (#) (r GeoSeq)) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_i_being_Element_of_NAT_holds_((r_GeoSeq)_^\_n)_._i_=_((r_|^_n)_(#)_(r_GeoSeq))_._i
let i be Element of NAT ; ::_thesis: ((r GeoSeq) ^\ n) . i = ((r |^ n) (#) (r GeoSeq)) . i
thus ((r GeoSeq) ^\ n) . i = (r GeoSeq) . (i + n) by NAT_1:def_3
.= r |^ (i + n) by PREPOWER:def_1
.= (r |^ n) * (r |^ i) by NEWTON:8
.= (r |^ n) * ((r GeoSeq) . i) by PREPOWER:def_1
.= ((r |^ n) (#) (r GeoSeq)) . i by A5, VALUED_1:def_5 ; ::_thesis: verum
end;
then A6: (r GeoSeq) ^\ n = (r |^ n) (#) (r GeoSeq) by FUNCT_2:63;
Sum (r GeoSeq) = 1 / (1 - r) by A3, A2, SERIES_1:24;
hence Sum ((r GeoSeq) ^\ n) = (r |^ n) * (1 / (1 - r)) by A4, A6, SERIES_1:10
.= ((r |^ n) * 1) / (1 - r) by XCMPLX_1:74
.= (r |^ n) / (1 - r) ;
::_thesis: verum
end;
theorem Th23: :: TOPGEN_3:23
for n being Element of NAT holds Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n
proof
let n be Element of NAT ; ::_thesis: Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n
set r = 1 / 2;
thus Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = ((1 / 2) |^ (n + 1)) / (1 - (1 / 2)) by Th22
.= (((1 / 2) |^ n) * (1 / 2)) / (1 / 2) by NEWTON:6
.= (1 / 2) |^ n ; ::_thesis: verum
end;
theorem :: TOPGEN_3:24
for r being real number
for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq)
proof
let r be real number ; ::_thesis: for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq)
let X be set ; ::_thesis: ( 0 < r & r < 1 implies Sum (X -powers r) <= Sum (r GeoSeq) )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: Sum (X -powers r) <= Sum (r GeoSeq)
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_0_<=_(X_-powers_r)_._n_&_(X_-powers_r)_._n_<=_(r_GeoSeq)_._n_)
let n be Element of NAT ; ::_thesis: ( 0 <= (X -powers r) . n & (X -powers r) . n <= (r GeoSeq) . n )
A4: ( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;
hence 0 <= (X -powers r) . n by A1, PREPOWER:6; ::_thesis: (X -powers r) . n <= (r GeoSeq) . n
(r GeoSeq) . n = r |^ n by PREPOWER:def_1;
hence (X -powers r) . n <= (r GeoSeq) . n by A1, A4, PREPOWER:6; ::_thesis: verum
end;
abs r = r by A1, ABSVALUE:def_1;
then r GeoSeq is summable by A2, SERIES_1:24;
hence Sum (X -powers r) <= Sum (r GeoSeq) by A3, SERIES_1:20; ::_thesis: verum
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
let X be set ; ::_thesis: for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
let n be Element of NAT ; ::_thesis: Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n
set r = 1 / 2;
abs (1 / 2) = 1 / 2 by ABSVALUE:def_1;
then A1: ((1 / 2) GeoSeq) ^\ (n + 1) is summable by SERIES_1:12, SERIES_1:24;
A2: now__::_thesis:_for_m_being_Element_of_NAT_holds_
(_0_<=_((X_-powers_(1_/_2))_^\_(n_+_1))_._m_&_((X_-powers_(1_/_2))_^\_(n_+_1))_._m_<=_(((1_/_2)_GeoSeq)_^\_(n_+_1))_._m_)
let m be Element of NAT ; ::_thesis: ( 0 <= ((X -powers (1 / 2)) ^\ (n + 1)) . m & ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m )
A3: ((X -powers (1 / 2)) ^\ (n + 1)) . m = (X -powers (1 / 2)) . (m + (n + 1)) by NAT_1:def_3;
A4: ( ( m + (n + 1) in X & (X -powers (1 / 2)) . (m + (n + 1)) = (1 / 2) |^ (m + (n + 1)) ) or ( not m + (n + 1) in X & (X -powers (1 / 2)) . (m + (n + 1)) = 0 ) ) by Def5;
hence 0 <= ((X -powers (1 / 2)) ^\ (n + 1)) . m by A3, PREPOWER:6; ::_thesis: ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m
A5: ((1 / 2) GeoSeq) . (m + (n + 1)) = (1 / 2) |^ (m + (n + 1)) by PREPOWER:def_1;
(((1 / 2) GeoSeq) ^\ (n + 1)) . m = ((1 / 2) GeoSeq) . (m + (n + 1)) by NAT_1:def_3;
hence ((X -powers (1 / 2)) ^\ (n + 1)) . m <= (((1 / 2) GeoSeq) ^\ (n + 1)) . m by A5, A3, A4, PREPOWER:6; ::_thesis: verum
end;
Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n by Th23;
hence Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n by A1, A2, SERIES_1:20; ::_thesis: verum
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
set r = 1 / 2;
let X be infinite Subset of NAT; ::_thesis: for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
let i be Nat; ::_thesis: (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
defpred S1[ Element of NAT ] means (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + $1);
not X c= i + 1 ;
then consider a being set such that
A1: a in X and
A2: not a in i + 1 by TARSKI:def_3;
reconsider a = a, j = i as Element of NAT by A1, ORDINAL1:def_12;
A3: (X -powers (1 / 2)) . a = (1 / 2) |^ a by A1, Def5;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(X_-powers_(1_/_2))_._n
let n be Element of NAT ; ::_thesis: 0 <= (X -powers (1 / 2)) . n
( ( n in X & (X -powers (1 / 2)) . n = (1 / 2) |^ n ) or ( not n in X & (X -powers (1 / 2)) . n = 0 ) ) by Def5;
hence 0 <= (X -powers (1 / 2)) . n by PREPOWER:6; ::_thesis: verum
end;
A5: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; ::_thesis: S1[k + 1]
i + (k + 1) = (i + k) + 1 ;
then A7: (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((X -powers (1 / 2)) . (j + (k + 1))) by SERIES_1:def_1;
(X -powers (1 / 2)) . (j + (k + 1)) >= 0 by A4;
then ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + 0 <= (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) by A7, XREAL_1:6;
hence S1[k + 1] by A6, XXREAL_0:2; ::_thesis: verum
end;
j + 1 c= a by A2, ORDINAL1:16;
then j + 1 <= a by NAT_1:39;
then consider k being Nat such that
A8: a = (j + 1) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(1 / 2) |^ a > 0 by PREPOWER:6;
then A9: ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) > ((Partial_Sums (X -powers (1 / 2))) . i) + 0 by XREAL_1:6;
A10: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A5);
then A11: (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + k) ;
j + (k + 1) = (j + k) + 1 ;
then (Partial_Sums (X -powers (1 / 2))) . a = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((1 / 2) |^ a) by A3, A8, SERIES_1:def_1;
then ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) <= (Partial_Sums (X -powers (1 / 2))) . a by A11, XREAL_1:6;
then A12: (Partial_Sums (X -powers (1 / 2))) . i < (Partial_Sums (X -powers (1 / 2))) . a by A9, XXREAL_0:2;
(Partial_Sums (X -powers (1 / 2))) . a <= Sum (X -powers (1 / 2)) by Th21, A4, IRRAT_1:29;
hence (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2)) by A12, XXREAL_0:2; ::_thesis: verum
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
set r = 1 / 2;
let X, Y be infinite Subset of NAT; ::_thesis: ( Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) implies X = Y )
assume that
A1: Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) and
A2: X <> Y ; ::_thesis: contradiction
defpred S1[ Nat] means ( ( $1 in X & not $1 in Y ) or ( $1 in Y & not $1 in X ) );
not for a being set holds
( a in X iff a in Y ) by A2, TARSKI:1;
then A3: ex i being Nat st S1[i] ;
consider i being Nat such that
A4: ( S1[i] & ( for n being Nat st S1[n] holds
i <= n ) ) from NAT_1:sch_5(A3);
reconsider i = i as Element of NAT by ORDINAL1:def_12;
consider A, B being infinite Subset of NAT such that
A5: ( ( A = X & B = Y ) or ( A = Y & B = X ) ) and
A6: i in A and
A7: not i in B by A4;
A8: (A -powers (1 / 2)) . i = (1 / 2) |^ i by A6, Def5;
defpred S2[ Element of NAT ] means ( $1 < i implies (Partial_Sums (A -powers (1 / 2))) . $1 = (Partial_Sums (B -powers (1 / 2))) . $1 );
A9: now__::_thesis:_for_j_being_Element_of_NAT_st_S2[j]_holds_
S2[j_+_1]
let j be Element of NAT ; ::_thesis: ( S2[j] implies S2[j + 1] )
assume A10: S2[j] ; ::_thesis: S2[j + 1]
thus S2[j + 1] ::_thesis: verum
proof
A11: ( ( j + 1 in B & (B -powers (1 / 2)) . (j + 1) = (1 / 2) |^ (j + 1) ) or ( not j + 1 in B & (B -powers (1 / 2)) . (j + 1) = 0 ) ) by Def5;
A12: ( ( j + 1 in A & (A -powers (1 / 2)) . (j + 1) = (1 / 2) |^ (j + 1) ) or ( not j + 1 in A & (A -powers (1 / 2)) . (j + 1) = 0 ) ) by Def5;
assume A13: j + 1 < i ; ::_thesis: (Partial_Sums (A -powers (1 / 2))) . (j + 1) = (Partial_Sums (B -powers (1 / 2))) . (j + 1)
hence (Partial_Sums (A -powers (1 / 2))) . (j + 1) = ((Partial_Sums (B -powers (1 / 2))) . j) + ((A -powers (1 / 2)) . (j + 1)) by A10, NAT_1:13, SERIES_1:def_1
.= (Partial_Sums (B -powers (1 / 2))) . (j + 1) by A12, A11, A13, A4, A5, SERIES_1:def_1 ;
::_thesis: verum
end;
end;
(Partial_Sums (A -powers (1 / 2))) . 0 = (A -powers (1 / 2)) . 0 by SERIES_1:def_1;
then A14: ( ( 0 in A & (Partial_Sums (A -powers (1 / 2))) . 0 = (1 / 2) |^ 0 ) or ( not 0 in A & (Partial_Sums (A -powers (1 / 2))) . 0 = 0 ) ) by Def5;
A15: (B -powers (1 / 2)) . i = 0 by A7, Def5;
A16: (Partial_Sums (B -powers (1 / 2))) . 0 = (B -powers (1 / 2)) . 0 by SERIES_1:def_1;
then ( ( 0 in B & (Partial_Sums (B -powers (1 / 2))) . 0 = (1 / 2) |^ 0 ) or ( not 0 in B & (Partial_Sums (B -powers (1 / 2))) . 0 = 0 ) ) by Def5;
then A17: S2[ 0 ] by A14, A4, A5;
A18: for j being Element of NAT holds S2[j] from NAT_1:sch_1(A17, A9);
A19: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
proof
percases ( i = 0 or ex j being Nat st i = j + 1 ) by NAT_1:6;
suppose i = 0 ; ::_thesis: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
hence (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i) by A8, A15, A16, SERIES_1:def_1; ::_thesis: verum
end;
suppose ex j being Nat st i = j + 1 ; ::_thesis: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
then consider j being Nat such that
A20: i = j + 1 ;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
j < i by A20, NAT_1:13;
then (Partial_Sums (A -powers (1 / 2))) . j = (Partial_Sums (B -powers (1 / 2))) . j by A18;
hence (Partial_Sums (A -powers (1 / 2))) . i = (((Partial_Sums (B -powers (1 / 2))) . j) + 0) + ((1 / 2) |^ i) by A8, A20, SERIES_1:def_1
.= ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i) by A15, A20, SERIES_1:def_1 ;
::_thesis: verum
end;
end;
end;
A21: (Partial_Sums (A -powers (1 / 2))) . i < Sum (A -powers (1 / 2)) by Th26;
A22: Sum ((B -powers (1 / 2)) ^\ (i + 1)) <= (1 / 2) |^ i by Th25;
Sum (B -powers (1 / 2)) = ((Partial_Sums (B -powers (1 / 2))) . i) + (Sum ((B -powers (1 / 2)) ^\ (i + 1))) by Th21, SERIES_1:15;
hence contradiction by A19, A1, A5, A21, A22, XREAL_1:6; ::_thesis: verum
end;
theorem Th28: :: TOPGEN_3:28
for X being set st X is countable holds
Fin X is countable
proof
let X be set ; ::_thesis: ( X is countable implies Fin X is countable )
defpred S1[ set , set ] means ex p being FinSequence st
( $2 = p & $1 = rng p );
A1: ( ( X = {} & {{}} is countable ) or X <> {} ) by CARD_4:1;
A2: for a being set st a in Fin X holds
ex b being set st
( b in X * & S1[a,b] )
proof
let a be set ; ::_thesis: ( a in Fin X implies ex b being set st
( b in X * & S1[a,b] ) )
assume A3: a in Fin X ; ::_thesis: ex b being set st
( b in X * & S1[a,b] )
then a is finite by FINSUB_1:def_5;
then consider p being FinSequence such that
A4: a = rng p by FINSEQ_1:52;
a c= X by A3, FINSUB_1:def_5;
then p is FinSequence of X by A4, FINSEQ_1:def_4;
then p in X * by FINSEQ_1:def_11;
hence ex b being set st
( b in X * & S1[a,b] ) by A4; ::_thesis: verum
end;
consider f being Function such that
A5: ( dom f = Fin X & rng f c= X * ) and
A6: for a being set st a in Fin X holds
S1[a,f . a] from FUNCT_1:sch_5(A2);
f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom f or not b1 in dom f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A7: a in dom f and
A8: b in dom f ; ::_thesis: ( not f . a = f . b or a = b )
A9: S1[b,f . b] by A8, A5, A6;
S1[a,f . a] by A7, A5, A6;
hence ( not f . a = f . b or a = b ) by A9; ::_thesis: verum
end;
then A10: card (Fin X) c= card (X *) by A5, CARD_1:10;
assume X is countable ; ::_thesis: Fin X is countable
then X * is countable by A1, CARD_4:13, FUNCT_7:17;
then card (X *) c= omega by CARD_3:def_14;
hence card (Fin X) c= omega by A10, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;
theorem Th29: :: TOPGEN_3:29
continuum = exp (2,omega)
proof
not [0,0] in RAT+ by ARYTM_3:33;
then A1: RAT = RAT+ \/ ([:{0},RAT+:] \ {[0,0]}) by NUMBERS:def_3, XBOOLE_1:87, ZFMISC_1:50;
then bool RAT+ c= bool RAT by XBOOLE_1:7, ZFMISC_1:67;
then A2: DEDEKIND_CUTS c= bool RAT by XBOOLE_1:1;
RAT+ c= RAT by A1, XBOOLE_1:7;
then RAT+ \/ DEDEKIND_CUTS c= RAT \/ (bool RAT) by A2, XBOOLE_1:13;
then REAL+ c= RAT \/ (bool RAT) by ARYTM_2:def_2, XBOOLE_1:1;
then A3: card REAL+ c= card (RAT \/ (bool RAT)) by CARD_1:11;
set INFNAT = (bool NAT) \ (Fin NAT);
A4: card RAT in card (bool RAT) by CARD_1:14;
card (RAT \/ (bool RAT)) c= (card RAT) +` (card (bool RAT)) by CARD_2:34;
then card REAL+ c= (card RAT) +` (card (bool RAT)) by A3, XBOOLE_1:1;
then card REAL+ c= card (bool RAT) by A4, CARD_2:76;
then card REAL+ c= exp (2,omega) by Th17, CARD_2:31;
then (card REAL+) +` (card REAL+) c= (exp (2,omega)) +` (exp (2,omega)) by CARD_2:83;
then A5: (card REAL+) +` (card REAL+) c= exp (2,omega) by CARD_2:76;
deffunc H1( set ) -> Element of REAL = Sum ($1 -powers (1 / 2));
A6: card [:{0},REAL+:] = card [:REAL+,{0}:] by CARD_2:4
.= card REAL+ by CARD_1:69 ;
A7: continuum c= card (REAL+ \/ [:{0},REAL+:]) by CARD_1:11, NUMBERS:def_1;
card (REAL+ \/ [:{0},REAL+:]) c= (card REAL+) +` (card [:{0},REAL+:]) by CARD_2:34;
then continuum c= (card REAL+) +` (card REAL+) by A7, A6, XBOOLE_1:1;
hence continuum c= exp (2,omega) by A5, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: exp (2,omega) c= continuum
Fin NAT is countable by Th28, CARD_4:2;
then A8: card (Fin NAT) c= omega by CARD_3:def_14;
then card (Fin NAT) in card (bool NAT) by CARD_1:14, CARD_1:47, ORDINAL1:12;
then A9: (card (bool NAT)) +` (card (Fin NAT)) = card (bool NAT) by CARD_2:76;
A10: omega in card (bool NAT) by CARD_1:14, CARD_1:47;
then reconsider INFNAT = (bool NAT) \ (Fin NAT) as non empty set by A8, CARD_1:68, ORDINAL1:12;
consider f being Function of INFNAT,REAL such that
A11: for X being Element of INFNAT holds f . X = H1(X) from FUNCT_2:sch_4();
A12: f is one-to-one
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom f or not b1 in dom f or not f . a = f . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume that
A13: a in dom f and
A14: b in dom f ; ::_thesis: ( not f . a = f . b or a = b )
A15: f . b = H1(b) by A11, A14;
not b in Fin NAT by A14, XBOOLE_0:def_5;
then A16: b is infinite Subset of NAT by A14, FINSUB_1:def_5, XBOOLE_0:def_5;
not a in Fin NAT by A13, XBOOLE_0:def_5;
then A17: a is infinite Subset of NAT by A13, FINSUB_1:def_5, XBOOLE_0:def_5;
f . a = H1(a) by A11, A13;
hence ( not f . a = f . b or a = b ) by A17, A16, A15, Th27; ::_thesis: verum
end;
A18: rng f c= REAL by RELAT_1:def_19;
dom f = INFNAT by FUNCT_2:def_1;
then card INFNAT c= continuum by A12, A18, CARD_1:10;
then card (bool NAT) c= continuum by A9, A8, A10, CARD_2:98, ORDINAL1:12;
hence exp (2,omega) c= continuum by CARD_1:47, CARD_2:31; ::_thesis: verum
end;
theorem Th30: :: TOPGEN_3:30
omega in continuum
proof
A1: omega = card omega by CARD_1:def_2;
card omega in card (bool omega) by CARD_1:14;
hence omega in continuum by A1, Th29, CARD_2:31; ::_thesis: verum
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
deffunc H1( set ) -> set = { x where x is Element of REAL : x is_local_minimum_of $1 } ;
let A be Subset-Family of REAL; ::_thesis: ( card A in continuum implies 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 )
assume A1: card A in continuum ; ::_thesis: 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
A2: now__::_thesis:_(card_A)_*`_omega_in_continuum
percases ( card A is empty or ( not card A is empty & card A is finite ) or card A is infinite ) ;
suppose card A is empty ; ::_thesis: (card A) *` omega in continuum
then (card A) *` omega = 0 by CARD_2:20;
hence (card A) *` omega in continuum by ORDINAL3:8; ::_thesis: verum
end;
supposeA3: ( not card A is empty & card A is finite ) ; ::_thesis: (card A) *` omega in continuum
then A4: card (card A) in omega by CARD_3:84;
0 in card A by A3, ORDINAL3:8;
hence (card A) *` omega in continuum by A4, Th30, CARD_4:16; ::_thesis: verum
end;
supposeA5: card A is infinite ; ::_thesis: (card A) *` omega in continuum
then omega c= card A by CARD_5:16;
hence (card A) *` omega in continuum by A1, A5, CARD_4:16; ::_thesis: verum
end;
end;
end;
set Y = { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ;
set X = { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ;
A6: for a being set st a in A holds
H1(a) in bool REAL
proof
let a be set ; ::_thesis: ( a in A implies H1(a) in bool REAL )
H1(a) c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in H1(a) or b in REAL )
assume b in H1(a) ; ::_thesis: b in REAL
then ex x being Element of REAL st
( b = x & x is_local_minimum_of a ) ;
hence b in REAL ; ::_thesis: verum
end;
hence ( a in A implies H1(a) in bool REAL ) ; ::_thesis: verum
end;
consider f being Function of A,(bool REAL) such that
A7: for a being set st a in A holds
f . a = H1(a) from FUNCT_2:sch_2(A6);
A8: { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } or a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } )
assume a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ; ::_thesis: a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }
then consider x being Element of REAL such that
A9: a = x and
A10: ex U being set st
( U in UniCl A & x is_local_minimum_of U ) ;
consider U being set such that
A11: U in UniCl A and
A12: x is_local_minimum_of U by A10;
reconsider U = U as Subset of REAL by A11;
consider B being Subset-Family of REAL such that
A13: B c= A and
A14: U = union B by A11, CANTOR_1:def_1;
x in U by A12, Def3;
then consider C being set such that
A15: x in C and
A16: C in B by A14, TARSKI:def_4;
consider y being real number such that
A17: y < x and
A18: ].y,x.[ misses U by A12, Def3;
reconsider C = C as Subset of REAL by A16;
].y,x.[ misses C
proof
assume not ].y,x.[ misses C ; ::_thesis: contradiction
then consider b being set such that
A19: b in ].y,x.[ and
A20: b in C by XBOOLE_0:3;
b in U by A14, A16, A20, TARSKI:def_4;
hence contradiction by A18, A19, XBOOLE_0:3; ::_thesis: verum
end;
then x is_local_minimum_of C by A17, A15, Def3;
hence a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } by A13, A16, A9; ::_thesis: verum
end;
{ x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } c= Union f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } or a in Union f )
A21: dom f = A by FUNCT_2:def_1;
assume a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ; ::_thesis: a in Union f
then consider x being Element of REAL such that
A22: a = x and
A23: ex U being set st
( U in A & x is_local_minimum_of U ) ;
consider U being set such that
A24: U in A and
A25: x is_local_minimum_of U by A23;
A26: f . U = H1(U) by A7, A24;
a in H1(U) by A22, A25;
hence a in Union f by A26, A21, A24, CARD_5:2; ::_thesis: verum
end;
then { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= Union f by A8, XBOOLE_1:1;
then A27: card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= card (Union f) by CARD_1:11;
A28: for a being set st a in A holds
card (f . a) c= omega
proof
let a be set ; ::_thesis: ( a in A implies card (f . a) c= omega )
assume A29: a in A ; ::_thesis: card (f . a) c= omega
then reconsider b = a as Subset of REAL ;
f . a = H1(b) by A7, A29;
then f . a is countable by Th19;
hence card (f . a) c= omega by CARD_3:def_14; ::_thesis: verum
end;
dom f = A by FUNCT_2:def_1;
then card (Union f) c= (card A) *` omega by A28, CARD_2:86;
hence 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 by A27, A2, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum
end;
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 & not [.x,q.[ in UniCl X )
proof
let X be Subset-Family of REAL; ::_thesis: ( card X in continuum implies ex x being real number ex q being rational number st
( x < q & not [.x,q.[ in UniCl X ) )
assume A1: card X in continuum ; ::_thesis: ex x being real number ex q being rational number st
( x < q & not [.x,q.[ in UniCl X )
set Z = { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } ;
set z = the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } ;
card { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } in continuum by A1, Th31;
then A2: REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } <> {} by CARD_1:68;
then A3: not the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } in { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } by XBOOLE_0:def_5;
reconsider z = the Element of REAL \ { x where x is Element of REAL : ex U being set st
( U in UniCl X & x is_local_minimum_of U ) } as Element of REAL by A2, XBOOLE_0:def_5;
z + 0 < z + 1 by XREAL_1:6;
then consider q being rational number such that
A4: z < q and
q < z + 1 by RAT_1:7;
take z ; ::_thesis: ex q being rational number st
( z < q & not [.z,q.[ in UniCl X )
take q ; ::_thesis: ( z < q & not [.z,q.[ in UniCl X )
thus z < q by A4; ::_thesis: not [.z,q.[ in UniCl X
z is_local_minimum_of [.z,q.[
proof
thus z in [.z,q.[ by A4, XXREAL_1:3; :: according to TOPGEN_3:def_3 ::_thesis: ex y being real number st
( y < z & ].y,z.[ misses [.z,q.[ )
take y = z - 1; ::_thesis: ( y < z & ].y,z.[ misses [.z,q.[ )
z - 0 = z ;
hence y < z by XREAL_1:15; ::_thesis: ].y,z.[ misses [.z,q.[
assume ].y,z.[ meets [.z,q.[ ; ::_thesis: contradiction
then consider a being set such that
A5: a in ].y,z.[ and
A6: a in [.z,q.[ by XBOOLE_0:3;
reconsider a = a as Element of REAL by A5;
a < z by A5, XXREAL_1:4;
hence contradiction by A6, XXREAL_1:3; ::_thesis: verum
end;
hence not [.z,q.[ in UniCl X by A3; ::_thesis: verum
end;
theorem :: TOPGEN_3:33
weight Sorgenfrey-line = continuum
proof
thus weight Sorgenfrey-line c= continuum by Lm5, Lm6, Th20, WAYBEL23:73; :: according to XBOOLE_0:def_10 ::_thesis: continuum c= weight Sorgenfrey-line
consider B being Basis of Sorgenfrey-line such that
A1: weight Sorgenfrey-line = card B by WAYBEL23:74;
assume not continuum c= weight Sorgenfrey-line ; ::_thesis: contradiction
then A2: weight Sorgenfrey-line in continuum by CARD_1:4;
the carrier of Sorgenfrey-line = REAL by Def2;
then consider x being real number , q being rational number such that
x < q and
A3: not [.x,q.[ in UniCl B by A2, A1, Th32;
[.x,q.[ is open Subset of Sorgenfrey-line by Th11;
then [.x,q.[ in the topology of Sorgenfrey-line by PRE_TOPC:def_2;
hence contradiction by A3, YELLOW_9:22; ::_thesis: verum
end;
begin
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
defpred S1[ set ] means ( ( $1 c= X & $1 is finite ) or $1 = X );
A1: X c= X ;
A2: for A, B being set st S1[A] & S1[B] holds
S1[A \/ B]
proof
let A, B be set ; ::_thesis: ( S1[A] & S1[B] implies S1[A \/ B] )
assume that
A3: S1[A] and
A4: S1[B] ; ::_thesis: S1[A \/ B]
reconsider A = A, B = B as Subset of X by A3, A4, A1;
A \/ B c= X ;
hence S1[A \/ B] by A3, A4, XBOOLE_1:12; ::_thesis: verum
end;
A5: for G being Subset-Family of X st ( for A being set st A in G holds
S1[A] ) holds
S1[ Intersect G]
proof
let G be Subset-Family of X; ::_thesis: ( ( for A being set st A in G holds
S1[A] ) implies S1[ Intersect G] )
assume A6: for A being set st A in G holds
S1[A] ; ::_thesis: S1[ Intersect G]
now__::_thesis:_(_G_<>_{}_&_G_<>_{X}_implies_(_Intersect_G_is_finite_&_Intersect_G_c=_X_)_)
assume that
A7: G <> {} and
A8: G <> {X} ; ::_thesis: ( Intersect G is finite & Intersect G c= X )
not G c= {X} by A7, A8, ZFMISC_1:33;
then consider a being set such that
A9: a in G and
A10: not a in {X} by TARSKI:def_3;
A11: a <> X by A10, TARSKI:def_1;
S1[a] by A6, A9;
hence ( Intersect G is finite & Intersect G c= X ) by A11, A9, FINSET_1:1, MSSUBFAM:2; ::_thesis: verum
end;
hence S1[ Intersect G] by A1, MSSUBFAM:9, SETFAM_1:def_9; ::_thesis: verum
end;
A12: ( S1[ {} ] & S1[X] ) by XBOOLE_1:2;
consider T being strict TopSpace such that
A13: ( the carrier of T = X & ( for A being Subset of T holds
( A is closed iff S1[A] ) ) ) from TOPGEN_3:sch_1(A12, A2, A5);
take T ; ::_thesis: ( the carrier of T = X & ( for F being Subset of T holds
( F is closed iff ( F is finite or F = X ) ) ) )
thus the carrier of T = X by A13; ::_thesis: for F being Subset of T holds
( F is closed iff ( F is finite or F = X ) )
let F be Subset of T; ::_thesis: ( F is closed iff ( F is finite or F = X ) )
thus ( F is closed iff ( F is finite or F = X ) ) by A13; ::_thesis: verum
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
let T1, T2 be strict TopSpace; ::_thesis: ( the carrier of T1 = X & ( for F being Subset of T1 holds
( F is closed iff ( F is finite or F = X ) ) ) & the carrier of T2 = X & ( for F being Subset of T2 holds
( F is closed iff ( F is finite or F = X ) ) ) implies T1 = T2 )
assume that
A14: the carrier of T1 = X and
A15: for F being Subset of T1 holds
( F is closed iff ( F is finite or F = X ) ) and
A16: the carrier of T2 = X and
A17: for F being Subset of T2 holds
( F is closed iff ( F is finite or F = X ) ) ; ::_thesis: T1 = T2
now__::_thesis:_for_F_being_set_holds_
(_F_is_closed_Subset_of_T1_iff_F_is_closed_Subset_of_T2_)
let F be set ; ::_thesis: ( F is closed Subset of T1 iff F is closed Subset of T2 )
( F is closed Subset of T1 iff ( F c= X & ( F is finite or F = X ) ) ) by A14, A15;
hence ( F is closed Subset of T1 iff F is closed Subset of T2 ) by A16, A17; ::_thesis: verum
end;
hence T1 = T2 by Th6; ::_thesis: verum
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 (ClFinTop X) holds
( A is open iff ( A = {} or A ` is finite ) )
proof
let X be set ; ::_thesis: for A being Subset of (ClFinTop X) holds
( A is open iff ( A = {} or A ` is finite ) )
let A be Subset of (ClFinTop X); ::_thesis: ( A is open iff ( A = {} or A ` is finite ) )
A1: the carrier of (ClFinTop X) = X by Def6;
hereby ::_thesis: ( ( A = {} or A ` is finite ) implies A is open )
assume that
A2: A is open and
A3: A <> {} ; ::_thesis: A ` is finite
(A `) ` = A ;
then A ` <> [#] the carrier of (ClFinTop X) by A3, XBOOLE_1:37;
hence A ` is finite by A2, A1, Def6; ::_thesis: verum
end;
assume ( A = {} or A ` is finite ) ; ::_thesis: A is open
then A ` is closed by Def6;
hence A is open by TOPS_1:4; ::_thesis: verum
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
let X be infinite set ; ::_thesis: for A being Subset of X st A is finite holds
A ` is infinite
let A be Subset of X; ::_thesis: ( A is finite implies A ` is infinite )
A \/ (A `) = [#] X by SUBSET_1:10
.= X ;
hence ( A is finite implies A ` is infinite ) ; ::_thesis: verum
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 (ClFinTop X) holds U meets V
proof
let X be infinite set ; ::_thesis: for U, V being non empty open Subset of (ClFinTop X) holds U meets V
let U, V be non empty open Subset of (ClFinTop X); ::_thesis: U meets V
assume U misses V ; ::_thesis: contradiction
then A1: U c= V ` by SUBSET_1:23;
A2: the carrier of (ClFinTop X) = X by Def6;
V ` is finite by Th34;
then U ` is infinite by A1, A2, Th35;
then U ` = [#] the carrier of (ClFinTop X) by A2, Def6;
then (U `) ` = {} the carrier of (ClFinTop X) by XBOOLE_1:37;
hence contradiction ; ::_thesis: verum
end;
begin
definition
let X, x0 be set ;
funcx0 -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
deffunc H1( set ) -> set = IFEQ ($1,{},$1,($1 \/ ({x0} /\ X)));
A1: for A being Subset of X holds
( A c= H1(A) & H1(A) c= X )
proof
let A be Subset of X; ::_thesis: ( A c= H1(A) & H1(A) c= X )
( A = {} or A <> {} ) ;
then A2: ( H1(A) = A or H1(A) = A \/ ({x0} /\ X) ) by FUNCOP_1:def_8;
hence A c= H1(A) by XBOOLE_1:7; ::_thesis: H1(A) c= X
{x0} /\ X c= X by XBOOLE_1:17;
hence H1(A) c= X by A2, XBOOLE_1:8; ::_thesis: verum
end;
A3: H1( {} ) = {} by FUNCOP_1:def_8;
A4: for A, B being Subset of X holds H1(A \/ B) = H1(A) \/ H1(B)
proof
let A, B be Subset of X; ::_thesis: H1(A \/ B) = H1(A) \/ H1(B)
percases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;
suppose ( A = {} or B = {} ) ; ::_thesis: H1(A \/ B) = H1(A) \/ H1(B)
hence H1(A \/ B) = H1(A) \/ H1(B) by A3; ::_thesis: verum
end;
supposeA5: ( A <> {} & B <> {} ) ; ::_thesis: H1(A \/ B) = H1(A) \/ H1(B)
then A6: H1(A \/ B) = (A \/ B) \/ ({x0} /\ X) by FUNCOP_1:def_8;
A7: H1(B) = B \/ ({x0} /\ X) by A5, FUNCOP_1:def_8;
H1(A) = A \/ ({x0} /\ X) by A5, FUNCOP_1:def_8;
hence H1(A \/ B) = H1(A) \/ H1(B) by A7, A6, XBOOLE_1:5; ::_thesis: verum
end;
end;
end;
A8: for A being Subset of X holds H1(H1(A)) = H1(A)
proof
let A be Subset of X; ::_thesis: H1(H1(A)) = H1(A)
( A = {} or A <> {} ) ;
then ( H1(A) = {} or ( A \/ ({x0} /\ X) <> {} & H1(A) = A \/ ({x0} /\ X) ) ) by FUNCOP_1:def_8;
then ( H1(H1(A)) = H1(A) or ( H1(A) = A \/ ({x0} /\ X) & H1(H1(A)) = (A \/ ({x0} /\ X)) \/ ({x0} /\ X) ) ) by FUNCOP_1:def_8;
hence H1(H1(A)) = H1(A) by XBOOLE_1:6; ::_thesis: verum
end;
consider T being strict TopSpace such that
A9: ( the carrier of T = X & ( for A being Subset of T holds Cl A = H1(A) ) ) from TOPGEN_3:sch_2(A3, A1, A4, A8);
take T ; ::_thesis: ( the carrier of T = X & ( for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) )
thus the carrier of T = X by A9; ::_thesis: for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X)))
let F be Subset of T; ::_thesis: Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X)))
thus Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X))) by A9; ::_thesis: verum
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
let T1, T2 be strict TopSpace; ::_thesis: ( the carrier of T1 = X & ( for A being Subset of T1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) & the carrier of T2 = X & ( for A being Subset of T2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) implies T1 = T2 )
assume that
A10: the carrier of T1 = X and
A11: for A being Subset of T1 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) and
A12: the carrier of T2 = X and
A13: for A being Subset of T2 holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ; ::_thesis: T1 = T2
now__::_thesis:_for_A1_being_Subset_of_T1
for_A2_being_Subset_of_T2_st_A1_=_A2_holds_
Cl_A1_=_Cl_A2
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2
let A2 be Subset of T2; ::_thesis: ( A1 = A2 implies Cl A1 = Cl A2 )
assume A1 = A2 ; ::_thesis: Cl A1 = Cl A2
hence Cl A1 = IFEQ (A2,{},A2,(A2 \/ ({x0} /\ X))) by A11
.= Cl A2 by A13 ;
::_thesis: verum
end;
hence T1 = T2 by A10, A12, Th8; ::_thesis: verum
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 ;
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}
proof
let X be non empty set ; ::_thesis: for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
let x0 be Element of X; ::_thesis: for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}
let A be non empty Subset of (x0 -PointClTop X); ::_thesis: Cl A = A \/ {x0}
thus Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) by Def7
.= A \/ ({x0} /\ X) by FUNCOP_1:def_8
.= A \/ {x0} by XBOOLE_1:28 ; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds
( A is closed iff x0 in A )
let x0 be Element of X; ::_thesis: for A being non empty Subset of (x0 -PointClTop X) holds
( A is closed iff x0 in A )
let A be non empty Subset of (x0 -PointClTop X); ::_thesis: ( A is closed iff x0 in A )
( A is closed iff Cl A = A ) by PRE_TOPC:22;
then ( A is closed iff A = A \/ {x0} ) by Th37;
then ( A is closed iff {x0} c= A ) by XBOOLE_1:7, XBOOLE_1:12;
hence ( A is closed iff x0 in A ) by ZFMISC_1:31; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for x0 being Element of X
for A being proper Subset of (x0 -PointClTop X) holds
( A is open iff not x0 in A )
let x0 be Element of X; ::_thesis: for A being proper Subset of (x0 -PointClTop X) holds
( A is open iff not x0 in A )
let A be proper Subset of (x0 -PointClTop X); ::_thesis: ( A is open iff not x0 in A )
( A is open iff A ` is closed ) by TOPS_1:4;
then A1: ( A is open iff x0 in A ` ) by Th38;
x0 is Element of (x0 -PointClTop X) by Def7;
hence ( A is open iff not x0 in A ) by A1, XBOOLE_0:def_5; ::_thesis: verum
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
let X, x0, x be set ; ::_thesis: ( x0 in X implies ( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 ) )
assume A1: x0 in X ; ::_thesis: ( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 )
hereby ::_thesis: ( x = x0 implies {x} is closed Subset of (x0 -PointClTop X) )
assume {x} is closed Subset of (x0 -PointClTop X) ; ::_thesis: x = x0
then x0 in {x} by A1, Th38;
hence x = x0 by TARSKI:def_1; ::_thesis: verum
end;
assume A2: x = x0 ; ::_thesis: {x} is closed Subset of (x0 -PointClTop X)
then A3: x0 in {x} by ZFMISC_1:31;
{x} c= X by A2, A1, ZFMISC_1:31;
hence {x} is closed Subset of (x0 -PointClTop X) by A3, Def7, Th38; ::_thesis: verum
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
let X, x0, x be set ; ::_thesis: ( {x0} c< X implies ( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) ) )
assume A1: {x0} c< X ; ::_thesis: ( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )
then reconsider Y = X as non empty set by XBOOLE_1:62;
reconsider A = {x0} as Subset of Y by A1, XBOOLE_0:def_8;
A2: x0 in A by TARSKI:def_1;
reconsider A = A as proper Subset of Y by A1, SUBSET_1:def_6;
A3: the carrier of (x0 -PointClTop X) = X by Def7;
hereby ::_thesis: ( x in X & x <> x0 implies {x} is open Subset of (x0 -PointClTop X) )
assume A4: {x} is open Subset of (x0 -PointClTop X) ; ::_thesis: ( x in X & not x = x0 )
hence x in X by A3, ZFMISC_1:31; ::_thesis: not x = x0
assume x = x0 ; ::_thesis: contradiction
then ( not x0 in {x0} or A is non proper Subset of (x0 -PointClTop X) ) by A4, Th39;
hence contradiction by A3, TARSKI:def_1; ::_thesis: verum
end;
assume that
A5: x in X and
A6: x <> x0 ; ::_thesis: {x} is open Subset of (x0 -PointClTop X)
A7: not x0 in {x} by A6, TARSKI:def_1;
x0 in Y by A2;
then {x} is proper Subset of (x0 -PointClTop Y) by A7, A5, A3, SUBSET_1:def_6, ZFMISC_1:31;
hence {x} is open Subset of (x0 -PointClTop X) by A7, A2, Th39; ::_thesis: verum
end;
begin
definition
let X, X0 be set ;
funcX0 -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
deffunc H1( set ) -> set = IFEQ ($1,X,$1,($1 /\ X0));
A1: for A being Subset of X holds H1(A) c= A
proof
let A be Subset of X; ::_thesis: H1(A) c= A
( A = X or A <> X ) ;
then ( H1(A) = A or H1(A) = A /\ X0 ) by FUNCOP_1:def_8;
hence H1(A) c= A by XBOOLE_1:17; ::_thesis: verum
end;
A2: for A, B being Subset of X holds H1(A /\ B) = H1(A) /\ H1(B)
proof
let A, B be Subset of X; ::_thesis: H1(A /\ B) = H1(A) /\ H1(B)
percases ( A = X or B = X or ( A <> X & B <> X ) ) ;
supposeA3: ( A = X or B = X ) ; ::_thesis: H1(A /\ B) = H1(A) /\ H1(B)
A4: B /\ X = B by XBOOLE_1:28;
( B = X or B <> X ) ;
then ( H1(B) = B or H1(B) = B /\ X0 ) by FUNCOP_1:def_8;
then A5: X /\ H1(B) = H1(B) by XBOOLE_1:28;
( A = X or A <> X ) ;
then ( H1(A) = A or H1(A) = A /\ X0 ) by FUNCOP_1:def_8;
then A6: H1(A) /\ X = H1(A) by XBOOLE_1:28;
A /\ X = A by XBOOLE_1:28;
hence H1(A /\ B) = H1(A) /\ H1(B) by A4, A6, A5, A3, FUNCOP_1:def_8; ::_thesis: verum
end;
supposeA7: ( A <> X & B <> X ) ; ::_thesis: H1(A /\ B) = H1(A) /\ H1(B)
A \/ (A /\ B) = A by XBOOLE_1:22;
then A /\ B <> X by A7, XBOOLE_1:12;
then A8: H1(A /\ B) = (A /\ B) /\ X0 by FUNCOP_1:def_8;
X0 = X0 /\ X0 ;
then H1(A /\ B) = ((A /\ B) /\ X0) /\ X0 by A8, XBOOLE_1:16;
then A9: H1(A /\ B) = ((B /\ X0) /\ A) /\ X0 by XBOOLE_1:16;
A10: H1(B) = B /\ X0 by A7, FUNCOP_1:def_8;
H1(A) = A /\ X0 by A7, FUNCOP_1:def_8;
hence H1(A /\ B) = H1(A) /\ H1(B) by A9, A10, XBOOLE_1:16; ::_thesis: verum
end;
end;
end;
A11: for A being Subset of X holds H1(H1(A)) = H1(A)
proof
let A be Subset of X; ::_thesis: H1(H1(A)) = H1(A)
( A = X or A <> X ) ;
then ( H1(A) = X or ( A /\ X0 <> X & H1(A) = A /\ X0 ) ) by FUNCOP_1:def_8;
then ( H1(H1(A)) = H1(A) or ( H1(A) = A /\ X0 & H1(H1(A)) = (A /\ X0) /\ X0 & X0 /\ X0 = X0 ) ) by FUNCOP_1:def_8;
hence H1(H1(A)) = H1(A) by XBOOLE_1:16; ::_thesis: verum
end;
A12: H1(X) = X by FUNCOP_1:def_8;
consider T being strict TopSpace such that
A13: ( the carrier of T = X & ( for A being Subset of T holds Int A = H1(A) ) ) from TOPGEN_3:sch_3(A12, A1, A2, A11);
take T ; ::_thesis: ( the carrier of T = X & ( for A being Subset of T holds Int A = IFEQ (A,X,A,(A /\ X0)) ) )
thus the carrier of T = X by A13; ::_thesis: for A being Subset of T holds Int A = IFEQ (A,X,A,(A /\ X0))
let F be Subset of T; ::_thesis: Int F = IFEQ (F,X,F,(F /\ X0))
thus Int F = IFEQ (F,X,F,(F /\ X0)) by A13; ::_thesis: verum
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
let T1, T2 be strict TopSpace; ::_thesis: ( the carrier of T1 = X & ( for A being Subset of T1 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) & the carrier of T2 = X & ( for A being Subset of T2 holds Int A = IFEQ (A,X,A,(A /\ X0)) ) implies T1 = T2 )
assume that
A14: the carrier of T1 = X and
A15: for A being Subset of T1 holds Int A = IFEQ (A,X,A,(A /\ X0)) and
A16: the carrier of T2 = X and
A17: for A being Subset of T2 holds Int A = IFEQ (A,X,A,(A /\ X0)) ; ::_thesis: T1 = T2
now__::_thesis:_for_A1_being_Subset_of_T1
for_A2_being_Subset_of_T2_st_A1_=_A2_holds_
Int_A1_=_Int_A2
let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2
let A2 be Subset of T2; ::_thesis: ( A1 = A2 implies Int A1 = Int A2 )
assume A1 = A2 ; ::_thesis: Int A1 = Int A2
hence Int A1 = IFEQ (A2,X,A2,(A2 /\ X0)) by A15
.= Int A2 by A17 ;
::_thesis: verum
end;
hence T1 = T2 by A14, A16, Th10; ::_thesis: verum
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 ;
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
proof
let X be non empty set ; ::_thesis: for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
let X0 be set ; ::_thesis: for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
let A be proper Subset of (X0 -DiscreteTop X); ::_thesis: Int A = A /\ X0
the carrier of (X0 -DiscreteTop X) = X by Def8;
then A1: X <> A by SUBSET_1:def_6;
thus Int A = IFEQ (A,X,A,(A /\ X0)) by Def8
.= A /\ X0 by A1, FUNCOP_1:def_8 ; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds
( A is open iff A c= X0 )
let X0 be set ; ::_thesis: for A being proper Subset of (X0 -DiscreteTop X) holds
( A is open iff A c= X0 )
let A be proper Subset of (X0 -DiscreteTop X); ::_thesis: ( A is open iff A c= X0 )
( A is open iff Int A = A ) by TOPS_1:23;
then ( A is open iff A = A /\ X0 ) by Th42;
hence ( A is open iff A c= X0 ) by XBOOLE_1:17, XBOOLE_1:28; ::_thesis: verum
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
let X be set ; ::_thesis: for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
let X0 be Subset of X; ::_thesis: the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)
A1: the carrier of (X0 -DiscreteTop X) = X by Def8;
thus the topology of (X0 -DiscreteTop X) c= {X} \/ (bool X0) :: according to XBOOLE_0:def_10 ::_thesis: {X} \/ (bool X0) c= the topology of (X0 -DiscreteTop X)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of (X0 -DiscreteTop X) or a in {X} \/ (bool X0) )
assume A2: a in the topology of (X0 -DiscreteTop X) ; ::_thesis: a in {X} \/ (bool X0)
then reconsider a = a as Subset of (X0 -DiscreteTop X) ;
A3: ( ( a is proper & not X is empty ) or not a is proper ) by A1;
a is open by A2, PRE_TOPC:def_2;
then ( a = X or a c= X0 ) by A3, A1, Th43, SUBSET_1:def_6;
then ( a in {X} or a in bool X0 ) by TARSKI:def_1;
hence a in {X} \/ (bool X0) by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {X} \/ (bool X0) or a in the topology of (X0 -DiscreteTop X) )
assume a in {X} \/ (bool X0) ; ::_thesis: a in the topology of (X0 -DiscreteTop X)
then A4: ( a in {X} or a in bool X0 ) by XBOOLE_0:def_3;
then ( a = X or a c= X0 ) by TARSKI:def_1;
then reconsider a = a as Subset of (X0 -DiscreteTop X) by A1, XBOOLE_1:1;
assume A5: not a in the topology of (X0 -DiscreteTop X) ; ::_thesis: contradiction
then A6: a <> [#] (X0 -DiscreteTop X) by PRE_TOPC:def_2;
then A7: not X is empty by A1;
A8: a is proper by A6, SUBSET_1:def_6;
A9: not a is open by A5, PRE_TOPC:def_2;
a <> X by A6, Def8;
hence contradiction by A7, A4, A9, A8, Th43, TARSKI:def_1; ::_thesis: verum
end;
theorem :: TOPGEN_3:45
for X being set holds ADTS X = {} -DiscreteTop X
proof
let X be set ; ::_thesis: ADTS X = {} -DiscreteTop X
set T = {} -DiscreteTop X;
A1: the carrier of ({} -DiscreteTop X) = X by Def8;
A2: cobool X = {{},X} by TEX_1:def_2;
A3: the topology of ({} -DiscreteTop X) c= cobool X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of ({} -DiscreteTop X) or a in cobool X )
assume A4: a in the topology of ({} -DiscreteTop X) ; ::_thesis: a in cobool X
then reconsider a = a as Subset of ({} -DiscreteTop X) ;
a is open by A4, PRE_TOPC:def_2;
then ( ( a c= X & X is empty ) or not a is proper or a c= {} ) by A1, Th43;
then ( a = {} or a = X ) by A1, SUBSET_1:def_6;
hence a in cobool X by A2, TARSKI:def_2; ::_thesis: verum
end;
{} ({} -DiscreteTop X) = {} ;
then A5: {} in the topology of ({} -DiscreteTop X) by PRE_TOPC:def_2;
[#] ({} -DiscreteTop X) = X by Def8;
then X in the topology of ({} -DiscreteTop X) by PRE_TOPC:def_2;
then cobool X c= the topology of ({} -DiscreteTop X) by A5, A2, ZFMISC_1:32;
then the topology of ({} -DiscreteTop X) = cobool X by A3, XBOOLE_0:def_10;
hence ADTS X = {} -DiscreteTop X by A1, TEX_1:def_3; ::_thesis: verum
end;
theorem :: TOPGEN_3:46
for X being set holds 1TopSp X = X -DiscreteTop X
proof
let X be set ; ::_thesis: 1TopSp X = X -DiscreteTop X
set T = X -DiscreteTop X;
A1: the carrier of (X -DiscreteTop X) = X by Def8;
A2: X c= X ;
then the topology of (X -DiscreteTop X) = {X} \/ (bool X) by Th44;
hence 1TopSp X = X -DiscreteTop X by A2, A1, ZFMISC_1:40; ::_thesis: verum
end;