Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### On the Decomposition of the Continuity

by
Marian Przemski

MML identifier: DECOMP_1
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, TOPS_1, BOOLE, SETFAM_1, RELAT_1, ORDINAL2, DECOMP_1;
notation TARSKI, ZFMISC_1, PRE_TOPC, STRUCT_0, TOPS_1;
constructors TOPS_1, MEMBERED, XBOOLE_0;
clusters PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0;
requirements BOOLE, SUBSET;

begin

definition
let T be non empty TopSpace;
mode alpha-set of T -> Subset of T means
:: DECOMP_1:def 1
it c= Int Cl Int it;
let IT be Subset of T;
attr IT is semi-open means
:: DECOMP_1:def 2
IT c= Cl Int IT;
attr IT is pre-open means
:: DECOMP_1:def 3
IT c= Int Cl IT;
attr IT is pre-semi-open means
:: DECOMP_1:def 4
IT c= Cl Int Cl IT;
attr IT is semi-pre-open means
:: DECOMP_1:def 5
IT c= Cl Int IT \/ Int Cl IT;
end;

definition
let T be non empty TopSpace;
let B be Subset of T;
func sInt B -> Subset of T equals
:: DECOMP_1:def 6
B /\ Cl Int B;
func pInt B -> Subset of T equals
:: DECOMP_1:def 7
B /\ Int Cl B;
func alphaInt B -> Subset of T equals
:: DECOMP_1:def 8
B /\ Int Cl Int B;
func psInt B -> Subset of T equals
:: DECOMP_1:def 9
B /\ Cl Int Cl B;
end;

definition
let T be non empty TopSpace;
let B be Subset of T;
func spInt B -> Subset of T equals
:: DECOMP_1:def 10
sInt B \/ pInt B;
end;

definition
let T be non empty 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};

func SO T -> Subset-Family of T equals
:: DECOMP_1:def 12
{B where B is Subset of T : B is semi-open};

func PO T -> Subset-Family of T equals
:: DECOMP_1:def 13
{B where B is Subset of T : B is pre-open};

func SPO T -> Subset-Family of T equals
:: DECOMP_1:def 14
{B where B is Subset of T:B is semi-pre-open};

func PSO T -> Subset-Family of T equals
:: DECOMP_1:def 15
{B where B is Subset of T:B is pre-semi-open};

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

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

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

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

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

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

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

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

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

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

reserve T for non empty TopSpace,
B for Subset of T;

theorem :: DECOMP_1:1
alphaInt B = pInt B iff sInt B = psInt B;

theorem :: DECOMP_1:2
B is alpha-set of T iff B = alphaInt B;

theorem :: DECOMP_1:3
B is semi-open iff B = sInt B;

theorem :: DECOMP_1:4
B is pre-open iff B = pInt B;

theorem :: DECOMP_1:5
B is pre-semi-open iff B = psInt B;

theorem :: DECOMP_1:6
B is semi-pre-open iff B = spInt B;

theorem :: DECOMP_1:7
T^alpha /\ D(c,alpha)(T) = the topology of T;

theorem :: DECOMP_1:8
SO T /\ D(c,s)(T) = the topology of T;

theorem :: DECOMP_1:9
PO T /\ D(c,p)(T) = the topology of T;

theorem :: DECOMP_1:10
PSO T /\ D(c,ps)(T) = the topology of T;

theorem :: DECOMP_1:11
PO T /\ D(alpha,p)(T) = T^alpha;

theorem :: DECOMP_1:12
SO T /\ D(alpha,s)(T) = T^alpha;

theorem :: DECOMP_1:13
PSO T /\ D(alpha,ps)(T) = T^alpha;

theorem :: DECOMP_1:14
SPO T /\ D(p,sp)(T) = PO T;

theorem :: DECOMP_1:15
PSO T /\ D(p,ps)(T) = PO T;

theorem :: DECOMP_1:16
PSO T /\ D(alpha,p)(T) = SO T;

theorem :: DECOMP_1:17
PSO T /\ D(sp,ps)(T) = SPO T;

definition let X,Y be non empty TopSpace; let f be map 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;
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;
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;
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;
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;
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
end;

reserve X,Y for non empty TopSpace; reserve f for map of X,Y;

theorem :: DECOMP_1:18
f is alpha-continuous iff f is p-continuous (alpha,p)-continuous;

theorem :: DECOMP_1:19
f is alpha-continuous iff f is s-continuous (alpha,s)-continuous;

theorem :: DECOMP_1:20
f is alpha-continuous iff f is ps-continuous (alpha,ps)-continuous;

theorem :: DECOMP_1:21
f is p-continuous iff f is sp-continuous (p,sp)-continuous;

theorem :: DECOMP_1:22
f is p-continuous iff f is ps-continuous (p,ps)-continuous;

theorem :: DECOMP_1:23
f is s-continuous iff f is ps-continuous (alpha,p)-continuous;

theorem :: DECOMP_1:24
f is sp-continuous iff f is ps-continuous (sp,ps)-continuous;

theorem :: DECOMP_1:25
f is continuous iff f is alpha-continuous (c,alpha)-continuous;

theorem :: DECOMP_1:26
f is continuous iff f is s-continuous (c,s)-continuous;

theorem :: DECOMP_1:27
f is continuous iff f is p-continuous (c,p)-continuous;

theorem :: DECOMP_1:28
f is continuous iff f is ps-continuous (c,ps)-continuous;

```