The abstract of the Mizar article:

Bases and Refinements of Topologies

by

Grzegorz Bancerek

Received March 9, 1998

MML identifier: YELLOW_9

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, SETFAM_1, WAYBEL_0, SUBSET_1, BOOLE, PRE_TOPC, FUNCT_1,
      RELAT_1, TARSKI, CANTOR_1, WAYBEL_9, REALSET1, RELAT_2, NATTRA_1,
      FINSET_1, BHSP_3, LATTICES, FUNCOP_1, YELLOW_0, ORDINAL2, FUNCT_3,
      SEQM_3, CAT_1, WELLORD1, OPPCAT_1, QUANTAL1, FUNCT_2, FRAENKEL, CONNSP_2,
      TOPS_1, LATTICE3, BORSUK_1, PRELAMB, WAYBEL11, PROB_1, YELLOW_6,
      YELLOW_9, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      FINSET_1, MCART_1, STRUCT_0, RELAT_2, RELSET_1, REALSET1, FRAENKEL,
      FUNCT_2, WELLORD1, GRCAT_1, ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0,
      WAYBEL_0, TDLAT_3, GROUP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6,
      YELLOW_7, WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
 constructors RELAT_2, WAYBEL11, CANTOR_1, TOPS_1, TDLAT_3, GROUP_1, TOLER_1,
      WAYBEL_3, WAYBEL_5, ORDERS_3, WAYBEL_1, GRCAT_1, TOPS_2, BORSUK_1,
      LATTICE3, PARTFUN1;
 clusters TDLAT_3, FRAENKEL, YELLOW_6, YELLOW_2, FINSET_1, RELSET_1, BORSUK_1,
      STRUCT_0, TEX_1, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_7, WAYBEL_9,
      WAYBEL11, SUBSET_1, RLVECT_2, FUNCT_2, SETFAM_1, XBOOLE_0, ZFMISC_1,
      PARTFUN1;
 requirements BOOLE, SUBSET;


begin :: Subsets as nets

scheme FraenkelInvolution
      {A() -> non empty set, X,Y() -> Subset of A(), F(set) -> Element of A()}:
 X() = {F(a) where a is Element of A(): a in Y()}
provided
 Y() = {F(a) where a is Element of A(): a in X()}
and
 for a being Element of A() holds F(F(a)) = a;

scheme FraenkelComplement1
      {A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
       F(set) -> Subset of A()}:
 COMPLEMENT X() = {F(a)` where a is Element of A(): a in Y()}
provided
 X() = {F(a) where a is Element of A(): a in Y()};

scheme FraenkelComplement2
      {A() -> non empty RelStr, X() -> Subset-Family of A(), Y() -> set,
       F(set) -> Subset of A()}:
 COMPLEMENT X() = {F(a) where a is Element of A(): a in Y()}
provided
 X() = {F(a)` where a is Element of A(): a in Y()};

theorem :: YELLOW_9:1
   for R being non empty RelStr, x,y being Element of R holds
   y in (uparrow x)` iff not x <= y;

theorem :: YELLOW_9:2
 for S being 1-sorted, T being non empty 1-sorted, f being map of S,T
  for X being Subset of T holds (f"X)` = f"X`;

