:: Bases and Refinements of Topologies
::  by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998-2021 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 XBOOLE_0, SUBSET_1, ORDERS_2, SETFAM_1, WAYBEL_0, XXREAL_0,
      STRUCT_0, PRE_TOPC, FUNCT_1, RELAT_1, TARSKI, REWRITE1, ZFMISC_1,
      WAYBEL_9, RELAT_2, NATTRA_1, FINSET_1, LATTICES, FUNCOP_1, YELLOW_0,
      ORDINAL2, FUNCT_3, SEQM_3, CAT_1, WELLORD1, ARYTM_0, RLVECT_3, CANTOR_1,
      FUNCT_2, RCOMP_1, CONNSP_2, TOPS_1, LATTICE3, BORSUK_1, PRELAMB,
      CARD_FIL, PROB_1, YELLOW_6, WAYBEL11, YELLOW_9, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      FINSET_1, MCART_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1,
      STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, ORDERS_3, YELLOW_0, WAYBEL_0,
      TDLAT_3, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2, YELLOW_6, YELLOW_7,
      WAYBEL_9, WAYBEL11, CANTOR_1, BORSUK_1;
 constructors SETFAM_1, TOLER_1, TOPS_1, TOPS_2, BORSUK_1, LATTICE3, TDLAT_3,
      CANTOR_1, ORDERS_3, WAYBEL11, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FINSET_1, STRUCT_0,
      BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_2,
      YELLOW_6, WAYBEL_9, WAYBEL11, FUNCT_2, CANTOR_1, RELSET_1;
 requirements BOOLE, SUBSET;


begin :: Subsets as nets

scheme :: YELLOW_9:sch 1
 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 :: YELLOW_9:sch 2
 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 :: YELLOW_9:sch 3
 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;

scheme :: YELLOW_9:sch 4
 ABC {A() -> TopSpace, F(set) -> set, f() -> Function, P[set]}:
  f()"union {F(x) where x is Subset of A(): P[x]} =
  union {f()"(F(y)) where y is Subset of A(): P[y]};

theorem :: YELLOW_9:2
  for S being 1-sorted, T being non empty 1-sorted, f being Function 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)`;

registration
  cluster strict complete 1-element for TopLattice;
end;

registration
  let S be non empty RelStr,
  T be upper-bounded non empty reflexive antisymmetric RelStr;
  cluster infs-preserving for Function of S,T;
end;

registration
  let S be non empty RelStr,
  T be lower-bounded non empty reflexive antisymmetric RelStr;
  cluster sups-preserving for Function 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) -> Function of S,R equals
:: YELLOW_9:def 1

  id the carrier of S;
end;

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

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

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

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

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

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

registration
  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 1-element 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 1-element 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
  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 Function 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 Function 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 Function 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 Function 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;

notation
  let R be RelStr;
  let T be TopAugmentation of R;
  synonym T is correct for T is TopSpace-like;
end;

registration
  let R be RelStr;
  cluster correct discrete strict for 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;

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

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

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

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

registration
  let R be complete non empty RelStr;
  cluster -> complete for 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;

registration
  let R be complete LATTICE;
  cluster Scott strict correct for 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;

registration
  let R be complete LATTICE;
  cluster Scott -> correct for 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;

registration
  let T be TopStruct;
  cluster strict discrete for 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;

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

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

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;