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