theorem :: YELLOW_9:3
 for T being 1-sorted, F being Subset-Family of T holds
  COMPLEMENT F = {a` where a is Subset of T: a in F};

theorem :: YELLOW_9:4
 for R being non empty RelStr
 for F being Subset of R holds
  uparrow F = union {uparrow x where x is Element of R: x in F} &
  downarrow F = union {downarrow x where x is Element of R: x in F};

theorem :: YELLOW_9:5
   for R being non empty RelStr
 for A being Subset-Family of R, F being Subset of R
  st A = {(uparrow x)` where x is Element of R: x in F}
  holds Intersect A = (uparrow F)`;

definition
 cluster strict trivial reflexive non empty discrete finite TopRelStr;
end;

definition
 cluster strict complete trivial TopLattice;
end;

definition
 let S be non empty RelStr,
     T be upper-bounded non empty reflexive antisymmetric RelStr;
 cluster infs-preserving map of S,T;
end;

definition
 let S be non empty RelStr,
     T be lower-bounded non empty reflexive antisymmetric RelStr;
 cluster sups-preserving map of S,T;
end;

definition
 let R,S be 1-sorted;
 assume
  the carrier of S c= the carrier of R;
 func incl(S,R) -> map of S,R equals
:: YELLOW_9:def 1

   id the carrier of S;
end;

definition
 let R be non empty RelStr;
 let S be non empty SubRelStr of R;
 cluster incl(S,R) -> monotone;
end;

definition
 let R be non empty RelStr, X be non empty Subset of R;
 func X+id -> strict non empty NetStr over R equals
:: YELLOW_9:def 2
   (incl(subrelstr X, R))*((subrelstr X)+id);
 func X opp+id -> strict non empty NetStr over R equals
:: YELLOW_9:def 3
   (incl(subrelstr X, R))*((subrelstr X)opp+id);
end;

theorem :: YELLOW_9:6
   for R being non empty RelStr, X being non empty Subset of R holds
  the carrier of X+id = X & X+id is full SubRelStr of R &
  for x being Element of X+id holds X+id.x = x;

theorem :: YELLOW_9:7
   for R being non empty RelStr, X being non empty Subset of R holds
  the carrier of X opp+id = X & X opp+id is full SubRelStr of R opp &
  for x being Element of X opp+id holds X opp+id.x = x;

definition
 let R be non empty reflexive RelStr;
 let X be non empty Subset of R;
 cluster X +id -> reflexive;
 cluster X opp+id -> reflexive;
end;

definition
 let R be non empty transitive RelStr;
 let X be non empty Subset of R;
 cluster X +id -> transitive;
 cluster X opp+id -> transitive;
end;

definition
 let R be non empty reflexive RelStr;
 let I be directed Subset of R;
 cluster subrelstr I -> directed;
end;

definition
 let R be non empty reflexive RelStr;
 let I be directed non empty Subset of R;
 cluster I+id -> directed;
end;

definition
 let R be non empty reflexive RelStr;
 let F be filtered non empty Subset of R;
 cluster (subrelstr F) opp+id -> directed;
end;

definition
 let R be non empty reflexive RelStr;
 let F be filtered non empty Subset of R;
 cluster F opp+id -> directed;
end;

begin :: Operations on families of open sets

theorem :: YELLOW_9:8
 for T being TopSpace st T is empty holds the topology of T = {{}};

theorem :: YELLOW_9:9
 for T being trivial non empty TopSpace holds
   the topology of T = bool the carrier of T &
   for x being Point of T holds
    the carrier of T = {x} & the topology of T = {{},{x}};

theorem :: YELLOW_9:10
   for T being trivial non empty TopSpace holds
   {the carrier of T} is Basis of T &
   {} is prebasis of T & {{}} is prebasis of T;

theorem :: YELLOW_9:11
 for X,Y being set, A being Subset-Family of X st A = {Y}
  holds FinMeetCl A = {Y,X} & UniCl A = {Y,{}};

theorem :: YELLOW_9:12
   for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ {X}
  holds Intersect A = Intersect B;

theorem :: YELLOW_9:13
   for X being set, A,B being Subset-Family of X st A = B \/ {X} or B = A \ {X}
  holds FinMeetCl A = FinMeetCl B;

theorem :: YELLOW_9:14
 for X being set, A being Subset-Family of X st X in A
 for x being set holds x in FinMeetCl A iff
  ex Y being finite non empty Subset-Family of X st Y c= A & x = Intersect Y;

theorem :: YELLOW_9:15
 for X being set, A being Subset-Family of X holds UniCl UniCl A = UniCl A;

theorem :: YELLOW_9:16
 for X being set, A being empty Subset-Family of X holds UniCl A = {{}};

theorem :: YELLOW_9:17
 for X being set, A being empty Subset-Family of X holds
  FinMeetCl A = {X};

theorem :: YELLOW_9:18
 for X being set, A being Subset-Family of X st A = {{},X}
  holds UniCl A = A & FinMeetCl A = A;

theorem :: YELLOW_9:19
 for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
  holds (A c= B implies UniCl A c= UniCl B) &
        (A = B implies UniCl A = UniCl B);

theorem :: YELLOW_9:20
 for X,Y being set, A being Subset-Family of X, B being Subset-Family of Y
  st A = B & X in A & X c= Y holds FinMeetCl B = {Y} \/ FinMeetCl A;

theorem :: YELLOW_9:21
 for X being set, A being Subset-Family of X holds
  UniCl FinMeetCl UniCl A = UniCl FinMeetCl A;

begin :: Bases

theorem :: YELLOW_9:22
 for T being TopSpace, K being Subset-Family of T
  holds the topology of T = UniCl K iff K is Basis of T;

theorem :: YELLOW_9:23
 for T being TopSpace, K being Subset-Family of T
  holds K is prebasis of T iff FinMeetCl K is Basis of T;

theorem :: YELLOW_9:24
 for T being non empty TopSpace, B being Subset-Family of T
  st UniCl B is prebasis of T
  holds B is prebasis of T;

theorem :: YELLOW_9:25
 for T1, T2 being TopSpace, B being Basis of T1
  st the carrier of T1 = the carrier of T2 & B is Basis of T2
  holds the topology of T1 = the topology of T2;

theorem :: YELLOW_9:26
 for T1, T2 being TopSpace, P being prebasis of T1
  st the carrier of T1 = the carrier of T2 & P is prebasis of T2
  holds the topology of T1 = the topology of T2;

theorem :: YELLOW_9:27
   for T being TopSpace, K being Basis of T holds K is open & K is prebasis of
T;

theorem :: YELLOW_9:28
   for T being TopSpace, K being prebasis of T holds K is open;

theorem :: YELLOW_9:29
 for T being non empty TopSpace, B being prebasis of T holds
   B \/ {the carrier of T} is prebasis of T;

theorem :: YELLOW_9:30
   for T being TopSpace, B being Basis of T holds
   B \/ {the carrier of T} is Basis of T;

theorem :: YELLOW_9:31
 for T being TopSpace, B being Basis of T
 for A being Subset of T holds
  A is open iff for p being Point of T st p in A
      ex a being Subset of T st a in B & p in a & a c= A;

theorem :: YELLOW_9:32
 for T being TopSpace, B being Subset-Family of T
  st B c= the topology of T &
   for A being Subset of T st A is open
    for p being Point of T st p in A
     ex a being Subset of T st a in B & p in a & a c= A
  holds B is Basis of T;

theorem :: YELLOW_9:33
 for S being TopSpace, T being non empty TopSpace, K being Basis of T
 for f being map of S,T holds
  f is continuous iff for A being Subset of T st A in K holds f"A` is closed;

