TOPGEN_3: On constructing topological spaces and Sorgenfrey line

:: On constructing topological spaces and Sorgenfrey line
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let X be set ;
let B be Subset-Family of X;

attr B is point-filtered means :: TOPGEN_3:def 1
for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds
ex U being Subset of X st
( U in B & x in U & U c= U1 /\ U2 );

end;

:: deftheorem defines point-filtered TOPGEN_3:def 1 :

::<DSCR monograph="topology" name="condition (B2)"/>

theorem Th1: :: TOPGEN_3:1

for X being set
for B being Subset-Family of X holds
( B is covering iff for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) )

proof end;

::<DSCR monograph="topology" label="1.2.1."/>

theorem Th2: :: TOPGEN_3:2

for X being set
for B being Subset-Family of X st B is point-filtered & B is covering holds
for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T )

proof end;

::<DSCR monograph="topology" label="1.2.3."/>

theorem :: TOPGEN_3:3

for X being set
for B being non-empty ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds
x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ) holds
ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )

proof end;

::<DSCR monograph="topology" label="1.2.5."/>

theorem Th4: :: TOPGEN_3:4

for X being set
for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )

proof end;

scheme :: TOPGEN_3:sch 1
TopDefByClosedPred{ F₁() -> set , P₁[ set ] } :

ex T being strict TopSpace st
( the carrier of T = F₁() & ( for A being Subset of T holds
( A is closed iff P₁[A] ) ) )

provided

A1: ( P₁[ {} ] & P₁[F₁()] ) and
A2: for A, B being set st P₁[A] & P₁[B] holds
P₁[A \/ B] and
A3: for G being Subset-Family of F₁() st ( for A being set st A in G holds
P₁[A] ) holds
P₁[ Intersect G]

proof end;

Lm1: for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )

proof end;

theorem :: TOPGEN_3:5

for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

proof end;

Lm2: for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )

proof end;

theorem Th6: :: TOPGEN_3:6

for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

proof end;

definition

let X, Y be set ;
let r be Subset of [:X,(bool Y):];
:: original: rng
redefine func rng r -> Subset-Family of Y;
coherence by RELAT_1:def 19;

end;

::<DSCR monograph="topology" label="1.2.7."/>

theorem Th7: :: TOPGEN_3:7

for X being set
for c being Function of (bool X),(bool X) st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds
( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

proof end;

scheme :: TOPGEN_3:sch 2
TopDefByClosureOp{ F₁() -> set , F₂( object ) -> set } :

ex T being strict TopSpace st
( the carrier of T = F₁() & ( for A being Subset of T holds Cl A = F₂(A) ) )

provided

A1: F₂({}) = {} and
A2: for A being Subset of F₁() holds
( A c= F₂(A) & F₂(A) c= F₁() ) and
A3: for A, B being Subset of F₁() holds F₂((A \/ B)) = F₂(A) \/ F₂(B) and
A4: for A being Subset of F₁() holds F₂(F₂(A)) = F₂(A)

proof end;

theorem Th8: :: TOPGEN_3:8

for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Cl A1 = Cl A2 ) holds
the topology of T1 = the topology of T2

proof end;

::<DSCR monograph="topology" label="1.2.9."/>

theorem Th9: :: TOPGEN_3:9

for X being set
for i being Function of (bool X),(bool X) st i . X = X & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = rng i holds
( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )

proof end;

scheme :: TOPGEN_3:sch 3
TopDefByInteriorOp{ F₁() -> set , F₂( object ) -> set } :

ex T being strict TopSpace st
( the carrier of T = F₁() & ( for A being Subset of T holds Int A = F₂(A) ) )

provided

A1: F₂(F₁()) = F₁() and
A2: for A being Subset of F₁() holds F₂(A) c= A and
A3: for A, B being Subset of F₁() holds F₂((A /\ B)) = F₂(A) /\ F₂(B) and
A4: for A being Subset of F₁() holds F₂(F₂(A)) = F₂(A)

proof end;

theorem Th10: :: TOPGEN_3:10

for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1
for A2 being Subset of T2 st A1 = A2 holds
Int A1 = Int A2 ) holds
the topology of T1 = the topology of T2

proof end;

definition

::

WP:

Sorgenfrey line

func Sorgenfrey-line -> non empty strict TopSpace means :Def2: :: TOPGEN_3:def 2
( the carrier of it = REAL & ex B being Subset-Family of REAL st
( the topology of it = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) );

uniqueness ;
existence

proof end;

end;

:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :

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 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 holds [.x,y.[ is open Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_3:12

for x, y being Real holds ].x,y.[ is open Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_3:13

for x being Real holds left_open_halfline x is open Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_3:14

for x being Real holds right_open_halfline x is open Subset of Sorgenfrey-line

proof end;

theorem :: TOPGEN_3:15

for x being Real holds right_closed_halfline x is open Subset of Sorgenfrey-line

proof end;

theorem Th16: :: TOPGEN_3:16

card INT = omega

proof end;

::

WP:

The Denumerability of the Rational Numbers

theorem Th17: :: TOPGEN_3:17

card RAT = omega

proof end;

theorem Th18: :: TOPGEN_3:18

for A being set st A is mutually-disjoint & ( for a being set st a in A holds
ex x, y being Real st
( x < y & ].x,y.[ c= a ) ) holds
A is countable

proof end;

definition

let X be set ;
let x be Real;

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

end;

:: deftheorem defines is_local_minimum_of TOPGEN_3:def 3 :

theorem Th19: :: TOPGEN_3:19

for U being Subset of REAL holds { x where x is Element of REAL : x is_local_minimum_of U } is countable

proof end;

registration

let M be Aleph;

cluster exp (2,M) -> infinite ;

proof end;

end;

definition

func continuum -> infinite cardinal number equals :: TOPGEN_3:def 4
card REAL;

end;

:: deftheorem defines continuum TOPGEN_3:def 4 :

theorem Th20: :: TOPGEN_3:20

card { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } = continuum

proof end;

definition

let X be set ;
let r be Real;

func X -powers r -> sequence of REAL means :Def5: :: TOPGEN_3:def 5
for i being Nat holds
( ( i in X & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :

theorem Th21: :: TOPGEN_3:21

for X being set
for r being Real st 0 < r & r < 1 holds
X -powers r is summable

proof end;

theorem Th22: :: TOPGEN_3:22

for r being Real
for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)

proof end;

theorem Th23: :: TOPGEN_3:23

for n being Element of NAT holds Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n

proof end;

theorem :: TOPGEN_3:24

for r being Real
for X being set st 0 < r & r < 1 holds
Sum (X -powers r) <= Sum (r GeoSeq)

proof end;

theorem Th25: :: TOPGEN_3:25

for X being set
for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n

proof end;

theorem Th26: :: TOPGEN_3:26

for X being infinite Subset of NAT
for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

proof end;

theorem Th27: :: TOPGEN_3:27

for X, Y being infinite Subset of NAT st Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) holds
X = Y

proof end;

theorem Th28: :: TOPGEN_3:28

for X being set st X is countable holds
Fin X is countable

proof end;

theorem Th29: :: TOPGEN_3:29

continuum = exp (2,omega)

proof end;

::

WP:

The Non-Denumerability of the Continuum

theorem Th30: :: TOPGEN_3:30

omega in continuum

proof end;

theorem Th31: :: TOPGEN_3:31

for A being Subset-Family of REAL st card A in continuum holds
card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum

proof end;

theorem Th32: :: TOPGEN_3:32

for X being Subset-Family of REAL st card X in continuum holds
ex x being Real ex q being Rational st
( x < q & not [.x,q.[ in UniCl X )

proof end;

theorem :: TOPGEN_3:33

weight Sorgenfrey-line = continuum

proof end;

definition

let X be set ;

func ClFinTop X -> strict TopSpace means :Def6: :: TOPGEN_3:def 6
( the carrier of it = X & ( for F being Subset of it holds
( F is closed iff ( F is finite or F = X ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :

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

theorem Th35: :: TOPGEN_3:35

for X being infinite set
for A being Subset of X st A is finite holds
A ` is infinite

proof end;

registration

let X be non empty set ;

cluster ClFinTop X -> non empty strict ;

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

definition

let X, x0 be set ;

func x0 -PointClTop X -> strict TopSpace means :Def7: :: TOPGEN_3:def 7
( the carrier of it = X & ( for A being Subset of it holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :

registration

let X be non empty set ;
let x0 be set ;

cluster x0 -PointClTop X -> non empty strict ;

coherence by Def7;

end;

theorem Th37: :: TOPGEN_3:37

for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}

proof end;

theorem Th38: :: TOPGEN_3:38

for X being non empty set
for x0 being Element of X
for A being non empty Subset of (x0 -PointClTop X) holds
( A is closed iff x0 in A )

proof end;

theorem Th39: :: TOPGEN_3:39

for X being non empty set
for x0 being Element of X
for A being proper Subset of (x0 -PointClTop X) holds
( A is open iff not x0 in A )

proof end;

theorem :: TOPGEN_3:40

for X, x0, x being set st x0 in X holds
( {x} is closed Subset of (x0 -PointClTop X) iff x = x0 )

proof end;

theorem :: TOPGEN_3:41

for X, x0, x being set st {x0} c< X holds
( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )

proof end;

definition

let X, X0 be set ;

func X0 -DiscreteTop X -> strict TopSpace means :Def8: :: TOPGEN_3:def 8
( the carrier of it = X & ( for A being Subset of it holds Int A = IFEQ (A,X,A,(A /\ X0)) ) );

proof end;

proof end;

end;

:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :

registration

let X be non empty set ;
let X0 be set ;

cluster X0 -DiscreteTop X -> non empty strict ;

coherence by Def8;

end;

theorem Th42: :: TOPGEN_3:42

for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0

proof end;

theorem Th43: :: TOPGEN_3:43

for X being non empty set
for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds
( A is open iff A c= X0 )

proof end;

theorem Th44: :: TOPGEN_3:44

for X being set
for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)

proof end;

theorem :: TOPGEN_3:45

for X being set holds ADTS X = {} -DiscreteTop X

proof end;

theorem :: TOPGEN_3:46

for X being set holds 1TopSp X = X -DiscreteTop X

proof end;