:: On constructing topological spaces and Sorgenfrey line
:: by Grzegorz Bancerek
::
:: Received December 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem Def1 defines point-filtered TOPGEN_3:def 1 :
theorem Th1: :: TOPGEN_3:1
theorem Th2: :: TOPGEN_3:2
theorem :: TOPGEN_3:3
theorem Th4: :: TOPGEN_3:4
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 )
theorem :: TOPGEN_3:5
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 )
theorem Th6: :: TOPGEN_3:6
theorem Th7: :: TOPGEN_3:7
theorem Th8: :: TOPGEN_3:8
theorem Th9: :: TOPGEN_3:9
theorem Th10: :: TOPGEN_3:10
:: 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 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;
theorem Th11: :: TOPGEN_3:11
theorem :: TOPGEN_3:12
theorem :: TOPGEN_3:13
theorem :: TOPGEN_3:14
theorem :: TOPGEN_3:15
theorem Th16: :: TOPGEN_3:16
theorem Th17: :: TOPGEN_3:17
theorem Th18: :: TOPGEN_3:18
:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def 3 :
theorem Th19: :: TOPGEN_3:19
:: deftheorem defines continuum TOPGEN_3:def 4 :
theorem Th20: :: TOPGEN_3:20
:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
theorem Th21: :: TOPGEN_3:21
theorem Th22: :: TOPGEN_3:22
theorem Th23: :: TOPGEN_3:23
theorem :: TOPGEN_3:24
theorem Th25: :: TOPGEN_3:25
theorem Th26: :: TOPGEN_3:26
theorem Th27: :: TOPGEN_3:27
theorem Th28: :: TOPGEN_3:28
theorem Th29: :: TOPGEN_3:29
theorem Th30: :: TOPGEN_3:30
theorem Th31: :: TOPGEN_3:31
theorem Th32: :: TOPGEN_3:32
theorem :: TOPGEN_3:33
:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :
theorem Th34: :: TOPGEN_3:34
theorem Th35: :: TOPGEN_3:35
theorem :: TOPGEN_3:36
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)) ) );
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)) ) )
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;
end;
:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :
theorem Th37: :: TOPGEN_3:37
theorem Th38: :: TOPGEN_3:38
theorem Th39: :: TOPGEN_3:39
theorem :: TOPGEN_3:40
theorem :: TOPGEN_3:41
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) ) );
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) ) )
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;
end;
:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :
theorem Th42: :: TOPGEN_3:42
theorem Th43: :: TOPGEN_3:43
theorem Th44: :: TOPGEN_3:44
theorem :: TOPGEN_3:45
theorem :: TOPGEN_3:46