theorem :: YELLOW_9:34
   for S being TopSpace,T being non empty TopSpace, K being Basis of T
 for f being map of S,T holds
  f is continuous iff for A being Subset of T st A in K holds f"A is open;

theorem :: YELLOW_9:35
 for S being TopSpace,T being non empty TopSpace, K being prebasis of T
 for f being map of S,T holds
  f is continuous iff for A being Subset of T st A in K holds f"A` is closed;

theorem :: YELLOW_9:36
   for S being TopSpace,T being non empty TopSpace, K being prebasis of T
 for f being map of S,T holds
  f is continuous iff for A being Subset of T st A in K holds f"A is open;

theorem :: YELLOW_9:37
 for T being non empty TopSpace, x being Point of T, X being Subset of T
 for K being Basis of T
  st for A being Subset of T st A in K & x in A holds A meets X
  holds x in Cl X;

theorem :: YELLOW_9:38
 for T being non empty TopSpace, x being Point of T, X being Subset of T
 for K being prebasis of T
  st for Z being finite Subset-Family of T st Z c= K & x in Intersect Z
      holds Intersect Z meets X
  holds x in Cl X;

theorem :: YELLOW_9:39
   for T being non empty TopSpace, K being prebasis of T, x being Point of T
 for N being net of T
  st for A being Subset of T st A in K & x in A holds N is_eventually_in A
 for S being Subset of T st rng netmap(N,T) c= S
  holds x in Cl S;

begin :: Product topology

