Copyright (c) 1994 Association of Mizar Users
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;
definitions TARSKI, XBOOLE_0;
theorems TOPS_1, PRE_TOPC, TOPS_2, SETFAM_1, XBOOLE_0, XBOOLE_1;
begin
definition
let T be non empty TopSpace;
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
:Def2: IT c= Cl Int IT;
attr IT is pre-open means
:Def3: IT c= Int Cl IT;
attr IT is pre-semi-open means
:Def4: IT c= Cl Int Cl IT;
attr IT is semi-pre-open means
:Def5: 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
:Def6: B /\ Cl Int B;
correctness;
func pInt B -> Subset of T equals
:Def7: B /\ Int Cl B;
correctness;
func alphaInt B -> Subset of T equals
:Def8: B /\ Int Cl Int B;
correctness;
func psInt B -> Subset of T equals
:Def9: B /\ Cl Int Cl B;
correctness;
end;
definition
let T be non empty TopSpace;
let B be Subset of T;
func spInt B -> Subset of T equals
:Def10: sInt B \/ pInt B;
correctness;
end;
SubsetSD{D() -> non empty TopSpace, P[set]}:
{d where d is Subset of D() : P[d]} is Subset-Family of D()
proof for D being non empty TopSpace holds
{d where d is Subset of D : P[d]} is Subset-Family of D
proof
let D be non empty TopSpace;
{d where d is Subset of D : P[d]} c= bool the carrier of D
proof
let x be set; assume x in {d where d is Subset of D : P[d]};
then consider e being Subset of D such that
A1: e = x & P[e];
thus thesis by A1;
end;
then {d where d is Subset of D : P[d]} is Subset-Family of
D
by SETFAM_1:def 7;
hence thesis;
end;
hence thesis;
end;
definition
let T be non empty TopSpace;
func T^alpha -> Subset-Family of T equals
:Def11: {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 SubsetSD;
hence thesis;
end;
func SO T -> Subset-Family of T equals
:Def12: {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 SubsetSD;
hence thesis;
end;
func PO T -> Subset-Family of T equals
:Def13: {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 SubsetSD;
hence thesis;
end;
func SPO T -> Subset-Family of T equals
:Def14: {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 SubsetSD;
hence thesis;
end;
func PSO T -> Subset-Family of T equals
:Def15: {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 SubsetSD;
hence thesis;
end;
func D(c,alpha)(T) -> Subset-Family of T equals
:Def16: {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 SubsetSD;
hence thesis;
end;
func D(c,p)(T) -> Subset-Family of T equals
:Def17: {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 SubsetSD;
hence thesis;
end;
func D(c,s)(T) -> Subset-Family of T equals
:Def18: {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 SubsetSD;
hence thesis;
end;
func D(c,ps)(T) -> Subset-Family of T equals
:Def19: {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 SubsetSD;
hence thesis;
end;
func D(alpha,p)(T) -> Subset-Family of T equals
:Def20: {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 SubsetSD;
hence thesis;
end;
func D(alpha,s)(T) -> Subset-Family of T equals
:Def21: {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 SubsetSD;
hence thesis;
end;
func D(alpha,ps)(T) -> Subset-Family of T equals
:Def22: {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 SubsetSD;
hence thesis;
end;
func D(p,sp)(T) -> Subset-Family of T equals
:Def23: {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 SubsetSD;
hence thesis;
end;
func D(p,ps)(T) -> Subset-Family of T equals
:Def24: {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 SubsetSD;
hence thesis;
end;
func D(sp,ps)(T) -> Subset-Family of T equals
:Def25: {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 SubsetSD;
hence thesis;
end;
end;
reserve T for non empty TopSpace,
B for Subset of T;
theorem Th1:
alphaInt B = pInt B iff sInt B = psInt B
proof
hereby assume alphaInt B = pInt B;
then pInt B = B /\ Int Cl Int B by Def8;
then pInt B c= Int Cl Int B by XBOOLE_1:17;
then B /\ Int Cl B c= Int Cl Int B by Def7;
then Cl (B /\ Int Cl B) c= Cl( Int Cl Int B) by PRE_TOPC:49;
then A1: Cl (B /\ Int Cl B) c= Cl Int B by TOPS_1:58;
Int Cl B is open by TOPS_1:51;
then A2: Cl(B /\ Int Cl B) = Cl(Cl B /\ Int Cl B) by TOPS_1:41;
Int Cl B c= Cl B by TOPS_1:44;
then Cl(B /\ Int Cl B) = Cl Int Cl B by A2,XBOOLE_1:28;
then B /\ Cl Int Cl B c= B /\ Cl Int B by A1,XBOOLE_1:26;
then psInt B c= B /\ Cl Int B by Def9;
then A3: psInt B c= sInt B by Def6;
Int B c= B by TOPS_1:44;
then Cl Int B c= Cl B by PRE_TOPC:49;
then Int Cl Int B c= Int Cl B by TOPS_1:48;
then Cl Int Cl Int B c= Cl Int Cl B by PRE_TOPC:49;
then Cl Int B c= Cl Int Cl B by TOPS_1:58;
then B /\ Cl Int B c= B /\ Cl Int Cl B by XBOOLE_1:26;
then sInt B c= B /\ Cl Int Cl B by Def6;
then sInt B c= psInt B by Def9;
hence sInt B = psInt B by A3,XBOOLE_0:def 10;
end;
assume psInt B = sInt B;
then psInt B = B /\ Cl Int B by Def6;
then psInt B c= Cl Int B by XBOOLE_1:17;
then A4: B /\ Cl Int Cl B c= Cl Int B by Def9;
Int Cl B c= Cl Int Cl B by PRE_TOPC:48;
then B /\ Int Cl B c= B /\ Cl Int Cl B by XBOOLE_1:26;
then B /\ Int Cl B c= Cl Int B by A4,XBOOLE_1:1;
then Cl(B /\ Int Cl B) c= Cl Cl Int B by PRE_TOPC:49;
then A5: Cl(B /\ Int Cl B) c= Cl Int B by TOPS_1:26;
Int Cl B is open by TOPS_1:51;
then A6: Cl(B /\ Int Cl B) = Cl(Cl B /\ Int Cl B) by TOPS_1:41;
Int Cl B c= Cl B by TOPS_1:44;
then A7: Cl Int Cl B c= Cl Int B by A5,A6,XBOOLE_1:28;
Int Cl B c= Cl Int Cl B by PRE_TOPC:48;
then Int Cl B c= Cl Int B by A7,XBOOLE_1:1;
then Int Int Cl B c= Int Cl Int B by TOPS_1:48;
then Int Cl B c= Int Cl Int B by TOPS_1:45;
then B /\ Int Cl B c= B /\ Int Cl Int B by XBOOLE_1:26;
then pInt B c= B /\ Int Cl Int B by Def7;
then A8: pInt B c= alphaInt B by Def8;
Int B c= B by TOPS_1:44;
then Cl Int B c= Cl B by PRE_TOPC:49;
then Int Cl Int B c= Int Cl B by TOPS_1:48;
then B /\ Int Cl Int B c= B /\ Int Cl B by XBOOLE_1:26;
then alphaInt B c= B /\ Int Cl B by Def8;
then alphaInt B c= pInt B by Def7;
hence alphaInt B = pInt B by A8,XBOOLE_0:def 10;
end;
theorem Th2:
B is alpha-set of T iff B = alphaInt B
proof
hereby assume B is alpha-set of T;
then B c= Int Cl Int B by Def1;
hence B = B /\ Int Cl Int B by XBOOLE_1:28
.= alphaInt B by Def8;
end;
assume B = alphaInt B;
then B = B /\ Int Cl Int B by Def8;
then B c= Int Cl Int B by XBOOLE_1:17;
hence thesis by Def1;
end;
theorem Th3:
B is semi-open iff B = sInt B
proof
hereby assume B is semi-open;
then B c= Cl Int B by Def2;
hence B = B /\ Cl Int B by XBOOLE_1:28
.= sInt B by Def6;
end;
assume B = sInt B;
then B = B /\ Cl Int B by Def6;
then B c= Cl Int B by XBOOLE_1:17;
hence thesis by Def2;
end;
theorem Th4:
B is pre-open iff B = pInt B
proof
hereby assume B is pre-open;
then B c= Int Cl B by Def3;
hence B = B /\ Int Cl B by XBOOLE_1:28
.= pInt B by Def7;
end;
assume B = pInt B;
then B = B /\ Int Cl B by Def7;
then B c= Int Cl B by XBOOLE_1:17;
hence thesis by Def3;
end;
theorem Th5:
B is pre-semi-open iff B = psInt B
proof
hereby assume B is pre-semi-open;
then B c= Cl Int Cl B by Def4;
hence B = B /\ Cl Int Cl B by XBOOLE_1:28
.= psInt B by Def9;
end;
assume B = psInt B;
then B = B /\ Cl Int Cl B by Def9;
then B c= Cl Int Cl B by XBOOLE_1:17;
hence thesis by Def4;
end;
theorem Th6:
B is semi-pre-open iff B = spInt B
proof
hereby assume B is semi-pre-open;
then B c= Cl Int B \/ Int Cl B by Def5;
then B = B /\ (Cl Int B \/ Int Cl B) by XBOOLE_1:28;
then B = (B /\ Cl Int B) \/ (B /\ Int Cl B) by XBOOLE_1:23;
then B = sInt B \/ (B /\ Int Cl B) by Def6;
then B = sInt B \/ pInt B by Def7;
hence B = spInt B by Def10;
end;
assume B = spInt B;
then B = sInt B \/ pInt B by Def10;
then B = sInt B \/ (B /\ Int Cl B) by Def7;
then B = (B /\ Cl Int B) \/ (B /\ Int Cl B) by Def6;
then B = B /\ (Cl Int B \/ Int Cl B) by XBOOLE_1:23;
then B c= Cl Int B \/ Int Cl B by XBOOLE_1:17;
hence thesis by Def5;
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 set;
assume x in T^alpha /\ D(c,alpha)(T);
then A1: x in T^alpha & x in D(c,alpha)(T) by XBOOLE_0:def 3;
then x in {B: B is alpha-set of T} by Def11;
then consider A being Subset of T such that
A2: x = A and
A3: A is alpha-set of T;
A4: A = alphaInt A by A3,Th2;
x in {B: Int B = alphaInt B} by A1,Def16;
then consider Z being Subset of T such that
A5: x = Z and
A6: Int Z = alphaInt Z;
Z is open by A2,A4,A5,A6,TOPS_1:51;
hence x in the topology of T by A5,PRE_TOPC:def 5;
end;
let x be set;
assume A7: x in the topology of T;
then reconsider K = x as Subset of T;
K is open by A7,PRE_TOPC:def 5;
then A8: K = Int K by TOPS_1:55;
then K c= Cl Int K by PRE_TOPC:48;
then K c= Int Cl Int K by A8,TOPS_1:48;
then A9: K is alpha-set of T by Def1;
then K in {B: B is alpha-set of T};
then A10: K in T^alpha by Def11;
Int K = alphaInt K by A8,A9,Th2;
then K in {B: Int B = alphaInt B};
then K in D(c,alpha)(T) by Def16;
hence thesis by A10,XBOOLE_0:def 3;
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 set;
assume x in SO T /\ D(c,s)(T);
then A1: x in SO T & x in D(c,s)(T) by XBOOLE_0:def 3;
then x in {B: B is semi-open} by Def12;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-open;
A4: A = sInt A by A3,Th3;
x in {B: Int B = sInt B} by A1,Def18;
then consider Z being Subset of T such that
A5: x = Z and
A6: Int Z = sInt Z;
Z is open by A2,A4,A5,A6,TOPS_1:51;
hence x in the topology of T by A5,PRE_TOPC:def 5;
end;
let x be set;
assume A7: x in the topology of T;
then reconsider K = x as Subset of T;
K is open by A7,PRE_TOPC:def 5;
then A8: K = Int K by TOPS_1:55;
then K c= Cl Int K by PRE_TOPC:48;
then A9: K is semi-open by Def2;
then K in {B: B is semi-open};
then A10: K in SO T by Def12;
Int K = sInt K by A8,A9,Th3;
then K in {B: Int B = sInt B};
then K in D(c,s)(T) by Def18;
hence thesis by A10,XBOOLE_0:def 3;
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 set;
assume x in PO T /\ D(c,p)(T);
then A1: x in PO T & x in D(c,p)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-open} by Def13;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-open;
A4: A = pInt A by A3,Th4;
x in {B: Int B = pInt B} by A1,Def17;
then consider Z being Subset of T such that
A5: x = Z and
A6: Int Z = pInt Z;
Z is open by A2,A4,A5,A6,TOPS_1:51;
hence x in the topology of T by A5,PRE_TOPC:def 5;
end;
let x be set;
assume A7: x in the topology of T;
then reconsider K = x as Subset of T;
K is open by A7,PRE_TOPC:def 5;
then A8: K = Int K by TOPS_1:55;
K c= Cl K by PRE_TOPC:48;
then K c= Int Cl K by A8,TOPS_1:48;
then A9: K is pre-open by Def3;
then K in {B: B is pre-open};
then A10: K in PO T by Def13;
Int K = pInt K by A8,A9,Th4;
then K in {B: Int B = pInt B};
then K in D(c,p)(T) by Def17;
hence thesis by A10,XBOOLE_0:def 3;
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 set;
assume x in PSO T /\ D(c,ps)(T);
then A1: x in PSO T & x in D(c,ps)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-semi-open} by Def15;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open;
A4: A = psInt A by A3,Th5;
x in {B: Int B = psInt B} by A1,Def19;
then consider Z being Subset of T such that
A5: x = Z and
A6: Int Z = psInt Z;
Z is open by A2,A4,A5,A6,TOPS_1:51;
hence x in the topology of T by A5,PRE_TOPC:def 5;
end;
let x be set;
assume A7: x in the topology of T;
then reconsider K = x as Subset of T;
K is open by A7,PRE_TOPC:def 5;
then A8: K = Int K by TOPS_1:55;
then K c= Cl Int K by PRE_TOPC:48;
then A9: K c= Int Cl K by A8,TOPS_1:48;
Int Cl K c= Cl Int Cl K by PRE_TOPC:48;
then K c= Cl Int Cl K by A9,XBOOLE_1:1;
then A10: K is pre-semi-open by Def4;
then K in {B: B is pre-semi-open};
then A11: K in PSO T by Def15;
Int K = psInt K by A8,A10,Th5;
then K in {B: Int B = psInt B};
then K in D(c,ps)(T) by Def19;
hence thesis by A11,XBOOLE_0:def 3;
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 set;
assume x in PO T /\ D(alpha,p)(T);
then A1: x in PO T & x in D(alpha,p)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-open} by Def13;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-open;
A4: A = pInt A by A3,Th4;
x in {B: alphaInt B = pInt B} by A1,Def20;
then consider Z being Subset of T such that
A5: x = Z and
A6: alphaInt Z = pInt Z;
Z is alpha-set of T by A2,A4,A5,A6,Th2;
then Z in {B: B is alpha-set of T};
hence x in T^alpha by A5,Def11;
end;
let x be set;
assume x in T^alpha;
then x in {B: B is alpha-set of T} by Def11;
then consider K being Subset of T such that
A7: x = K and
A8: K is alpha-set of T;
A9: K c= Int Cl Int K by A8,Def1;
Int K c= K by TOPS_1:44;
then Cl Int K c= Cl K by PRE_TOPC:49;
then Int Cl Int K c= Int Cl K by TOPS_1:48;
then K c= Int Cl K by A9,XBOOLE_1:1;
then A10: K is pre-open by Def3;
then A11: K = pInt K by Th4;
K in {B: B is pre-open} by A10;
then A12: K in PO T by Def13;
alphaInt K = pInt K by A8,A11,Th2;
then K in {B: alphaInt B = pInt B};
then K in D(alpha,p)(T) by Def20;
hence thesis by A7,A12,XBOOLE_0:def 3;
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 set;
assume x in SO T /\ D(alpha,s)(T);
then A1: x in SO T & x in D(alpha,s)(T) by XBOOLE_0:def 3;
then x in {B: B is semi-open} by Def12;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-open;
A4: A = sInt A by A3,Th3;
x in {B: alphaInt B= sInt B} by A1,Def21;
then consider Z being Subset of T such that
A5: x = Z and
A6: alphaInt Z = sInt Z;
Z is alpha-set of T by A2,A4,A5,A6,Th2;
then Z in {B: B is alpha-set of T};
hence x in T^alpha by A5,Def11;
end;
let x be set;
assume x in T^alpha;
then x in {B: B is alpha-set of T} by Def11;
then consider K being Subset of T such that
A7: x = K and
A8: K is alpha-set of T;
A9: K c= Int Cl Int K by A8,Def1;
Int Cl Int K c= Cl Int K by TOPS_1:44;
then K c= Cl Int K by A9,XBOOLE_1:1;
then A10: K is semi-open by Def2;
then A11: K = sInt K by Th3;
A12: K in {B:B is semi-open} by A10;
alphaInt K = sInt K by A8,A11,Th2;
then K in {B: alphaInt B = sInt B};
then K in SO T & K in D(alpha,s)(T) by A12,Def12,Def21;
hence thesis by A7,XBOOLE_0:def 3;
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 set;
assume x in PSO T /\ D(alpha,ps)(T);
then A1: x in PSO T & x in D(alpha,ps)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-semi-open} by Def15;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open;
A4: A = psInt A by A3,Th5;
x in {B: alphaInt B = psInt B} by A1,Def22;
then consider Z being Subset of T such that
A5: x = Z and
A6: alphaInt Z = psInt Z;
Z is alpha-set of T by A2,A4,A5,A6,Th2;
then Z in {B: B is alpha-set of T};
hence x in T^alpha by A5,Def11;
end;
let x be set;
assume x in T^alpha;
then x in {B: B is alpha-set of T} by Def11;
then consider K being Subset of T such that
A7: x = K and
A8: K is alpha-set of T;
A9: K c= Int Cl Int K by A8,Def1;
Int K c= K by TOPS_1:44;
then Cl Int K c= Cl K by PRE_TOPC:49;
then A10: Int Cl Int K c= Int Cl K by TOPS_1:48;
Int Cl K c= Cl Int Cl K by PRE_TOPC:48;
then Int Cl Int K c= Cl Int Cl K by A10,XBOOLE_1:1;
then K c= Cl Int Cl K by A9,XBOOLE_1:1;
then A11: K is pre-semi-open by Def4;
then A12: K = psInt K by Th5;
K in {B: B is pre-semi-open} by A11;
then A13: K in PSO T by Def15;
alphaInt K = psInt K by A8,A12,Th2;
then K in {B: alphaInt B = psInt B};
then K in D(alpha,ps)(T) by Def22;
hence thesis by A7,A13,XBOOLE_0:def 3;
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 set;
assume x in SPO T /\ D(p,sp)(T);
then A1: x in SPO T & x in D(p,sp)(T) by XBOOLE_0:def 3;
then x in {B: B is semi-pre-open} by Def14;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-pre-open;
A4: A = spInt A by A3,Th6;
x in {B: pInt B = spInt B} by A1,Def23;
then consider Z being Subset of T such that
A5: x = Z and
A6: pInt Z = spInt Z;
Z is pre-open by A2,A4,A5,A6,Th4;
then Z in {B: B is pre-open};
hence x in PO T by A5,Def13;
end;
let x be set;
assume x in PO T;
then x in {B: B is pre-open} by Def13;
then consider K being Subset of T such that
A7: x = K and
A8: K is pre-open;
A9: K c= Int Cl K by A8,Def3;
Int Cl K c= Cl Int K \/ Int Cl K by XBOOLE_1:7;
then K c= Cl Int K \/ Int Cl K by A9,XBOOLE_1:1;
then A10: K is semi-pre-open by Def5;
then A11: K = spInt K by Th6;
K in {B: B is semi-pre-open} by A10;
then A12: K in SPO T by Def14;
pInt K = spInt K by A8,A11,Th4;
then K in {B: pInt B = spInt B};
then K in D(p,sp)(T) by Def23;
hence thesis by A7,A12,XBOOLE_0:def 3;
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 set;
assume x in PSO T /\ D(p,ps)(T);
then A1: x in PSO T & x in D(p,ps)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-semi-open} by Def15;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open;
A4: A = psInt A by A3,Th5;
x in {B: pInt B = psInt B} by A1,Def24;
then consider Z being Subset of T such that
A5: x = Z and
A6: pInt Z = psInt Z;
Z is pre-open by A2,A4,A5,A6,Th4;
then Z in {B: B is pre-open};
hence x in PO T by A5,Def13;
end;
let x be set;
assume x in PO T;
then x in {B: B is pre-open} by Def13;
then consider K being Subset of T such that
A7: x = K and
A8: K is pre-open;
A9: K c= Int Cl K by A8,Def3;
Int Cl K c= Cl Int Cl K by PRE_TOPC:48;
then K c= Cl Int Cl K by A9,XBOOLE_1:1;
then A10: K is pre-semi-open by Def4;
then A11: K = psInt K by Th5;
K in {B: B is pre-semi-open} by A10;
then A12: K in PSO T by Def15;
pInt K = psInt K by A8,A11,Th4;
then K in {B: pInt B = psInt B};
then K in D(p,ps)(T) by Def24;
hence thesis by A7,A12,XBOOLE_0:def 3;
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 set;
assume x in PSO T /\ D(alpha,p)(T);
then A1: x in PSO T & x in D(alpha,p)(T) by XBOOLE_0:def 3;
then x in {B: B is pre-semi-open} by Def15;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open;
A4: A = psInt A by A3,Th5;
x in {B: alphaInt B = pInt B} by A1,Def20;
then consider Z being Subset of T such that
A5: x = Z and
A6: alphaInt Z = pInt Z;
Z = sInt Z by A2,A4,A5,A6,Th1;
then Z is semi-open by Th3;
then Z in {B: B is semi-open};
hence x in SO T by A5,Def12;
end;
let x be set;
assume x in SO T;
then x in {B: B is semi-open} by Def12;
then consider K being Subset of T such that
A7: x = K and
A8: K is semi-open;
A9: K c= Cl Int K by A8,Def2;
Int K c= K by TOPS_1:44;
then Cl Int K c= Cl K by PRE_TOPC:49;
then Int Cl Int K c= Int Cl K by TOPS_1:48;
then Cl Int Cl Int K c= Cl Int Cl K by PRE_TOPC:49;
then Cl Int K c= Cl Int Cl K by TOPS_1:58;
then K c= Cl Int Cl K by A9,XBOOLE_1:1;
then A10: K is pre-semi-open by Def4;
then A11: K = psInt K by Th5;
K in {B: B is pre-semi-open} by A10;
then A12: K in PSO T by Def15;
sInt K = psInt K by A8,A11,Th3;
then alphaInt K = pInt K by Th1;
then K in {B: alphaInt B = pInt B};
then K in D(alpha,p)(T) by Def20;
hence thesis by A7,A12,XBOOLE_0:def 3;
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 set;
assume x in PSO T /\ D(sp,ps)(T);
then A1: x in PSO T & x in D(sp,ps)(T) by XBOOLE_0:def 3;
then x in {B:B is pre-semi-open} by Def15;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open;
A4: A = psInt A by A3,Th5;
x in {B: spInt B = psInt B} by A1,Def25;
then consider Z being Subset of T such that
A5: x = Z and
A6: spInt Z = psInt Z;
Z is semi-pre-open by A2,A4,A5,A6,Th6;
then Z in {B: B is semi-pre-open};
hence x in SPO T by A5,Def14;
end;
let x be set;
assume x in SPO T;
then x in {B: B is semi-pre-open} by Def14;
then consider K being Subset of T such that
A7: x = K and
A8: K is semi-pre-open;
A9: K c= Cl Int K \/ Int Cl K by A8,Def5;
Int K c= K by TOPS_1:44;
then Cl Int K c= Cl K by PRE_TOPC:49;
then Int Cl Int K c= Int Cl K by TOPS_1:48;
then Cl Int Cl Int K c= Cl Int Cl K by PRE_TOPC:49;
then A10: Cl Int K c= Cl Int Cl K by TOPS_1:58;
Int Cl K c= Cl Int Cl K by PRE_TOPC:48;
then Cl Int K \/ Int Cl K c= Cl Int Cl K by A10,XBOOLE_1:8;
then K c= Cl Int Cl K by A9,XBOOLE_1:1;
then A11: K is pre-semi-open by Def4;
then A12: K = psInt K by Th5;
K in {B: B is pre-semi-open} by A11;
then A13: K in PSO T by Def15;
spInt K = psInt K by A8,A12,Th6;
then K in {B: spInt B = psInt B};
then K in D(sp,ps)(T) by Def25;
hence thesis by A7,A13,XBOOLE_0:def 3;
end;
definition let X,Y be non empty TopSpace; let f be map of X,Y;
attr f is s-continuous means
:Def26: for G being Subset of Y st G is open holds f"G in SO X;
attr f is p-continuous means
:Def27: for G being Subset of Y st G is open holds f"G in PO X;
attr f is alpha-continuous means
:Def28: for G being Subset of Y st G is open holds f"G in X^alpha;
attr f is ps-continuous means
:Def29: for G being Subset of Y st G is open holds f"G in PSO X;
attr f is sp-continuous means
:Def30: for G being Subset of Y st G is open holds f"G in SPO X;
attr f is (c,alpha)-continuous means
:Def31: 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
:Def32: 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
:Def33: 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
:Def34: 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
:Def35: 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
:Def36: 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
:Def37: 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
:Def38: 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
:Def39: 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
:Def40: 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
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,Def28;
then f"V in PO X /\ D(alpha,p)(X) by Th11;
hence f"V in PO X by XBOOLE_0:def 3;
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,Def28;
then f"G in PO X /\ D(alpha,p)(X) by Th11;
hence f"G in D(alpha,p)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is p-continuous (alpha,p)-continuous;
let V be Subset of Y; assume A3: V is open;
then A4: f"V in PO X by A2,Def27;
f"V in D(alpha,p)(X) by A2,A3,Def35;
then f"V in PO X /\ D(alpha,p)(X) by A4,XBOOLE_0:def 3;
hence f"V in X^alpha 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,Def28;
then f"V in SO X /\ D(alpha,s)(X) by Th12;
hence f"V in SO X by XBOOLE_0:def 3;
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,Def28;
then f"G in SO X /\ D(alpha,s)(X) by Th12;
hence f"G in D(alpha,s)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is s-continuous (alpha,s)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in SO X by A2,Def26;
f"V in D(alpha,s)(X) by A2,A3,Def36;
then f"V in SO X /\ D(alpha,s)(X) by A4,XBOOLE_0:def 3;
hence f"V in X^alpha 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,Def28;
then f"V in PSO X /\ D(alpha,ps)(X) by Th13;
hence f"V in PSO X by XBOOLE_0:def 3;
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,Def28;
then f"G in PSO X /\ D(alpha,ps)(X) by Th13;
hence f"G in D(alpha,ps)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is ps-continuous (alpha,ps)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in PSO X by A2,Def29;
f"V in D(alpha,ps)(X) by A2,A3,Def37;
then f"V in PSO X /\ D(alpha,ps)(X) by A4,XBOOLE_0:def 3;
hence f"V in X^alpha 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,Def27;
then f"V in SPO X /\ D(p,sp)(X) by Th14;
hence f"V in SPO X by XBOOLE_0:def 3;
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,Def27;
then f"G in SPO X /\ D(p,sp)(X) by Th14;
hence f"G in D(p,sp)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is sp-continuous (p,sp)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in SPO X by A2,Def30;
f"V in D(p,sp)(X) by A2,A3,Def39;
then f"V in SPO X /\ D(p,sp)(X) by A4,XBOOLE_0:def 3;
hence f"V in PO X 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,Def27;
then f"V in PSO X /\ D(p,ps)(X) by Th15;
hence f"V in PSO X by XBOOLE_0:def 3;
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,Def27;
then f"G in PSO X /\ D(p,ps)(X) by Th15;
hence f"G in D(p,ps)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is ps-continuous (p,ps)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in PSO X by A2,Def29;
f"V in D(p,ps)(X) by A2,A3,Def38;
then f"V in PSO X /\ D(p,ps)(X) by A4,XBOOLE_0:def 3;
hence f"V in PO X 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,Def26;
then f"V in PSO X /\ D(alpha,p)(X) by Th16;
hence f"V in PSO X by XBOOLE_0:def 3;
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,Def26;
then f"G in PSO X /\ D(alpha,p)(X) by Th16;
hence f"G in D(alpha,p)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is ps-continuous (alpha,p)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in PSO X by A2,Def29;
f"V in D(alpha,p)(X) by A2,A3,Def35;
then f"V in PSO X /\ D(alpha,p)(X) by A4,XBOOLE_0:def 3;
hence f"V in SO X 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,Def30;
then f"V in PSO X /\ D(sp,ps)(X) by Th17;
hence f"V in PSO X by XBOOLE_0:def 3;
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,Def30;
then f"G in PSO X /\ D(sp,ps)(X) by Th17;
hence f"G in D(sp,ps)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is ps-continuous (sp,ps)-continuous;
let V be Subset of Y; assume
A3: V is open;
then A4: f"V in PSO X by A2,Def29;
f"V in D(sp,ps)(X) by A2,A3,Def40;
then f"V in PSO X /\ D(sp,ps)(X) by A4,XBOOLE_0:def 3;
hence f"V in SPO X by Th17;
end;
theorem
f is continuous iff f is alpha-continuous (c,alpha)-continuous
proof
hereby assume
A1: 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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in X^alpha /\ D(c,alpha)(X) by Th7;
hence f"V in X^alpha by XBOOLE_0:def 3;
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,TOPS_2:55;
then f"G in the topology of X by PRE_TOPC:def 5;
then f"G in X^alpha /\ D(c,alpha)(X) by Th7;
hence f"G in D(c,alpha)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is alpha-continuous (c,alpha)-continuous;
now let V be Subset of Y; assume
A3: V is open;
then A4: f"V in X^alpha by A2,Def28;
f"V in D(c,alpha)(X) by A2,A3,Def31;
then f"V in X^alpha /\ D(c,alpha)(X) by A4,XBOOLE_0:def 3;
then f"V in the topology of X by Th7;
hence f"V is open by PRE_TOPC:def 5;
end;
hence thesis by TOPS_2:55;
end;
theorem
f is continuous iff f is s-continuous (c,s)-continuous
proof
hereby assume
A1: 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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in SO X /\ D(c,s)(X) by Th8;
hence f"V in SO X by XBOOLE_0:def 3;
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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in SO X /\ D(c,s)(X) by Th8;
hence f"V in D(c,s)(X) by XBOOLE_0:def 3;
end;
end;
assume A2:f is s-continuous (c,s)-continuous;
now let V be Subset of Y; assume
A3: V is open;
then A4:f"V in SO X by A2,Def26;
f"V in D(c,s)(X) by A2,A3,Def32;
then f"V in SO X /\ D(c,s)(X) by A4,XBOOLE_0:def 3;
then f"V in the topology of X by Th8;
hence f"V is open by PRE_TOPC:def 5;
end;
hence thesis by TOPS_2:55;
end;
theorem
f is continuous iff f is p-continuous (c,p)-continuous
proof
hereby assume
A1: 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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in PO X /\ D(c,p)(X) by Th9;
hence f"V in PO X by XBOOLE_0:def 3;
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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in PO X /\ D(c,p)(X) by Th9;
hence f"V in D(c,p)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is p-continuous (c,p)-continuous;
now let V be Subset of Y; assume
A3: V is open;
then A4:f"V in PO X by A2,Def27;
f"V in D(c,p)(X) by A2,A3,Def33;
then f"V in PO X /\ D(c,p)(X) by A4,XBOOLE_0:def 3;
then f"V in the topology of X by Th9;
hence f"V is open by PRE_TOPC:def 5;
end;
hence thesis by TOPS_2:55;
end;
theorem
f is continuous iff f is ps-continuous (c,ps)-continuous
proof
hereby assume
A1: 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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in PSO X /\ D(c,ps)(X) by Th10;
hence f"V in PSO X by XBOOLE_0:def 3;
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,TOPS_2:55;
then f"V in the topology of X by PRE_TOPC:def 5;
then f"V in PSO X /\ D(c,ps)(X) by Th10;
hence f"V in D(c,ps)(X) by XBOOLE_0:def 3;
end;
end;
assume A2: f is ps-continuous (c,ps)-continuous;
now let V be Subset of Y; assume
A3: V is open;
then A4: f"V in PSO X by A2,Def29;
f"V in D(c,ps)(X) by A2,A3,Def34;
then f"V in PSO X /\ D(c,ps)(X) by A4,XBOOLE_0:def 3;
then f"V in the topology of X by Th10;
hence f"V is open by PRE_TOPC:def 5;
end;
hence thesis by TOPS_2:55;
end;