:: On constructing topological spaces and Sorgenfrey line :: by Grzegorz Bancerek :: :: Received December 10, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SETFAM_1, XBOOLE_0, SUBSET_1, TARSKI, ABIAN, PRE_TOPC, STRUCT_0, CANTOR_1, RLVECT_3, ZFMISC_1, RELAT_1, PBOOLE, FUNCT_1, CARD_3, TOPGEN_2, RCOMP_1, YELLOW_8, TOPS_1, XXREAL_1, ARYTM_3, RAT_1, XXREAL_0, CARD_1, ORDINAL1, LIMFUNC1, CARD_2, INT_1, ARYTM_1, TAXONOM2, CARD_5, ORDINAL2, FINSET_1, MCART_1, NEWTON, FUNCT_7, SERIES_1, PREPOWER, COMPLEX1, NAT_1, VALUED_1, FINSUB_1, FINSEQ_1, ARYTM_2, WAYBEL23, FUNCOP_1, TEX_1, COMPTS_1, TOPGEN_3, REAL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSET_1, DOMAIN_1, FINSUB_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FINSEQ_1, ORDINAL1, CARD_1, CARD_3, FUNCOP_1, TAXONOM2, CARD_2, CARD_5, ARYTM_3, ARYTM_2, XCMPLX_0, COMPLEX1, XXREAL_0, XREAL_0, NEWTON, INT_1, NAT_1, RAT_1, NUMBERS, ABIAN, FUNCT_7, VALUED_1, PREPOWER, SERIES_1, RCOMP_1, PBOOLE, LIMFUNC1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, TEX_1, CANTOR_1, YELLOW_8, WAYBEL23, TOPGEN_2; constructors DOMAIN_1, ARYTM_2, FINSUB_1, REAL_1, SQUARE_1, CARD_2, PROB_1, RCOMP_1, LIMFUNC1, NEWTON, PREPOWER, SERIES_1, ABIAN, TOPS_1, COMPTS_1, TEX_1, TAXONOM2, WAYBEL23, TOPGEN_2, RELSET_1, FINSEQ_2; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, INT_1, RAT_1, CARD_1, MEMBERED, NEWTON, PBOOLE, CARD_5, STRUCT_0, PRE_TOPC, TOPS_1, TEX_2, VALUED_0, VALUED_1, FUNCT_2, NAT_1, XTUPLE_0; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; begin :: Introducing topology reserve a,b,c for set; definition let X be set; let B be Subset-Family of X; attr B is point-filtered means :: TOPGEN_3:def 1 for x,U1,U2 being set st U1 in B & U2 in B & x in U1 /\ U2 ex U being Subset of X st U in B & x in U & U c= U1 /\ U2; end; :: theorem :: TOPGEN_3:1 :: (B1) for X being set, B being Subset-Family of X holds B is covering iff for x being set st x in X ex U being Subset of X st U in B & x in U; :: theorem :: TOPGEN_3:2 :: (B2) for X being set, B being Subset-Family of X st B is point-filtered covering 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; :: theorem :: TOPGEN_3:3 for X being set, 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 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 ex U being set st U in B.x & U c= U1 /\ U2) 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; :: theorem :: TOPGEN_3:4 for X being set, 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) 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; scheme :: TOPGEN_3:sch 1 TopDefByClosedPred{X() -> set, C[set]}: ex T being strict TopSpace st the carrier of T = X() & for A being Subset of T holds A is closed iff C[A] provided C[{}] & C[X()] and for A,B being set st C[A] & C[B] holds C[A \/ B] and for G being Subset-Family of X() st for A being set st A in G holds C[A] holds C[Intersect G]; 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 the TopStruct of T1 = the TopStruct of T2 ; theorem :: 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 the TopStruct of T1 = the TopStruct of T2; definition let X,Y be set; let r be Subset of [:X, bool Y:]; redefine func rng r -> Subset-Family of Y; end; :: theorem :: TOPGEN_3:7 for X being set, 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) 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; scheme :: TOPGEN_3:sch 2 TopDefByClosureOp{X() -> set, ClOp(object) -> set}: ex T being strict TopSpace st the carrier of T = X() & for A being Subset of T holds Cl A = ClOp(A) provided ClOp({}) = {} and for A being Subset of X() holds A c= ClOp(A) & ClOp(A) c= X() and for A,B being Subset of X() holds ClOp(A \/ B) = ClOp(A) \/ ClOp(B) and for A being Subset of X() holds ClOp(ClOp(A)) = ClOp(A); theorem :: TOPGEN_3:8 for T1,T2 being TopSpace st the carrier of T1 = the carrier of T2 & for A1 being Subset of T1, A2 being Subset of T2 st A1 = A2 holds Cl A1 = Cl A2 holds the topology of T1 = the topology of T2; :: theorem :: TOPGEN_3:9 for X being set, 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) 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; scheme :: TOPGEN_3:sch 3 TopDefByInteriorOp{X() -> set, IntOp(object) -> set}: ex T being strict TopSpace st the carrier of T = X() & for A being Subset of T holds Int A = IntOp(A) provided IntOp(X()) = X() and for A being Subset of X() holds IntOp(A) c= A and for A,B being Subset of X() holds IntOp(A /\ B) = IntOp(A) /\ IntOp( B) and for A being Subset of X() holds IntOp(IntOp(A)) = IntOp(A); theorem :: TOPGEN_3:10 for T1,T2 being TopSpace st the carrier of T1 = the carrier of T2 & for A1 being Subset of T1, A2 being Subset of T2 st A1 = A2 holds Int A1 = Int A2 holds the topology of T1 = the topology of T2; begin :: Sorgenfrey line (1.2.2) definition ::$N Sorgenfrey line func Sorgenfrey-line -> strict non empty TopSpace means :: TOPGEN_3:def 2 the carrier of it = REAL & ex B being Subset-Family of REAL st the topology of it = UniCl B & B = {[.x,q.[ where x,q is Real: x < q & q is rational}; end; theorem :: TOPGEN_3:11 for x,y being Real holds [.x,y.[ is open Subset of Sorgenfrey-line; theorem :: TOPGEN_3:12 for x,y being Real holds ].x,y.[ is open Subset of Sorgenfrey-line; theorem :: TOPGEN_3:13 for x being Real holds left_open_halfline x is open Subset of Sorgenfrey-line; theorem :: TOPGEN_3:14 for x being Real holds right_open_halfline x is open Subset of Sorgenfrey-line; theorem :: TOPGEN_3:15 for x being Real holds right_closed_halfline x is open Subset of Sorgenfrey-line; theorem :: TOPGEN_3:16 card INT = omega; ::$N The Denumerability of the Rational Numbers theorem :: TOPGEN_3:17 card RAT = omega; theorem :: TOPGEN_3:18 for A being set st A is mutually-disjoint & for a st a in A ex x ,y being Real st x < y & ].x,y.[ c= a holds A is countable; definition let X be set; let x be Real; pred x is_local_minimum_of X means :: TOPGEN_3:def 3 x in X & ex y being Real st y < x & ].y,x.[ misses X; end; theorem :: 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; registration let M be Aleph; cluster exp(2,M) -> infinite; end; definition func continuum -> infinite cardinal number equals :: TOPGEN_3:def 4 card REAL; end; theorem :: TOPGEN_3:20 card {[.x,q.[ where x,q is Real: x < q & q is rational} = continuum; definition let X be set, r being Real; func X-powers r -> sequence of REAL means :: TOPGEN_3:def 5 for i being Nat holds i in X & it.i = r|^i or not i in X & it.i = 0; end; theorem :: TOPGEN_3:21 for X being set, r being Real st 0 < r & r < 1 holds X -powers r is summable; reserve r for Real, X for set, n for Element of NAT; theorem :: TOPGEN_3:22 0 < r & r < 1 implies Sum ((r GeoSeq)^\n) = r|^n / (1-r); theorem :: TOPGEN_3:23 Sum (((1/2) GeoSeq)^\(n+1)) = (1/2)|^n; theorem :: TOPGEN_3:24 0 < r & r < 1 implies Sum (X-powers r) <= Sum (r GeoSeq); theorem :: TOPGEN_3:25 Sum ((X-powers (1/2))^\(n+1)) <= (1/2)|^n; theorem :: TOPGEN_3:26 for X being infinite Subset of NAT, i being Nat holds (Partial_Sums (X-powers (1/2))).i < Sum (X-powers (1/2)); theorem :: 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; theorem :: TOPGEN_3:28 X is countable implies Fin X is countable; theorem :: TOPGEN_3:29 continuum = exp(2, omega); ::$N The Non-Denumerability of the Continuum theorem :: TOPGEN_3:30 omega in continuum; theorem :: 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; theorem :: TOPGEN_3:32 for X being Subset-Family of REAL st card X in continuum ex x being Real, q being Rational st x < q & not [.x,q.[ in UniCl X; theorem :: TOPGEN_3:33 weight Sorgenfrey-line = continuum; begin :: Example: topological space with finite sets closed definition let X be set; func ClFinTop(X) -> strict TopSpace means :: 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; end; theorem :: TOPGEN_3:34 for X being set, A being Subset of ClFinTop(X) holds A is open iff A = {} or A` is finite; theorem :: TOPGEN_3:35 for X being infinite set, A being Subset of X st A is finite holds A` is infinite; registration let X be non empty set; cluster ClFinTop(X) -> non empty; 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; begin :: Example: toplogical space with one point clusure definition let X,x0 be set; func x0-PointClTop(X) -> strict TopSpace means :: TOPGEN_3:def 7 the carrier of it = X & for A being Subset of it holds Cl A = IFEQ(A,{},A,A \/ {x0} /\ X); end; registration let X be non empty set; let x0 be set; cluster x0-PointClTop X -> non empty; end; theorem :: TOPGEN_3:37 for X being non empty set, x0 being Element of X for A being non empty Subset of x0-PointClTop(X) holds Cl A = A \/ {x0}; theorem :: TOPGEN_3:38 for X being non empty set, x0 being Element of X for A being non empty Subset of x0-PointClTop(X) holds A is closed iff x0 in A; theorem :: TOPGEN_3:39 for X being non empty set, x0 being Element of X for A being proper Subset of x0-PointClTop(X) holds A is open iff not x0 in A; 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; 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; begin :: Example: topological space discrete on subset definition let X,X0 be set; func X0-DiscreteTop(X) -> strict TopSpace means :: TOPGEN_3:def 8 the carrier of it = X & for A being Subset of it holds Int A = IFEQ(A,X,A,A /\ X0); end; registration let X be non empty set; let X0 be set; cluster X0-DiscreteTop X -> non empty; end; theorem :: TOPGEN_3:42 for X being non empty set, X0 being set for A being proper Subset of X0-DiscreteTop(X) holds Int A = A /\ X0; theorem :: TOPGEN_3:43 for X being non empty set, X0 being set for A being proper Subset of X0-DiscreteTop(X) holds A is open iff A c= X0; theorem :: TOPGEN_3:44 for X be set, X0 being Subset of X holds the topology of X0 -DiscreteTop X = {X} \/ bool X0; theorem :: TOPGEN_3:45 for X being set holds ADTS X = {}-DiscreteTop(X); theorem :: TOPGEN_3:46 for X being set holds 1TopSp X = X-DiscreteTop(X);