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);
```