:: by Marian Przemski

::

:: Received December 12, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

definition

let T be TopStruct ;

existence

ex b_{1} being Subset of T st b_{1} c= Int (Cl (Int b_{1}))

end;
existence

ex b

proof end;

let IT be Subset of T;:: deftheorem Def1 defines alpha-set DECOMP_1:def 1 :

for T being TopStruct

for b_{2} being Subset of T holds

( b_{2} is alpha-set of T iff b_{2} c= Int (Cl (Int b_{2})) );

for T being TopStruct

for b

( b

:: deftheorem 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) );

for T being TopStruct

for IT being Subset of T holds

( IT is semi-open iff IT c= Cl (Int IT) );

:: deftheorem 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) );

for T being TopStruct

for IT being Subset of T holds

( IT is pre-open iff IT c= Int (Cl IT) );

:: deftheorem 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)) );

for T being TopStruct

for IT being Subset of T holds

( IT is pre-semi-open iff IT c= Cl (Int (Cl IT)) );

:: deftheorem 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)) );

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;

coherence

B /\ (Cl (Int B)) is Subset of T ;

coherence

B /\ (Int (Cl B)) is Subset of T ;

coherence

B /\ (Int (Cl (Int B))) is Subset of T ;

coherence

B /\ (Cl (Int (Cl B))) is Subset of T ;

end;
let B be Subset of T;

coherence

B /\ (Cl (Int B)) is Subset of T ;

coherence

B /\ (Int (Cl B)) is Subset of T ;

coherence

B /\ (Int (Cl (Int B))) is Subset of T ;

coherence

B /\ (Cl (Int (Cl B))) is Subset of T ;

:: deftheorem defines sInt DECOMP_1:def 6 :

for T being TopStruct

for B being Subset of T holds sInt B = B /\ (Cl (Int B));

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

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

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

for T being TopStruct

for B being Subset of T holds psInt B = B /\ (Cl (Int (Cl B)));

definition
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);

for T being TopStruct

for B being Subset of T holds spInt B = (sInt B) \/ (pInt B);

definition

let T be TopSpace;

{ B where B is Subset of T : B is alpha-set of T } is Subset-Family of T

{ B where B is Subset of T : B is semi-open } is Subset-Family of T

{ B where B is Subset of T : B is pre-open } is Subset-Family of T

{ B where B is Subset of T : B is semi-pre-open } is Subset-Family of T

{ B where B is Subset of T : B is pre-semi-open } is Subset-Family of T

{ B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T

{ B where B is Subset of T : Int B = pInt B } is Subset-Family of T

{ B where B is Subset of T : Int B = sInt B } is Subset-Family of T

{ B where B is Subset of T : Int B = psInt B } is Subset-Family of T

{ B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T

{ B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T

{ B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T

{ B where B is Subset of T : pInt B = spInt B } is Subset-Family of T

{ B where B is Subset of T : pInt B = psInt B } is Subset-Family of T

{ B where B is Subset of T : spInt B = psInt B } is Subset-Family of T

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

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ 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 } ;

{ B where B is Subset of T : spInt B = psInt B } is Subset-Family of T

proof 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 } ;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th2: :: DECOMP_1:2

for T being TopSpace

for B being Subset of T holds

( B is alpha-set of T iff B = alphaInt B ) by Def1, XBOOLE_1:17, XBOOLE_1:28;

for B being Subset of T holds

( B is alpha-set of T iff B = alphaInt B ) by Def1, XBOOLE_1:17, XBOOLE_1:28;

theorem Th3: :: DECOMP_1:3

for T being TopSpace

for B being Subset of T holds

( B is semi-open iff B = sInt B ) by XBOOLE_1:17, XBOOLE_1:28;

for B being Subset of T holds

( B is semi-open iff B = sInt B ) by XBOOLE_1:17, XBOOLE_1:28;

theorem Th4: :: DECOMP_1:4

for T being TopSpace

for B being Subset of T holds

( B is pre-open iff B = pInt B ) by XBOOLE_1:17, XBOOLE_1:28;

for B being Subset of T holds

( B is pre-open iff B = pInt B ) by XBOOLE_1:17, XBOOLE_1:28;

theorem Th5: :: DECOMP_1:5

for T being TopSpace

for B being Subset of T holds

( B is pre-semi-open iff B = psInt B ) by XBOOLE_1:17, XBOOLE_1:28;

for B being Subset of T holds

( B is pre-semi-open iff B = psInt B ) by XBOOLE_1:17, XBOOLE_1:28;

definition

let X, Y be non empty TopSpace;

let f be Function of X,Y;

end;
let f be Function of X,Y;

attr f is s-continuous means :: DECOMP_1:def 26

for G being Subset of Y st G is open holds

f " G in SO X;

for G being Subset of Y st G is open holds

f " G in SO X;

attr f is p-continuous means :: DECOMP_1:def 27

for G being Subset of Y st G is open holds

f " G in PO X;

for G being Subset of Y st G is open holds

f " G in PO X;

attr f is alpha-continuous means :: DECOMP_1:def 28

for G being Subset of Y st G is open holds

f " G in X ^alpha ;

for G being Subset of Y st G is open holds

f " G in X ^alpha ;

attr f is ps-continuous means :: DECOMP_1:def 29

for G being Subset of Y st G is open holds

f " G in PSO X;

for G being Subset of Y st G is open holds

f " G in PSO X;

attr f is sp-continuous means :: DECOMP_1:def 30

for G being Subset of Y st G is open holds

f " G in SPO X;

for G being Subset of Y st G is open holds

f " G in SPO X;

attr f is (c,alpha)-continuous means :: DECOMP_1:def 31

for G being Subset of Y st G is open holds

f " G in D(c,alpha) X;

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 :: DECOMP_1:def 32

for G being Subset of Y st G is open holds

f " G in D(c,s) X;

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 :: DECOMP_1:def 33

for G being Subset of Y st G is open holds

f " G in D(c,p) X;

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 :: DECOMP_1:def 34

for G being Subset of Y st G is open holds

f " G in D(c,ps) X;

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 :: DECOMP_1:def 35

for G being Subset of Y st G is open holds

f " G in D(alpha,p) X;

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 :: DECOMP_1:def 36

for G being Subset of Y st G is open holds

f " G in D(alpha,s) X;

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 :: DECOMP_1:def 37

for G being Subset of Y st G is open holds

f " G in D(alpha,ps) X;

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 :: DECOMP_1:def 38

for G being Subset of Y st G is open holds

f " G in D(p,ps) X;

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 :: DECOMP_1:def 39

for G being Subset of Y st G is open holds

f " G in D(p,sp) X;

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 :: DECOMP_1:def 40

for G being Subset of Y st G is open holds

f " G in D(sp,ps) X;

for G being Subset of Y st G is open holds

f " G in D(sp,ps) X;

:: deftheorem 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 );

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

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

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 ) )

for f being Function of X,Y holds

( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )

proof end;