:: DECOMP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let T be TopStruct ;
mode alpha-set of T -> Subset of T means :Def1: :: DECOMP_1:def 1
it c= Int (Cl (Int it));
existence
ex b1 being Subset of T st b1 c= Int (Cl (Int b1))
proof end;
let IT be Subset of T;
attr IT is semi-open means :Def2: :: DECOMP_1:def 2
IT c= Cl (Int IT);
attr IT is pre-open means :Def3: :: DECOMP_1:def 3
IT c= Int (Cl IT);
attr IT is pre-semi-open means :Def4: :: DECOMP_1:def 4
IT c= Cl (Int (Cl IT));
attr IT is semi-pre-open means :Def5: :: DECOMP_1:def 5
IT c= (Cl (Int IT)) \/ (Int (Cl IT));
end;

:: deftheorem Def1 defines alpha-set DECOMP_1:def 1 :
for T being TopStruct
for b2 being Subset of T holds
( b2 is alpha-set of T iff b2 c= Int (Cl (Int b2)) );

:: deftheorem Def2 defines semi-open DECOMP_1:def 2 :
for T being TopStruct
for IT being Subset of T holds
( IT is semi-open iff IT c= Cl (Int IT) );

:: deftheorem Def3 defines pre-open DECOMP_1:def 3 :
for T being TopStruct
for IT being Subset of T holds
( IT is pre-open iff IT c= Int (Cl IT) );

:: deftheorem Def4 defines pre-semi-open DECOMP_1:def 4 :
for T being TopStruct
for IT being Subset of T holds
( IT is pre-semi-open iff IT c= Cl (Int (Cl IT)) );

:: deftheorem Def5 defines semi-pre-open DECOMP_1:def 5 :
for T being TopStruct
for IT being Subset of T holds
( IT is semi-pre-open iff IT c= (Cl (Int IT)) \/ (Int (Cl IT)) );

definition
let T be TopStruct ;
let B be Subset of T;
func sInt B -> Subset of T equals :: DECOMP_1:def 6
B /\ (Cl (Int B));
coherence
B /\ (Cl (Int B)) is Subset of T ;
func pInt B -> Subset of T equals :: DECOMP_1:def 7
B /\ (Int (Cl B));
coherence
B /\ (Int (Cl B)) is Subset of T ;
func alphaInt B -> Subset of T equals :: DECOMP_1:def 8
B /\ (Int (Cl (Int B)));
coherence
B /\ (Int (Cl (Int B))) is Subset of T ;
func psInt B -> Subset of T equals :: DECOMP_1:def 9
B /\ (Cl (Int (Cl B)));
coherence
B /\ (Cl (Int (Cl B))) is Subset of T ;
end;

:: deftheorem defines sInt DECOMP_1:def 6 :
for T being TopStruct
for B being Subset of T holds sInt B = B /\ (Cl (Int B));

:: deftheorem defines pInt DECOMP_1:def 7 :
for T being TopStruct
for B being Subset of T holds pInt B = B /\ (Int (Cl B));

:: deftheorem defines alphaInt DECOMP_1:def 8 :
for T being TopStruct
for B being Subset of T holds alphaInt B = B /\ (Int (Cl (Int B)));

:: deftheorem defines psInt DECOMP_1:def 9 :
for T being TopStruct
for B being Subset of T holds psInt B = B /\ (Cl (Int (Cl B)));

definition
let T be TopStruct ;
let B be Subset of T;
func spInt B -> Subset of T equals :: DECOMP_1:def 10
(sInt B) \/ (pInt B);
coherence
(sInt B) \/ (pInt B) is Subset of T ;
end;

:: deftheorem defines spInt DECOMP_1:def 10 :
for T being TopStruct
for B being Subset of T holds spInt B = (sInt B) \/ (pInt B);

