:: On the Decomposition of the Continuity
:: by Marian Przemski
::
:: Received December 12, 1994
:: Copyright (c) 1994-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, SUBSET_1, TARSKI, TOPS_1, XBOOLE_0, SETFAM_1, RCOMP_1,
FUNCT_1, RELAT_1, ORDINAL2, DECOMP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1;
constructors TOPS_1, RELSET_1;
registrations SUBSET_1, PRE_TOPC, TOPS_1;
requirements SUBSET;
begin
definition
let T be TopStruct;
mode alpha-set of T -> Subset of T means
:: DECOMP_1:def 1
it c= Int Cl Int it;
let IT be Subset of T;
attr IT is semi-open means
:: DECOMP_1:def 2
IT c= Cl Int IT;
attr IT is pre-open means
:: DECOMP_1:def 3
IT c= Int Cl IT;
attr IT is pre-semi-open means
:: DECOMP_1:def 4
IT c= Cl Int Cl IT;
attr IT is semi-pre-open means
:: DECOMP_1:def 5
IT c= Cl Int IT \/ Int Cl IT;
end;
definition
let T be TopStruct;
let B be Subset of T;
func sInt B -> Subset of T equals
:: DECOMP_1:def 6
B /\ Cl Int B;
func pInt B -> Subset of T equals
:: DECOMP_1:def 7
B /\ Int Cl B;
func alphaInt B -> Subset of T equals
:: DECOMP_1:def 8
B /\ Int Cl Int B;
func psInt B -> Subset of T equals
:: DECOMP_1:def 9
B /\ Cl Int Cl B;
end;
definition
let T be TopStruct;
let B be Subset of T;
func spInt B -> Subset of T equals
:: DECOMP_1:def 10
sInt B \/ pInt B;
end;
definition
let T be TopSpace;
func T^alpha -> Subset-Family of T equals
:: DECOMP_1:def 11
{B where B is Subset of T: B is alpha-set of T};
func SO T -> Subset-Family of T equals
:: DECOMP_1:def 12
{B where B is Subset of T : B is semi-open};
func PO T -> Subset-Family of T equals
:: DECOMP_1:def 13
{B where B is Subset of T : B is pre-open};
func SPO T -> Subset-Family of T equals
:: DECOMP_1:def 14
{B where B is Subset of T:B is semi-pre-open};
func PSO T -> Subset-Family of T equals
:: DECOMP_1:def 15
{B where B is Subset of T:B is pre-semi-open};
func D(c,alpha)(T) -> Subset-Family of T equals
:: DECOMP_1:def 16
{B where B is Subset of T: Int B = alphaInt B};
func D(c,p)(T) -> Subset-Family of T equals
:: DECOMP_1:def 17
{B where B is Subset of T: Int B = pInt B};
func D(c,s)(T) -> Subset-Family of T equals
:: DECOMP_1:def 18
{B where B is Subset of T: Int B = sInt B};
func D(c,ps)(T) -> Subset-Family of T equals
:: DECOMP_1:def 19
{B where B is Subset of T: Int B = psInt B};
func D(alpha,p)(T) -> Subset-Family of T equals
:: DECOMP_1:def 20
{B where B is Subset of T: alphaInt B = pInt B};
func D(alpha,s)(T) -> Subset-Family of T equals
:: DECOMP_1:def 21
{B where B is Subset of T: alphaInt B = sInt B};
func D(alpha,ps)(T) -> Subset-Family of T equals
:: DECOMP_1:def 22
{B where B is Subset of T: alphaInt B = psInt B};
func D(p,sp)(T) -> Subset-Family of T equals
:: DECOMP_1:def 23
{B where B is Subset of T: pInt B = spInt B};
func D(p,ps)(T) -> Subset-Family of T equals
:: DECOMP_1:def 24
{B where B is Subset of T: pInt B = psInt B};
func D(sp,ps)(T) -> Subset-Family of T equals
:: DECOMP_1:def 25
{B where B is Subset of T: spInt B = psInt B};
end;
reserve T for TopSpace,
B for Subset of T;
theorem :: DECOMP_1:1
alphaInt B = pInt B iff sInt B = psInt B;
theorem :: DECOMP_1:2
B is alpha-set of T iff B = alphaInt B;
theorem :: DECOMP_1:3
B is semi-open iff B = sInt B;
theorem :: DECOMP_1:4
B is pre-open iff B = pInt B;
theorem :: DECOMP_1:5
B is pre-semi-open iff B = psInt B;
theorem :: DECOMP_1:6
B is semi-pre-open iff B = spInt B;
theorem :: DECOMP_1:7
T^alpha /\ D(c,alpha)(T) = the topology of T;
theorem :: DECOMP_1:8
SO T /\ D(c,s)(T) = the topology of T;
theorem :: DECOMP_1:9
PO T /\ D(c,p)(T) = the topology of T;
theorem :: DECOMP_1:10
PSO T /\ D(c,ps)(T) = the topology of T;
theorem :: DECOMP_1:11
PO T /\ D(alpha,p)(T) = T^alpha;
theorem :: DECOMP_1:12
SO T /\ D(alpha,s)(T) = T^alpha;
theorem :: DECOMP_1:13
PSO T /\ D(alpha,ps)(T) = T^alpha;
theorem :: DECOMP_1:14
SPO T /\ D(p,sp)(T) = PO T;
theorem :: DECOMP_1:15
PSO T /\ D(p,ps)(T) = PO T;
theorem :: DECOMP_1:16
PSO T /\ D(alpha,p)(T) = SO T;
theorem :: DECOMP_1:17
PSO T /\ D(sp,ps)(T) = SPO T;
definition
let X,Y be non empty TopSpace;
let f be Function of X,Y;
attr f is s-continuous means
:: DECOMP_1:def 26
for G being Subset of Y st G is open holds f"G in SO X;
attr f is p-continuous means
:: DECOMP_1:def 27
for G being Subset of Y st G is open holds f"G in PO X;
attr f is alpha-continuous means
:: DECOMP_1:def 28
for G being Subset of Y st G is open holds f"G in X^alpha;
attr f is ps-continuous means
:: DECOMP_1:def 29
for G being Subset of Y st G is open holds f"G in PSO X;
attr f is sp-continuous means
:: DECOMP_1:def 30
for G being Subset of Y st G is open holds f"G in SPO X;
attr f is (c,alpha)-continuous means
:: DECOMP_1:def 31
for G being Subset of Y st G is open holds f"G in D(c,alpha)(X);
attr f is (c,s)-continuous means
:: DECOMP_1:def 32
for G being Subset of Y st G is open holds f"G in D(c,s)(X);
attr f is (c,p)-continuous means
:: DECOMP_1:def 33
for G being Subset of Y st G is open holds f"G in D(c,p)(X);
attr f is (c,ps)-continuous means
:: DECOMP_1:def 34
for G being Subset of Y st G is open holds f"G in D(c,ps)(X);
attr f is (alpha,p)-continuous means
:: DECOMP_1:def 35
for G being Subset of Y st G is open holds f"G in D(alpha,p)(X);
attr f is (alpha,s)-continuous means
:: DECOMP_1:def 36
for G being Subset of Y st G is open holds f"G in D(alpha,s)(X);
attr f is (alpha,ps)-continuous means
:: DECOMP_1:def 37
for G being Subset of Y st G is open holds f"G in D(alpha,ps)(X);
attr f is (p,ps)-continuous means
:: DECOMP_1:def 38
for G being Subset of Y st G is open holds f"G in D(p,ps)(X);
attr f is (p,sp)-continuous means
:: DECOMP_1:def 39
for G being Subset of Y st G is open holds f"G in D(p,sp)(X);
attr f is (sp,ps)-continuous means
:: DECOMP_1:def 40
for G being Subset of Y st G is open holds f"G in D(sp,ps)(X);
end;
reserve X,Y for non empty TopSpace;
reserve f for Function of X,Y;
theorem :: DECOMP_1:18
f is alpha-continuous iff f is p-continuous (alpha,p)-continuous;
theorem :: DECOMP_1:19
f is alpha-continuous iff f is s-continuous (alpha,s)-continuous;
theorem :: DECOMP_1:20
f is alpha-continuous iff f is ps-continuous (alpha,ps)-continuous;
theorem :: DECOMP_1:21
f is p-continuous iff f is sp-continuous (p,sp)-continuous;
theorem :: DECOMP_1:22
f is p-continuous iff f is ps-continuous (p,ps)-continuous;
theorem :: DECOMP_1:23
f is s-continuous iff f is ps-continuous (alpha,p)-continuous;
theorem :: DECOMP_1:24
f is sp-continuous iff f is ps-continuous (sp,ps)-continuous;
theorem :: DECOMP_1:25
f is continuous iff f is alpha-continuous (c,alpha)-continuous;
theorem :: DECOMP_1:26
f is continuous iff f is s-continuous (c,s)-continuous;
theorem :: DECOMP_1:27
f is continuous iff f is p-continuous (c,p)-continuous;
theorem :: DECOMP_1:28
f is continuous iff f is ps-continuous (c,ps)-continuous;