:: On the Decomposition of the Continuity :: by Marian Przemski :: :: Received December 12, 1994 :: Copyright (c) 1994-2017 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; definitions TARSKI, XBOOLE_0; equalities XBOOLE_0, STRUCT_0; expansions TARSKI, XBOOLE_0; theorems TOPS_1, PRE_TOPC, TOPS_2, XBOOLE_0, XBOOLE_1; schemes DOMAIN_1; begin definition let T be TopStruct; mode alpha-set of T -> Subset of T means :Def1: it c= Int Cl Int it; existence proof take {} T; thus thesis by XBOOLE_1:2; end; let IT be Subset of T; attr IT is semi-open means IT c= Cl Int IT; attr IT is pre-open means IT c= Int Cl IT; attr IT is pre-semi-open means IT c= Cl Int Cl IT; attr IT is semi-pre-open means 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 B /\ Cl Int B; coherence; func pInt B -> Subset of T equals B /\ Int Cl B; coherence; func alphaInt B -> Subset of T equals B /\ Int Cl Int B; coherence; func psInt B -> Subset of T equals B /\ Cl Int Cl B; coherence; end; definition let T be TopStruct; let B be Subset of T; func spInt B -> Subset of T equals sInt B \/ pInt B; coherence; end; definition let T be TopSpace; func T^alpha -> Subset-Family of T equals {B where B is Subset of T: B is alpha-set of T}; coherence proof defpred P[set] means \$1 is alpha-set of T; {B where B is Subset of T : P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func SO T -> Subset-Family of T equals {B where B is Subset of T : B is semi-open}; coherence proof defpred P[Subset of T] means \$1 is semi-open; {B where B is Subset of T : P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func PO T -> Subset-Family of T equals {B where B is Subset of T : B is pre-open}; coherence proof defpred P[Subset of T] means \$1 is pre-open; {B where B is Subset of T : P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func SPO T -> Subset-Family of T equals {B where B is Subset of T:B is semi-pre-open}; coherence proof defpred P[Subset of T] means \$1 is semi-pre-open; {B where B is Subset of T : P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func PSO T -> Subset-Family of T equals {B where B is Subset of T:B is pre-semi-open}; coherence proof defpred P[Subset of T] means \$1 is pre-semi-open; {B where B is Subset of T : P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(c,alpha)(T) -> Subset-Family of T equals {B where B is Subset of T: Int B = alphaInt B}; coherence proof defpred P[Subset of T] means Int \$1 = alphaInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(c,p)(T) -> Subset-Family of T equals {B where B is Subset of T: Int B = pInt B}; coherence proof defpred P[Subset of T] means Int \$1 = pInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(c,s)(T) -> Subset-Family of T equals {B where B is Subset of T: Int B = sInt B}; coherence proof defpred P[Subset of T] means Int \$1 = sInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(c,ps)(T) -> Subset-Family of T equals {B where B is Subset of T: Int B = psInt B}; coherence proof defpred P[Subset of T] means Int \$1 = psInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(alpha,p)(T) -> Subset-Family of T equals {B where B is Subset of T: alphaInt B = pInt B}; coherence proof defpred P[Subset of T] means alphaInt \$1 = pInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(alpha,s)(T) -> Subset-Family of T equals {B where B is Subset of T: alphaInt B = sInt B}; coherence proof defpred P[Subset of T] means alphaInt \$1 = sInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(alpha,ps)(T) -> Subset-Family of T equals {B where B is Subset of T: alphaInt B = psInt B}; coherence proof defpred P[Subset of T] means alphaInt \$1 = psInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(p,sp)(T) -> Subset-Family of T equals {B where B is Subset of T: pInt B = spInt B}; coherence proof defpred P[Subset of T] means pInt \$1 = spInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(p,ps)(T) -> Subset-Family of T equals {B where B is Subset of T: pInt B = psInt B}; coherence proof defpred P[Subset of T] means pInt \$1 = psInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; func D(sp,ps)(T) -> Subset-Family of T equals {B where B is Subset of T: spInt B = psInt B}; coherence proof defpred P[Subset of T] means spInt \$1 = psInt \$1; {B where B is Subset of T: P[B]} is Subset-Family of T from DOMAIN_1: sch 7; hence thesis; end; end; reserve T for TopSpace, B for Subset of T; theorem Th1: alphaInt B = pInt B iff sInt B = psInt B proof hereby Cl Int B c= Cl B by PRE_TOPC:19,TOPS_1:16; then Int Cl Int B c= Int Cl B by TOPS_1:19; then Cl Int Cl Int B c= Cl Int Cl B by PRE_TOPC:19; then Cl Int B c= Cl Int Cl B by TOPS_1:26; then A1: sInt B c= B /\ Cl Int Cl B by XBOOLE_1:26; assume alphaInt B = pInt B; then Cl (B /\ Int Cl B) c= Cl( Int Cl Int B) by PRE_TOPC:19,XBOOLE_1:17; then A2: Cl (B /\ Int Cl B) c= Cl Int B by TOPS_1:26; Cl(B /\ Int Cl B) = Cl(Cl B /\ Int Cl B) by TOPS_1:14; then Cl(B /\ Int Cl B) = Cl Int Cl B by TOPS_1:16,XBOOLE_1:28; then B /\ Cl Int Cl B c= B /\ Cl Int B by A2,XBOOLE_1:26; hence sInt B = psInt B by A1; end; A3: Int Cl B c= Cl Int Cl B by PRE_TOPC:18; assume psInt B = sInt B; then A4: psInt B c= Cl Int B by XBOOLE_1:17; B /\ Int Cl B c= B /\ Cl Int Cl B by PRE_TOPC:18,XBOOLE_1:26; then B /\ Int Cl B c= Cl Int B by A4; then A5: Cl(B /\ Int Cl B) c= Cl Cl Int B by PRE_TOPC:19; Cl(B /\ Int Cl B) = Cl(Cl B /\ Int Cl B) by TOPS_1:14; then Cl Int Cl B c= Cl Int B by A5,TOPS_1:16,XBOOLE_1:28; then Int Cl B c= Cl Int B by A3; then Int Int Cl B c= Int Cl Int B by TOPS_1:19; then A6: B /\ Int Cl B c= B /\ Int Cl Int B by XBOOLE_1:26; Cl Int B c= Cl B by PRE_TOPC:19,TOPS_1:16; then Int Cl Int B c= Int Cl B by TOPS_1:19; then alphaInt B c= B /\ Int Cl B by XBOOLE_1:26; hence thesis by A6; end; theorem Th2: B is alpha-set of T iff B = alphaInt B by Def1,XBOOLE_1:17,28; theorem Th3: B is semi-open iff B = sInt B by XBOOLE_1:17,28; theorem Th4: B is pre-open iff B = pInt B by XBOOLE_1:17,28; theorem Th5: B is pre-semi-open iff B = psInt B by XBOOLE_1:17,28; theorem Th6: B is semi-pre-open iff B = spInt B proof hereby assume B is semi-pre-open; then B = B /\ (Cl Int B \/ Int Cl B) by XBOOLE_1:28; hence B = spInt B by XBOOLE_1:23; end; assume B = spInt B; then B = B /\ (Cl Int B \/ Int Cl B) by XBOOLE_1:23; hence thesis by XBOOLE_1:17; end; theorem Th7: T^alpha /\ D(c,alpha)(T) = the topology of T proof thus T^alpha /\ D(c,alpha)(T) c= the topology of T proof let x be object; assume A1: x in T^alpha /\ D(c,alpha)(T); then x in T^alpha by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is alpha-set of T; x in D(c,alpha)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: Int Z = alphaInt Z; A = alphaInt A by A3,Th2; then Z is open by A2,A4,A5; hence thesis by A4,PRE_TOPC:def 2; end; let x be object; assume A6: x in the topology of T; then reconsider K = x as Subset of T; K is open by A6,PRE_TOPC:def 2; then A7: K = Int K by TOPS_1:23; then K c= Int Cl Int K by PRE_TOPC:18,TOPS_1:19; then A8: K is alpha-set of T by Def1; then Int K = alphaInt K by A7,Th2; then A9: K in {B: Int B = alphaInt B}; K in T^alpha by A8; hence thesis by A9,XBOOLE_0:def 4; end; theorem Th8: SO T /\ D(c,s)(T) = the topology of T proof thus SO T /\ D(c,s)(T) c= the topology of T proof let x be object; assume A1: x in SO T /\ D(c,s)(T); then x in SO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is semi-open; x in D(c,s)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: Int Z = sInt Z; A = sInt A by A3,Th3; hence thesis by A4,PRE_TOPC:def 2,A2,A5; end; let x be object; assume A6: x in the topology of T; then reconsider K = x as Subset of T; K is open by A6,PRE_TOPC:def 2; then A7: K = Int K by TOPS_1:23; then A8: K is semi-open by PRE_TOPC:18; then Int K = sInt K by A7,Th3; then A9: K in {B: Int B = sInt B}; K in SO T by A8; hence thesis by A9,XBOOLE_0:def 4; end; theorem Th9: PO T /\ D(c,p)(T) = the topology of T proof thus PO T /\ D(c,p)(T) c= the topology of T proof let x be object; assume A1: x in PO T /\ D(c,p)(T); then x in PO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is pre-open; x in D(c,p)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: Int Z = pInt Z; A = pInt A by A3,Th4; hence thesis by A4,PRE_TOPC:def 2,A2,A5; end; let x be object; assume A6: x in the topology of T; then reconsider K = x as Subset of T; K is open by A6,PRE_TOPC:def 2; then A7: K = Int K by TOPS_1:23; then A8: K is pre-open by PRE_TOPC:18,TOPS_1:19; then Int K = pInt K by A7,Th4; then A9: K in {B: Int B = pInt B}; K in PO T by A8; hence thesis by A9,XBOOLE_0:def 4; end; theorem Th10: PSO T /\ D(c,ps)(T) = the topology of T proof thus PSO T /\ D(c,ps)(T) c= the topology of T proof let x be object; assume A1: x in PSO T /\ D(c,ps)(T); then x in PSO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is pre-semi-open; x in D(c,ps)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: Int Z = psInt Z; A = psInt A by A3,Th5; hence thesis by A4,PRE_TOPC:def 2,A2,A5; end; let x be object; assume A6: x in the topology of T; then reconsider K = x as Subset of T; A7: Int Cl K c= Cl Int Cl K by PRE_TOPC:18; K is open by A6,PRE_TOPC:def 2; then A8: K = Int K by TOPS_1:23; then K c= Int Cl K by PRE_TOPC:18,TOPS_1:19; then K c= Cl Int Cl K by A7; then A9: K is pre-semi-open; then Int K = psInt K by A8,Th5; then A10: K in {B: Int B = psInt B}; K in PSO T by A9; hence thesis by A10,XBOOLE_0:def 4; end; theorem Th11: PO T /\ D(alpha,p)(T) = T^alpha proof thus PO T /\ D(alpha,p)(T) c= T^alpha proof let x be object; assume A1: x in PO T /\ D(alpha,p)(T); then x in PO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is pre-open; x in D(alpha,p)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: alphaInt Z = pInt Z; A = pInt A by A3,Th4; then Z is alpha-set of T by A2,A4,A5,Th2; hence thesis by A4; end; let x be object; assume x in T^alpha; then consider K being Subset of T such that A6: x = K and A7: K is alpha-set of T; Cl Int K c= Cl K by PRE_TOPC:19,TOPS_1:16; then A8: Int Cl Int K c= Int Cl K by TOPS_1:19; K c= Int Cl Int K by A7,Def1; then K c= Int Cl K by A8; then A9: K is pre-open; then K = pInt K by Th4; then alphaInt K = pInt K by A7,Th2; then A10: K in {B: alphaInt B = pInt B}; K in PO T by A9; hence thesis by A6,A10,XBOOLE_0:def 4; end; theorem Th12: SO T /\ D(alpha,s)(T) = T^alpha proof thus SO T /\ D(alpha,s)(T) c= T^alpha proof let x be object; assume A1: x in SO T /\ D(alpha,s)(T); then x in SO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is semi-open; x in D(alpha,s)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: alphaInt Z = sInt Z; Z is alpha-set of T by A2,A4,A5,Th2,A3,Th3; hence thesis by A4; end; let x be object; assume x in T^alpha; then consider K being Subset of T such that A6: x = K and A7: K is alpha-set of T; A8: Int Cl Int K c= Cl Int K by TOPS_1:16; K c= Int Cl Int K by A7,Def1; then K c= Cl Int K by A8; then A9: K is semi-open; then K = sInt K by Th3; then alphaInt K = sInt K by A7,Th2; then A10: K in {B: alphaInt B = sInt B}; K in {B:B is semi-open} by A9; hence thesis by A6,A10,XBOOLE_0:def 4; end; theorem Th13: PSO T /\ D(alpha,ps)(T) = T^alpha proof thus PSO T /\ D(alpha,ps)(T) c= T^alpha proof let x be object; assume A1: x in PSO T /\ D(alpha,ps)(T); then x in PSO T by XBOOLE_0:def 4; then consider A being Subset of T such that A2: x = A and A3: A is pre-semi-open; x in D(alpha,ps)(T) by A1,XBOOLE_0:def 4; then consider Z being Subset of T such that A4: x = Z and A5: alphaInt Z = psInt Z; A = psInt A by A3,Th5; then Z is alpha-set of T by A2,A4,A5,Th2; hence thesis by A4; end; let x be object; assume x in T^alpha; then consider K being Subset of T such that A6: x = K and A7: K is alpha-set of T; Cl Int K c= Cl K by PRE_TOPC:19,TOPS_1:16; then A8: Int Cl Int K c= Int Cl K by TOPS_1:19; Int Cl K c= Cl Int Cl K by PRE_TOPC:18; then A9: Int Cl Int K c= Cl Int Cl K by A8; K c= Int Cl Int K by A7,Def1; then K c= Cl Int Cl K by A9; then A10: K is pre-semi-open; then K = psInt K by Th5; then alphaInt K = psInt K by A7,Th2; then A11: K in {B: alphaInt B = psInt B}; K in PSO T by A10; hence thesis by A6,A11,XBOOLE_0:def 4; end; theorem Th14: SPO T /\ D(p,sp)(T) = PO T proof thus SPO T /\ D(p,sp)(T) c= PO T proof let x be object; assume x in SPO T /\ D(p,sp)(T); then A0: x in SPO T & x in D(p,sp)(T) by XBOOLE_0:def 4; then consider B being Subset of T such that A1: x = B & B is semi-pre-open; A3: B = spInt B by A1,Th6; consider B1 being Subset of T such that A2: x = B1 & pInt B1 = spInt B1 by A0; pInt B = B by A2,A3,A1; then B is pre-open by Th4; hence thesis by A1; end; let x be object; assume x in PO T; then consider K being Subset of T such that A1: x = K and A2: K is pre-open; A3: Int Cl K c= Cl Int K \/ Int Cl K by XBOOLE_1:7; K c= Int Cl K by A2; then K c= Cl Int K \/ Int Cl K by A3; then A4: K is semi-pre-open; then K = spInt K by Th6; then pInt K = spInt K by A2,Th4; then A5: K in {B: pInt B = spInt B}; K in SPO T by A4; hence thesis by A1,A5,XBOOLE_0:def 4; end; theorem Th15: PSO T /\ D(p,ps)(T) = PO T proof thus PSO T /\ D(p,ps)(T) c= PO T proof let x be object; assume x in PSO T /\ D(p,ps)(T); then A0: x in PSO T & x in D(p,ps)(T) by XBOOLE_0:def 4; then consider B being Subset of T such that A1: x = B & B is pre-semi-open; A3: B = psInt B by A1,Th5; consider B1 being Subset of T such that A2: x = B1 & pInt B1 = psInt B1 by A0; pInt B = B by A2,A3,A1; then B is pre-open by Th4; then x in {B where B is Subset of T: B is pre-open} by A1; hence thesis; end; let x be object; assume x in PO T; then consider K being Subset of T such that A1: x = K and A2: K is pre-open; Int Cl K c= Cl Int Cl K by PRE_TOPC:18; then K c= Cl Int Cl K by A2; then A4: K is pre-semi-open; then K = psInt K by Th5; then pInt K = psInt K by A2,Th4; then A5: K in {B: pInt B = psInt B}; K in PSO T by A4; hence thesis by A1,A5,XBOOLE_0:def 4; end; theorem Th16: PSO T /\ D(alpha,p)(T) = SO T proof thus PSO T /\ D(alpha,p)(T) c= SO T proof let x be object; assume x in PSO T /\ D(alpha,p)(T); then A0: x in PSO T & x in D(alpha,p)(T) by XBOOLE_0:def 4; then consider B being Subset of T such that A1: x = B & B is pre-semi-open; A3: B = psInt B by A1,Th5; consider B1 being Subset of T such that A2: x = B1 & alphaInt B1 = pInt B1 by A0; sInt B = psInt B by A2,A1,Th1; then sInt B = B by A3; then B is semi-open by Th3; then x in SO T by A1; hence thesis; end; let x be object; assume x in SO T; then consider K being Subset of T such that A1: x = K and A2: K is semi-open; Cl Int K c= Cl K by PRE_TOPC:19,TOPS_1:16; then Int Cl Int K c= Int Cl K by TOPS_1:19; then Cl Int Cl Int K c= Cl Int Cl K by PRE_TOPC:19; then Cl Int K c= Cl Int Cl K by TOPS_1:26; then K c= Cl Int Cl K by A2; then A4: K is pre-semi-open; then K = psInt K by Th5; then sInt K = psInt K by A2,Th3; then alphaInt K = pInt K by Th1; then A5: K in {B: alphaInt B = pInt B}; K in PSO T by A4; hence thesis by A1,A5,XBOOLE_0:def 4; end; theorem Th17: PSO T /\ D(sp,ps)(T) = SPO T proof thus PSO T /\ D(sp,ps)(T) c= SPO T proof let x be object; assume x in PSO T /\ D(sp,ps)(T); then A0: x in PSO T & x in D(sp,ps)(T) by XBOOLE_0:def 4; then consider B being Subset of T such that A1: x = B & B is pre-semi-open; A3: B = psInt B by A1,Th5; consider B1 being Subset of T such that A2: x = B1 & spInt B1 = psInt B1 by A0; B is semi-pre-open by A1,A2,A3,Th6; hence thesis by A1; end; let x be object; assume x in SPO T; then consider K being Subset of T such that A1: x = K and A2: K is semi-pre-open; Cl Int K c= Cl K by PRE_TOPC:19,TOPS_1:16; then Int Cl Int K c= Int Cl K by TOPS_1:19; then Cl Int Cl Int K c= Cl Int Cl K by PRE_TOPC:19; then A3: Cl Int K c= Cl Int Cl K by TOPS_1:26; Int Cl K c= Cl Int Cl K by PRE_TOPC:18; then Cl Int K \/ Int Cl K c= Cl Int Cl K by A3,XBOOLE_1:8; then K c= Cl Int Cl K by A2; then A5: K is pre-semi-open; then K = psInt K by Th5; then spInt K = psInt K by A2,Th6; then A6: K in {B: spInt B = psInt B}; K in PSO T by A5; hence thesis by A1,A6,XBOOLE_0:def 4; end; definition let X,Y be non empty TopSpace; let f be Function of X,Y; attr f is s-continuous means for G being Subset of Y st G is open holds f"G in SO X; attr f is p-continuous means for G being Subset of Y st G is open holds f"G in PO X; attr f is alpha-continuous means for G being Subset of Y st G is open holds f"G in X^alpha; attr f is ps-continuous means for G being Subset of Y st G is open holds f"G in PSO X; attr f is sp-continuous means for G being Subset of Y st G is open holds f"G in SPO X; attr f is (c,alpha)-continuous means 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 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 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 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 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 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 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 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 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 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 f is alpha-continuous iff f is p-continuous (alpha,p)-continuous proof hereby assume A1: f is alpha-continuous; thus f is p-continuous proof let V be Subset of Y; assume V is open; then f"V in X^alpha by A1; then f"V in PO X /\ D(alpha,p)(X) by Th11; hence thesis by XBOOLE_0:def 4; end; thus f is (alpha,p)-continuous proof let G be Subset of Y; assume G is open; then f"G in X^alpha by A1; then f"G in PO X /\ D(alpha,p)(X) by Th11; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is p-continuous (alpha,p)-continuous; let V be Subset of Y; assume V is open; then f"V in PO X & f"V in D(alpha,p)(X) by A2; then f"V in PO X /\ D(alpha,p)(X) by XBOOLE_0:def 4; hence thesis by Th11; end; theorem f is alpha-continuous iff f is s-continuous (alpha,s)-continuous proof hereby assume A1: f is alpha-continuous; thus f is s-continuous proof let V be Subset of Y; assume V is open; then f"V in X^alpha by A1; then f"V in SO X /\ D(alpha,s)(X) by Th12; hence thesis by XBOOLE_0:def 4; end; thus f is (alpha,s)-continuous proof let G be Subset of Y; assume G is open; then f"G in X^alpha by A1; then f"G in SO X /\ D(alpha,s)(X) by Th12; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is s-continuous (alpha,s)-continuous; let V be Subset of Y; assume V is open; then f"V in SO X & f"V in D(alpha,s)(X) by A2; then f"V in SO X /\ D(alpha,s)(X) by XBOOLE_0:def 4; hence thesis by Th12; end; theorem f is alpha-continuous iff f is ps-continuous (alpha,ps)-continuous proof hereby assume A1: f is alpha-continuous; thus f is ps-continuous proof let V be Subset of Y; assume V is open; then f"V in X^alpha by A1; then f"V in PSO X /\ D(alpha,ps)(X) by Th13; hence thesis by XBOOLE_0:def 4; end; thus f is (alpha,ps)-continuous proof let G be Subset of Y; assume G is open; then f"G in X^alpha by A1; then f"G in PSO X /\ D(alpha,ps)(X) by Th13; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is ps-continuous (alpha,ps)-continuous; let V be Subset of Y; assume V is open; then f"V in PSO X & f"V in D(alpha,ps)(X) by A2; then f"V in PSO X /\ D(alpha,ps)(X) by XBOOLE_0:def 4; hence thesis by Th13; end; theorem f is p-continuous iff f is sp-continuous (p,sp)-continuous proof hereby assume A1: f is p-continuous; thus f is sp-continuous proof let V be Subset of Y; assume V is open; then f"V in PO X by A1; then f"V in SPO X /\ D(p,sp)(X) by Th14; hence f"V in SPO X by XBOOLE_0:def 4; end; thus f is (p,sp)-continuous proof let G be Subset of Y; assume G is open; then f"G in PO X by A1; then f"G in SPO X /\ D(p,sp)(X) by Th14; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is sp-continuous (p,sp)-continuous; let V be Subset of Y; assume V is open; then f"V in SPO X & f"V in D(p,sp)(X) by A2; then f"V in SPO X /\ D(p,sp)(X) by XBOOLE_0:def 4; hence thesis by Th14; end; theorem f is p-continuous iff f is ps-continuous (p,ps)-continuous proof hereby assume A1: f is p-continuous; thus f is ps-continuous proof let V be Subset of Y; assume V is open; then f"V in PO X by A1; then f"V in PSO X /\ D(p,ps)(X) by Th15; hence f"V in PSO X by XBOOLE_0:def 4; end; thus f is (p,ps)-continuous proof let G be Subset of Y; assume G is open; then f"G in PO X by A1; then f"G in PSO X /\ D(p,ps)(X) by Th15; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is ps-continuous (p,ps)-continuous; let V be Subset of Y; assume V is open; then f"V in PSO X & f"V in D(p,ps)(X) by A2; then f"V in PSO X /\ D(p,ps)(X) by XBOOLE_0:def 4; hence thesis by Th15; end; theorem f is s-continuous iff f is ps-continuous (alpha,p)-continuous proof hereby assume A1: f is s-continuous; thus f is ps-continuous proof let V be Subset of Y; assume V is open; then f"V in SO X by A1; then f"V in PSO X /\ D(alpha,p)(X) by Th16; hence f"V in PSO X by XBOOLE_0:def 4; end; thus f is (alpha,p)-continuous proof let G be Subset of Y; assume G is open; then f"G in SO X by A1; then f"G in PSO X /\ D(alpha,p)(X) by Th16; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is ps-continuous (alpha,p)-continuous; let V be Subset of Y; assume V is open; then f"V in PSO X & f"V in D(alpha,p)(X) by A2; then f"V in PSO X /\ D(alpha,p)(X) by XBOOLE_0:def 4; hence thesis by Th16; end; theorem f is sp-continuous iff f is ps-continuous (sp,ps)-continuous proof hereby assume A1: f is sp-continuous; thus f is ps-continuous proof let V be Subset of Y; assume V is open; then f"V in SPO X by A1; then f"V in PSO X /\ D(sp,ps)(X) by Th17; hence f"V in PSO X by XBOOLE_0:def 4; end; thus f is (sp,ps)-continuous proof let G be Subset of Y; assume G is open; then f"G in SPO X by A1; then f"G in PSO X /\ D(sp,ps)(X) by Th17; hence thesis by XBOOLE_0:def 4; end; end; assume A2: f is ps-continuous (sp,ps)-continuous; let V be Subset of Y; assume V is open; then f"V in PSO X & f"V in D(sp,ps)(X) by A2; then f"V in PSO X /\ D(sp,ps)(X) by XBOOLE_0:def 4; hence thesis by Th17; end; theorem f is continuous iff f is alpha-continuous (c,alpha)-continuous proof A1: [#]Y <> {}; hereby assume A2: f is continuous; thus f is alpha-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in X^alpha /\ D(c,alpha)(X) by Th7; hence thesis by XBOOLE_0:def 4; end; thus f is (c,alpha)-continuous proof let G be Subset of Y; assume G is open; then f"G is open by A1,A2,TOPS_2:43; then f"G in the topology of X by PRE_TOPC:def 2; then f"G in X^alpha /\ D(c,alpha)(X) by Th7; hence thesis by XBOOLE_0:def 4; end; end; assume A3: f is alpha-continuous (c,alpha)-continuous; now let V be Subset of Y; assume V is open; then f"V in X^alpha & f"V in D(c,alpha)(X) by A3; then f"V in X^alpha /\ D(c,alpha)(X) by XBOOLE_0:def 4; then f"V in the topology of X by Th7; hence f"V is open by PRE_TOPC:def 2; end; hence thesis by A1,TOPS_2:43; end; theorem f is continuous iff f is s-continuous (c,s)-continuous proof A1: [#]Y <> {}; hereby assume A2: f is continuous; thus f is s-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in SO X /\ D(c,s)(X) by Th8; hence thesis by XBOOLE_0:def 4; end; thus f is (c,s)-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in SO X /\ D(c,s)(X) by Th8; hence thesis by XBOOLE_0:def 4; end; end; assume A3: f is s-continuous (c,s)-continuous; now let V be Subset of Y; assume V is open; then f"V in SO X & f"V in D(c,s)(X) by A3; then f"V in SO X /\ D(c,s)(X) by XBOOLE_0:def 4; then f"V in the topology of X by Th8; hence f"V is open by PRE_TOPC:def 2; end; hence thesis by A1,TOPS_2:43; end; theorem f is continuous iff f is p-continuous (c,p)-continuous proof A1: [#]Y <> {}; hereby assume A2: f is continuous; thus f is p-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in PO X /\ D(c,p)(X) by Th9; hence thesis by XBOOLE_0:def 4; end; thus f is (c,p)-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in PO X /\ D(c,p)(X) by Th9; hence thesis by XBOOLE_0:def 4; end; end; assume A3: f is p-continuous (c,p)-continuous; now let V be Subset of Y; assume V is open; then f"V in PO X & f"V in D(c,p)(X) by A3; then f"V in PO X /\ D(c,p)(X) by XBOOLE_0:def 4; then f"V in the topology of X by Th9; hence f"V is open by PRE_TOPC:def 2; end; hence thesis by A1,TOPS_2:43; end; theorem f is continuous iff f is ps-continuous (c,ps)-continuous proof A1: [#]Y <> {}; hereby assume A2: f is continuous; thus f is ps-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in PSO X /\ D(c,ps)(X) by Th10; hence thesis by XBOOLE_0:def 4; end; thus f is (c,ps)-continuous proof let V be Subset of Y; assume V is open; then f"V is open by A1,A2,TOPS_2:43; then f"V in the topology of X by PRE_TOPC:def 2; then f"V in PSO X /\ D(c,ps)(X) by Th10; hence thesis by XBOOLE_0:def 4; end; end; assume A3: f is ps-continuous (c,ps)-continuous; now let V be Subset of Y; assume V is open; then f"V in PSO X & f"V in D(c,ps)(X) by A3; then f"V in PSO X /\ D(c,ps)(X) by XBOOLE_0:def 4; then f"V in the topology of X by Th10; hence f"V is open by PRE_TOPC:def 2; end; hence thesis by A1,TOPS_2:43; end;