:: 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;