theorem :: YELLOW_9:40
 for T1,T2 being non empty TopSpace
 for B1 being Basis of T1, B2 being Basis of T2 holds
   {[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
     is Basis of [:T1,T2:];

theorem :: YELLOW_9:41
 for T1,T2 being non empty TopSpace
 for B1 being prebasis of T1, B2 being prebasis of T2 holds
   {[:the carrier of T1, b:] where b is Subset of T2: b in B2} \/
   {[:a, the carrier of T2:] where a is Subset of T1: a in B1}
     is prebasis of [:T1,T2:];

theorem :: YELLOW_9:42
   for X1,X2 being set, A being Subset-Family of [:X1,X2:]
 for A1 being non empty Subset-Family of X1
 for A2 being non empty Subset-Family of X2
  st A = {[:a,b:] where a is Subset of X1, b is Subset of X2: a in A1 & b in
 A2}
  holds Intersect A = [:Intersect A1, Intersect A2:];

theorem :: YELLOW_9:43
   for T1,T2 being non empty TopSpace
 for B1 being prebasis of T1, B2 being prebasis of T2
  st union B1 = the carrier of T1 & union B2 = the carrier of T2
  holds
   {[:a,b:] where a is Subset of T1, b is Subset of T2: a in B1 & b in B2}
     is prebasis of [:T1,T2:];

begin :: Topological augmentations

definition
 let R be RelStr;
 mode TopAugmentation of R -> TopRelStr means
:: YELLOW_9:def 4

  the RelStr of it = the RelStr of R;
end;

definition
 let R be RelStr;
 let T be TopAugmentation of R;
 redefine attr T is TopSpace-like; synonym T is correct;
end;

definition
 let R be RelStr;
 cluster correct discrete strict TopAugmentation of R;
end;

theorem :: YELLOW_9:44
   for T being TopRelStr holds T is TopAugmentation of T;

theorem :: YELLOW_9:45
   for S being TopRelStr, T being TopAugmentation of S holds
   S is TopAugmentation of T;

theorem :: YELLOW_9:46
   for R being RelStr, T1 being TopAugmentation of R
 for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R;

definition
 let R be non empty RelStr;
 cluster -> non empty TopAugmentation of R;
end;

definition
 let R be reflexive RelStr;
 cluster -> reflexive TopAugmentation of R;
end;

definition
 let R be transitive RelStr;
 cluster -> transitive TopAugmentation of R;
end;

definition
 let R be antisymmetric RelStr;
 cluster -> antisymmetric TopAugmentation of R;
end;

definition
 let R be complete (non empty RelStr);
 cluster -> complete TopAugmentation of R;
end;

theorem :: YELLOW_9:47
 for S being up-complete antisymmetric (non empty reflexive RelStr),
     T being non empty reflexive RelStr
  st the RelStr of S = the RelStr of T
 for A being Subset of S, C being Subset of T st A = C & A is inaccessible
  holds C is inaccessible;

theorem :: YELLOW_9:48
 for S being non empty reflexive RelStr, T being TopAugmentation of S
  st the topology of T = sigma S
  holds T is correct;

theorem :: YELLOW_9:49
 for S being complete LATTICE, T being TopAugmentation of S
  st the topology of T = sigma S
  holds T is Scott;

definition
 let R be complete LATTICE;
 cluster Scott strict correct TopAugmentation of R;
end;

theorem :: YELLOW_9:50
 for S,T being complete
  Scott (non empty reflexive transitive antisymmetric TopRelStr)
  st the RelStr of S = the RelStr of T
 for F being Subset of S, G being Subset of T st F = G
  holds F is open implies G is open;

theorem :: YELLOW_9:51
 for S being complete LATTICE, T being Scott TopAugmentation of S
  holds the topology of T = sigma S;

theorem :: YELLOW_9:52
   for S,T being complete LATTICE st the RelStr of S = the RelStr of T
  holds sigma S = sigma T;

definition
 let R be complete LATTICE;
 cluster Scott -> correct TopAugmentation of R;
end;

begin :: Refinements

definition
 let T be TopStruct;
 mode TopExtension of T -> TopSpace means
:: YELLOW_9:def 5

  the carrier of T = the carrier of it &
  the topology of T c= the topology of it;
end;

theorem :: YELLOW_9:53
 for S being TopStruct ex T being TopExtension of S st
   T is strict & the topology of S is prebasis of T;

definition
 let T be TopStruct;
 cluster strict discrete TopExtension of T;
end;

definition
 let T1,T2 be TopStruct;
 mode Refinement of T1,T2 -> TopSpace means
:: YELLOW_9:def 6

  the carrier of it = (the carrier of T1) \/ (the carrier of T2) &
  (the topology of T1) \/ (the topology of T2) is prebasis of it;
end;

definition
 let T1 be non empty TopStruct, T2 be TopStruct;
 cluster -> non empty Refinement of T1,T2;
 cluster -> non empty Refinement of T2,T1;
end;

theorem :: YELLOW_9:54
   for T1,T2 being TopStruct, T, T' being Refinement of T1,T2 holds
  the TopStruct of T = the TopStruct of T';

theorem :: YELLOW_9:55
   for T1,T2 being TopStruct, T being Refinement of T1,T2
  holds T is Refinement of T2,T1;

theorem :: YELLOW_9:56
   for T1,T2 being TopStruct, T being Refinement of T1,T2
 for X being Subset-Family of T
  st X = (the topology of T1) \/ (the topology of T2)
  holds the topology of T = UniCl FinMeetCl X;

theorem :: YELLOW_9:57
   for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2
 for T being Refinement of T1, T2
  holds T is TopExtension of T1 & T is TopExtension of T2;

theorem :: YELLOW_9:58
   for T1,T2 being non empty TopSpace, T be Refinement of T1, T2
 for B1 being prebasis of T1, B2 being prebasis of T2
  holds B1 \/ B2 \/ {the carrier of T1, the carrier of T2} is prebasis of T;

theorem :: YELLOW_9:59
 for T1,T2 being non empty TopSpace
 for B1 being Basis of T1, B2 being Basis of T2
 for T being Refinement of T1, T2
  holds B1 \/ B2 \/ INTERSECTION(B1,B2) is Basis of T;

theorem :: YELLOW_9:60
 for T1,T2 being non empty TopSpace st the carrier of T1 = the carrier of T2
 for T being Refinement of T1, T2
  holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T;

theorem :: YELLOW_9:61
   for L being non empty RelStr
 for T1,T2 being correct TopAugmentation of L
 for T be Refinement of T1, T2
  holds INTERSECTION(the topology of T1, the topology of T2) is Basis of T;