:: DECOMP_1 semantic presentation
begin
definition
let T be TopStruct ;
mode alpha-set of T -> Subset of T means :Def1: :: DECOMP_1:def 1
it c= Int (Cl (Int it));
existence
ex b1 being Subset of T st b1 c= Int (Cl (Int b1))
proof
take {} T ; ::_thesis: {} T c= Int (Cl (Int ({} T)))
thus {} T c= Int (Cl (Int ({} T))) by XBOOLE_1:2; ::_thesis: verum
end;
let IT be Subset of T;
attrIT is semi-open means :Def2: :: DECOMP_1:def 2
IT c= Cl (Int IT);
attrIT is pre-open means :Def3: :: DECOMP_1:def 3
IT c= Int (Cl IT);
attrIT is pre-semi-open means :Def4: :: DECOMP_1:def 4
IT c= Cl (Int (Cl IT));
attrIT is semi-pre-open means :Def5: :: DECOMP_1:def 5
IT c= (Cl (Int IT)) \/ (Int (Cl IT));
end;
:: deftheorem Def1 defines alpha-set DECOMP_1:def_1_:_
for T being TopStruct
for b2 being Subset of T holds
( b2 is alpha-set of T iff b2 c= Int (Cl (Int b2)) );
:: deftheorem Def2 defines semi-open DECOMP_1:def_2_:_
for T being TopStruct
for IT being Subset of T holds
( IT is semi-open iff IT c= Cl (Int IT) );
:: deftheorem Def3 defines pre-open DECOMP_1:def_3_:_
for T being TopStruct
for IT being Subset of T holds
( IT is pre-open iff IT c= Int (Cl IT) );
:: deftheorem Def4 defines pre-semi-open DECOMP_1:def_4_:_
for T being TopStruct
for IT being Subset of T holds
( IT is pre-semi-open iff IT c= Cl (Int (Cl IT)) );
:: deftheorem Def5 defines semi-pre-open DECOMP_1:def_5_:_
for T being TopStruct
for IT being Subset of T holds
( IT is semi-pre-open iff IT c= (Cl (Int IT)) \/ (Int (Cl IT)) );
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));
coherence
B /\ (Cl (Int B)) is Subset of T ;
func pInt B -> Subset of T equals :: DECOMP_1:def 7
B /\ (Int (Cl B));
coherence
B /\ (Int (Cl B)) is Subset of T ;
func alphaInt B -> Subset of T equals :: DECOMP_1:def 8
B /\ (Int (Cl (Int B)));
coherence
B /\ (Int (Cl (Int B))) is Subset of T ;
func psInt B -> Subset of T equals :: DECOMP_1:def 9
B /\ (Cl (Int (Cl B)));
coherence
B /\ (Cl (Int (Cl B))) is Subset of T ;
end;
:: deftheorem defines sInt DECOMP_1:def_6_:_
for T being TopStruct
for B being Subset of T holds sInt B = B /\ (Cl (Int B));
:: deftheorem defines pInt DECOMP_1:def_7_:_
for T being TopStruct
for B being Subset of T holds pInt B = B /\ (Int (Cl B));
:: deftheorem defines alphaInt DECOMP_1:def_8_:_
for T being TopStruct
for B being Subset of T holds alphaInt B = B /\ (Int (Cl (Int B)));
:: deftheorem defines psInt DECOMP_1:def_9_:_
for T being TopStruct
for B being Subset of T holds psInt B = B /\ (Cl (Int (Cl B)));
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);
coherence
(sInt B) \/ (pInt B) is Subset of T ;
end;
:: deftheorem defines spInt DECOMP_1:def_10_:_
for T being TopStruct
for B being Subset of T holds spInt B = (sInt B) \/ (pInt B);
definition
let T be TopSpace;
funcT ^alpha -> Subset-Family of T equals :: DECOMP_1:def 11
{ B where B is Subset of T : B is alpha-set of T } ;
coherence
{ B where B is Subset of T : B is alpha-set of T } is Subset-Family of T
proof
defpred S1[ set ] means $1 is alpha-set of T;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : B is alpha-set of T } is Subset-Family of T ; ::_thesis: verum
end;
func SO T -> Subset-Family of T equals :: DECOMP_1:def 12
{ B where B is Subset of T : B is semi-open } ;
coherence
{ B where B is Subset of T : B is semi-open } is Subset-Family of T
proof
defpred S1[ Subset of T] means $1 is semi-open ;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : B is semi-open } is Subset-Family of T ; ::_thesis: verum
end;
func PO T -> Subset-Family of T equals :: DECOMP_1:def 13
{ B where B is Subset of T : B is pre-open } ;
coherence
{ B where B is Subset of T : B is pre-open } is Subset-Family of T
proof
defpred S1[ Subset of T] means $1 is pre-open ;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : B is pre-open } is Subset-Family of T ; ::_thesis: verum
end;
func SPO T -> Subset-Family of T equals :: DECOMP_1:def 14
{ B where B is Subset of T : B is semi-pre-open } ;
coherence
{ B where B is Subset of T : B is semi-pre-open } is Subset-Family of T
proof
defpred S1[ Subset of T] means $1 is semi-pre-open ;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : B is semi-pre-open } is Subset-Family of T ; ::_thesis: verum
end;
func PSO T -> Subset-Family of T equals :: DECOMP_1:def 15
{ B where B is Subset of T : B is pre-semi-open } ;
coherence
{ B where B is Subset of T : B is pre-semi-open } is Subset-Family of T
proof
defpred S1[ Subset of T] means $1 is pre-semi-open ;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : B is pre-semi-open } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means Int $1 = alphaInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : Int B = pInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means Int $1 = pInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : Int B = pInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : Int B = sInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means Int $1 = sInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : Int B = sInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : Int B = psInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means Int $1 = psInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : Int B = psInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means alphaInt $1 = pInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means alphaInt $1 = sInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means alphaInt $1 = psInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : pInt B = spInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means pInt $1 = spInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : pInt B = spInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : pInt B = psInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means pInt $1 = psInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : pInt B = psInt B } is Subset-Family of T ; ::_thesis: verum
end;
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 } ;
coherence
{ B where B is Subset of T : spInt B = psInt B } is Subset-Family of T
proof
defpred S1[ Subset of T] means spInt $1 = psInt $1;
{ B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7();
hence { B where B is Subset of T : spInt B = psInt B } is Subset-Family of T ; ::_thesis: verum
end;
end;
:: deftheorem defines ^alpha DECOMP_1:def_11_:_
for T being TopSpace holds T ^alpha = { B where B is Subset of T : B is alpha-set of T } ;
:: deftheorem defines SO DECOMP_1:def_12_:_
for T being TopSpace holds SO T = { B where B is Subset of T : B is semi-open } ;
:: deftheorem defines PO DECOMP_1:def_13_:_
for T being TopSpace holds PO T = { B where B is Subset of T : B is pre-open } ;
:: deftheorem defines SPO DECOMP_1:def_14_:_
for T being TopSpace holds SPO T = { B where B is Subset of T : B is semi-pre-open } ;
:: deftheorem defines PSO DECOMP_1:def_15_:_
for T being TopSpace holds PSO T = { B where B is Subset of T : B is pre-semi-open } ;
:: deftheorem defines D(c,alpha) DECOMP_1:def_16_:_
for T being TopSpace holds D(c,alpha) T = { B where B is Subset of T : Int B = alphaInt B } ;
:: deftheorem defines D(c,p) DECOMP_1:def_17_:_
for T being TopSpace holds D(c,p) T = { B where B is Subset of T : Int B = pInt B } ;
:: deftheorem defines D(c,s) DECOMP_1:def_18_:_
for T being TopSpace holds D(c,s) T = { B where B is Subset of T : Int B = sInt B } ;
:: deftheorem defines D(c,ps) DECOMP_1:def_19_:_
for T being TopSpace holds D(c,ps) T = { B where B is Subset of T : Int B = psInt B } ;
:: deftheorem defines D(alpha,p) DECOMP_1:def_20_:_
for T being TopSpace holds D(alpha,p) T = { B where B is Subset of T : alphaInt B = pInt B } ;
:: deftheorem defines D(alpha,s) DECOMP_1:def_21_:_
for T being TopSpace holds D(alpha,s) T = { B where B is Subset of T : alphaInt B = sInt B } ;
:: deftheorem defines D(alpha,ps) DECOMP_1:def_22_:_
for T being TopSpace holds D(alpha,ps) T = { B where B is Subset of T : alphaInt B = psInt B } ;
:: deftheorem defines D(p,sp) DECOMP_1:def_23_:_
for T being TopSpace holds D(p,sp) T = { B where B is Subset of T : pInt B = spInt B } ;
:: deftheorem defines D(p,ps) DECOMP_1:def_24_:_
for T being TopSpace holds D(p,ps) T = { B where B is Subset of T : pInt B = psInt B } ;
:: deftheorem defines D(sp,ps) DECOMP_1:def_25_:_
for T being TopSpace holds D(sp,ps) T = { B where B is Subset of T : spInt B = psInt B } ;
theorem Th1: :: DECOMP_1:1
for T being TopSpace
for B being Subset of T holds
( alphaInt B = pInt B iff sInt B = psInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( alphaInt B = pInt B iff sInt B = psInt B )
let B be Subset of T; ::_thesis: ( alphaInt B = pInt B iff sInt B = psInt B )
hereby ::_thesis: ( sInt B = psInt B implies alphaInt B = pInt B )
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 ; ::_thesis: sInt B = psInt 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, XBOOLE_0:def_10; ::_thesis: verum
end;
A3: Int (Cl B) c= Cl (Int (Cl B)) by PRE_TOPC:18;
assume psInt B = sInt B ; ::_thesis: alphaInt B = pInt 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, XBOOLE_1:1;
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, XBOOLE_1:1;
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 alphaInt B = pInt B by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: DECOMP_1:2
for T being TopSpace
for B being Subset of T holds
( B is alpha-set of T iff B = alphaInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( B is alpha-set of T iff B = alphaInt B )
let B be Subset of T; ::_thesis: ( B is alpha-set of T iff B = alphaInt B )
hereby ::_thesis: ( B = alphaInt B implies B is alpha-set of T )
assume B is alpha-set of T ; ::_thesis: B = alphaInt B
then B c= Int (Cl (Int B)) by Def1;
hence B = alphaInt B by XBOOLE_1:28; ::_thesis: verum
end;
assume B = alphaInt B ; ::_thesis: B is alpha-set of T
then B c= Int (Cl (Int B)) by XBOOLE_1:17;
hence B is alpha-set of T by Def1; ::_thesis: verum
end;
theorem Th3: :: DECOMP_1:3
for T being TopSpace
for B being Subset of T holds
( B is semi-open iff B = sInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( B is semi-open iff B = sInt B )
let B be Subset of T; ::_thesis: ( B is semi-open iff B = sInt B )
hereby ::_thesis: ( B = sInt B implies B is semi-open )
assume B is semi-open ; ::_thesis: B = sInt B
then B c= Cl (Int B) by Def2;
hence B = sInt B by XBOOLE_1:28; ::_thesis: verum
end;
assume B = sInt B ; ::_thesis: B is semi-open
then B c= Cl (Int B) by XBOOLE_1:17;
hence B is semi-open by Def2; ::_thesis: verum
end;
theorem Th4: :: DECOMP_1:4
for T being TopSpace
for B being Subset of T holds
( B is pre-open iff B = pInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( B is pre-open iff B = pInt B )
let B be Subset of T; ::_thesis: ( B is pre-open iff B = pInt B )
hereby ::_thesis: ( B = pInt B implies B is pre-open )
assume B is pre-open ; ::_thesis: B = pInt B
then B c= Int (Cl B) by Def3;
hence B = pInt B by XBOOLE_1:28; ::_thesis: verum
end;
assume B = pInt B ; ::_thesis: B is pre-open
then B c= Int (Cl B) by XBOOLE_1:17;
hence B is pre-open by Def3; ::_thesis: verum
end;
theorem Th5: :: DECOMP_1:5
for T being TopSpace
for B being Subset of T holds
( B is pre-semi-open iff B = psInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( B is pre-semi-open iff B = psInt B )
let B be Subset of T; ::_thesis: ( B is pre-semi-open iff B = psInt B )
hereby ::_thesis: ( B = psInt B implies B is pre-semi-open )
assume B is pre-semi-open ; ::_thesis: B = psInt B
then B c= Cl (Int (Cl B)) by Def4;
hence B = psInt B by XBOOLE_1:28; ::_thesis: verum
end;
assume B = psInt B ; ::_thesis: B is pre-semi-open
then B c= Cl (Int (Cl B)) by XBOOLE_1:17;
hence B is pre-semi-open by Def4; ::_thesis: verum
end;
theorem Th6: :: DECOMP_1:6
for T being TopSpace
for B being Subset of T holds
( B is semi-pre-open iff B = spInt B )
proof
let T be TopSpace; ::_thesis: for B being Subset of T holds
( B is semi-pre-open iff B = spInt B )
let B be Subset of T; ::_thesis: ( B is semi-pre-open iff B = spInt B )
hereby ::_thesis: ( B = spInt B implies B is semi-pre-open )
assume B is semi-pre-open ; ::_thesis: B = spInt B
then B c= (Cl (Int B)) \/ (Int (Cl B)) by Def5;
then B = B /\ ((Cl (Int B)) \/ (Int (Cl B))) by XBOOLE_1:28;
hence B = spInt B by XBOOLE_1:23; ::_thesis: verum
end;
assume B = spInt B ; ::_thesis: B is semi-pre-open
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 B is semi-pre-open by Def5; ::_thesis: verum
end;
theorem Th7: :: DECOMP_1:7
for T being TopSpace holds (T ^alpha) /\ (D(c,alpha) T) = the topology of T
proof
let T be TopSpace; ::_thesis: (T ^alpha) /\ (D(c,alpha) T) = the topology of T
thus (T ^alpha) /\ (D(c,alpha) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (T ^alpha) /\ (D(c,alpha) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (T ^alpha) /\ (D(c,alpha) T) or x in the topology of T )
assume A1: x in (T ^alpha) /\ (D(c,alpha) T) ; ::_thesis: x in the topology of 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 x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (T ^alpha) /\ (D(c,alpha) T) )
assume A6: x in the topology of T ; ::_thesis: x in (T ^alpha) /\ (D(c,alpha) 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 where B is Subset of T : Int B = alphaInt B } ;
K in T ^alpha by A8;
hence x in (T ^alpha) /\ (D(c,alpha) T) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th8: :: DECOMP_1:8
for T being TopSpace holds (SO T) /\ (D(c,s) T) = the topology of T
proof
let T be TopSpace; ::_thesis: (SO T) /\ (D(c,s) T) = the topology of T
thus (SO T) /\ (D(c,s) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (SO T) /\ (D(c,s) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SO T) /\ (D(c,s) T) or x in the topology of T )
assume A1: x in (SO T) /\ (D(c,s) T) ; ::_thesis: x in the topology of 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;
then Z is open by A2, A4, A5;
hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (SO T) /\ (D(c,s) T) )
assume A6: x in the topology of T ; ::_thesis: x in (SO T) /\ (D(c,s) 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= Cl (Int K) by PRE_TOPC:18;
then A8: K is semi-open by Def2;
then Int K = sInt K by A7, Th3;
then A9: K in { B where B is Subset of T : Int B = sInt B } ;
K in SO T by A8;
hence x in (SO T) /\ (D(c,s) T) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th9: :: DECOMP_1:9
for T being TopSpace holds (PO T) /\ (D(c,p) T) = the topology of T
proof
let T be TopSpace; ::_thesis: (PO T) /\ (D(c,p) T) = the topology of T
thus (PO T) /\ (D(c,p) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (PO T) /\ (D(c,p) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PO T) /\ (D(c,p) T) or x in the topology of T )
assume A1: x in (PO T) /\ (D(c,p) T) ; ::_thesis: x in the topology of 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;
then Z is open by A2, A4, A5;
hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (PO T) /\ (D(c,p) T) )
assume A6: x in the topology of T ; ::_thesis: x in (PO T) /\ (D(c,p) 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 K) by PRE_TOPC:18, TOPS_1:19;
then A8: K is pre-open by Def3;
then Int K = pInt K by A7, Th4;
then A9: K in { B where B is Subset of T : Int B = pInt B } ;
K in PO T by A8;
hence x in (PO T) /\ (D(c,p) T) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th10: :: DECOMP_1:10
for T being TopSpace holds (PSO T) /\ (D(c,ps) T) = the topology of T
proof
let T be TopSpace; ::_thesis: (PSO T) /\ (D(c,ps) T) = the topology of T
thus (PSO T) /\ (D(c,ps) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (PSO T) /\ (D(c,ps) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(c,ps) T) or x in the topology of T )
assume A1: x in (PSO T) /\ (D(c,ps) T) ; ::_thesis: x in the topology of 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;
then Z is open by A2, A4, A5;
hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (PSO T) /\ (D(c,ps) T) )
assume A6: x in the topology of T ; ::_thesis: x in (PSO T) /\ (D(c,ps) 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, XBOOLE_1:1;
then A9: K is pre-semi-open by Def4;
then Int K = psInt K by A8, Th5;
then A10: K in { B where B is Subset of T : Int B = psInt B } ;
K in PSO T by A9;
hence x in (PSO T) /\ (D(c,ps) T) by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th11: :: DECOMP_1:11
for T being TopSpace holds (PO T) /\ (D(alpha,p) T) = T ^alpha
proof
let T be TopSpace; ::_thesis: (PO T) /\ (D(alpha,p) T) = T ^alpha
thus (PO T) /\ (D(alpha,p) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (PO T) /\ (D(alpha,p) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PO T) /\ (D(alpha,p) T) or x in T ^alpha )
assume A1: x in (PO T) /\ (D(alpha,p) T) ; ::_thesis: x in T ^alpha
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 x in T ^alpha by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (PO T) /\ (D(alpha,p) T) )
assume x in T ^alpha ; ::_thesis: x in (PO T) /\ (D(alpha,p) T)
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, XBOOLE_1:1;
then A9: K is pre-open by Def3;
then K = pInt K by Th4;
then alphaInt K = pInt K by A7, Th2;
then A10: K in { B where B is Subset of T : alphaInt B = pInt B } ;
K in PO T by A9;
hence x in (PO T) /\ (D(alpha,p) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th12: :: DECOMP_1:12
for T being TopSpace holds (SO T) /\ (D(alpha,s) T) = T ^alpha
proof
let T be TopSpace; ::_thesis: (SO T) /\ (D(alpha,s) T) = T ^alpha
thus (SO T) /\ (D(alpha,s) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (SO T) /\ (D(alpha,s) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SO T) /\ (D(alpha,s) T) or x in T ^alpha )
assume A1: x in (SO T) /\ (D(alpha,s) T) ; ::_thesis: x in T ^alpha
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 ;
A = sInt A by A3, Th3;
then Z is alpha-set of T by A2, A4, A5, Th2;
hence x in T ^alpha by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (SO T) /\ (D(alpha,s) T) )
assume x in T ^alpha ; ::_thesis: x in (SO T) /\ (D(alpha,s) T)
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, XBOOLE_1:1;
then A9: K is semi-open by Def2;
then K = sInt K by Th3;
then alphaInt K = sInt K by A7, Th2;
then A10: K in { B where B is Subset of T : alphaInt B = sInt B } ;
K in { B where B is Subset of T : B is semi-open } by A9;
hence x in (SO T) /\ (D(alpha,s) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th13: :: DECOMP_1:13
for T being TopSpace holds (PSO T) /\ (D(alpha,ps) T) = T ^alpha
proof
let T be TopSpace; ::_thesis: (PSO T) /\ (D(alpha,ps) T) = T ^alpha
thus (PSO T) /\ (D(alpha,ps) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (PSO T) /\ (D(alpha,ps) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(alpha,ps) T) or x in T ^alpha )
assume A1: x in (PSO T) /\ (D(alpha,ps) T) ; ::_thesis: x in T ^alpha
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 x in T ^alpha by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (PSO T) /\ (D(alpha,ps) T) )
assume x in T ^alpha ; ::_thesis: x in (PSO T) /\ (D(alpha,ps) T)
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, XBOOLE_1:1;
K c= Int (Cl (Int K)) by A7, Def1;
then K c= Cl (Int (Cl K)) by A9, XBOOLE_1:1;
then A10: K is pre-semi-open by Def4;
then K = psInt K by Th5;
then alphaInt K = psInt K by A7, Th2;
then A11: K in { B where B is Subset of T : alphaInt B = psInt B } ;
K in PSO T by A10;
hence x in (PSO T) /\ (D(alpha,ps) T) by A6, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th14: :: DECOMP_1:14
for T being TopSpace holds (SPO T) /\ (D(p,sp) T) = PO T
proof
let T be TopSpace; ::_thesis: (SPO T) /\ (D(p,sp) T) = PO T
thus (SPO T) /\ (D(p,sp) T) c= PO T :: according to XBOOLE_0:def_10 ::_thesis: PO T c= (SPO T) /\ (D(p,sp) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SPO T) /\ (D(p,sp) T) or x in PO T )
assume A1: x in (SPO T) /\ (D(p,sp) T) ; ::_thesis: x in PO T
then x in SPO T by XBOOLE_0:def_4;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-pre-open ;
x in D(p,sp) T by A1, XBOOLE_0:def_4;
then consider Z being Subset of T such that
A4: x = Z and
A5: pInt Z = spInt Z ;
A = spInt A by A3, Th6;
then Z is pre-open by A2, A4, A5, Th4;
hence x in PO T by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PO T or x in (SPO T) /\ (D(p,sp) T) )
assume x in PO T ; ::_thesis: x in (SPO T) /\ (D(p,sp) T)
then consider K being Subset of T such that
A6: x = K and
A7: K is pre-open ;
A8: Int (Cl K) c= (Cl (Int K)) \/ (Int (Cl K)) by XBOOLE_1:7;
K c= Int (Cl K) by A7, Def3;
then K c= (Cl (Int K)) \/ (Int (Cl K)) by A8, XBOOLE_1:1;
then A9: K is semi-pre-open by Def5;
then K = spInt K by Th6;
then pInt K = spInt K by A7, Th4;
then A10: K in { B where B is Subset of T : pInt B = spInt B } ;
K in SPO T by A9;
hence x in (SPO T) /\ (D(p,sp) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th15: :: DECOMP_1:15
for T being TopSpace holds (PSO T) /\ (D(p,ps) T) = PO T
proof
let T be TopSpace; ::_thesis: (PSO T) /\ (D(p,ps) T) = PO T
thus (PSO T) /\ (D(p,ps) T) c= PO T :: according to XBOOLE_0:def_10 ::_thesis: PO T c= (PSO T) /\ (D(p,ps) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(p,ps) T) or x in PO T )
assume A1: x in (PSO T) /\ (D(p,ps) T) ; ::_thesis: x in PO 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(p,ps) T by A1, XBOOLE_0:def_4;
then consider Z being Subset of T such that
A4: x = Z and
A5: pInt Z = psInt Z ;
A = psInt A by A3, Th5;
then Z is pre-open by A2, A4, A5, Th4;
hence x in PO T by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PO T or x in (PSO T) /\ (D(p,ps) T) )
assume x in PO T ; ::_thesis: x in (PSO T) /\ (D(p,ps) T)
then consider K being Subset of T such that
A6: x = K and
A7: K is pre-open ;
A8: Int (Cl K) c= Cl (Int (Cl K)) by PRE_TOPC:18;
K c= Int (Cl K) by A7, Def3;
then K c= Cl (Int (Cl K)) by A8, XBOOLE_1:1;
then A9: K is pre-semi-open by Def4;
then K = psInt K by Th5;
then pInt K = psInt K by A7, Th4;
then A10: K in { B where B is Subset of T : pInt B = psInt B } ;
K in PSO T by A9;
hence x in (PSO T) /\ (D(p,ps) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th16: :: DECOMP_1:16
for T being TopSpace holds (PSO T) /\ (D(alpha,p) T) = SO T
proof
let T be TopSpace; ::_thesis: (PSO T) /\ (D(alpha,p) T) = SO T
thus (PSO T) /\ (D(alpha,p) T) c= SO T :: according to XBOOLE_0:def_10 ::_thesis: SO T c= (PSO T) /\ (D(alpha,p) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(alpha,p) T) or x in SO T )
assume A1: x in (PSO T) /\ (D(alpha,p) T) ; ::_thesis: x in SO 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,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 = psInt A by A3, Th5;
then Z = sInt Z by A2, A4, A5, Th1;
then Z is semi-open by Th3;
hence x in SO T by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SO T or x in (PSO T) /\ (D(alpha,p) T) )
assume x in SO T ; ::_thesis: x in (PSO T) /\ (D(alpha,p) T)
then consider K being Subset of T such that
A6: x = K and
A7: 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 A8: Cl (Int K) c= Cl (Int (Cl K)) by TOPS_1:26;
K c= Cl (Int K) by A7, Def2;
then K c= Cl (Int (Cl K)) by A8, XBOOLE_1:1;
then A9: K is pre-semi-open by Def4;
then K = psInt K by Th5;
then sInt K = psInt K by A7, Th3;
then alphaInt K = pInt K by Th1;
then A10: K in { B where B is Subset of T : alphaInt B = pInt B } ;
K in PSO T by A9;
hence x in (PSO T) /\ (D(alpha,p) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th17: :: DECOMP_1:17
for T being TopSpace holds (PSO T) /\ (D(sp,ps) T) = SPO T
proof
let T be TopSpace; ::_thesis: (PSO T) /\ (D(sp,ps) T) = SPO T
thus (PSO T) /\ (D(sp,ps) T) c= SPO T :: according to XBOOLE_0:def_10 ::_thesis: SPO T c= (PSO T) /\ (D(sp,ps) T)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(sp,ps) T) or x in SPO T )
assume A1: x in (PSO T) /\ (D(sp,ps) T) ; ::_thesis: x in SPO 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(sp,ps) T by A1, XBOOLE_0:def_4;
then consider Z being Subset of T such that
A4: x = Z and
A5: spInt Z = psInt Z ;
A = psInt A by A3, Th5;
then Z is semi-pre-open by A2, A4, A5, Th6;
hence x in SPO T by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SPO T or x in (PSO T) /\ (D(sp,ps) T) )
assume x in SPO T ; ::_thesis: x in (PSO T) /\ (D(sp,ps) T)
then consider K being Subset of T such that
A6: x = K and
A7: 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 A8: 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 A9: (Cl (Int K)) \/ (Int (Cl K)) c= Cl (Int (Cl K)) by A8, XBOOLE_1:8;
K c= (Cl (Int K)) \/ (Int (Cl K)) by A7, Def5;
then K c= Cl (Int (Cl K)) by A9, XBOOLE_1:1;
then A10: K is pre-semi-open by Def4;
then K = psInt K by Th5;
then spInt K = psInt K by A7, Th6;
then A11: K in { B where B is Subset of T : spInt B = psInt B } ;
K in PSO T by A10;
hence x in (PSO T) /\ (D(sp,ps) T) by A6, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
definition
let X, Y be non empty TopSpace;
let f be Function of X,Y;
attrf is s-continuous means :Def26: :: DECOMP_1:def 26
for G being Subset of Y st G is open holds
f " G in SO X;
attrf is p-continuous means :Def27: :: DECOMP_1:def 27
for G being Subset of Y st G is open holds
f " G in PO X;
attrf is alpha-continuous means :Def28: :: DECOMP_1:def 28
for G being Subset of Y st G is open holds
f " G in X ^alpha ;
attrf is ps-continuous means :Def29: :: DECOMP_1:def 29
for G being Subset of Y st G is open holds
f " G in PSO X;
attrf is sp-continuous means :Def30: :: DECOMP_1:def 30
for G being Subset of Y st G is open holds
f " G in SPO X;
attrf is (c,alpha)-continuous means :Def31: :: DECOMP_1:def 31
for G being Subset of Y st G is open holds
f " G in D(c,alpha) X;
attrf is (c,s)-continuous means :Def32: :: DECOMP_1:def 32
for G being Subset of Y st G is open holds
f " G in D(c,s) X;
attrf is (c,p)-continuous means :Def33: :: DECOMP_1:def 33
for G being Subset of Y st G is open holds
f " G in D(c,p) X;
attrf is (c,ps)-continuous means :Def34: :: DECOMP_1:def 34
for G being Subset of Y st G is open holds
f " G in D(c,ps) X;
attrf is (alpha,p)-continuous means :Def35: :: DECOMP_1:def 35
for G being Subset of Y st G is open holds
f " G in D(alpha,p) X;
attrf is (alpha,s)-continuous means :Def36: :: DECOMP_1:def 36
for G being Subset of Y st G is open holds
f " G in D(alpha,s) X;
attrf is (alpha,ps)-continuous means :Def37: :: DECOMP_1:def 37
for G being Subset of Y st G is open holds
f " G in D(alpha,ps) X;
attrf 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;
attrf 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;
attrf 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;
:: deftheorem Def26 defines s-continuous DECOMP_1:def_26_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is s-continuous iff for G being Subset of Y st G is open holds
f " G in SO X );
:: deftheorem Def27 defines p-continuous DECOMP_1:def_27_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff for G being Subset of Y st G is open holds
f " G in PO X );
:: deftheorem Def28 defines alpha-continuous DECOMP_1:def_28_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff for G being Subset of Y st G is open holds
f " G in X ^alpha );
:: deftheorem Def29 defines ps-continuous DECOMP_1:def_29_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is ps-continuous iff for G being Subset of Y st G is open holds
f " G in PSO X );
:: deftheorem Def30 defines sp-continuous DECOMP_1:def_30_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is sp-continuous iff for G being Subset of Y st G is open holds
f " G in SPO X );
:: deftheorem Def31 defines (c,alpha)-continuous DECOMP_1:def_31_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,alpha)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,alpha) X );
:: deftheorem Def32 defines (c,s)-continuous DECOMP_1:def_32_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,s)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,s) X );
:: deftheorem Def33 defines (c,p)-continuous DECOMP_1:def_33_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,p)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,p) X );
:: deftheorem Def34 defines (c,ps)-continuous DECOMP_1:def_34_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (c,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(c,ps) X );
:: deftheorem Def35 defines (alpha,p)-continuous DECOMP_1:def_35_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,p)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,p) X );
:: deftheorem Def36 defines (alpha,s)-continuous DECOMP_1:def_36_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,s)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,s) X );
:: deftheorem Def37 defines (alpha,ps)-continuous DECOMP_1:def_37_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (alpha,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(alpha,ps) X );
:: deftheorem defines (p,ps)-continuous DECOMP_1:def_38_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (p,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(p,ps) X );
:: deftheorem defines (p,sp)-continuous DECOMP_1:def_39_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (p,sp)-continuous iff for G being Subset of Y st G is open holds
f " G in D(p,sp) X );
:: deftheorem defines (sp,ps)-continuous DECOMP_1:def_40_:_
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is (sp,ps)-continuous iff for G being Subset of Y st G is open holds
f " G in D(sp,ps) X );
theorem :: DECOMP_1:18
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) )
hereby ::_thesis: ( f is p-continuous & f is (alpha,p)-continuous implies f is alpha-continuous )
assume A1: f is alpha-continuous ; ::_thesis: ( f is p-continuous & f is (alpha,p)-continuous )
thus f is p-continuous ::_thesis: f is (alpha,p)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X )
assume V is open ; ::_thesis: f " V in PO X
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_4; ::_thesis: verum
end;
thus f is (alpha,p)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_35 ::_thesis: ( G is open implies f " G in D(alpha,p) X )
assume G is open ; ::_thesis: f " G in D(alpha,p) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is p-continuous & f is (alpha,p)-continuous ) ; ::_thesis: f is alpha-continuous
let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha )
assume V is open ; ::_thesis: f " V in X ^alpha
then ( f " V in PO X & f " V in D(alpha,p) X ) by A2, Def27, Def35;
then f " V in (PO X) /\ (D(alpha,p) X) by XBOOLE_0:def_4;
hence f " V in X ^alpha by Th11; ::_thesis: verum
end;
theorem :: DECOMP_1:19
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) )
hereby ::_thesis: ( f is s-continuous & f is (alpha,s)-continuous implies f is alpha-continuous )
assume A1: f is alpha-continuous ; ::_thesis: ( f is s-continuous & f is (alpha,s)-continuous )
thus f is s-continuous ::_thesis: f is (alpha,s)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X )
assume V is open ; ::_thesis: f " V in SO X
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_4; ::_thesis: verum
end;
thus f is (alpha,s)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_36 ::_thesis: ( G is open implies f " G in D(alpha,s) X )
assume G is open ; ::_thesis: f " G in D(alpha,s) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is s-continuous & f is (alpha,s)-continuous ) ; ::_thesis: f is alpha-continuous
let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha )
assume V is open ; ::_thesis: f " V in X ^alpha
then ( f " V in SO X & f " V in D(alpha,s) X ) by A2, Def26, Def36;
then f " V in (SO X) /\ (D(alpha,s) X) by XBOOLE_0:def_4;
hence f " V in X ^alpha by Th12; ::_thesis: verum
end;
theorem :: DECOMP_1:20
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) )
hereby ::_thesis: ( f is ps-continuous & f is (alpha,ps)-continuous implies f is alpha-continuous )
assume A1: f is alpha-continuous ; ::_thesis: ( f is ps-continuous & f is (alpha,ps)-continuous )
thus f is ps-continuous ::_thesis: f is (alpha,ps)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X )
assume V is open ; ::_thesis: f " V in PSO X
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_4; ::_thesis: verum
end;
thus f is (alpha,ps)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_37 ::_thesis: ( G is open implies f " G in D(alpha,ps) X )
assume G is open ; ::_thesis: f " G in D(alpha,ps) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is ps-continuous & f is (alpha,ps)-continuous ) ; ::_thesis: f is alpha-continuous
let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha )
assume V is open ; ::_thesis: f " V in X ^alpha
then ( f " V in PSO X & f " V in D(alpha,ps) X ) by A2, Def29, Def37;
then f " V in (PSO X) /\ (D(alpha,ps) X) by XBOOLE_0:def_4;
hence f " V in X ^alpha by Th13; ::_thesis: verum
end;
theorem :: DECOMP_1:21
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) )
hereby ::_thesis: ( f is sp-continuous & f is (p,sp)-continuous implies f is p-continuous )
assume A1: f is p-continuous ; ::_thesis: ( f is sp-continuous & f is (p,sp)-continuous )
thus f is sp-continuous ::_thesis: f is (p,sp)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_30 ::_thesis: ( V is open implies f " V in SPO X )
assume V is open ; ::_thesis: f " V in SPO X
then f " V in PO X by A1, Def27;
hence f " V in SPO X ; ::_thesis: verum
end;
thus f is (p,sp)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_39 ::_thesis: ( G is open implies f " G in D(p,sp) X )
assume G is open ; ::_thesis: f " G in D(p,sp) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is sp-continuous & f is (p,sp)-continuous ) ; ::_thesis: f is p-continuous
let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X )
assume V is open ; ::_thesis: f " V in PO X
then f " V in SPO X by A2, Def30;
hence f " V in PO X ; ::_thesis: verum
end;
theorem :: DECOMP_1:22
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) )
hereby ::_thesis: ( f is ps-continuous & f is (p,ps)-continuous implies f is p-continuous )
assume A1: f is p-continuous ; ::_thesis: ( f is ps-continuous & f is (p,ps)-continuous )
thus f is ps-continuous ::_thesis: f is (p,ps)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X )
assume V is open ; ::_thesis: f " V in PSO X
then f " V in PO X by A1, Def27;
hence f " V in PSO X ; ::_thesis: verum
end;
thus f is (p,ps)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_38 ::_thesis: ( G is open implies f " G in D(p,ps) X )
assume G is open ; ::_thesis: f " G in D(p,ps) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is ps-continuous & f is (p,ps)-continuous ) ; ::_thesis: f is p-continuous
let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X )
assume V is open ; ::_thesis: f " V in PO X
then f " V in PSO X by A2, Def29;
hence f " V in PO X ; ::_thesis: verum
end;
theorem :: DECOMP_1:23
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) )
hereby ::_thesis: ( f is ps-continuous & f is (alpha,p)-continuous implies f is s-continuous )
assume A1: f is s-continuous ; ::_thesis: ( f is ps-continuous & f is (alpha,p)-continuous )
thus f is ps-continuous ::_thesis: f is (alpha,p)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X )
assume V is open ; ::_thesis: f " V in PSO X
then f " V in SO X by A1, Def26;
hence f " V in PSO X ; ::_thesis: verum
end;
thus f is (alpha,p)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_35 ::_thesis: ( G is open implies f " G in D(alpha,p) X )
assume G is open ; ::_thesis: f " G in D(alpha,p) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is ps-continuous & f is (alpha,p)-continuous ) ; ::_thesis: f is s-continuous
let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X )
assume V is open ; ::_thesis: f " V in SO X
then f " V in PSO X by A2, Def29;
hence f " V in SO X ; ::_thesis: verum
end;
theorem :: DECOMP_1:24
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) )
hereby ::_thesis: ( f is ps-continuous & f is (sp,ps)-continuous implies f is sp-continuous )
assume A1: f is sp-continuous ; ::_thesis: ( f is ps-continuous & f is (sp,ps)-continuous )
thus f is ps-continuous ::_thesis: f is (sp,ps)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X )
assume V is open ; ::_thesis: f " V in PSO X
then f " V in SPO X by A1, Def30;
hence f " V in PSO X ; ::_thesis: verum
end;
thus f is (sp,ps)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_40 ::_thesis: ( G is open implies f " G in D(sp,ps) X )
assume G is open ; ::_thesis: f " G in D(sp,ps) X
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_4; ::_thesis: verum
end;
end;
assume A2: ( f is ps-continuous & f is (sp,ps)-continuous ) ; ::_thesis: f is sp-continuous
let V be Subset of Y; :: according to DECOMP_1:def_30 ::_thesis: ( V is open implies f " V in SPO X )
assume V is open ; ::_thesis: f " V in SPO X
then f " V in PSO X by A2, Def29;
hence f " V in SPO X ; ::_thesis: verum
end;
theorem :: DECOMP_1:25
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) )
A1: [#] Y <> {} ;
hereby ::_thesis: ( f is alpha-continuous & f is (c,alpha)-continuous implies f is continuous )
assume A2: f is continuous ; ::_thesis: ( f is alpha-continuous & f is (c,alpha)-continuous )
thus f is alpha-continuous ::_thesis: f is (c,alpha)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha )
assume V is open ; ::_thesis: f " V in X ^alpha
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 f " V in X ^alpha by XBOOLE_0:def_4; ::_thesis: verum
end;
thus f is (c,alpha)-continuous ::_thesis: verum
proof
let G be Subset of Y; :: according to DECOMP_1:def_31 ::_thesis: ( G is open implies f " G in D(c,alpha) X )
assume G is open ; ::_thesis: f " G in D(c,alpha) X
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 f " G in D(c,alpha) X by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A3: ( f is alpha-continuous & f is (c,alpha)-continuous ) ; ::_thesis: f is continuous
now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_
f_"_V_is_open
let V be Subset of Y; ::_thesis: ( V is open implies f " V is open )
assume V is open ; ::_thesis: f " V is open
then ( f " V in X ^alpha & f " V in D(c,alpha) X ) by A3, Def28, Def31;
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; ::_thesis: verum
end;
hence f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
theorem :: DECOMP_1:26
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) )
A1: [#] Y <> {} ;
hereby ::_thesis: ( f is s-continuous & f is (c,s)-continuous implies f is continuous )
assume A2: f is continuous ; ::_thesis: ( f is s-continuous & f is (c,s)-continuous )
thus f is s-continuous ::_thesis: f is (c,s)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X )
assume V is open ; ::_thesis: f " V in SO X
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 f " V in SO X by XBOOLE_0:def_4; ::_thesis: verum
end;
thus f is (c,s)-continuous ::_thesis: verum
proof
let V be Subset of Y; :: according to DECOMP_1:def_32 ::_thesis: ( V is open implies f " V in D(c,s) X )
assume V is open ; ::_thesis: f " V in D(c,s) X
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 f " V in D(c,s) X by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A3: ( f is s-continuous & f is (c,s)-continuous ) ; ::_thesis: f is continuous
now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_
f_"_V_is_open
let V be Subset of Y; ::_thesis: ( V is open implies f " V is open )
assume V is open ; ::_thesis: f " V is open
then ( f " V in SO X & f " V in D(c,s) X ) by A3, Def26, Def32;
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; ::_thesis: verum
end;
hence f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
theorem :: DECOMP_1:27
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) )
A1: [#] Y <> {} ;
hereby ::_thesis: ( f is p-continuous & f is (c,p)-continuous implies f is continuous )
assume A2: f is continuous ; ::_thesis: ( f is p-continuous & f is (c,p)-continuous )
thus f is p-continuous ::_thesis: f is (c,p)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X )
assume V is open ; ::_thesis: f " V in PO X
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 f " V in PO X by XBOOLE_0:def_4; ::_thesis: verum
end;
thus f is (c,p)-continuous ::_thesis: verum
proof
let V be Subset of Y; :: according to DECOMP_1:def_33 ::_thesis: ( V is open implies f " V in D(c,p) X )
assume V is open ; ::_thesis: f " V in D(c,p) X
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 f " V in D(c,p) X by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A3: ( f is p-continuous & f is (c,p)-continuous ) ; ::_thesis: f is continuous
now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_
f_"_V_is_open
let V be Subset of Y; ::_thesis: ( V is open implies f " V is open )
assume V is open ; ::_thesis: f " V is open
then ( f " V in PO X & f " V in D(c,p) X ) by A3, Def27, Def33;
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; ::_thesis: verum
end;
hence f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;
theorem :: DECOMP_1:28
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds
( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) )
A1: [#] Y <> {} ;
hereby ::_thesis: ( f is ps-continuous & f is (c,ps)-continuous implies f is continuous )
assume A2: f is continuous ; ::_thesis: ( f is ps-continuous & f is (c,ps)-continuous )
thus f is ps-continuous ::_thesis: f is (c,ps)-continuous
proof
let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X )
assume V is open ; ::_thesis: f " V in PSO X
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 f " V in PSO X by XBOOLE_0:def_4; ::_thesis: verum
end;
thus f is (c,ps)-continuous ::_thesis: verum
proof
let V be Subset of Y; :: according to DECOMP_1:def_34 ::_thesis: ( V is open implies f " V in D(c,ps) X )
assume V is open ; ::_thesis: f " V in D(c,ps) X
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 f " V in D(c,ps) X by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A3: ( f is ps-continuous & f is (c,ps)-continuous ) ; ::_thesis: f is continuous
now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_
f_"_V_is_open
let V be Subset of Y; ::_thesis: ( V is open implies f " V is open )
assume V is open ; ::_thesis: f " V is open
then ( f " V in PSO X & f " V in D(c,ps) X ) by A3, Def29, Def34;
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; ::_thesis: verum
end;
hence f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;