The abstract of the Mizar article:

Families of Subsets, Subspaces and Mappings in Topological Spaces

by

Agata Darmochwal

Received June 21, 1989

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