definition
let T be TopSpace;
func T ^alpha -> Subset-Family of T equals :: DECOMP_1:def 11
{ B where B is Subset of T : B is alpha-set of T } ;
coherence
{ B where B is Subset of T : B is alpha-set of T } is Subset-Family of T
proof end;
func SO T -> Subset-Family of T equals :: DECOMP_1:def 12
{ B where B is Subset of T : B is semi-open } ;
coherence
{ B where B is Subset of T : B is semi-open } is Subset-Family of T
proof end;
func PO T -> Subset-Family of T equals :: DECOMP_1:def 13
{ B where B is Subset of T : B is pre-open } ;
coherence
{ B where B is Subset of T : B is pre-open } is Subset-Family of T
proof end;
func SPO T -> Subset-Family of T equals :: DECOMP_1:def 14
{ B where B is Subset of T : B is semi-pre-open } ;
coherence
{ B where B is Subset of T : B is semi-pre-open } is Subset-Family of T
proof end;
func PSO T -> Subset-Family of T equals :: DECOMP_1:def 15
{ B where B is Subset of T : B is pre-semi-open } ;
coherence
{ B where B is Subset of T : B is pre-semi-open } is Subset-Family of T
proof end;
func D(c,alpha) T -> Subset-Family of T equals :: DECOMP_1:def 16
{ B where B is Subset of T : Int B = alphaInt B } ;
coherence
{ B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T
proof end;
func D(c,p) T -> Subset-Family of T equals :: DECOMP_1:def 17
{ B where B is Subset of T : Int B = pInt B } ;
coherence
{ B where B is Subset of T : Int B = pInt B } is Subset-Family of T
proof end;
func D(c,s) T -> Subset-Family of T equals :: DECOMP_1:def 18
{ B where B is Subset of T : Int B = sInt B } ;
coherence
{ B where B is Subset of T : Int B = sInt B } is Subset-Family of T
proof end;
func D(c,ps) T -> Subset-Family of T equals :: DECOMP_1:def 19
{ B where B is Subset of T : Int B = psInt B } ;
coherence
{ B where B is Subset of T : Int B = psInt B } is Subset-Family of T
proof end;
func D(alpha,p) T -> Subset-Family of T equals :: DECOMP_1:def 20
{ B where B is Subset of T : alphaInt B = pInt B } ;
coherence
{ B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T
proof end;
func D(alpha,s) T -> Subset-Family of T equals :: DECOMP_1:def 21
{ B where B is Subset of T : alphaInt B = sInt B } ;
coherence
{ B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T
proof end;
func D(alpha,ps) T -> Subset-Family of T equals :: DECOMP_1:def 22
{ B where B is Subset of T : alphaInt B = psInt B } ;
coherence
{ B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T
proof end;
func D(p,sp) T -> Subset-Family of T equals :: DECOMP_1:def 23
{ B where B is Subset of T : pInt B = spInt B } ;
coherence
{ B where B is Subset of T : pInt B = spInt B } is Subset-Family of T
proof end;
func D(p,ps) T -> Subset-Family of T equals :: DECOMP_1:def 24
{ B where B is Subset of T : pInt B = psInt B } ;
coherence
{ B where B is Subset of T : pInt B = psInt B } is Subset-Family of T
proof end;
func D(sp,ps) T -> Subset-Family of T equals :: DECOMP_1:def 25
{ B where B is Subset of T : spInt B = psInt B } ;
coherence
{ B where B is Subset of T : spInt B = psInt B } is Subset-Family of T
proof end;
end;

:: deftheorem defines ^alpha DECOMP_1:def 11 :
for T being TopSpace holds T ^alpha = { B where B is Subset of T : B is alpha-set of T } ;

:: deftheorem defines SO DECOMP_1:def 12 :
for T being TopSpace holds SO T = { B where B is Subset of T : B is semi-open } ;

:: deftheorem defines PO DECOMP_1:def 13 :
for T being TopSpace holds PO T = { B where B is Subset of T : B is pre-open } ;

:: deftheorem defines SPO DECOMP_1:def 14 :
for T being TopSpace holds SPO T = { B where B is Subset of T : B is semi-pre-open } ;

:: deftheorem defines PSO DECOMP_1:def 15 :
for T being TopSpace holds PSO T = { B where B is Subset of T : B is pre-semi-open } ;

:: deftheorem defines D(c,alpha) DECOMP_1:def 16 :
for T being TopSpace holds D(c,alpha) T = { B where B is Subset of T : Int B = alphaInt B } ;

:: deftheorem defines D(c,p) DECOMP_1:def 17 :
for T being TopSpace holds D(c,p) T = { B where B is Subset of T : Int B = pInt B } ;

:: deftheorem defines D(c,s) DECOMP_1:def 18 :
for T being TopSpace holds D(c,s) T = { B where B is Subset of T : Int B = sInt B } ;

:: deftheorem defines D(c,ps) DECOMP_1:def 19 :
for T being TopSpace holds D(c,ps) T = { B where B is Subset of T : Int B = psInt B } ;

:: deftheorem defines D(alpha,p) DECOMP_1:def 20 :
for T being TopSpace holds D(alpha,p) T = { B where B is Subset of T : alphaInt B = pInt B } ;

:: deftheorem defines D(alpha,s) DECOMP_1:def 21 :
for T being TopSpace holds D(alpha,s) T = { B where B is Subset of T : alphaInt B = sInt B } ;

:: deftheorem defines D(alpha,ps) DECOMP_1:def 22 :
for T being TopSpace holds D(alpha,ps) T = { B where B is Subset of T : alphaInt B = psInt B } ;

:: deftheorem defines D(p,sp) DECOMP_1:def 23 :
for T being TopSpace holds D(p,sp) T = { B where B is Subset of T : pInt B = spInt B } ;

:: deftheorem defines D(p,ps) DECOMP_1:def 24 :
for T being TopSpace holds D(p,ps) T = { B where B is Subset of T : pInt B = psInt B } ;

:: deftheorem defines D(sp,ps) DECOMP_1:def 25 :
for T being TopSpace holds D(sp,ps) T = { B where B is Subset of T : spInt B = psInt B } ;

theorem Th1: :: DECOMP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( alphaInt B = pInt B iff sInt B = psInt B )
proof end;

theorem Th2: :: DECOMP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( B is alpha-set of T iff B = alphaInt B )
proof end;

theorem Th3: :: DECOMP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( B is semi-open iff B = sInt B )
proof end;

theorem Th4: :: DECOMP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( B is pre-open iff B = pInt B )
proof end;

theorem Th5: :: DECOMP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( B is pre-semi-open iff B = psInt B )
proof end;

theorem Th6: :: DECOMP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B being Subset of T holds
( B is semi-pre-open iff B = spInt B )
proof end;

theorem Th7: :: DECOMP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (T ^alpha ) /\ (D(c,alpha) T) = the topology of T
proof end;

theorem Th8: :: DECOMP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (SO T) /\ (D(c,s) T) = the topology of T
proof end;

theorem Th9: :: DECOMP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PO T) /\ (D(c,p) T) = the topology of T
proof end;

theorem Th10: :: DECOMP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PSO T) /\ (D(c,ps) T) = the topology of T
proof end;

theorem Th11: :: DECOMP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PO T) /\ (D(alpha,p) T) = T ^alpha
proof end;

theorem Th12: :: DECOMP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (SO T) /\ (D(alpha,s) T) = T ^alpha
proof end;

theorem Th13: :: DECOMP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PSO T) /\ (D(alpha,ps) T) = T ^alpha
proof end;

