The abstract of the Mizar article:

On the Decomposition of the Continuity

by

Marian Przemski

Received December 12, 1994

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;