Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Families of Subsets, Subspaces and Mappings in Topological Spaces

by
Agata Darmochwal

MML identifier: TOPS_2
[ Mizar article, MML identifier index ]

environ

vocabulary PRE_TOPC, SETFAM_1, SUBSET_1, BOOLE, TARSKI, FINSET_1, FUNCT_1,
RELAT_1, FINSEQ_1, ORDINAL2, TOPS_2, SEQ_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0,
PRE_TOPC;
constructors FUNCT_3, NAT_1, FINSEQ_1, PRE_TOPC, XREAL_0, MEMBERED;
clusters PRE_TOPC, STRUCT_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve x, y for set,
k for Nat,
T for TopStruct,
GX for TopSpace,
P, Q for Subset of T,
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;

canceled;

theorem :: TOPS_2:3
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;

canceled;

theorem :: TOPS_2:5
for T being non empty 1-sorted, F being Subset-Family of T st
F is_a_cover_of T holds F <> {};

theorem :: TOPS_2:6
for T being 1-sorted, F, G being Subset-Family of T holds
union F \ union G c= union(F \ G);

canceled 2;

theorem :: TOPS_2:9
for T being 1-sorted, F being Subset-Family of T holds
COMPLEMENT(COMPLEMENT(F)) = F;

theorem :: TOPS_2:10
for T being 1-sorted, F being Subset-Family of T holds
F <> {} iff COMPLEMENT(F) <> {};

theorem :: TOPS_2:11
for T being 1-sorted, F being Subset-Family of T holds
F <> {} implies meet COMPLEMENT(F) = (union F)`;

theorem :: TOPS_2:12
for T being 1-sorted, F being Subset-Family of T holds
F <> {} implies union COMPLEMENT(F) = (meet F)`;

theorem :: TOPS_2:13
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;

canceled 2;

theorem :: TOPS_2:16
F is closed iff COMPLEMENT(F) is open;

theorem :: TOPS_2:17
F is open iff COMPLEMENT(F) is closed;

theorem :: TOPS_2:18
F c= G & G is open implies F is open;

theorem :: TOPS_2:19
F c= G & G is closed implies F is closed;

theorem :: TOPS_2:20
F is open & G is open implies F \/ G is open;

theorem :: TOPS_2:21
F is open implies F /\ G is open;

theorem :: TOPS_2:22
F is open implies F \ G is open;

theorem :: TOPS_2:23
F is closed & G is closed implies F \/ G is closed;

theorem :: TOPS_2:24
F is closed implies F /\ G is closed;

theorem :: TOPS_2:25
F is closed implies F \ G is closed;

theorem :: TOPS_2:26
W is open implies union W is open;

theorem :: TOPS_2:27
W is open & W is finite implies meet W is open;

theorem :: TOPS_2:28
W is closed & W is finite implies union W is closed;

theorem :: TOPS_2:29
W is closed implies meet W is closed;

::
::      SUBSPACES OF A TOPOLOGICAL SPACE
::

canceled;

theorem :: TOPS_2:31
for F being Subset-Family of A holds
F is Subset-Family of T;

theorem :: TOPS_2:32
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:33
Q is open implies
for P being Subset of A st P=Q holds P is open;

theorem :: TOPS_2:34
Q is closed implies
for P being Subset of A st P=Q holds P is closed;

theorem :: TOPS_2:35
F is open implies for G being Subset-Family of A st G=F holds
G is open;

theorem :: TOPS_2:36
F is closed implies for G being Subset-Family of A st G=F
holds G is closed;

canceled;

theorem :: TOPS_2:38
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;

canceled;

theorem :: TOPS_2:40
F c= G implies F|M c= G|M;

theorem :: TOPS_2:41
Q in F implies Q /\ M in F|M;

theorem :: TOPS_2:42
Q c= union F implies Q /\ M c= union(F|M);

theorem :: TOPS_2:43
M c= union F implies M = union (F|M);

theorem :: TOPS_2:44
union(F|M) c= union F;

theorem :: TOPS_2:45
M c= union (F|M) implies M c= union F;

theorem :: TOPS_2:46
F is finite implies F|M is finite;

theorem :: TOPS_2:47
F is open implies F|M is open;

theorem :: TOPS_2:48
F is closed implies F|M is closed;

theorem :: TOPS_2:49
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:50
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;

::
::       MAPPING OF THE TOPOLOGICAL SPACES
::

theorem :: TOPS_2:51
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S holds
dom f = [#]T & rng f c= [#]S;

theorem :: TOPS_2:52
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S holds
f"([#]S) = [#]T;

canceled;

theorem :: TOPS_2:54
for T being 1-sorted, S being non empty 1-sorted,
f being map of T, S,
H being Subset-Family of S holds
("f).:H is Subset-Family of T;

::
::          CONTINUOUS MAPPING
::

reserve S, V for non empty TopStruct,
f for map of T, S,
g for map of S, V,
H for Subset-Family of S,
P1 for Subset of S;

theorem :: TOPS_2:55
f is continuous iff
(for P1 st P1 is open holds f"P1 is open);

theorem :: TOPS_2:56
for T being TopSpace, S being non empty TopSpace, f being map 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:57
for T being TopSpace, S being non empty TopSpace, f being map 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:58
f is continuous & g is continuous implies g*f is continuous;

theorem :: TOPS_2:59
f is continuous & H is open implies
for F st F=("f).:H holds F is open;

theorem :: TOPS_2:60
for T, S being TopStruct, f being map 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 T, S be 1-sorted, f be map of T,S;
assume that
rng f = [#]S and
f is one-to-one;
func f/" -> map of S,T equals
:: TOPS_2:def 4
f";
synonym f";
end;

canceled;

theorem :: TOPS_2:62
for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds
dom(f") = [#]S & rng(f") = [#]T;

theorem :: TOPS_2:63
for T, S being 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds f" is one-to-one;

theorem :: TOPS_2:64
for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st
rng f = [#]S & f is one-to-one holds (f")" = f;

theorem :: TOPS_2:65
for T, S being 1-sorted, f being map 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:66
for T being 1-sorted, S, V being non empty 1-sorted,
f being map of T,S, g being map of S,V st
dom f = [#]T & 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:67
for T, S being 1-sorted, f being map 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:68
for T, S being 1-sorted, f being map 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 map 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;
synonym f is_homeomorphism;
end;

canceled;

theorem :: TOPS_2:70
f is_homeomorphism implies f" is_homeomorphism;

theorem :: TOPS_2:71
for T, S, V being non empty TopStruct,
f being map of T,S, g being map of S,V st
f is_homeomorphism & g is_homeomorphism holds g*f is_homeomorphism;

theorem :: TOPS_2:72
f is_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, S for non empty TopSpace,
P for Subset of T,
P1 for Subset of S,
f for map of T, S;

theorem :: TOPS_2:73
f is_homeomorphism iff
dom f = [#]T & rng f = [#]S & f is one-to-one &
for P1 holds f"(Cl P1) = Cl(f"P1);

theorem :: TOPS_2:74
f is_homeomorphism iff
dom f = [#]T & rng f = [#]
S & f is one-to-one & for P holds f.:(Cl P) = Cl(f.:P);