:: On constructing topological spaces and Sorgenfrey line
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-2016 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);