:: On the Decomposition of the Continuity
::  by Marian Przemski
::
:: Received December 12, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PRE_TOPC, SUBSET_1, TARSKI, TOPS_1, XBOOLE_0, SETFAM_1, RCOMP_1,
      FUNCT_1, RELAT_1, ORDINAL2, DECOMP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1;
 constructors TOPS_1, RELSET_1;
 registrations SUBSET_1, PRE_TOPC, TOPS_1;
 requirements SUBSET;


begin

definition
  let T be TopStruct;
  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 TopStruct;
  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 TopStruct;
  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 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 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 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;
  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 Function 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;