theorem Th14: :: DECOMP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (SPO T) /\ (D(p,sp) T) = PO T
proof end;

theorem Th15: :: DECOMP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PSO T) /\ (D(p,ps) T) = PO T
proof end;

theorem Th16: :: DECOMP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PSO T) /\ (D(alpha,p) T) = SO T
proof end;

theorem Th17: :: DECOMP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace holds (PSO T) /\ (D(sp,ps) T) = SPO T
proof end;

definition
let X, Y be non empty TopSpace;
let f be Function of X,Y;
attr f is s-continuous means :Def26: :: DECOMP_1:def 26
for G being Subset of Y st G is open holds
f " G in SO X;
attr f is p-continuous means :Def27: :: DECOMP_1:def 27
for G being Subset of Y st G is open holds
f " G in PO X;
attr f is alpha-continuous means :Def28: :: DECOMP_1:def 28
for G being Subset of Y st G is open holds
f " G in X ^alpha ;
attr f is ps-continuous means :Def29: :: DECOMP_1:def 29
for G being Subset of Y st G is open holds
f " G in PSO X;
attr f is sp-continuous means :Def30: :: DECOMP_1:def 30
for G being Subset of Y st G is open holds
f " G in SPO X;
attr f is (c,alpha)-continuous means :Def31: :: DECOMP_1:def 31
for G being Subset of Y st G is open holds
f " G in D(c,alpha) X;
attr f is (c,s)-continuous means :Def32: :: DECOMP_1:def 32
for G being Subset of Y st G is open holds
f " G in D(c,s) X;
attr f is (c,p)-continuous means :Def33: :: DECOMP_1:def 33
for G being Subset of Y st G is open holds
f " G in D(c,p) X;
attr f is (c,ps)-continuous means :Def34: :: DECOMP_1:def 34
for G being Subset of Y st G is open holds
f " G in D(c,ps) X;
attr f is (alpha,p)-continuous means :Def35: :: DECOMP_1:def 35
for G being Subset of Y st G is open holds
f " G in D(alpha,p) X;
attr f is (alpha,s)-continuous means :Def36: :: DECOMP_1:def 36
for G being Subset of Y st G is open holds
f " G in D(alpha,s) X;
attr f is (alpha,ps)-continuous means :Def37: :: DECOMP_1:def 37
for G being Subset of Y st G is open holds
f " G in D(alpha,ps) X;
attr f is (p,ps)-continuous means :Def38: :: DECOMP_1:def 38
for G being Subset of Y st G is open holds
f " G in D(p,ps) X;
attr f is (p,sp)-continuous means :Def39: :: DECOMP_1:def 39
for G being Subset of Y st G is open holds
f " G in D(p,sp) X;
attr f is (sp,ps)-continuous means :Def40: :: DECOMP_1:def 40
for G being Subset of Y st G is open holds
f " G in D(sp,ps) X;
end;

