:: Families of Subsets, Subspaces and Mappings in Topological Spaces
:: by Agata Darmochwa{\l}
::
:: Received June 21, 1989
:: Copyright (c) 1990-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 SUBSET_1, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, FUNCT_2,
ZFMISC_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1, RCOMP_1, FINSEQ_1, NAT_1,
XXREAL_0, ARYTM_3, CARD_1, ORDINAL2, VALUED_1, RELAT_2, CONNSP_1, TOPS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, XCMPLX_0, NAT_1,
FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
constructors SETFAM_1, PARTFUN1, FUNCT_3, XXREAL_0, XREAL_0, NAT_1, MEMBERED,
FINSEQ_1, CONNSP_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC,
XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve x, y for set,
T for TopStruct,
GX for TopSpace,
P, Q, M, N for Subset of T,
F, G for Subset-Family of T,
W, Z for Subset-Family of GX,
A for SubSpace of T;
::
:: A FAMILY OF SETS IN TOPOLOGICAL SPACES
::
theorem :: TOPS_2:1
for T being 1-sorted, F being Subset-Family of T holds F c= bool [#]T;
theorem :: TOPS_2:2
for T being 1-sorted, F being Subset-Family of T, X being set st
X c= F holds X is Subset-Family of T;
theorem :: TOPS_2:3
for T being non empty 1-sorted, F being Subset-Family of T st F is
Cover of T holds F <> {};
theorem :: TOPS_2:4
for T being 1-sorted, F, G being Subset-Family of T holds union F \
union G c= union(F \ G);
theorem :: TOPS_2:5
for T being set, F being Subset-Family of T holds F <> {} iff
COMPLEMENT(F) <> {};
theorem :: TOPS_2:6
for T being set, F being Subset-Family of T holds F <> {}
implies meet COMPLEMENT(F) = (union F)`;
theorem :: TOPS_2:7
for T being set, F being Subset-Family of T holds F <> {}
implies union COMPLEMENT(F) = (meet F)`;
theorem :: TOPS_2:8
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT(F) is finite iff F is finite;
::
:: CLOSED AND OPEN FAMILIES
::
definition
let T be TopStruct, F be Subset-Family of T;
attr F is open means
:: TOPS_2:def 1
for P being Subset of T holds P in F implies P is open;
attr F is closed means
:: TOPS_2:def 2
for P being Subset of T holds P in F implies P is closed;
end;
theorem :: TOPS_2:9
F is closed iff COMPLEMENT(F) is open;
theorem :: TOPS_2:10
F is open iff COMPLEMENT(F) is closed;
theorem :: TOPS_2:11
F c= G & G is open implies F is open;
theorem :: TOPS_2:12
F c= G & G is closed implies F is closed;
theorem :: TOPS_2:13
F is open & G is open implies F \/ G is open;
theorem :: TOPS_2:14
F is open implies F /\ G is open;
theorem :: TOPS_2:15
F is open implies F \ G is open;
theorem :: TOPS_2:16
F is closed & G is closed implies F \/ G is closed;
theorem :: TOPS_2:17
F is closed implies F /\ G is closed;
theorem :: TOPS_2:18
F is closed implies F \ G is closed;
theorem :: TOPS_2:19
W is open implies union W is open;
theorem :: TOPS_2:20
W is open & W is finite implies meet W is open;
theorem :: TOPS_2:21
W is closed & W is finite implies union W is closed;
theorem :: TOPS_2:22
W is closed implies meet W is closed;
::
:: SUBSPACES OF A TOPOLOGICAL SPACE
::
theorem :: TOPS_2:23
for F being Subset-Family of A holds F is Subset-Family of T;
theorem :: TOPS_2:24
for B being Subset of A holds B is open iff ex C being Subset of
T st C is open & C /\ [#](A) = B;
theorem :: TOPS_2:25
Q is open implies for P being Subset of A st P=Q holds P is open;
theorem :: TOPS_2:26
Q is closed implies for P being Subset of A st P=Q holds P is closed;
theorem :: TOPS_2:27
F is open implies for G being Subset-Family of A st G=F holds G is open;
theorem :: TOPS_2:28
F is closed implies for G being Subset-Family of A st G=F holds G is closed;
theorem :: TOPS_2:29
M /\ N is Subset of T|N;
::
:: RESTRICTION OF A FAMILY
::
definition
let T be TopStruct, P be Subset of T, F be Subset-Family of T;
func F|P -> Subset-Family of T|P means
:: TOPS_2:def 3
for Q being Subset of T|P
holds Q in it iff ex R being Subset of T st R in F & R /\ P = Q;
end;
theorem :: TOPS_2:30
F c= G implies F|M c= G|M;
theorem :: TOPS_2:31
Q in F implies Q /\ M in F|M;
theorem :: TOPS_2:32
Q c= union F implies Q /\ M c= union(F|M);
theorem :: TOPS_2:33
M c= union F implies M = union (F|M);
theorem :: TOPS_2:34
union(F|M) c= union F;
theorem :: TOPS_2:35
M c= union (F|M) implies M c= union F;
theorem :: TOPS_2:36
F is finite implies F|M is finite;
theorem :: TOPS_2:37
F is open implies F|M is open;
theorem :: TOPS_2:38
F is closed implies F|M is closed;
theorem :: TOPS_2:39
for F being Subset-Family of A st F is open ex G being Subset-Family
of T st G is open & for AA being Subset of T st AA = [#] A holds F = G|AA;
theorem :: TOPS_2:40
ex f being Function st dom f = F & rng f = F|P & for x st x in F for Q
st Q = x holds f.x = Q /\ P;
theorem :: TOPS_2:41
for X,Y being 1-sorted, f being Function of X, Y st [#]Y = {}
implies [#]X = {} holds f"([#]Y) = [#]X;
theorem :: TOPS_2:42
for T being 1-sorted, S being non empty 1-sorted, f being Function of
T, S, H being Subset-Family of S holds ("f).:H is Subset-Family of T;
::
:: CONTINUOUS MAPPING
::
reserve S for non empty TopStruct,
f for Function of T, S,
H for Subset-Family of S;
theorem :: TOPS_2:43
for X,Y being TopStruct, f being Function of X,Y st [#]Y = {}
implies [#]X = {} holds f is continuous iff for P being Subset of Y st P is
open holds f"P is open;
theorem :: TOPS_2:44
for T being TopSpace, S being TopSpace, f being Function of T, S
holds f is continuous iff for P1 being Subset of S holds Cl(f"P1) c= f"(Cl P1);
theorem :: TOPS_2:45
for T being TopSpace, S being non empty TopSpace, f being
Function of T, S holds f is continuous iff for P being Subset of T holds f.:(Cl
P) c= Cl(f.:P);
theorem :: TOPS_2:46
for T,V being TopStruct,S being non empty TopStruct, f being
Function of T,S, g being Function of S,V holds f is continuous & g is
continuous implies g*f is continuous;
theorem :: TOPS_2:47
f is continuous & H is open implies for F st F=("f).:H holds F is open;
theorem :: TOPS_2:48
for T, S being TopStruct, f being Function of T, S, H being
Subset-Family of S st f is continuous & H is closed holds for F being
Subset-Family of T st F=("f).:H holds F is closed;
definition
let S, T be set, f be Function of S,T;
assume
f is bijective;
func f/" -> Function of T,S equals
:: TOPS_2:def 4
f";
end;
notation
let S, T be set, f be Function of S,T;
synonym f" for f/";
end;
theorem :: TOPS_2:49
for T being 1-sorted, S being non empty 1-sorted, f being Function of T,S
st rng f = [#]S & f is one-to-one holds dom(f") = [#]S & rng(f") = [#]T;
theorem :: TOPS_2:50
for T, S being 1-sorted, f being Function of T,S st rng f = [#]S
& f is one-to-one holds f" is one-to-one;
theorem :: TOPS_2:51
for T being 1-sorted, S being non empty 1-sorted, f being
Function of T,S st rng f = [#]S & f is one-to-one holds (f")" = f;
theorem :: TOPS_2:52
for T, S being 1-sorted, f being Function of T,S st rng f = [#]S & f
is one-to-one holds f"*f = id dom f & f*f" = id rng f;
theorem :: TOPS_2:53
for T being 1-sorted, S, V being non empty 1-sorted, f being
Function of T,S, g being Function of S,V st rng f = [#]S & f is one-to-one &
dom g = [#]S & rng g = [#]V & g is one-to-one holds (g*f)" = f"*g";
theorem :: TOPS_2:54
for T, S being 1-sorted, f being Function of T, S, P being
Subset of T st rng f = [#]S & f is one-to-one holds f.:P = (f")"P;
theorem :: TOPS_2:55
for T, S being 1-sorted, f being Function of T,S, P1 being
Subset of S st rng f = [#]S & f is one-to-one holds f"P1 = (f").:P1;
::
:: HOMEOMORPHISM
::
definition
let S, T be TopStruct, f be Function of S, T;
attr f is being_homeomorphism means
:: TOPS_2:def 5
dom f = [#]S & rng f = [#]T & f
is one-to-one & f is continuous & f" is continuous;
end;
theorem :: TOPS_2:56
f is being_homeomorphism implies f" is being_homeomorphism;
theorem :: TOPS_2:57
for T, S, V being non empty TopStruct, f being Function of T,S, g
being Function of S,V st f is being_homeomorphism & g is being_homeomorphism
holds g*f is being_homeomorphism;
theorem :: TOPS_2:58
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P holds P is closed iff f.:P is closed;
reserve T for non empty TopSpace,
S for TopSpace,
P1 for Subset of S,
f for Function of T, S;
theorem :: TOPS_2:59
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P1 holds f"(Cl P1) = Cl(f"P1);
reserve T for TopSpace,
S for non empty TopSpace,
P for Subset of T,
f for Function of T, S;
theorem :: TOPS_2:60
f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is
one-to-one & for P holds f.:(Cl P) = Cl(f.:P);
theorem :: TOPS_2:61 :: TOPREAL5:5, AK, 21.02.2006
for X,Y being non empty TopSpace for f being Function of X,Y, A
being Subset of X st f is continuous & A is connected holds f.:A is connected
;
theorem :: TOPS_2:62 :: JORDAN18:2, AK, 21.02.2006
for S,T being non empty TopSpace, f being Function of S,T, A being
Subset of T st f is being_homeomorphism & A is connected holds f"A is connected
;
begin :: Addenda
:: from JORDAN1, 2008.07.07, A.T.
reserve GX,GY for non empty TopSpace;
theorem :: TOPS_2:63
for GX being non empty TopSpace st (for x,y being Point of GX ex GY st
(GY is connected & ex f being Function of GY,GX st f is continuous & x in rng(f
)& y in rng(f))) holds GX is connected;
:: Added by AK, 2009.09.20
theorem :: TOPS_2:64
for X being TopStruct, F being Subset-Family of X holds
F is open iff F c= the topology of X;
theorem :: TOPS_2:65
for X being TopStruct, F being Subset-Family of X holds
F is closed iff F c= COMPLEMENT the topology of X;
registration
let X be TopStruct;
cluster the topology of X -> open;
cluster open for Subset-Family of X;
end;