:: On the Decomposition of the Continuity :: by Marian Przemski :: :: Received December 12, 1994 :: Copyright (c) 1994-2018 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;