:: DECOMP_1 semantic presentation

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th1: :: DECOMP_1:1
for b1 being TopSpace
for b2 being Subset of b1 holds
( alphaInt b2 = pInt b2 iff sInt b2 = psInt b2 )
proof end;

theorem Th2: :: DECOMP_1:2
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is alpha-set of b1 iff b2 = alphaInt b2 )
proof end;

theorem Th3: :: DECOMP_1:3
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is semi-open iff b2 = sInt b2 )
proof end;

theorem Th4: :: DECOMP_1:4
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is pre-open iff b2 = pInt b2 )
proof end;

theorem Th5: :: DECOMP_1:5
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is pre-semi-open iff b2 = psInt b2 )
proof end;

theorem Th6: :: DECOMP_1:6
for b1 being TopSpace
for b2 being Subset of b1 holds
( b2 is semi-pre-open iff b2 = spInt b2 )
proof end;

theorem Th7: :: DECOMP_1:7
for b1 being TopSpace holds (b1 ^alpha ) /\ (D(c,alpha) b1) = the topology of b1
proof end;

theorem Th8: :: DECOMP_1:8
for b1 being TopSpace holds (SO b1) /\ (D(c,s) b1) = the topology of b1
proof end;

theorem Th9: :: DECOMP_1:9
for b1 being TopSpace holds (PO b1) /\ (D(c,p) b1) = the topology of b1
proof end;

theorem Th10: :: DECOMP_1:10
for b1 being TopSpace holds (PSO b1) /\ (D(c,ps) b1) = the topology of b1
proof end;

theorem Th11: :: DECOMP_1:11
for b1 being TopSpace holds (PO b1) /\ (D(alpha,p) b1) = b1 ^alpha
proof end;

theorem Th12: :: DECOMP_1:12
for b1 being TopSpace holds (SO b1) /\ (D(alpha,s) b1) = b1 ^alpha
proof end;

theorem Th13: :: DECOMP_1:13
for b1 being TopSpace holds (PSO b1) /\ (D(alpha,ps) b1) = b1 ^alpha
proof end;

theorem Th14: :: DECOMP_1:14
for b1 being TopSpace holds (SPO b1) /\ (D(p,sp) b1) = PO b1
proof end;

theorem Th15: :: DECOMP_1:15
for b1 being TopSpace holds (PSO b1) /\ (D(p,ps) b1) = PO b1
proof end;

theorem Th16: :: DECOMP_1:16
for b1 being TopSpace holds (PSO b1) /\ (D(alpha,p) b1) = SO b1
proof end;

theorem Th17: :: DECOMP_1:17
for b1 being TopSpace holds (PSO b1) /\ (D(sp,ps) b1) = SPO b1
proof end;

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

:: deftheorem Def26 defines s-continuous DECOMP_1:def 26 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is s-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in SO b1 );

:: deftheorem Def27 defines p-continuous DECOMP_1:def 27 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is p-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in PO b1 );

:: deftheorem Def28 defines alpha-continuous DECOMP_1:def 28 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is alpha-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in b1 ^alpha );

:: deftheorem Def29 defines ps-continuous DECOMP_1:def 29 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is ps-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in PSO b1 );

:: deftheorem Def30 defines sp-continuous DECOMP_1:def 30 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is sp-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in SPO b1 );

:: deftheorem Def31 defines (c,alpha)-continuous DECOMP_1:def 31 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (c,alpha)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(c,alpha) b1 );

:: deftheorem Def32 defines (c,s)-continuous DECOMP_1:def 32 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (c,s)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(c,s) b1 );

:: deftheorem Def33 defines (c,p)-continuous DECOMP_1:def 33 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (c,p)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(c,p) b1 );

:: deftheorem Def34 defines (c,ps)-continuous DECOMP_1:def 34 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (c,ps)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(c,ps) b1 );

:: deftheorem Def35 defines (alpha,p)-continuous DECOMP_1:def 35 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (alpha,p)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(alpha,p) b1 );

:: deftheorem Def36 defines (alpha,s)-continuous DECOMP_1:def 36 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (alpha,s)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(alpha,s) b1 );

:: deftheorem Def37 defines (alpha,ps)-continuous DECOMP_1:def 37 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (alpha,ps)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(alpha,ps) b1 );

:: deftheorem Def38 defines (p,ps)-continuous DECOMP_1:def 38 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (p,ps)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(p,ps) b1 );

:: deftheorem Def39 defines (p,sp)-continuous DECOMP_1:def 39 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (p,sp)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(p,sp) b1 );

:: deftheorem Def40 defines (sp,ps)-continuous DECOMP_1:def 40 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is (sp,ps)-continuous iff for b4 being Subset of b2 st b4 is open holds
b3 " b4 in D(sp,ps) b1 );

theorem Th18: :: DECOMP_1:18
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is alpha-continuous iff ( b3 is p-continuous & b3 is (alpha,p)-continuous ) )
proof end;

theorem Th19: :: DECOMP_1:19
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is alpha-continuous iff ( b3 is s-continuous & b3 is (alpha,s)-continuous ) )
proof end;

theorem Th20: :: DECOMP_1:20
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is alpha-continuous iff ( b3 is ps-continuous & b3 is (alpha,ps)-continuous ) )
proof end;

theorem Th21: :: DECOMP_1:21
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is p-continuous iff ( b3 is sp-continuous & b3 is (p,sp)-continuous ) )
proof end;

theorem Th22: :: DECOMP_1:22
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is p-continuous iff ( b3 is ps-continuous & b3 is (p,ps)-continuous ) )
proof end;

theorem Th23: :: DECOMP_1:23
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is s-continuous iff ( b3 is ps-continuous & b3 is (alpha,p)-continuous ) )
proof end;

theorem Th24: :: DECOMP_1:24
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is sp-continuous iff ( b3 is ps-continuous & b3 is (sp,ps)-continuous ) )
proof end;

theorem Th25: :: DECOMP_1:25
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is continuous iff ( b3 is alpha-continuous & b3 is (c,alpha)-continuous ) )
proof end;

theorem Th26: :: DECOMP_1:26
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is continuous iff ( b3 is s-continuous & b3 is (c,s)-continuous ) )
proof end;

theorem Th27: :: DECOMP_1:27
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is continuous iff ( b3 is p-continuous & b3 is (c,p)-continuous ) )
proof end;

theorem Th28: :: DECOMP_1:28
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is continuous iff ( b3 is ps-continuous & b3 is (c,ps)-continuous ) )
proof end;