:: TOPGEN_3 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem Def1 defines point-filtered TOPGEN_3:def 1 :
theorem Th1: :: TOPGEN_3:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th2: :: TOPGEN_3:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: TOPGEN_3:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: TOPGEN_3:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: TOPGEN_3:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: TOPGEN_3:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th10: :: TOPGEN_3:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: 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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th16: :: TOPGEN_3:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th17: :: TOPGEN_3:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th18: :: TOPGEN_3:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def 3 :
theorem Th19: :: TOPGEN_3:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines continuum TOPGEN_3:def 4 :
theorem Th20: :: TOPGEN_3:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
theorem Th21: :: TOPGEN_3:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th22: :: TOPGEN_3:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th23: :: TOPGEN_3:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: TOPGEN_3:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th26: :: TOPGEN_3:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th27: :: TOPGEN_3:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th28: :: TOPGEN_3:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th29: :: TOPGEN_3:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th30: :: TOPGEN_3:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th31: :: TOPGEN_3:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th32: :: TOPGEN_3:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :
theorem Th34: :: TOPGEN_3:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th35: :: TOPGEN_3:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th38: :: TOPGEN_3:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th39: :: TOPGEN_3:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th43: :: TOPGEN_3:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm7:
for X being set
for A being Subset of X st A is proper holds
not X is empty
theorem Th44: :: TOPGEN_3:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: TOPGEN_3:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)