:: deftheorem Def26 defines s-continuous DECOMP_1:def 26 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is s-continuous iff for G being Subset of Y st G is open holds
f " G in SO X );

:: deftheorem Def27 defines p-continuous DECOMP_1:def 27 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff for G being Subset of Y st G is open holds
f " G in PO X );

:: deftheorem Def28 defines alpha-continuous DECOMP_1:def 28 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff for G being Subset of Y st G is open holds
f " G in X ^alpha );

:: deftheorem Def29 defines ps-continuous DECOMP_1:def 29 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is ps-continuous iff for G being Subset of Y st G is open holds
f " G in PSO X );

:: deftheorem Def30 defines sp-continuous DECOMP_1:def 30 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is sp-continuous iff for G being Subset of Y st G is open holds
f " G in SPO X );

:: deftheorem Def31 defines (c,alpha)-continuous DECOMP_1:def 31 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,alpha)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,alpha) X );

:: deftheorem Def32 defines (c,s)-continuous DECOMP_1:def 32 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,s)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,s) X );

:: deftheorem Def33 defines (c,p)-continuous DECOMP_1:def 33 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,p)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,p) X );

:: deftheorem Def34 defines (c,ps)-continuous DECOMP_1:def 34 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,ps) X );

:: deftheorem Def35 defines (alpha,p)-continuous DECOMP_1:def 35 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,p)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,p) X );

:: deftheorem Def36 defines (alpha,s)-continuous DECOMP_1:def 36 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,s)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,s) X );

:: deftheorem Def37 defines (alpha,ps)-continuous DECOMP_1:def 37 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,ps) X );

:: deftheorem Def38 defines (p,ps)-continuous DECOMP_1:def 38 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (p,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(p,ps) X );

:: deftheorem Def39 defines (p,sp)-continuous DECOMP_1:def 39 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (p,sp)-continuous iff for G being Subset of Y st G is open holds
f " G in D(p,sp) X );

:: deftheorem Def40 defines (sp,ps)-continuous DECOMP_1:def 40 :
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (sp,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(sp,ps) X );

theorem :: DECOMP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) )
proof end;

theorem :: DECOMP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )
proof end;

theorem :: DECOMP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) )
proof end;

theorem :: DECOMP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )
proof end;

theorem :: DECOMP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) )
proof end;

theorem :: DECOMP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) )
proof end;

theorem :: DECOMP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) )
proof end;

theorem :: DECOMP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) )
proof end;

theorem :: DECOMP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) )
proof end;

theorem :: DECOMP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
proof end;

theorem :: DECOMP_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
proof end;